mmtheorems80 - 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-10674

Color key:

Metamath Proof Explorer (1-8741)

Hilbert Space Explorer (8742-10674)

**Statement List for Metamath Proof Explorer -** 7901-8000 - Page 80 of 107
Type	Label	Description
Statement

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

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

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

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

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

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

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

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

Theorem	iscms 7909	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 7910	The convergence of a Cauchy sequence in a complete metric space.
CMet $/\$ Cau

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

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

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

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

Theorem	lmsslem 7915	Lemma for lmss 7916 and causs 7918.

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

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

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

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

Theorem	lmfexlem2 7920	Lemma for lmfex 7922. When the value of exists, it equals the value of .

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

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

Theorem	lmle 7923	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 7924	A complete metric space is a metric space.
CMet Met

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

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

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

Theorem	metelcls 7928	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 7929	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 7930	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 7931	Lemma for metcnp4 7933.

Theorem	metcnp4lem2 7932	Lemma for metcnp4 7933.

Theorem	metcnp4 7933	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 7934	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 7935	Convergence carries through a continuous mapping.
Open Open $/\$ Met $/\$ Met $/\$ Cn $/\$ $/\$

Theorem	xplmi 7936	Two sequences converge if the sequence of their ordered pairs converges