mmtheorems82 - Metamath Proof Explorer

Home	Metamath Proof Explorer	< Previous Next >
		Browser slow? Try the Unicode version.

Jump to page: Contents + 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12229

Color key:

Metamath Proof Explorer
(1-9062)

Hilbert Space Explorer
(9063-10650)

Users' Mathboxes
(10651-12229)

**Statement List for Metamath Proof Explorer -** 8101-8200 - Page 82 of 123
Type	Label	Description
Statement

Theorem	metcnpi 8101	Epsilon-delta property of a continuous metric space function, with function arguments as in metcnp 8098.
Open Open Met $/\$ Met $/\$ $/\$ CnP $/\$ $/\$ $/\$

Theorem	metcnpi2 8102	Epsilon-delta property of a continuous metric space function, with swapped distance function arguments as in metcnp2 8099.
Open Open Met $/\$ Met $/\$ $/\$ CnP $/\$ $/\$ $/\$

Theorem	metcnpi3 8103	Epsilon-delta property of a metric space function continuous at . A variation of metcnpi2 8102 with non-strict ordering.
Open Open Met $/\$ Met $/\$ $/\$ CnP $/\$ $/\$ $/\$

Theorem	metcnpi4 8104	Epsilon-delta property of a metric space function continuous at . A variation of metcnpi 8101 with non-strict ordering.
Open Open Met $/\$ Met $/\$ $/\$ CnP $/\$ $/\$ $/\$

Theorem	metcni 8105	Epsilon-delta property of a continuous metric space function.
Open Open Met $/\$ Met $/\$ Cn $/\$ $/\$ $/\$ $/\$

Theorem	metcni2 8106	Epsilon-delta property of a continuous metric space function.
Open Open Met $/\$ Met $/\$ Cn $/\$ $/\$ $/\$ $/\$

Theorem	metcnp3 8107	Two ways to express that is continuous at for metric spaces. Proposition 14-4.2 of [Gleason] p. 240.
Open Open Met $/\$ Met $/\$ CnP $/\$ $/\$ ball ball

Theorem	metcnco 8108	Composition of two continuous functions (metric space version of cnco 7978).
Open Open Open Met $/\$ Met $/\$ Met $/\$ Cn $/\$ Cn Cn

Theorem	metcnss 8109	Subset relationship for continuity of metric spaces.
Open Open Open Met $/\$ Met $/\$ Met $/\$ Cn Cn

Theorem	metcnss2 8110	Subset relationship for continuity of metric spaces.
Open Open Open Met $/\$ Met $/\$ Met $/\$ $/\$ Cn Cn

Theorem	metidcn 8111	The identity function is continuous (metric space version of idcn 7976).
Open Open Met $/\$ Met $/\$ Cn

Theorem	metdnsconst 8112	If a continuous mapping to a metric space is constant on a dense subset, it is constant on the entire space (metric space version of dnsconst 7998).
Open Open Met $/\$ Met $/\$ Cn $/\$ $/\$ $/\$ cls

Examples of metric spaces

Theorem	cnmetdval 8113	Value of the distance function of the metric space of complex numbers.
$/\$

Theorem	cnmetba 8114	The base set of the metric for complex numbers.


Theorem	cnmet 8115	The absolute value metric determines a metric space on the complex numbers. This theorem provides a link between complex numbers and metrics spaces, making metric space theorems available for use with complex numbers. (Contributed by FL, 9-Oct-2006.)
Met

Theorem	cncfmet 8116	Relate complex function continuity to metric space continuity. (Contributed by Paul Chapman, 26-Nov-2007.)
Open Open $/\$ Cn

Theorem	cncfmet1 8117	Relate complex function continuity to metric space continuity. (Contributed by Paul Chapman, 28-Nov-2007.)
Open Cn

Theorem	cn2met 8118	The standard metric space on .
$/\$ $/\$ Met

Theorem	remetdval 8119	Value of the distance function of the metric space of real numbers.
$/\$

Theorem	remetba 8120	The base set for the metric for real numbers.


Theorem	remet 8121	The absolute value metric determines a metric space on the reals.
Met

Theorem	bl2ioo 8122	A ball in terms of an open interval of reals.
$/\$ $/\$ ball (,)

Theorem	ioo2bl 8123	An open interval of reals in terms of a ball.
$/\$ $/\$ (,) ball

Theorem	blssioo 8124	The balls of the standard real metric space are included in the open real intervals.
ball (,)

Theorem	tgioolem 8125	Lemma for tgioo 8126. An open interval includes a ball around any of its points. Warning: The HTML proof page is 0.6MB in size.

Theorem	tgioo 8126	The topology generated by open intervals of reals is the same as the open sets of the standard metric space on the reals.
Open topGen (,)

Theorem	qdensere2 8127	is dense in .
Open cls

Theorem	rehaus 8128	The standard topology on the reals is Hausdorff.
topGen (,) Haus

Theorem	dscmet 8129	The discrete metric on any set . Definition 1.1-8 of [Kreyszig] p. 8. (Contributed by FL, 12-Oct-2006.)
$/\$ $/\$ Met

Convergence and completeness

Syntax	clm 8130	Extend class notation with a function on metric spaces whose value is the convergence relation for limit sequences in the space.


Syntax	cca 8131	Extend class notation with a function on metric spaces whose value is the set of all Cauchy sequences of the space.
Cau

Syntax	cms 8132	Extend class notation with class of complete metric spaces.
CMet

Definition	df-lm 8133	Define a function on metric spaces whose value is the convergence relation for the space. Although is typically a function from upper integers to the metric space, it doesn't have to be. Unfortunately, the expression after " " must exist to use fvopab4 3891, and we use the otherwise unnecessary conjunct to ensure that. This could be changed to the more liberal (but more complex) if we want to allow for functions with undefined values.
Met $/\$ $/\$ $/\$ $/\$

Definition	df-cau 8134	Define a function on metric spaces whose value is the set of Cauchy sequences of the space.
Cau Met $/\$ $/\$ $/\$ $/\$ $/\$

Definition	df-cmet 8135	Define the class of complete metrics.
CMet Met Cau

Theorem	lmfval 8136	The relation "sequence converges to point " in a metric space.
Met $/\$ $/\$ $/\$

Theorem	caufval 8137	The set of Cauchy sequences on a metric space.
Met Cau $/\$ $/\$ $/\$ $/\$

Theorem	lmrel 8138	The metric space convergence relation is a relation.
Met

Theorem	lmbr 8139	Express the binary relation "sequence converges to point " in a metric space. Definition 1.4-1 of [Kreyszig] p. 25. The condition allows us to use objects more general than sequences when convenient; see the comment in df-lm 8133.
Met $/\$ $/\$ $/\$ $/\$

Theorem	lmbr2 8140	Express the binary relation "sequence converges to point " in a metric space using an abitrary set of upper integers.
Met $/\$ $/\$ $/\$ $/\$

Theorem	lmbrf 8141	Express the binary relation "sequence converges to point " in a metric space using an abitrary set of upper integers. This version of lmbr2 8140 presupposes that is a function.
Met $/\$ $/\$ $/\$

Theorem	lmbrf2 8142	Express the binary relation "sequence converges to point " in a metric space using an abitrary set of upper integers. This version of lmbrf 8141 presupposes that the convergence point is in the metric space.
Met $/\$ $/\$

Theorem	lmcvg 8143	Convergence property of a converging sequence.
Met $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	lmcvg2 8144	Convergence property of a converging sequence.
Met $/\$ $/\$ $/\$ $/\$

Theorem	lmconst 8145	A constant sequence converges to its value.
Met $/\$

Theorem	lmnn 8146	A condition that implies convergence.
Met $/\$ $/\$ $/\$

Theorem	iscau 8147	Express the property " is a Cauchy sequence of metric ." Part of Definition 1.4-3 of [Kreyszig] p. 28. The condition allows us to use objects more general than sequences when convenient; see the comment in df-lm 8133.
Met Cau $/\$ $/\$ $/\$ $/\$

Theorem	iscau2 8148	Express the property " is a Cauchy sequence of metric ," using an abitrary set of upper integers.
Met Cau $/\$ $/\$ $/\$ $/\$

Theorem	iscau3 8149	Express the property " is a Cauchy sequence of metric " with one less quantifier.
Met Cau $/\$ $/\$ $/\$

Theorem	iscauf 8150	Express the property " is a Cauchy sequence of metric " presupposing is a function.
Met $/\$ Cau

Theorem	iscau4 8151	Express the property " is a Cauchy sequence of metric ."
Met Cau $/\$ $/\$ $/\$

Theorem	iscau5 8152	Express the property " is a Cauchy sequence of metric ."
Met $/\$ Cau

Theorem	lmbrnns 8153	Express the binary relation "sequence converges to point " in a metric space."
Met $/\$ $/\$

Theorem	lmcvgnns 8154	Convergence property of a converging sequence.
Met $/\$ $/\$ $/\$

Theorem	iscaunns 8155	Express the property " is a Cauchy sequence of metric ."
Met $/\$ Cau

Theorem	caun0 8156	A metric with a Cauchy sequence cannot be empty.
Met $/\$ Cau

Theorem	iscms 8157	The property " is a complete metric," meaning all Cauchy sequences converge to a point in the space. Part of Definition 1.4-3 of [Kreyszig] p. 28.
CMet Met $/\$ Cau

Theorem	cmscvg 8158	The convergence of a Cauchy sequence in a complete metric space.
CMet $/\$ Cau

Theorem	lmfss 8159	Inclusion of a function having a limit (used to ensure the limit relation is a set, under our definition).
Met $/\$ $/\$

Theorem	lmcl 8160	Closure of a limit.
Met $/\$ $/\$

Theorem	caufss 8161	Inclusion of a Cauchy sequence, under our definition.
Met $/\$ Cau

Theorem	lmuni 8162	A sequence converges to at most one limit. Part of Lemma 1.4-2(a) of [Kreyszig] p. 26.
Met $/\$ $/\$

Theorem	lmsslem 8163	Lemma for lmss 8164 and causs 8166.

Theorem	lmss 8164	Limit on a metric subspace.
Met $/\$ $/\$

Theorem	caussi 8165	Cauchy sequence on a metric subspace.
Met $/\$ Cau Cau

Theorem	causs 8166	Cauchy sequence on a metric subspace.
Met $/\$ Cau Cau

Theorem	lmfexlem1 8167	Lemma for lmfex 8170. is a function constructed from an arbitrary sequence , from to the metric space base set.

Theorem	lmfexlem2 8168	Lemma for lmfex 8170. When the value of exists, it equals the value of .

Theorem	lmfexlem3 8169	Lemma for lmfex 8170. If converges, so does the function constructed from it.

Theorem	lmfex 8170	If (not necessarily a function) converges, there is a function that converges to the same point.
Met $/\$ $/\$ $/\$

Theorem	lmle 8171	If the distance from each member of a converging sequence to a given point is less than or equal to a given amount, so is the convergence value. Warning: The HTML proof page is 0.5MB in size.
Met $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cmsmet 8172	A complete metric space is a metric space.
CMet Met

Theorem	cmsmeti 8173	A complete metric space is a metric space.
CMet Met

Theorem	lmclim 8174	Relate a limit on the metric space of complex numbers to our complex number limit notation.
$/\$

Theorem	lmclimnn 8175	Relate a limit on the metric space of complex numbers to our complex number limit notation.
$/\$

Theorem	metelcls 8176	A point belongs to the closure of a subset iff there is a sequence in the subset converging to it. Theorem 1.4-6(a) of [Kreyszig] p. 30. Warning: The HTML proof page is 0.5MB in size.
Open Met $/\$ cls $/\$

Theorem	metcls 8177	The closure of a subset of a metric space is equal to its points of convergence. Theorem 1.4-6(a) of [Kreyszig] p. 30.
Open Met $/\$ cls $/\$

Theorem	metcld 8178	A subset of a metric space is closed iff every convergent sequence on it converges to a point in the subset. Theorem 1.4-6(b) of [Kreyszig] p. 30.
Open Met $/\$ Clsd $/\$

Theorem	metcnp4lem1 8179	Lemma for metcnp4 8181.

Theorem	metcnp4lem2 8180	Lemma for metcnp4 8181.

Theorem	metcnp4 8181	Two ways to say a mapping from metric to metric is continuous at point . Theorem 14-4.3 of [Gleason] p. 240.
Open Open $/\$ Met $/\$ Met $/\$ CnP $/\$ $/\$

Theorem	metcn4 8182	Two ways to say a mapping from metric to metric is continuous. Theorem 10.3 of [Munkres] p. 128.
Open Open $/\$ Met $/\$ Met $/\$ Cn

Theorem	metcn4i 8183	Convergence carries through a continuous mapping.
Open Open $/\$ Met $/\$ Met $/\$ Cn $/\$ $/\$

Theorem	xplmi 8184	Two sequences converge if the sequence of their ordered pairs converges. One direction of Proposition 14-2.6 of [Gleason] p. 230. Warning: The HTML proof page is 0.5MB in size.
Met Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	xplmi2 8185	Two sequences converge if the sequence of their ordered pairs converges. Part of Proposition 14-2.6 of [Gleason] p. 230. Note: The hypothesis is redundant but is kept for convenience.
Met Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	xplm 8186	Two sequences converge iff the sequence of their ordered pairs converges. Proposition 14-2.6 of [Gleason] p. 230. Warning: The HTML proof page is 0.5MB in size.
Met Met $/\$ $/\$ $/\$ $/\$

Theorem	xpcn 8187	Construct a continuous function to the product of the codomains of two continuous functions on a common metric space. Warning: The HTML proof page is 0.5MB in size.
Met Met Met $/\$ $/\$ Open Open Open Open $/\$ Cn $/\$ Cn Cn

Theorem	oprcn 8188	Construct a continuous function built from two functions and (on a common metric space ) applied to an operation . This can be used to show, e.g., that is continuous if we know that , , and are.
Met Met Met Met Open Open Open Open Open $/\$ $/\$ Cn $/\$ Cn $/\$ Cn Cn

Theorem	opr1cn 8189	Construct a continuous function built from a function and a constant applied to an operation .
Met Met Met Met Open Open Open Open Open $/\$ $/\$ Cn $/\$ Cn $/\$ Cn

Theorem	opr2cn 8190	Construct a continuous function built from a function and a constant applied to an operation .
Met Met Met Met Open Open Open Open Open $/\$ $/\$ Cn $/\$ $/\$ Cn Cn

Theorem	opr1scn 8191	Construct a continuous function from a continuous operation with the second argument held constant.
Met Met Met $/\$ $/\$ Open Open Open Cn $/\$ Cn

Theorem	bopcnlem1 8192	Lemma for bopcn 8196.

Theorem	bopcnlem2 8193	Lemma for bopcn 8196.

Theorem	bopcnlem3 8194	Lemma for bopcn 8196.

Theorem	bopcnlem4 8195	Lemma for bopcn 8196.

Theorem	bopcn 8196	Conditions for a binary operation on to be continuous.
$/\$ $/\$ Open Open $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Cn

Theorem	addcn 8197	Complex number addition is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243.
$/\$ $/\$ Open Open Cn

Theorem	subcn 8198	Complex number subtraction is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243.
$/\$ $/\$ Open Open Cn

Theorem	mulcn 8199	Complex number multiplication is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243.
$/\$ $/\$ Open Open Cn

Theorem	fsumcnlem 8200	Lemma for fsumcn 8201. Warning: The HTML proof page is 0.4MB in size.

MPE Home Contents

< Previous Next >