P. 257 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 25601-25700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	clsocv 25601	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 25602	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 25603	Extend class notation with the class of Cauchy filters.
class CauFil
Syntax	ccau 25604	Extend class notation with the class of Cauchy sequences.
class Cau
Syntax	ccmet 25605	Extend class notation with the class of complete metrics.
class CMet
Definition	df-cfil 25606*	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 25607*	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 25608*	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 25609*	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 23577. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 1-May-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ 𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥))))
Theorem	lmmbr2 25610*	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 23577. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 1-May-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ 𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷𝑃) < 𝑥))))
Theorem	lmmbr3 25611*	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 25612*	Convergence property of a converging sequence. (Contributed by NM, 1-Jun-2007.) (Revised by Mario Carneiro, 1-May-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    &   ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐴 ∈ 𝑋 ∧ (𝐴𝐷𝑃) < 𝑅))
Theorem	lmmbrf 25613*	Express the binary relation "sequence 𝐹 converges to point 𝑃 " in a metric space using an arbitrary upper set of integers. This version of lmmbr2 25610 presupposes that 𝐹 is a function. (Contributed by NM, 20-Jul-2007.) (Revised by Mario Carneiro, 1-May-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    &   ⊢ (𝜑 → 𝐹:𝑍⟶𝑋)    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐴𝐷𝑃) < 𝑥)))
Theorem	lmnn 25614*	A condition that implies convergence. (Contributed by NM, 8-Jun-2007.) (Revised by Mario Carneiro, 1-May-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝑃 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹:ℕ⟶𝑋)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘)𝐷𝑃) < (1 / 𝑘))    ⇒   ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃)
Theorem	cfilfval 25615*	The set of Cauchy filters on a metric space. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → (CauFil‘𝐷) = {𝑓 ∈ (Fil‘𝑋) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)})
Theorem	iscfil 25616*	The property of being a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (CauFil‘𝐷) ↔ (𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐹 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))))
Theorem	iscfil2 25617*	The property of being a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (CauFil‘𝐷) ↔ (𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐹 ∀𝑧 ∈ 𝑦 ∀𝑤 ∈ 𝑦 (𝑧𝐷𝑤) < 𝑥)))
Theorem	cfilfil 25618	A Cauchy filter is a filter. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (CauFil‘𝐷)) → 𝐹 ∈ (Fil‘𝑋))
Theorem	cfili 25619*	Property of a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ ((𝐹 ∈ (CauFil‘𝐷) ∧ 𝑅 ∈ ℝ+) → ∃𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦𝐷𝑧) < 𝑅)
Theorem	cfil3i 25620*	A Cauchy filter contains balls of any pre-chosen size. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (CauFil‘𝐷) ∧ 𝑅 ∈ ℝ+) → ∃𝑥 ∈ 𝑋 (𝑥(ball‘𝐷)𝑅) ∈ 𝐹)
Theorem	cfilss 25621	A filter finer than a Cauchy filter is Cauchy. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (CauFil‘𝐷)) ∧ (𝐺 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝐺)) → 𝐺 ∈ (CauFil‘𝐷))
Theorem	fgcfil 25622*	The Cauchy filter condition for a filter base. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) → ((𝑋filGen𝐵) ∈ (CauFil‘𝐷) ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑦 ∀𝑤 ∈ 𝑦 (𝑧𝐷𝑤) < 𝑥))
Theorem	fmcfil 25623*	The Cauchy filter condition for a filter map. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (((𝑋 FilMap 𝐹)‘𝐵) ∈ (CauFil‘𝐷) ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑦 ∀𝑤 ∈ 𝑦 ((𝐹‘𝑧)𝐷(𝐹‘𝑤)) < 𝑥))
Theorem	iscfil3 25624*	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 25625	Similar to ultrafilters (uffclsflim 24380), 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 25626*	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 25627*	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 23577. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 14-Nov-2013.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ ∀𝑥 ∈ ℝ+ ∃𝑘 ∈ ℤ (𝐹 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝐹‘𝑘)(ball‘𝐷)𝑥))))
Theorem	iscau2 25628*	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 25629*	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 25630*	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 25631*	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 25632	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 25633	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 25634	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 25635*	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 25636	The convergence of a Cauchy filter in a complete metric space. (Contributed by Mario Carneiro, 14-Oct-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝐹 ∈ (CauFil‘𝐷)) → (𝐽 fLim 𝐹) ≠ ∅)
Theorem	cmetmet 25637	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 25638	A complete metric space is a metric space. (Contributed by NM, 26-Oct-2007.)
⊢ 𝐷 ∈ (CMet‘𝑋)    ⇒   ⊢ 𝐷 ∈ (Met‘𝑋)
Theorem	cmetcaulem 25639*	Lemma for cmetcau 25640. (Contributed by Mario Carneiro, 14-Oct-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ (𝜑 → 𝑃 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ (Cau‘𝐷))    &   ⊢ 𝐺 = (𝑥 ∈ ℕ ↦ if(𝑥 ∈ dom 𝐹, (𝐹‘𝑥), 𝑃))    ⇒   ⊢ (𝜑 → 𝐹 ∈ dom (⇝𝑡‘𝐽))
Theorem	cmetcau 25640	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 25641*	Lemma for iscmet3 25644. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((1 / 2)↑𝑘) < 𝑅)
Theorem	iscmet3lem1 25642*	Lemma for iscmet3 25644. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝐹:𝑍⟶𝑋)    &   ⊢ (𝜑 → ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑆‘𝑘)∀𝑣 ∈ (𝑆‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘))    &   ⊢ (𝜑 → ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝐹‘𝑘) ∈ (𝑆‘𝑛))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (Cau‘𝐷))
Theorem	iscmet3lem2 25643*	Lemma for iscmet3 25644. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝐹:𝑍⟶𝑋)    &   ⊢ (𝜑 → ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑆‘𝑘)∀𝑣 ∈ (𝑆‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘))    &   ⊢ (𝜑 → ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝐹‘𝑘) ∈ (𝑆‘𝑛))    &   ⊢ (𝜑 → 𝐺 ∈ (Fil‘𝑋))    &   ⊢ (𝜑 → 𝑆:ℤ⟶𝐺)    &   ⊢ (𝜑 → 𝐹 ∈ dom (⇝𝑡‘𝐽))    ⇒   ⊢ (𝜑 → (𝐽 fLim 𝐺) ≠ ∅)
Theorem	iscmet3 25644*	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 25645	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 25646	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 25647	Cauchy filter on a metric subspace. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → (𝐹 ∈ (CauFil‘𝐷) ↔ (𝐹 ↾t 𝑌) ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))))
Theorem	caussi 25648	Cauchy sequence on a metric subspace. (Contributed by NM, 30-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → (Cau‘(𝐷 ↾ (𝑌 × 𝑌))) ⊆ (Cau‘𝐷))
Theorem	causs 25649	Cauchy sequence on a metric subspace. (Contributed by NM, 29-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶𝑌) → (𝐹 ∈ (Cau‘𝐷) ↔ 𝐹 ∈ (Cau‘(𝐷 ↾ (𝑌 × 𝑌)))))
Theorem	equivcfil 25650*	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 25651*	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 25652*	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 25653*	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 25654	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 25655	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 25656*	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 10540. 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 25657*	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 25658	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 25659*	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 25660*	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 25661*	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 25662*	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 25663*	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 25664	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 25665	Every convergent filter in a metric space is a Cauchy filter. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝐹)) → 𝐹 ∈ (CauFil‘𝐷))
Theorem	metsscmetcld 25666	A complete subspace of a metric space is closed in the parent space. Formerly part of proof for cmetss 25667. (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 25667	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 25668*	If two metrics are strongly equivalent, one is complete iff the other is. Unlike equivcau 25651, metss2 24861, 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 25669*	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 25670	A compact metric space is complete. One half of heibor 38947. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    ⇒   ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))
Theorem	cfilucfil3 25671	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 25672	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 25673	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 25674	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‘ℝ)
12.5.6  Baire's Category Theorem
Theorem	bcthlem1 25675*	Lemma for bcth 25680. Substitutions for the function 𝐹. (Contributed by Mario Carneiro, 9-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ 𝐹 = (𝑘 ∈ ℕ, 𝑧 ∈ (𝑋 × ℝ+) ↦ {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))})    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ ℕ ∧ 𝐵 ∈ (𝑋 × ℝ+))) → (𝐶 ∈ (𝐴𝐹𝐵) ↔ (𝐶 ∈ (𝑋 × ℝ+) ∧ (2nd ‘𝐶) < (1 / 𝐴) ∧ ((cls‘𝐽)‘((ball‘𝐷)‘𝐶)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴)))))
Theorem	bcthlem2 25676*	Lemma for bcth 25680. The balls in the sequence form an inclusion chain. (Contributed by Mario Carneiro, 7-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ 𝐹 = (𝑘 ∈ ℕ, 𝑧 ∈ (𝑋 × ℝ+) ↦ {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))})    &   ⊢ (𝜑 → 𝑀:ℕ⟶(Clsd‘𝐽))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑔:ℕ⟶(𝑋 × ℝ+))    &   ⊢ (𝜑 → (𝑔‘1) = ⟨𝐶, 𝑅⟩)    &   ⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔‘𝑘)))    ⇒   ⊢ (𝜑 → ∀𝑛 ∈ ℕ ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝑔‘𝑛)))
Theorem	bcthlem3 25677*	Lemma for bcth 25680. The limit point of the centers in the sequence is in the intersection of every ball in the sequence. (Contributed by Mario Carneiro, 7-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ 𝐹 = (𝑘 ∈ ℕ, 𝑧 ∈ (𝑋 × ℝ+) ↦ {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))})    &   ⊢ (𝜑 → 𝑀:ℕ⟶(Clsd‘𝐽))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑔:ℕ⟶(𝑋 × ℝ+))    &   ⊢ (𝜑 → (𝑔‘1) = ⟨𝐶, 𝑅⟩)    &   ⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔‘𝑘)))    ⇒   ⊢ ((𝜑 ∧ (1st ∘ 𝑔)(⇝𝑡‘𝐽)𝑥 ∧ 𝐴 ∈ ℕ) → 𝑥 ∈ ((ball‘𝐷)‘(𝑔‘𝐴)))
Theorem	bcthlem4 25678*	Lemma for bcth 25680. Given any open ball (𝐶(ball‘𝐷)𝑅) as starting point (and in particular, a ball in int(∪ ran 𝑀)), the limit point 𝑥 of the centers of the induced sequence of balls 𝑔 is outside ∪ ran 𝑀. Note that a set 𝐴 has empty interior iff every nonempty open set 𝑈 contains points outside 𝐴, i.e. (𝑈 ∖ 𝐴) ≠ ∅. (Contributed by Mario Carneiro, 7-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ 𝐹 = (𝑘 ∈ ℕ, 𝑧 ∈ (𝑋 × ℝ+) ↦ {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))})    &   ⊢ (𝜑 → 𝑀:ℕ⟶(Clsd‘𝐽))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑔:ℕ⟶(𝑋 × ℝ+))    &   ⊢ (𝜑 → (𝑔‘1) = ⟨𝐶, 𝑅⟩)    &   ⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔‘𝑘)))    ⇒   ⊢ (𝜑 → ((𝐶(ball‘𝐷)𝑅) ∖ ∪ ran 𝑀) ≠ ∅)
Theorem	bcthlem5 25679*	Lemma for bcth 25680. The proof makes essential use of the Axiom of Dependent Choice axdc4uz 14154, which in the form used here accepts a "selection" function 𝐹 from each element of 𝐾 to a nonempty subset of 𝐾, and the result function 𝑔 maps 𝑔(𝑛 + 1) to an element of 𝐹(𝑛, 𝑔(𝑛)). The trick here is thus in the choice of 𝐹 and 𝐾: we let 𝐾 be the set of all tagged nonempty open sets (tagged here meaning that we have a point and an open set, in an ordered pair), and 𝐹(𝑘, ⟨𝑥, 𝑧⟩) gives the set of all balls of size less than 1 / 𝑘, tagged by their centers, whose closures fit within the given open set 𝑧 and miss 𝑀(𝑘). Since 𝑀(𝑘) is closed, 𝑧 ∖ 𝑀(𝑘) is open and also nonempty, since 𝑧 is nonempty and 𝑀(𝑘) has empty interior. Then there is some ball contained in it, and hence our function 𝐹 is valid (it never maps to the empty set). Now starting at a point in the interior of ∪ ran 𝑀, DC gives us the function 𝑔 all whose elements are constrained by 𝐹 acting on the previous value. (This is all proven in this lemma.) Now 𝑔 is a sequence of tagged open balls, forming an inclusion chain (see bcthlem2 25676) and whose sizes tend to zero, since they are bounded above by 1 / 𝑘. Thus, the centers of these balls form a Cauchy sequence, and converge to a point 𝑥 (see bcthlem4 25678). Since the inclusion chain also ensures the closure of each ball is in the previous ball, the point 𝑥 must be in all these balls (see bcthlem3 25677) and hence misses each 𝑀(𝑘), contradicting the fact that 𝑥 is in the interior of ∪ ran 𝑀 (which was the starting point). (Contributed by Mario Carneiro, 6-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ 𝐹 = (𝑘 ∈ ℕ, 𝑧 ∈ (𝑋 × ℝ+) ↦ {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))})    &   ⊢ (𝜑 → 𝑀:ℕ⟶(Clsd‘𝐽))    &   ⊢ (𝜑 → ∀𝑘 ∈ ℕ ((int‘𝐽)‘(𝑀‘𝑘)) = ∅)    ⇒   ⊢ (𝜑 → ((int‘𝐽)‘∪ ran 𝑀) = ∅)
Theorem	bcth 25680*	Baire's Category Theorem. If a nonempty metric space is complete, it is nonmeager in itself. In other words, no open set in the metric space can be the countable union of rare closed subsets (where rare means having a closure with empty interior), so some subset 𝑀‘𝑘 must have a nonempty interior. Theorem 4.7-2 of [Kreyszig] p. 247. (The terminology "meager" and "nonmeager" is used by Kreyszig to replace Baire's "of the first category" and "of the second category." The latter terms are going out of favor to avoid confusion with category theory.) See bcthlem5 25679 for an overview of the proof. (Contributed by NM, 28-Oct-2007.) (Proof shortened by Mario Carneiro, 6-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑀:ℕ⟶(Clsd‘𝐽) ∧ ((int‘𝐽)‘∪ ran 𝑀) ≠ ∅) → ∃𝑘 ∈ ℕ ((int‘𝐽)‘(𝑀‘𝑘)) ≠ ∅)
Theorem	bcth2 25681*	Baire's Category Theorem, version 2: If countably many closed sets cover 𝑋, then one of them has an interior. (Contributed by Mario Carneiro, 10-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑋 ≠ ∅) ∧ (𝑀:ℕ⟶(Clsd‘𝐽) ∧ ∪ ran 𝑀 = 𝑋)) → ∃𝑘 ∈ ℕ ((int‘𝐽)‘(𝑀‘𝑘)) ≠ ∅)
Theorem	bcth3 25682*	Baire's Category Theorem, version 3: The intersection of countably many dense open sets is dense. (Contributed by Mario Carneiro, 10-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑀:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ ((cls‘𝐽)‘(𝑀‘𝑘)) = 𝑋) → ((cls‘𝐽)‘∩ ran 𝑀) = 𝑋)
12.5.7  Banach spaces and subcomplex Hilbert spaces
Syntax	ccms 25683	Extend class notation with the class of complete metric spaces.
class CMetSp
Syntax	cbn 25684	Extend class notation with the class of Banach spaces.
class Ban
Syntax	chl 25685	Extend class notation with the class of subcomplex Hilbert spaces.
class ℂHil
Definition	df-cms 25686*	Define the class of complete metric spaces. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ CMetSp = {𝑤 ∈ MetSp ∣ [(Base‘𝑤) / 𝑏]((dist‘𝑤) ↾ (𝑏 × 𝑏)) ∈ (CMet‘𝑏)}
Definition	df-bn 25687	Define the class of all Banach spaces. A Banach space is a normed vector space such that both the vector space and the scalar field are complete under their respective norm-induced metrics. (Contributed by NM, 5-Dec-2006.) (Revised by Mario Carneiro, 15-Oct-2015.)
⊢ Ban = {𝑤 ∈ (NrmVec ∩ CMetSp) ∣ (Scalar‘𝑤) ∈ CMetSp}
Definition	df-hl 25688	Define the class of all subcomplex Hilbert spaces. A subcomplex Hilbert space is a Banach space which is also an inner product space over a subfield of the field of complex numbers closed under square roots of nonnegative reals. (Contributed by Steve Rodriguez, 28-Apr-2007.)
⊢ ℂHil = (Ban ∩ ℂPreHil)
Theorem	isbn 25689	A Banach space is a normed vector space with a complete induced metric. (Contributed by NM, 5-Dec-2006.) (Revised by Mario Carneiro, 15-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ Ban ↔ (𝑊 ∈ NrmVec ∧ 𝑊 ∈ CMetSp ∧ 𝐹 ∈ CMetSp))
Theorem	bnsca 25690	The scalar field of a Banach space is complete. (Contributed by NM, 8-Sep-2007.) (Revised by Mario Carneiro, 15-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ Ban → 𝐹 ∈ CMetSp)
Theorem	bnnvc 25691	A Banach space is a normed vector space. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ (𝑊 ∈ Ban → 𝑊 ∈ NrmVec)
Theorem	bnnlm 25692	A Banach space is a normed module. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ (𝑊 ∈ Ban → 𝑊 ∈ NrmMod)
Theorem	bnngp 25693	A Banach space is a normed group. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ (𝑊 ∈ Ban → 𝑊 ∈ NrmGrp)
Theorem	bnlmod 25694	A Banach space is a left module. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ (𝑊 ∈ Ban → 𝑊 ∈ LMod)
Theorem	bncms 25695	A Banach space is a complete metric space. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ (𝑊 ∈ Ban → 𝑊 ∈ CMetSp)
Theorem	iscms 25696	A complete metric space is a metric space with a complete metric. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑋 = (Base‘𝑀)    &   ⊢ 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋))    ⇒   ⊢ (𝑀 ∈ CMetSp ↔ (𝑀 ∈ MetSp ∧ 𝐷 ∈ (CMet‘𝑋)))
Theorem	cmscmet 25697	The induced metric on a complete normed group is complete. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑋 = (Base‘𝑀)    &   ⊢ 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋))    ⇒   ⊢ (𝑀 ∈ CMetSp → 𝐷 ∈ (CMet‘𝑋))
Theorem	bncmet 25698	The induced metric on Banach space is complete. (Contributed by NM, 8-Sep-2007.) (Revised by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑋 = (Base‘𝑀)    &   ⊢ 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋))    ⇒   ⊢ (𝑀 ∈ Ban → 𝐷 ∈ (CMet‘𝑋))
Theorem	cmsms 25699	A complete metric space is a metric space. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ (𝐺 ∈ CMetSp → 𝐺 ∈ MetSp)
Theorem	cmspropd 25700	Property deduction for a complete metric space. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵)))    &   ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿))    ⇒   ⊢ (𝜑 → (𝐾 ∈ CMetSp ↔ 𝐿 ∈ CMetSp))