P. 253 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 25201-25300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tcphvsca 25201	The scalar multiplication of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    ⇒   ⊢ · = ( ·𝑠 ‘𝐺)
Theorem	tcphip 25202	The inner product of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ · = (·𝑖‘𝑊)    ⇒   ⊢ · = (·𝑖‘𝐺)
Theorem	tcphtopn 25203	The topology of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ 𝐷 = (dist‘𝐺)    &   ⊢ 𝐽 = (TopOpen‘𝐺)    ⇒   ⊢ (𝑊 ∈ 𝑉 → 𝐽 = (MetOpen‘𝐷))
Theorem	tcphphl 25204	Augmentation of a subcomplex pre-Hilbert space with a norm does not affect whether it is still a pre-Hilbert space (because all the original components are the same). (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    ⇒   ⊢ (𝑊 ∈ PreHil ↔ 𝐺 ∈ PreHil)
Theorem	tchnmfval 25205*	The norm of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    ⇒   ⊢ (𝑊 ∈ Grp → 𝑁 = (𝑥 ∈ 𝑉 ↦ (√‘(𝑥 , 𝑥))))
Theorem	tcphnmval 25206	The norm of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    ⇒   ⊢ ((𝑊 ∈ Grp ∧ 𝑋 ∈ 𝑉) → (𝑁‘𝑋) = (√‘(𝑋 , 𝑋)))
Theorem	cphtcphnm 25207	The norm of a norm-augmented subcomplex pre-Hilbert space is the same as the original norm on it. (Contributed by Mario Carneiro, 11-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    ⇒   ⊢ (𝑊 ∈ ℂPreHil → 𝑁 = (norm‘𝐺))
Theorem	tcphds 25208	The distance of a pre-Hilbert space augmented with norm. (Contributed by Thierry Arnoux, 30-Jun-2019.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ − = (-g‘𝑊)    ⇒   ⊢ (𝑊 ∈ Grp → (𝑁 ∘ − ) = (dist‘𝐺))
Theorem	phclm 25209	A pre-Hilbert space whose field of scalars is a restriction of the field of complex numbers is a subcomplex module. TODO: redundant hypotheses. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ PreHil)    &   ⊢ (𝜑 → 𝐹 = (ℂfld ↾s 𝐾))    ⇒   ⊢ (𝜑 → 𝑊 ∈ ℂMod)
Theorem	tcphcphlem3 25210	Lemma for tcphcph 25214: real closure of an inner product of a vector with itself. (Contributed by Mario Carneiro, 10-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ PreHil)    &   ⊢ (𝜑 → 𝐹 = (ℂfld ↾s 𝐾))    &   ⊢ , = (·𝑖‘𝑊)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉) → (𝑋 , 𝑋) ∈ ℝ)
Theorem	ipcau2 25211*	The Cauchy-Schwarz inequality for a subcomplex pre-Hilbert space built from a pre-Hilbert space with certain properties. The main theorem is ipcau 25215. (Contributed by Mario Carneiro, 11-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ PreHil)    &   ⊢ (𝜑 → 𝐹 = (ℂfld ↾s 𝐾))    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) → (√‘𝑥) ∈ 𝐾)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 0 ≤ (𝑥 , 𝑥))    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ 𝐶 = ((𝑌 , 𝑋) / (𝑌 , 𝑌))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (abs‘(𝑋 , 𝑌)) ≤ ((𝑁‘𝑋) · (𝑁‘𝑌)))
Theorem	tcphcphlem1 25212*	Lemma for tcphcph 25214: the triangle inequality. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ PreHil)    &   ⊢ (𝜑 → 𝐹 = (ℂfld ↾s 𝐾))    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) → (√‘𝑥) ∈ 𝐾)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 0 ≤ (𝑥 , 𝑥))    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ − = (-g‘𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (√‘((𝑋 − 𝑌) , (𝑋 − 𝑌))) ≤ ((√‘(𝑋 , 𝑋)) + (√‘(𝑌 , 𝑌))))
Theorem	tcphcphlem2 25213*	Lemma for tcphcph 25214: homogeneity. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ PreHil)    &   ⊢ (𝜑 → 𝐹 = (ℂfld ↾s 𝐾))    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) → (√‘𝑥) ∈ 𝐾)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 0 ≤ (𝑥 , 𝑥))    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (√‘((𝑋 · 𝑌) , (𝑋 · 𝑌))) = ((abs‘𝑋) · (√‘(𝑌 , 𝑌))))
Theorem	tcphcph 25214*	The standard definition of a norm turns any pre-Hilbert space over a subfield of ℂfld closed under square roots of nonnegative reals into a subcomplex pre-Hilbert space (which allows access to a norm, metric, and topology). (Contributed by Mario Carneiro, 11-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ PreHil)    &   ⊢ (𝜑 → 𝐹 = (ℂfld ↾s 𝐾))    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) → (√‘𝑥) ∈ 𝐾)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 0 ≤ (𝑥 , 𝑥))    ⇒   ⊢ (𝜑 → 𝐺 ∈ ℂPreHil)
Theorem	ipcau 25215	The Cauchy-Schwarz inequality for a subcomplex pre-Hilbert space. Part of Lemma 3.2-1(a) of [Kreyszig] p. 137. This is Metamath 100 proof #78. (Contributed by NM, 12-Jan-2008.) (Revised by Mario Carneiro, 11-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (abs‘(𝑋 , 𝑌)) ≤ ((𝑁‘𝑋) · (𝑁‘𝑌)))
Theorem	nmparlem 25216	Lemma for nmpar 25217. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (((𝑁‘(𝐴 + 𝐵))↑2) + ((𝑁‘(𝐴 − 𝐵))↑2)) = (2 · (((𝑁‘𝐴)↑2) + ((𝑁‘𝐵)↑2))))
Theorem	nmpar 25217	A subcomplex pre-Hilbert space satisfies the parallelogram law. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (((𝑁‘(𝐴 + 𝐵))↑2) + ((𝑁‘(𝐴 − 𝐵))↑2)) = (2 · (((𝑁‘𝐴)↑2) + ((𝑁‘𝐵)↑2))))
Theorem	cphipval2 25218	Value of the inner product expressed by the norm defined by it. (Contributed by NM, 31-Jan-2007.) (Revised by AV, 18-Oct-2021.)
⊢ 𝑋 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 , 𝐵) = (((((𝑁‘(𝐴 + 𝐵))↑2) − ((𝑁‘(𝐴 − 𝐵))↑2)) + (i · (((𝑁‘(𝐴 + (i · 𝐵)))↑2) − ((𝑁‘(𝐴 − (i · 𝐵)))↑2)))) / 4))
Theorem	4cphipval2 25219	Four times the inner product value cphipval2 25218. (Contributed by NM, 1-Feb-2008.) (Revised by AV, 18-Oct-2021.)
⊢ 𝑋 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (4 · (𝐴 , 𝐵)) = ((((𝑁‘(𝐴 + 𝐵))↑2) − ((𝑁‘(𝐴 − 𝐵))↑2)) + (i · (((𝑁‘(𝐴 + (i · 𝐵)))↑2) − ((𝑁‘(𝐴 − (i · 𝐵)))↑2)))))
Theorem	cphipval 25220*	Value of the inner product expressed by a sum of terms with the norm defined by the inner product. Equation 6.45 of [Ponnusamy] p. 361. (Contributed by NM, 31-Jan-2007.) (Revised by AV, 18-Oct-2021.)
⊢ 𝑋 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 , 𝐵) = (Σ𝑘 ∈ (1...4)((i↑𝑘) · ((𝑁‘(𝐴 + ((i↑𝑘) · 𝐵)))↑2)) / 4))
Theorem	ipcnlem2 25221	The inner product operation of a subcomplex pre-Hilbert space is continuous. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝐷 = (dist‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ 𝑇 = ((𝑅 / 2) / ((𝑁‘𝐴) + 1))    &   ⊢ 𝑈 = ((𝑅 / 2) / ((𝑁‘𝐵) + 𝑇))    &   ⊢ (𝜑 → 𝑊 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → (𝐴𝐷𝑋) < 𝑈)    &   ⊢ (𝜑 → (𝐵𝐷𝑌) < 𝑇)    ⇒   ⊢ (𝜑 → (abs‘((𝐴 , 𝐵) − (𝑋 , 𝑌))) < 𝑅)
Theorem	ipcnlem1 25222*	The inner product operation of a subcomplex pre-Hilbert space is continuous. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝐷 = (dist‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ 𝑇 = ((𝑅 / 2) / ((𝑁‘𝐴) + 1))    &   ⊢ 𝑈 = ((𝑅 / 2) / ((𝑁‘𝐵) + 𝑇))    &   ⊢ (𝜑 → 𝑊 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (((𝐴𝐷𝑥) < 𝑟 ∧ (𝐵𝐷𝑦) < 𝑟) → (abs‘((𝐴 , 𝐵) − (𝑥 , 𝑦))) < 𝑅))
Theorem	ipcn 25223	The inner product operation of a subcomplex pre-Hilbert space is continuous. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ , = (·if‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝐾 = (TopOpen‘ℂfld)    ⇒   ⊢ (𝑊 ∈ ℂPreHil → , ∈ ((𝐽 ×t 𝐽) Cn 𝐾))
Theorem	cnmpt1ip 25224*	Continuity of inner product; analogue of cnmpt12f 23641 which cannot be used directly because ·𝑖 is not a function. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝐶 = (TopOpen‘ℂfld)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐾 Cn 𝐽))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐾 Cn 𝐽))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 , 𝐵)) ∈ (𝐾 Cn 𝐶))
Theorem	cnmpt2ip 25225*	Continuity of inner product; analogue of cnmpt22f 23650 which cannot be used directly because ·𝑖 is not a function. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝐶 = (TopOpen‘ℂfld)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐾 ×t 𝐿) Cn 𝐽))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐾 ×t 𝐿) Cn 𝐽))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝐴 , 𝐵)) ∈ ((𝐾 ×t 𝐿) Cn 𝐶))
Theorem	csscld 25226	A "closed subspace" in a subcomplex pre-Hilbert space is actually closed in the topology induced by the norm, thus justifying the terminology "closed subspace". (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ 𝐶 = (ClSubSp‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑆 ∈ 𝐶) → 𝑆 ∈ (Clsd‘𝐽))
Theorem	clsocv 25227	The orthogonal complement of the closure of a subset is the same as the orthogonal complement of the subset itself. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑂 = (ocv‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) → (𝑂‘((cls‘𝐽)‘𝑆)) = (𝑂‘𝑆))
Theorem	cphsscph 25228	A subspace of a subcomplex pre-Hilbert space is a subcomplex pre-Hilbert space. (Contributed by NM, 1-Feb-2008.) (Revised by AV, 25-Sep-2022.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ ℂPreHil)
12.5.5  Convergence and completeness
Syntax	ccfil 25229	Extend class notation with the class of Cauchy filters.
class CauFil
Syntax	ccau 25230	Extend class notation with the class of Cauchy sequences.
class Cau
Syntax	ccmet 25231	Extend class notation with the class of complete metrics.
class CMet
Definition	df-cfil 25232*	Define the set of Cauchy filters on a given extended metric space. A Cauchy filter is a filter on the set such that for every 0 < 𝑥 there is an element of the filter whose metric diameter is less than 𝑥. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ CauFil = (𝑑 ∈ ∪ ran ∞Met ↦ {𝑓 ∈ (Fil‘dom dom 𝑑) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)})
Definition	df-cau 25233*	Define the set of Cauchy sequences on a given extended metric space. (Contributed by NM, 8-Sep-2006.)
⊢ Cau = (𝑑 ∈ ∪ ran ∞Met ↦ {𝑓 ∈ (dom dom 𝑑 ↑pm ℂ) ∣ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝑑)𝑥)})
Definition	df-cmet 25234*	Define the set of complete metrics on a given set. (Contributed by Mario Carneiro, 1-May-2014.)
⊢ CMet = (𝑥 ∈ V ↦ {𝑑 ∈ (Met‘𝑥) ∣ ∀𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅})
Theorem	lmmbr 25235*	Express the binary relation "sequence 𝐹 converges to point 𝑃 " in a metric space. Definition 1.4-1 of [Kreyszig] p. 25. The condition 𝐹 ⊆ (ℂ × 𝑋) allows to use objects more general than sequences when convenient; see the comment in df-lm 23204. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 1-May-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ 𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥))))
Theorem	lmmbr2 25236*	Express the binary relation "sequence 𝐹 converges to point 𝑃 " in a metric space. Definition 1.4-1 of [Kreyszig] p. 25. The condition 𝐹 ⊆ (ℂ × 𝑋) allows to use objects more general than sequences when convenient; see the comment in df-lm 23204. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 1-May-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ 𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷𝑃) < 𝑥))))
Theorem	lmmbr3 25237*	Express the binary relation "sequence 𝐹 converges to point 𝑃 " in a metric space using an arbitrary upper set of integers. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 1-May-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ 𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷𝑃) < 𝑥))))
Theorem	lmmcvg 25238*	Convergence property of a converging sequence. (Contributed by NM, 1-Jun-2007.) (Revised by Mario Carneiro, 1-May-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    &   ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐴 ∈ 𝑋 ∧ (𝐴𝐷𝑃) < 𝑅))
Theorem	lmmbrf 25239*	Express the binary relation "sequence 𝐹 converges to point 𝑃 " in a metric space using an arbitrary upper set of integers. This version of lmmbr2 25236 presupposes that 𝐹 is a function. (Contributed by NM, 20-Jul-2007.) (Revised by Mario Carneiro, 1-May-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    &   ⊢ (𝜑 → 𝐹:𝑍⟶𝑋)    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐴𝐷𝑃) < 𝑥)))
Theorem	lmnn 25240*	A condition that implies convergence. (Contributed by NM, 8-Jun-2007.) (Revised by Mario Carneiro, 1-May-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝑃 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹:ℕ⟶𝑋)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘)𝐷𝑃) < (1 / 𝑘))    ⇒   ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃)
Theorem	cfilfval 25241*	The set of Cauchy filters on a metric space. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → (CauFil‘𝐷) = {𝑓 ∈ (Fil‘𝑋) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)})
Theorem	iscfil 25242*	The property of being a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (CauFil‘𝐷) ↔ (𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐹 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))))
Theorem	iscfil2 25243*	The property of being a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (CauFil‘𝐷) ↔ (𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐹 ∀𝑧 ∈ 𝑦 ∀𝑤 ∈ 𝑦 (𝑧𝐷𝑤) < 𝑥)))
Theorem	cfilfil 25244	A Cauchy filter is a filter. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (CauFil‘𝐷)) → 𝐹 ∈ (Fil‘𝑋))
Theorem	cfili 25245*	Property of a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ ((𝐹 ∈ (CauFil‘𝐷) ∧ 𝑅 ∈ ℝ+) → ∃𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦𝐷𝑧) < 𝑅)
Theorem	cfil3i 25246*	A Cauchy filter contains balls of any pre-chosen size. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (CauFil‘𝐷) ∧ 𝑅 ∈ ℝ+) → ∃𝑥 ∈ 𝑋 (𝑥(ball‘𝐷)𝑅) ∈ 𝐹)
Theorem	cfilss 25247	A filter finer than a Cauchy filter is Cauchy. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (CauFil‘𝐷)) ∧ (𝐺 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝐺)) → 𝐺 ∈ (CauFil‘𝐷))
Theorem	fgcfil 25248*	The Cauchy filter condition for a filter base. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) → ((𝑋filGen𝐵) ∈ (CauFil‘𝐷) ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑦 ∀𝑤 ∈ 𝑦 (𝑧𝐷𝑤) < 𝑥))
Theorem	fmcfil 25249*	The Cauchy filter condition for a filter map. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (((𝑋 FilMap 𝐹)‘𝐵) ∈ (CauFil‘𝐷) ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑦 ∀𝑤 ∈ 𝑦 ((𝐹‘𝑧)𝐷(𝐹‘𝑤)) < 𝑥))
Theorem	iscfil3 25250*	A filter is Cauchy iff it contains a ball of any chosen size. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (CauFil‘𝐷) ↔ (𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑟 ∈ ℝ+ ∃𝑥 ∈ 𝑋 (𝑥(ball‘𝐷)𝑟) ∈ 𝐹)))
Theorem	cfilfcls 25251	Similar to ultrafilters (uffclsflim 24006), the cluster points and limit points of a Cauchy filter coincide. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝑋 = dom dom 𝐷    ⇒   ⊢ (𝐹 ∈ (CauFil‘𝐷) → (𝐽 fClus 𝐹) = (𝐽 fLim 𝐹))
Theorem	caufval 25252*	The set of Cauchy sequences on a metric space. (Contributed by NM, 8-Sep-2006.) (Revised by Mario Carneiro, 5-Sep-2015.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → (Cau‘𝐷) = {𝑓 ∈ (𝑋 ↑pm ℂ) ∣ ∀𝑥 ∈ ℝ+ ∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)𝑥)})
Theorem	iscau 25253*	Express the property "𝐹 is a Cauchy sequence of metric 𝐷". Part of Definition 1.4-3 of [Kreyszig] p. 28. The condition 𝐹 ⊆ (ℂ × 𝑋) allows to use objects more general than sequences when convenient; see the comment in df-lm 23204. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 14-Nov-2013.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ ∀𝑥 ∈ ℝ+ ∃𝑘 ∈ ℤ (𝐹 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝐹‘𝑘)(ball‘𝐷)𝑥))))
Theorem	iscau2 25254*	Express the property "𝐹 is a Cauchy sequence of metric 𝐷 " using an arbitrary upper set of integers. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 14-Nov-2013.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑥))))
Theorem	iscau3 25255*	Express the Cauchy sequence property in the more conventional three-quantifier form. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 14-Nov-2013.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑚)) < 𝑥))))
Theorem	iscau4 25256*	Express the property "𝐹 is a Cauchy sequence of metric 𝐷 " using an arbitrary upper set of integers. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 23-Dec-2013.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐹‘𝑗) = 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ∧ (𝐴𝐷𝐵) < 𝑥))))
Theorem	iscauf 25257*	Express the property "𝐹 is a Cauchy sequence of metric 𝐷 " presupposing 𝐹 is a function. (Contributed by NM, 24-Jul-2007.) (Revised by Mario Carneiro, 23-Dec-2013.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    &   ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐹‘𝑗) = 𝐵)    &   ⊢ (𝜑 → 𝐹:𝑍⟶𝑋)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵𝐷𝐴) < 𝑥))
Theorem	caun0 25258	A metric with a Cauchy sequence cannot be empty. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 24-Dec-2013.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Cau‘𝐷)) → 𝑋 ≠ ∅)
Theorem	caufpm 25259	Inclusion of a Cauchy sequence, under our definition. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 24-Dec-2013.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Cau‘𝐷)) → 𝐹 ∈ (𝑋 ↑pm ℂ))
Theorem	caucfil 25260	A Cauchy sequence predicate can be expressed in terms of the Cauchy filter predicate for a suitably chosen filter. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝐿 = ((𝑋 FilMap 𝐹)‘(ℤ≥ “ 𝑍))    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶𝑋) → (𝐹 ∈ (Cau‘𝐷) ↔ 𝐿 ∈ (CauFil‘𝐷)))
Theorem	iscmet 25261*	The property "𝐷 is a complete metric." meaning all Cauchy filters converge to a point in the space. (Contributed by Mario Carneiro, 1-May-2014.) (Revised by Mario Carneiro, 13-Oct-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ (𝐷 ∈ (CMet‘𝑋) ↔ (𝐷 ∈ (Met‘𝑋) ∧ ∀𝑓 ∈ (CauFil‘𝐷)(𝐽 fLim 𝑓) ≠ ∅))
Theorem	cmetcvg 25262	The convergence of a Cauchy filter in a complete metric space. (Contributed by Mario Carneiro, 14-Oct-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝐹 ∈ (CauFil‘𝐷)) → (𝐽 fLim 𝐹) ≠ ∅)
Theorem	cmetmet 25263	A complete metric space is a metric space. (Contributed by NM, 18-Dec-2006.) (Revised by Mario Carneiro, 29-Jan-2014.)
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
Theorem	cmetmeti 25264	A complete metric space is a metric space. (Contributed by NM, 26-Oct-2007.)
⊢ 𝐷 ∈ (CMet‘𝑋)    ⇒   ⊢ 𝐷 ∈ (Met‘𝑋)
Theorem	cmetcaulem 25265*	Lemma for cmetcau 25266. (Contributed by Mario Carneiro, 14-Oct-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ (𝜑 → 𝑃 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ (Cau‘𝐷))    &   ⊢ 𝐺 = (𝑥 ∈ ℕ ↦ if(𝑥 ∈ dom 𝐹, (𝐹‘𝑥), 𝑃))    ⇒   ⊢ (𝜑 → 𝐹 ∈ dom (⇝𝑡‘𝐽))
Theorem	cmetcau 25266	The convergence of a Cauchy sequence in a complete metric space. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 14-Oct-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝐹 ∈ (Cau‘𝐷)) → 𝐹 ∈ dom (⇝𝑡‘𝐽))
Theorem	iscmet3lem3 25267*	Lemma for iscmet3 25270. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((1 / 2)↑𝑘) < 𝑅)
Theorem	iscmet3lem1 25268*	Lemma for iscmet3 25270. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝐹:𝑍⟶𝑋)    &   ⊢ (𝜑 → ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑆‘𝑘)∀𝑣 ∈ (𝑆‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘))    &   ⊢ (𝜑 → ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝐹‘𝑘) ∈ (𝑆‘𝑛))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (Cau‘𝐷))
Theorem	iscmet3lem2 25269*	Lemma for iscmet3 25270. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝐹:𝑍⟶𝑋)    &   ⊢ (𝜑 → ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑆‘𝑘)∀𝑣 ∈ (𝑆‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘))    &   ⊢ (𝜑 → ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝐹‘𝑘) ∈ (𝑆‘𝑛))    &   ⊢ (𝜑 → 𝐺 ∈ (Fil‘𝑋))    &   ⊢ (𝜑 → 𝑆:ℤ⟶𝐺)    &   ⊢ (𝜑 → 𝐹 ∈ dom (⇝𝑡‘𝐽))    ⇒   ⊢ (𝜑 → (𝐽 fLim 𝐺) ≠ ∅)
Theorem	iscmet3 25270*	The property "𝐷 is a complete metric" expressed in terms of functions on ℕ (or any other upper integer set). Thus, we only have to look at functions on ℕ, and not all possible Cauchy filters, to determine completeness. (The proof uses countable choice.) (Contributed by NM, 18-Dec-2006.) (Revised by Mario Carneiro, 5-May-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    ⇒   ⊢ (𝜑 → (𝐷 ∈ (CMet‘𝑋) ↔ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽))))
Theorem	iscmet2 25271	A metric 𝐷 is complete iff all Cauchy sequences converge to a point in the space. The proof uses countable choice. Part of Definition 1.4-3 of [Kreyszig] p. 28. (Contributed by NM, 7-Sep-2006.) (Revised by Mario Carneiro, 15-Oct-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ (𝐷 ∈ (CMet‘𝑋) ↔ (𝐷 ∈ (Met‘𝑋) ∧ (Cau‘𝐷) ⊆ dom (⇝𝑡‘𝐽)))
Theorem	cfilresi 25272	A Cauchy filter on a metric subspace extends to a Cauchy filter in the larger space. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → (𝑋filGen𝐹) ∈ (CauFil‘𝐷))
Theorem	cfilres 25273	Cauchy filter on a metric subspace. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → (𝐹 ∈ (CauFil‘𝐷) ↔ (𝐹 ↾t 𝑌) ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))))
Theorem	caussi 25274	Cauchy sequence on a metric subspace. (Contributed by NM, 30-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → (Cau‘(𝐷 ↾ (𝑌 × 𝑌))) ⊆ (Cau‘𝐷))
Theorem	causs 25275	Cauchy sequence on a metric subspace. (Contributed by NM, 29-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶𝑌) → (𝐹 ∈ (Cau‘𝐷) ↔ 𝐹 ∈ (Cau‘(𝐷 ↾ (𝑌 × 𝑌)))))
Theorem	equivcfil 25276*	If the metric 𝐷 is "strongly finer" than 𝐶 (meaning that there is a positive real constant 𝑅 such that 𝐶(𝑥, 𝑦) ≤ 𝑅 · 𝐷(𝑥, 𝑦)), all the 𝐷-Cauchy filters are also 𝐶-Cauchy. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then they have the same Cauchy sequences.) (Contributed by Mario Carneiro, 14-Sep-2015.)
⊢ (𝜑 → 𝐶 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐶𝑦) ≤ (𝑅 · (𝑥𝐷𝑦)))    ⇒   ⊢ (𝜑 → (CauFil‘𝐷) ⊆ (CauFil‘𝐶))
Theorem	equivcau 25277*	If the metric 𝐷 is "strongly finer" than 𝐶 (meaning that there is a positive real constant 𝑅 such that 𝐶(𝑥, 𝑦) ≤ 𝑅 · 𝐷(𝑥, 𝑦)), all the 𝐷-Cauchy sequences are also 𝐶-Cauchy. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then they have the same Cauchy sequences.) (Contributed by Mario Carneiro, 14-Sep-2015.)
⊢ (𝜑 → 𝐶 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐶𝑦) ≤ (𝑅 · (𝑥𝐷𝑦)))    ⇒   ⊢ (𝜑 → (Cau‘𝐷) ⊆ (Cau‘𝐶))
Theorem	lmle 25278*	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. (Contributed by NM, 23-Dec-2007.) (Proof shortened by Mario Carneiro, 1-May-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ*)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑄𝐷(𝐹‘𝑘)) ≤ 𝑅)    ⇒   ⊢ (𝜑 → (𝑄𝐷𝑃) ≤ 𝑅)
Theorem	nglmle 25279*	If the norm of each member of a converging sequence is less than or equal to a given amount, so is the norm of the convergence value. (Contributed by NM, 25-Dec-2007.) (Revised by AV, 16-Oct-2021.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐷 = ((dist‘𝐺) ↾ (𝑋 × 𝑋))    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ NrmGrp)    &   ⊢ (𝜑 → 𝐹:ℕ⟶𝑋)    &   ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ*)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑁‘(𝐹‘𝑘)) ≤ 𝑅)    ⇒   ⊢ (𝜑 → (𝑁‘𝑃) ≤ 𝑅)
Theorem	lmclim 25280	Relate a limit on the metric space of complex numbers to our complex number limit notation. (Contributed by NM, 9-Dec-2006.) (Revised by Mario Carneiro, 1-May-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ ((𝑀 ∈ ℤ ∧ 𝑍 ⊆ dom 𝐹) → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ∈ (ℂ ↑pm ℂ) ∧ 𝐹 ⇝ 𝑃)))
Theorem	lmclimf 25281	Relate a limit on the metric space of complex numbers to our complex number limit notation. (Contributed by NM, 24-Jul-2007.) (Revised by Mario Carneiro, 1-May-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ ((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℂ) → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ 𝐹 ⇝ 𝑃))
Theorem	metelcls 25282*	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. This proof uses countable choice ax-cc 10348. The statement can be generalized to first-countable spaces, not just metrizable spaces. (Contributed by NM, 8-Nov-2007.) (Proof shortened by Mario Carneiro, 1-May-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)))
Theorem	metcld 25283*	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. (Contributed by NM, 11-Nov-2007.) (Revised by Mario Carneiro, 1-May-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ (Clsd‘𝐽) ↔ ∀𝑥∀𝑓((𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑥) → 𝑥 ∈ 𝑆)))
Theorem	metcld2 25284	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. (Contributed by Mario Carneiro, 1-May-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ (Clsd‘𝐽) ↔ ((⇝𝑡‘𝐽) “ (𝑆 ↑m ℕ)) ⊆ 𝑆))
Theorem	caubl 25285*	Sufficient condition to ensure a sequence of nested balls is Cauchy. (Contributed by Mario Carneiro, 18-Jan-2014.) (Revised by Mario Carneiro, 1-May-2014.)
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝐹:ℕ⟶(𝑋 × ℝ+))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ ((ball‘𝐷)‘(𝐹‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)))    &   ⊢ (𝜑 → ∀𝑟 ∈ ℝ+ ∃𝑛 ∈ ℕ (2nd ‘(𝐹‘𝑛)) < 𝑟)    ⇒   ⊢ (𝜑 → (1st ∘ 𝐹) ∈ (Cau‘𝐷))
Theorem	caublcls 25286*	The convergent point of a sequence of nested balls is in the closures of any of the balls (i.e. it is in the intersection of the closures). Indeed, it is the only point in the intersection because a metric space is Hausdorff, but we don't prove this here. (Contributed by Mario Carneiro, 21-Jan-2014.) (Revised by Mario Carneiro, 1-May-2014.)
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝐹:ℕ⟶(𝑋 × ℝ+))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ ((ball‘𝐷)‘(𝐹‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)))    &   ⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝜑 ∧ (1st ∘ 𝐹)(⇝𝑡‘𝐽)𝑃 ∧ 𝐴 ∈ ℕ) → 𝑃 ∈ ((cls‘𝐽)‘((ball‘𝐷)‘(𝐹‘𝐴))))
Theorem	metcnp4 25287*	Two ways to say a mapping from metric 𝐶 to metric 𝐷 is continuous at point 𝑃. Theorem 14-4.3 of [Gleason] p. 240. (Contributed by NM, 17-May-2007.) (Revised by Mario Carneiro, 4-May-2014.)
⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑌))    &   ⊢ (𝜑 → 𝑃 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))))
Theorem	metcn4 25288*	Two ways to say a mapping from metric 𝐶 to metric 𝐷 is continuous. Theorem 10.3 of [Munkres] p. 128. (Contributed by NM, 13-Jun-2007.) (Revised by Mario Carneiro, 4-May-2014.)
⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑌))    &   ⊢ (𝜑 → 𝐹:𝑋⟶𝑌)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ∀𝑓(𝑓:ℕ⟶𝑋 → ∀𝑥(𝑓(⇝𝑡‘𝐽)𝑥 → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑥)))))
Theorem	iscmet3i 25289*	Properties that determine a complete metric space. (Contributed by NM, 15-Apr-2007.) (Revised by Mario Carneiro, 5-May-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐷 ∈ (Met‘𝑋)    &   ⊢ ((𝑓 ∈ (Cau‘𝐷) ∧ 𝑓:ℕ⟶𝑋) → 𝑓 ∈ dom (⇝𝑡‘𝐽))    ⇒   ⊢ 𝐷 ∈ (CMet‘𝑋)
Theorem	lmcau 25290	Every convergent sequence in a metric space is a Cauchy sequence. Theorem 1.4-5 of [Kreyszig] p. 28. (Contributed by NM, 29-Jan-2008.) (Proof shortened by Mario Carneiro, 5-May-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → dom (⇝𝑡‘𝐽) ⊆ (Cau‘𝐷))
Theorem	flimcfil 25291	Every convergent filter in a metric space is a Cauchy filter. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝐹)) → 𝐹 ∈ (CauFil‘𝐷))
Theorem	metsscmetcld 25292	A complete subspace of a metric space is closed in the parent space. Formerly part of proof for cmetss 25293. (Contributed by NM, 28-Jan-2008.) (Revised by Mario Carneiro, 15-Oct-2015.) (Revised by AV, 9-Oct-2022.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐷 ↾ (𝑌 × 𝑌)) ∈ (CMet‘𝑌)) → 𝑌 ∈ (Clsd‘𝐽))
Theorem	cmetss 25293	A subspace of a complete metric space is complete iff it is closed in the parent space. Theorem 1.4-7 of [Kreyszig] p. 30. (Contributed by NM, 28-Jan-2008.) (Revised by Mario Carneiro, 15-Oct-2015.) (Proof shortened by AV, 9-Oct-2022.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ (𝐷 ∈ (CMet‘𝑋) → ((𝐷 ↾ (𝑌 × 𝑌)) ∈ (CMet‘𝑌) ↔ 𝑌 ∈ (Clsd‘𝐽)))
Theorem	equivcmet 25294*	If two metrics are strongly equivalent, one is complete iff the other is. Unlike equivcau 25277, metss2 24487, this theorem does not have a one-directional form - it is possible for a metric 𝐶 that is strongly finer than the complete metric 𝐷 to be incomplete and vice versa. Consider 𝐷 = the metric on ℝ induced by the usual homeomorphism from (0, 1) against the usual metric 𝐶 on ℝ and against the discrete metric 𝐸 on ℝ. Then both 𝐶 and 𝐸 are complete but 𝐷 is not, and 𝐶 is strongly finer than 𝐷, which is strongly finer than 𝐸. (Contributed by Mario Carneiro, 15-Sep-2015.)
⊢ (𝜑 → 𝐶 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑆 ∈ ℝ+)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐶𝑦) ≤ (𝑅 · (𝑥𝐷𝑦)))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐷𝑦) ≤ (𝑆 · (𝑥𝐶𝑦)))    ⇒   ⊢ (𝜑 → (𝐶 ∈ (CMet‘𝑋) ↔ 𝐷 ∈ (CMet‘𝑋)))
Theorem	relcmpcmet 25295*	If 𝐷 is a metric space such that all the balls of some fixed size are relatively compact, then 𝐷 is complete. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐽 ↾t ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑅))) ∈ Comp)    ⇒   ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))
Theorem	cmpcmet 25296	A compact metric space is complete. One half of heibor 38156. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    ⇒   ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))
Theorem	cfilucfil3 25297	Given a metric 𝐷 and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the Cauchy filters for the metric. (Contributed by Thierry Arnoux, 15-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (∞Met‘𝑋)) → ((𝐶 ∈ (Fil‘𝑋) ∧ 𝐶 ∈ (CauFilu‘(metUnif‘𝐷))) ↔ 𝐶 ∈ (CauFil‘𝐷)))
Theorem	cfilucfil4 25298	Given a metric 𝐷 and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the Cauchy filters for the metric. (Contributed by Thierry Arnoux, 15-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (∞Met‘𝑋) ∧ 𝐶 ∈ (Fil‘𝑋)) → (𝐶 ∈ (CauFilu‘(metUnif‘𝐷)) ↔ 𝐶 ∈ (CauFil‘𝐷)))
Theorem	cncmet 25299	The set of complex numbers is a complete metric space under the absolute value metric. (Contributed by NM, 20-Dec-2006.) (Revised by Mario Carneiro, 15-Oct-2015.)
⊢ 𝐷 = (abs ∘ − )    ⇒   ⊢ 𝐷 ∈ (CMet‘ℂ)
Theorem	recmet 25300	The real numbers are a complete metric space. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
⊢ ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (CMet‘ℝ)