HomeUnicode version.
| Home |
Metamath Proof Explorer | < Previous Next > |
| Browser slow? Try the
Unicode version. |
| Color key: | Metamath Proof Explorer
(1-8757)
|
Hilbert Space Explorer
(8758-10682)
|
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | iscauf 7901 |
Express the property " is a Cauchy sequence of metric  "
presupposing
is a function.
|
              Met     Cau           | ||
| Theorem | iscau5 7902 |
Express the property " is a Cauchy sequence of metric
."
|
Met  Cau 
| ||
| Theorem | lmcvgnns 7903 | Convergence property of a converging sequence. |
 Met
  
 | ||
| Theorem | caun0 7904 | A metric with a Cauchy sequence cannot be empty. |
Met
Cau   | ||
| Theorem | iscms 7905 |
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 7906 | The convergence of a Cauchy sequence in a complete metric space. |
| CMet
Cau
| ||
| Theorem | lmfss 7907 | Inclusion of a function having a limit (used to ensure the limit relation is a set, under our definition). |
Met
   | ||
| Theorem | lmcl 7908 | Closure of a limit. |
| Met
| ||
| Theorem | caufss 7909 | Inclusion of a Cauchy sequence, under our definition. |
| Met
Cau | ||
| Theorem | lmuni 7910 | A sequence converges to at most one limit. Part of Lemma 1.4-2(a) of [Kreyszig] p. 26. |
 Met
| ||
| Theorem | lmsslem 7911 | Lemma for lmss 7912 and causs 7914. |
| Theorem | lmss 7912 | Limit on a metric subspace. |
Met
  | ||
| Theorem | caussi 7913 | Cauchy sequence on a metric subspace. |
| Met
Cau
Cau | ||
| Theorem | causs 7914 | Cauchy sequence on a metric subspace. |
| Met Cau Cau
| ||
| Theorem | lmfexlem1 7915 |
Lemma for lmfex 7918.  is a function constructed from an arbitrary
sequence , from
to the metric space
base set.
|
| Theorem | lmfexlem2 7916 |
Lemma for lmfex 7918. When the value of exists, it equals the
value of .
|
| Theorem | lmfexlem3 7917 |
Lemma for lmfex 7918. If converges, so does the function
constructed from it.
|
| Theorem | lmfex 7918 |
If (not necessarily a
function) converges, there is a function
 that converges to
the same point.
|
| Met
| ||
| Theorem | lmle 7919 | 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 7920 | A complete metric space is a metric space. |
| CMet Met | ||
| Theorem | cmsmeti 7921 | A complete metric space is a metric space. |
|
CMet Met | ||
| Theorem | lmclim 7922 | Relate a limit on the metric space of complex numbers to our complex number limit notation. |
  
 | ||
| Theorem | lmclimnn 7923 | Relate a limit on the metric space of complex numbers to our complex number limit notation. |
| | ||
| Theorem | metelcls 7924 | 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 | metcld 7925 | 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 7926 | Lemma for metcnp4 7928. |
| Theorem | metcnp4lem2 7927 | Lemma for metcnp4 7928. |
| Theorem | metcnp4 7928 |
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 7929 |
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 7930 | Convergence carries through a continuous mapping. |
Open Open  Met
Met Cn | ||
| Theorem | xplmi 7931 | 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 7932 |
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
| ||