![]() |
Metamath
Proof Explorer Theorem List (p. 254 of 491) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | ccmet 25301 | Extend class notation with the class of complete metrics. |
class CMet | ||
Definition | df-cfil 25302* | 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 25303* | 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 25304* | 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 25305* | 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 23252. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 1-May-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ 𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥)))) | ||
Theorem | lmmbr2 25306* | 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 23252. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 1-May-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ 𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷𝑃) < 𝑥)))) | ||
Theorem | lmmbr3 25307* | 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 25308* | Convergence property of a converging sequence. (Contributed by NM, 1-Jun-2007.) (Revised by Mario Carneiro, 1-May-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) & ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐴 ∈ 𝑋 ∧ (𝐴𝐷𝑃) < 𝑅)) | ||
Theorem | lmmbrf 25309* | Express the binary relation "sequence 𝐹 converges to point 𝑃 " in a metric space using an arbitrary upper set of integers. This version of lmmbr2 25306 presupposes that 𝐹 is a function. (Contributed by NM, 20-Jul-2007.) (Revised by Mario Carneiro, 1-May-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) & ⊢ (𝜑 → 𝐹:𝑍⟶𝑋) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐴𝐷𝑃) < 𝑥))) | ||
Theorem | lmnn 25310* | A condition that implies convergence. (Contributed by NM, 8-Jun-2007.) (Revised by Mario Carneiro, 1-May-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑃 ∈ 𝑋) & ⊢ (𝜑 → 𝐹:ℕ⟶𝑋) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘)𝐷𝑃) < (1 / 𝑘)) ⇒ ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃) | ||
Theorem | cfilfval 25311* | The set of Cauchy filters on a metric space. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ (𝐷 ∈ (∞Met‘𝑋) → (CauFil‘𝐷) = {𝑓 ∈ (Fil‘𝑋) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)}) | ||
Theorem | iscfil 25312* | The property of being a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (CauFil‘𝐷) ↔ (𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐹 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))) | ||
Theorem | iscfil2 25313* | The property of being a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (CauFil‘𝐷) ↔ (𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐹 ∀𝑧 ∈ 𝑦 ∀𝑤 ∈ 𝑦 (𝑧𝐷𝑤) < 𝑥))) | ||
Theorem | cfilfil 25314 | A Cauchy filter is a filter. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (CauFil‘𝐷)) → 𝐹 ∈ (Fil‘𝑋)) | ||
Theorem | cfili 25315* | Property of a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ ((𝐹 ∈ (CauFil‘𝐷) ∧ 𝑅 ∈ ℝ+) → ∃𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦𝐷𝑧) < 𝑅) | ||
Theorem | cfil3i 25316* | A Cauchy filter contains balls of any pre-chosen size. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (CauFil‘𝐷) ∧ 𝑅 ∈ ℝ+) → ∃𝑥 ∈ 𝑋 (𝑥(ball‘𝐷)𝑅) ∈ 𝐹) | ||
Theorem | cfilss 25317 | A filter finer than a Cauchy filter is Cauchy. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (CauFil‘𝐷)) ∧ (𝐺 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝐺)) → 𝐺 ∈ (CauFil‘𝐷)) | ||
Theorem | fgcfil 25318* | The Cauchy filter condition for a filter base. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) → ((𝑋filGen𝐵) ∈ (CauFil‘𝐷) ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑦 ∀𝑤 ∈ 𝑦 (𝑧𝐷𝑤) < 𝑥)) | ||
Theorem | fmcfil 25319* | The Cauchy filter condition for a filter map. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (((𝑋 FilMap 𝐹)‘𝐵) ∈ (CauFil‘𝐷) ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑦 ∀𝑤 ∈ 𝑦 ((𝐹‘𝑧)𝐷(𝐹‘𝑤)) < 𝑥)) | ||
Theorem | iscfil3 25320* | 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 25321 | Similar to ultrafilters (uffclsflim 24054), 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 25322* | 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 25323* | 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 23252. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 14-Nov-2013.) |
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ ∀𝑥 ∈ ℝ+ ∃𝑘 ∈ ℤ (𝐹 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝐹‘𝑘)(ball‘𝐷)𝑥)))) | ||
Theorem | iscau2 25324* | 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 25325* | 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 25326* | 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 25327* | 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 25328 | 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 25329 | 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 25330 | 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 25331* | 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 25332 | The convergence of a Cauchy filter in a complete metric space. (Contributed by Mario Carneiro, 14-Oct-2015.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝐹 ∈ (CauFil‘𝐷)) → (𝐽 fLim 𝐹) ≠ ∅) | ||
Theorem | cmetmet 25333 | 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 25334 | A complete metric space is a metric space. (Contributed by NM, 26-Oct-2007.) |
⊢ 𝐷 ∈ (CMet‘𝑋) ⇒ ⊢ 𝐷 ∈ (Met‘𝑋) | ||
Theorem | cmetcaulem 25335* | Lemma for cmetcau 25336. (Contributed by Mario Carneiro, 14-Oct-2015.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) & ⊢ (𝜑 → 𝑃 ∈ 𝑋) & ⊢ (𝜑 → 𝐹 ∈ (Cau‘𝐷)) & ⊢ 𝐺 = (𝑥 ∈ ℕ ↦ if(𝑥 ∈ dom 𝐹, (𝐹‘𝑥), 𝑃)) ⇒ ⊢ (𝜑 → 𝐹 ∈ dom (⇝𝑡‘𝐽)) | ||
Theorem | cmetcau 25336 | 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 25337* | Lemma for iscmet3 25340. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((1 / 2)↑𝑘) < 𝑅) | ||
Theorem | iscmet3lem1 25338* | Lemma for iscmet3 25340. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝐹:𝑍⟶𝑋) & ⊢ (𝜑 → ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑆‘𝑘)∀𝑣 ∈ (𝑆‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)) & ⊢ (𝜑 → ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝐹‘𝑘) ∈ (𝑆‘𝑛)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (Cau‘𝐷)) | ||
Theorem | iscmet3lem2 25339* | Lemma for iscmet3 25340. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝐹:𝑍⟶𝑋) & ⊢ (𝜑 → ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑆‘𝑘)∀𝑣 ∈ (𝑆‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)) & ⊢ (𝜑 → ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝐹‘𝑘) ∈ (𝑆‘𝑛)) & ⊢ (𝜑 → 𝐺 ∈ (Fil‘𝑋)) & ⊢ (𝜑 → 𝑆:ℤ⟶𝐺) & ⊢ (𝜑 → 𝐹 ∈ dom (⇝𝑡‘𝐽)) ⇒ ⊢ (𝜑 → (𝐽 fLim 𝐺) ≠ ∅) | ||
Theorem | iscmet3 25340* | 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 25341 | 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 25342 | 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 25343 | Cauchy filter on a metric subspace. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → (𝐹 ∈ (CauFil‘𝐷) ↔ (𝐹 ↾t 𝑌) ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌))))) | ||
Theorem | caussi 25344 | Cauchy sequence on a metric subspace. (Contributed by NM, 30-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.) |
⊢ (𝐷 ∈ (∞Met‘𝑋) → (Cau‘(𝐷 ↾ (𝑌 × 𝑌))) ⊆ (Cau‘𝐷)) | ||
Theorem | causs 25345 | Cauchy sequence on a metric subspace. (Contributed by NM, 29-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶𝑌) → (𝐹 ∈ (Cau‘𝐷) ↔ 𝐹 ∈ (Cau‘(𝐷 ↾ (𝑌 × 𝑌))))) | ||
Theorem | equivcfil 25346* | 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 25347* | 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 25348* | 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 25349* | 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 25350 | 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 25351 | 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 25352* | 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 10472. 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 25353* | 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 25354 | 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 25355* | 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 25356* | 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 25357* | 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 25358* | 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 25359* | 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 25360 | 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 25361 | Every convergent filter in a metric space is a Cauchy filter. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝐹)) → 𝐹 ∈ (CauFil‘𝐷)) | ||
Theorem | metsscmetcld 25362 | A complete subspace of a metric space is closed in the parent space. Formerly part of proof for cmetss 25363. (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 25363 | 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 25364* | If two metrics are strongly equivalent, one is complete iff the other is. Unlike equivcau 25347, metss2 24540, 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 25365* | 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 25366 | A compact metric space is complete. One half of heibor 37807. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝐽 ∈ Comp) ⇒ ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) | ||
Theorem | cfilucfil3 25367 | 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 25368 | 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 25369 | 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 25370 | 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‘ℝ) | ||
Theorem | bcthlem1 25371* | Lemma for bcth 25376. Substitutions for the function 𝐹. (Contributed by Mario Carneiro, 9-Jan-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) & ⊢ 𝐹 = (𝑘 ∈ ℕ, 𝑧 ∈ (𝑋 × ℝ+) ↦ {〈𝑥, 𝑟〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))}) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ ℕ ∧ 𝐵 ∈ (𝑋 × ℝ+))) → (𝐶 ∈ (𝐴𝐹𝐵) ↔ (𝐶 ∈ (𝑋 × ℝ+) ∧ (2nd ‘𝐶) < (1 / 𝐴) ∧ ((cls‘𝐽)‘((ball‘𝐷)‘𝐶)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴))))) | ||
Theorem | bcthlem2 25372* | Lemma for bcth 25376. 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 25373* | Lemma for bcth 25376. 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 25374* | Lemma for bcth 25376. 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 25375* |
Lemma for bcth 25376. The proof makes essential use of the Axiom
of
Dependent Choice axdc4uz 14021, 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 25372) 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 25374). 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 25373) 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 25376* | 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 25375 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 25377* | 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 25378* | 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 𝑀) = 𝑋) | ||
Syntax | ccms 25379 | Extend class notation with the class of complete metric spaces. |
class CMetSp | ||
Syntax | cbn 25380 | Extend class notation with the class of Banach spaces. |
class Ban | ||
Syntax | chl 25381 | Extend class notation with the class of subcomplex Hilbert spaces. |
class ℂHil | ||
Definition | df-cms 25382* | Define the class of complete metric spaces. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ CMetSp = {𝑤 ∈ MetSp ∣ [(Base‘𝑤) / 𝑏]((dist‘𝑤) ↾ (𝑏 × 𝑏)) ∈ (CMet‘𝑏)} | ||
Definition | df-bn 25383 | 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 25384 | 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 25385 | 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 25386 | 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 25387 | A Banach space is a normed vector space. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ (𝑊 ∈ Ban → 𝑊 ∈ NrmVec) | ||
Theorem | bnnlm 25388 | A Banach space is a normed module. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ (𝑊 ∈ Ban → 𝑊 ∈ NrmMod) | ||
Theorem | bnngp 25389 | A Banach space is a normed group. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ (𝑊 ∈ Ban → 𝑊 ∈ NrmGrp) | ||
Theorem | bnlmod 25390 | A Banach space is a left module. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ (𝑊 ∈ Ban → 𝑊 ∈ LMod) | ||
Theorem | bncms 25391 | A Banach space is a complete metric space. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ (𝑊 ∈ Ban → 𝑊 ∈ CMetSp) | ||
Theorem | iscms 25392 | 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 25393 | The induced metric on a complete normed group is complete. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ 𝑋 = (Base‘𝑀) & ⊢ 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝑀 ∈ CMetSp → 𝐷 ∈ (CMet‘𝑋)) | ||
Theorem | bncmet 25394 | 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 25395 | A complete metric space is a metric space. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ (𝐺 ∈ CMetSp → 𝐺 ∈ MetSp) | ||
Theorem | cmspropd 25396 | Property deduction for a complete metric space. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵))) & ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿)) ⇒ ⊢ (𝜑 → (𝐾 ∈ CMetSp ↔ 𝐿 ∈ CMetSp)) | ||
Theorem | cmssmscld 25397 | The restriction of a metric space is closed if it is complete. (Contributed by AV, 9-Oct-2022.) |
⊢ 𝐾 = (𝑀 ↾s 𝐴) & ⊢ 𝑋 = (Base‘𝑀) & ⊢ 𝐽 = (TopOpen‘𝑀) ⇒ ⊢ ((𝑀 ∈ MetSp ∧ 𝐴 ⊆ 𝑋 ∧ 𝐾 ∈ CMetSp) → 𝐴 ∈ (Clsd‘𝐽)) | ||
Theorem | cmsss 25398 | The restriction of a complete metric space is complete iff it is closed. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ 𝐾 = (𝑀 ↾s 𝐴) & ⊢ 𝑋 = (Base‘𝑀) & ⊢ 𝐽 = (TopOpen‘𝑀) ⇒ ⊢ ((𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋) → (𝐾 ∈ CMetSp ↔ 𝐴 ∈ (Clsd‘𝐽))) | ||
Theorem | lssbn 25399 | A subspace of a Banach space is a Banach space iff it is closed. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) ⇒ ⊢ ((𝑊 ∈ Ban ∧ 𝑈 ∈ 𝑆) → (𝑋 ∈ Ban ↔ 𝑈 ∈ (Clsd‘𝐽))) | ||
Theorem | cmetcusp1 25400 | If the uniform set of a complete metric space is the uniform structure generated by its metric, then it is a complete uniform space. (Contributed by Thierry Arnoux, 15-Dec-2017.) |
⊢ 𝑋 = (Base‘𝐹) & ⊢ 𝐷 = ((dist‘𝐹) ↾ (𝑋 × 𝑋)) & ⊢ 𝑈 = (UnifSt‘𝐹) ⇒ ⊢ ((𝑋 ≠ ∅ ∧ 𝐹 ∈ CMetSp ∧ 𝑈 = (metUnif‘𝐷)) → 𝐹 ∈ CUnifSp) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |