Home | Metamath
Proof Explorer Theorem List (p. 227 of 450) | < 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: | Metamath Proof Explorer
(1-28697) |
Hilbert Space Explorer
(28698-30220) |
Users' Mathboxes
(30221-44913) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | flfnei 22601* | The property of being a limit point of a function in terms of neighborhoods. (Contributed by Jeff Hankins, 9-Nov-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})∃𝑠 ∈ 𝐿 (𝐹 “ 𝑠) ⊆ 𝑛))) | ||
Theorem | flfneii 22602* | A neighborhood of a limit point of a function contains the image of a filter element. (Contributed by Jeff Hankins, 11-Nov-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴})) → ∃𝑠 ∈ 𝐿 (𝐹 “ 𝑠) ⊆ 𝑁) | ||
Theorem | isflf 22603* | The property of being a limit point of a function. (Contributed by Jeff Hankins, 8-Nov-2009.) (Revised by Stefan O'Rear, 7-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → ∃𝑠 ∈ 𝐿 (𝐹 “ 𝑠) ⊆ 𝑜)))) | ||
Theorem | flfelbas 22604 | A limit point of a function is in the topological space. (Contributed by Jeff Hankins, 10-Nov-2009.) (Revised by Stefan O'Rear, 7-Aug-2015.) |
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹)) → 𝐴 ∈ 𝑋) | ||
Theorem | flffbas 22605* | Limit points of a function can be defined using filter bases. (Contributed by Jeff Hankins, 9-Nov-2009.) (Revised by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝐿 = (𝑌filGen𝐵) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → ∃𝑠 ∈ 𝐵 (𝐹 “ 𝑠) ⊆ 𝑜)))) | ||
Theorem | flftg 22606* | Limit points of a function can be defined using topological bases. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ 𝐽 = (topGen‘𝐵) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐵 (𝐴 ∈ 𝑜 → ∃𝑠 ∈ 𝐿 (𝐹 “ 𝑠) ⊆ 𝑜)))) | ||
Theorem | hausflf 22607* | If a function has its values in a Hausdorff space, then it has at most one limit value. (Contributed by FL, 14-Nov-2010.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Haus ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ∃*𝑥 𝑥 ∈ ((𝐽 fLimf 𝐿)‘𝐹)) | ||
Theorem | hausflf2 22608 | If a convergent function has its values in a Hausdorff space, then it has a unique limit. (Contributed by FL, 14-Nov-2010.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (((𝐽 ∈ Haus ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ ((𝐽 fLimf 𝐿)‘𝐹) ≠ ∅) → ((𝐽 fLimf 𝐿)‘𝐹) ≈ 1o) | ||
Theorem | cnpflfi 22609 | Forward direction of cnpflf 22611. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
⊢ ((𝐴 ∈ (𝐽 fLim 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝐿)‘𝐹)) | ||
Theorem | cnpflf2 22610 | 𝐹 is continuous at point 𝐴 iff a limit of 𝐹 when 𝑥 tends to 𝐴 is (𝐹‘𝐴). Proposition 9 of [BourbakiTop1] p. TG I.50. (Contributed by FL, 29-May-2011.) (Revised by Mario Carneiro, 9-Apr-2015.) |
⊢ 𝐿 = ((nei‘𝐽)‘{𝐴}) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝐿)‘𝐹)))) | ||
Theorem | cnpflf 22611* | Continuity of a function at a point in terms of filter limits. (Contributed by Jeff Hankins, 7-Sep-2009.) (Revised by Stefan O'Rear, 7-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fLim 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝑓)‘𝐹))))) | ||
Theorem | cnflf 22612* | A function is continuous iff it respects filter limits. (Contributed by Jeff Hankins, 6-Sep-2009.) (Revised by Stefan O'Rear, 7-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)∀𝑥 ∈ (𝐽 fLim 𝑓)(𝐹‘𝑥) ∈ ((𝐾 fLimf 𝑓)‘𝐹)))) | ||
Theorem | cnflf2 22613* | A function is continuous iff it respects filter limits. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐹 “ (𝐽 fLim 𝑓)) ⊆ ((𝐾 fLimf 𝑓)‘𝐹)))) | ||
Theorem | flfcnp 22614 | A continuous function preserves filter limits. (Contributed by Mario Carneiro, 18-Sep-2015.) |
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐴))) → (𝐺‘𝐴) ∈ ((𝐾 fLimf 𝐿)‘(𝐺 ∘ 𝐹))) | ||
Theorem | lmflf 22615 | The topological limit relation on functions can be written in terms of the filter limit along the filter generated by the upper integer sets. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝐿 = (𝑍filGen(ℤ≥ “ 𝑍)) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶𝑋) → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ 𝑃 ∈ ((𝐽 fLimf 𝐿)‘𝐹))) | ||
Theorem | txflf 22616* | Two sequences converge in a filter iff the sequence of their ordered pairs converges. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑍)) & ⊢ (𝜑 → 𝐹:𝑍⟶𝑋) & ⊢ (𝜑 → 𝐺:𝑍⟶𝑌) & ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉) ⇒ ⊢ (𝜑 → (〈𝑅, 𝑆〉 ∈ (((𝐽 ×t 𝐾) fLimf 𝐿)‘𝐻) ↔ (𝑅 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝑆 ∈ ((𝐾 fLimf 𝐿)‘𝐺)))) | ||
Theorem | flfcnp2 22617* | The image of a convergent sequence under a continuous map is convergent to the image of the original point. Binary operation version. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑍)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐴 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 ∈ ((𝐽 fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ 𝐴))) & ⊢ (𝜑 → 𝑆 ∈ ((𝐾 fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ 𝐵))) & ⊢ (𝜑 → 𝑂 ∈ (((𝐽 ×t 𝐾) CnP 𝑁)‘〈𝑅, 𝑆〉)) ⇒ ⊢ (𝜑 → (𝑅𝑂𝑆) ∈ ((𝑁 fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ (𝐴𝑂𝐵)))) | ||
Theorem | fclsval 22618* | The set of all cluster points of a filter. (Contributed by Jeff Hankins, 10-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ (Fil‘𝑌)) → (𝐽 fClus 𝐹) = if(𝑋 = 𝑌, ∩ 𝑡 ∈ 𝐹 ((cls‘𝐽)‘𝑡), ∅)) | ||
Theorem | isfcls 22619* | A cluster point of a filter. (Contributed by Jeff Hankins, 10-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐴 ∈ (𝐽 fClus 𝐹) ↔ (𝐽 ∈ Top ∧ 𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑠 ∈ 𝐹 𝐴 ∈ ((cls‘𝐽)‘𝑠))) | ||
Theorem | fclsfil 22620 | Reverse closure for the cluster point predicate. (Contributed by Mario Carneiro, 11-Apr-2015.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐹 ∈ (Fil‘𝑋)) | ||
Theorem | fclstop 22621 | Reverse closure for the cluster point predicate. (Contributed by Mario Carneiro, 11-Apr-2015.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐽 ∈ Top) | ||
Theorem | fclstopon 22622 | Reverse closure for the cluster point predicate. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → (𝐽 ∈ (TopOn‘𝑋) ↔ 𝐹 ∈ (Fil‘𝑋))) | ||
Theorem | isfcls2 22623* | A cluster point of a filter. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fClus 𝐹) ↔ ∀𝑠 ∈ 𝐹 𝐴 ∈ ((cls‘𝐽)‘𝑠))) | ||
Theorem | fclsopn 22624* | Write the cluster point condition in terms of open sets. (Contributed by Jeff Hankins, 10-Nov-2009.) (Revised by Mario Carneiro, 26-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fClus 𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → ∀𝑠 ∈ 𝐹 (𝑜 ∩ 𝑠) ≠ ∅)))) | ||
Theorem | fclsopni 22625 | An open neighborhood of a cluster point of a filter intersects any element of that filter. (Contributed by Mario Carneiro, 11-Apr-2015.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ (𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑈 ∧ 𝑆 ∈ 𝐹)) → (𝑈 ∩ 𝑆) ≠ ∅) | ||
Theorem | fclselbas 22626 | A cluster point is in the base set. (Contributed by Jeff Hankins, 11-Nov-2009.) (Revised by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐴 ∈ 𝑋) | ||
Theorem | fclsneii 22627 | A neighborhood of a cluster point of a filter intersects any element of that filter. (Contributed by Jeff Hankins, 11-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → (𝑁 ∩ 𝑆) ≠ ∅) | ||
Theorem | fclssscls 22628 | The set of cluster points is a subset of the closure of any filter element. (Contributed by Mario Carneiro, 11-Apr-2015.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
⊢ (𝑆 ∈ 𝐹 → (𝐽 fClus 𝐹) ⊆ ((cls‘𝐽)‘𝑆)) | ||
Theorem | fclsnei 22629* | Cluster points in terms of neighborhoods. (Contributed by Jeff Hankins, 11-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fClus 𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})∀𝑠 ∈ 𝐹 (𝑛 ∩ 𝑠) ≠ ∅))) | ||
Theorem | supnfcls 22630* | The filter of supersets of 𝑋 ∖ 𝑈 does not cluster at any point of the open set 𝑈. (Contributed by Mario Carneiro, 11-Apr-2015.) (Revised by Mario Carneiro, 26-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑈) → ¬ 𝐴 ∈ (𝐽 fClus {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑈) ⊆ 𝑥})) | ||
Theorem | fclsbas 22631* | Cluster points in terms of filter bases. (Contributed by Jeff Hankins, 13-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
⊢ 𝐹 = (𝑋filGen𝐵) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) → (𝐴 ∈ (𝐽 fClus 𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → ∀𝑠 ∈ 𝐵 (𝑜 ∩ 𝑠) ≠ ∅)))) | ||
Theorem | fclsss1 22632 | A finer topology has fewer cluster points. (Contributed by Jeff Hankins, 11-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝐽 ⊆ 𝐾) → (𝐾 fClus 𝐹) ⊆ (𝐽 fClus 𝐹)) | ||
Theorem | fclsss2 22633 | A finer filter has fewer cluster points. (Contributed by Jeff Hankins, 11-Nov-2009.) (Revised by Mario Carneiro, 26-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝐺) → (𝐽 fClus 𝐺) ⊆ (𝐽 fClus 𝐹)) | ||
Theorem | fclsrest 22634 | The set of cluster points in a restricted topological space. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → ((𝐽 ↾t 𝑌) fClus (𝐹 ↾t 𝑌)) = ((𝐽 fClus 𝐹) ∩ 𝑌)) | ||
Theorem | fclscf 22635* | Characterization of fineness of topologies in terms of cluster points. (Contributed by Jeff Hankins, 12-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) → (𝐽 ⊆ 𝐾 ↔ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓))) | ||
Theorem | flimfcls 22636 | A limit point is a cluster point. (Contributed by Jeff Hankins, 12-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
⊢ (𝐽 fLim 𝐹) ⊆ (𝐽 fClus 𝐹) | ||
Theorem | fclsfnflim 22637* | A filter clusters at a point iff a finer filter converges to it. (Contributed by Jeff Hankins, 12-Nov-2009.) (Revised by Mario Carneiro, 26-Aug-2015.) |
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐴 ∈ (𝐽 fClus 𝐹) ↔ ∃𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ (𝐽 fLim 𝑔)))) | ||
Theorem | flimfnfcls 22638* | A filter converges to a point iff every finer filter clusters there. Along with fclsfnflim 22637, this theorem illustrates the duality between convergence and clustering. (Contributed by Jeff Hankins, 12-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ ∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔)))) | ||
Theorem | fclscmpi 22639 | Forward direction of fclscmp 22640. Every filter clusters in a compact space. (Contributed by Mario Carneiro, 11-Apr-2015.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Comp ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝐽 fClus 𝐹) ≠ ∅) | ||
Theorem | fclscmp 22640* | A space is compact iff every filter clusters. (Contributed by Jeff Hankins, 20-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Comp ↔ ∀𝑓 ∈ (Fil‘𝑋)(𝐽 fClus 𝑓) ≠ ∅)) | ||
Theorem | uffclsflim 22641 | The cluster points of an ultrafilter are its limit points. (Contributed by Jeff Hankins, 11-Dec-2009.) (Revised by Mario Carneiro, 26-Aug-2015.) |
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝐽 fClus 𝐹) = (𝐽 fLim 𝐹)) | ||
Theorem | ufilcmp 22642* | A space is compact iff every ultrafilter converges. (Contributed by Jeff Hankins, 11-Dec-2009.) (Proof shortened by Mario Carneiro, 12-Apr-2015.) (Revised by Mario Carneiro, 26-Aug-2015.) |
⊢ ((𝑋 ∈ UFL ∧ 𝐽 ∈ (TopOn‘𝑋)) → (𝐽 ∈ Comp ↔ ∀𝑓 ∈ (UFil‘𝑋)(𝐽 fLim 𝑓) ≠ ∅)) | ||
Theorem | fcfval 22643 | The set of cluster points of a function. (Contributed by Jeff Hankins, 24-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝐽 fClusf 𝐿)‘𝐹) = (𝐽 fClus ((𝑋 FilMap 𝐹)‘𝐿))) | ||
Theorem | isfcf 22644* | The property of being a cluster point of a function. (Contributed by Jeff Hankins, 24-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝐴 ∈ ((𝐽 fClusf 𝐿)‘𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → ∀𝑠 ∈ 𝐿 (𝑜 ∩ (𝐹 “ 𝑠)) ≠ ∅)))) | ||
Theorem | fcfnei 22645* | The property of being a cluster point of a function in terms of neighborhoods. (Contributed by Jeff Hankins, 26-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝐴 ∈ ((𝐽 fClusf 𝐿)‘𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})∀𝑠 ∈ 𝐿 (𝑛 ∩ (𝐹 “ 𝑠)) ≠ ∅))) | ||
Theorem | fcfelbas 22646 | A cluster point of a function is in the base set of the topology. (Contributed by Jeff Hankins, 26-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝐴 ∈ ((𝐽 fClusf 𝐿)‘𝐹)) → 𝐴 ∈ 𝑋) | ||
Theorem | fcfneii 22647 | A neighborhood of a cluster point of a function contains a function value from every tail. (Contributed by Jeff Hankins, 27-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝐴 ∈ ((𝐽 fClusf 𝐿)‘𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐿)) → (𝑁 ∩ (𝐹 “ 𝑆)) ≠ ∅) | ||
Theorem | flfssfcf 22648 | A limit point of a function is a cluster point of the function. (Contributed by Jeff Hankins, 28-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝐽 fLimf 𝐿)‘𝐹) ⊆ ((𝐽 fClusf 𝐿)‘𝐹)) | ||
Theorem | uffcfflf 22649 | If the domain filter is an ultrafilter, the cluster points of the function are the limit points. (Contributed by Jeff Hankins, 12-Dec-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (UFil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝐽 fClusf 𝐿)‘𝐹) = ((𝐽 fLimf 𝐿)‘𝐹)) | ||
Theorem | cnpfcfi 22650 | Lemma for cnpfcf 22651. If a function is continuous at a point, it respects clustering there. (Contributed by Jeff Hankins, 20-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
⊢ ((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝐿)‘𝐹)) | ||
Theorem | cnpfcf 22651* | A function 𝐹 is continuous at point 𝐴 iff 𝐹 respects cluster points there. (Contributed by Jeff Hankins, 14-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹))))) | ||
Theorem | cnfcf 22652* | Continuity of a function in terms of cluster points of a function. (Contributed by Jeff Hankins, 28-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)∀𝑥 ∈ (𝐽 fClus 𝑓)(𝐹‘𝑥) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))) | ||
Theorem | flfcntr 22653 | A continuous function's value is always in the trace of its filter limit. (Contributed by Thierry Arnoux, 30-Aug-2020.) |
⊢ 𝐶 = ∪ 𝐽 & ⊢ 𝐵 = ∪ 𝐾 & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝐴 ⊆ 𝐶) & ⊢ (𝜑 → 𝐹 ∈ ((𝐽 ↾t 𝐴) Cn 𝐾)) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐹‘𝑋) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹)) | ||
Theorem | alexsublem 22654* | Lemma for alexsub 22655. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ (𝜑 → 𝑋 ∈ UFL) & ⊢ (𝜑 → 𝑋 = ∪ 𝐵) & ⊢ (𝜑 → 𝐽 = (topGen‘(fi‘𝐵))) & ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥)) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦) & ⊢ (𝜑 → 𝐹 ∈ (UFil‘𝑋)) & ⊢ (𝜑 → (𝐽 fLim 𝐹) = ∅) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | alexsub 22655* | The Alexander Subbase Theorem: If 𝐵 is a subbase for the topology 𝐽, and any cover taken from 𝐵 has a finite subcover, then the generated topology is compact. This proof uses the ultrafilter lemma; see alexsubALT 22661 for a proof using Zorn's lemma. (Contributed by Jeff Hankins, 24-Jan-2010.) (Revised by Mario Carneiro, 26-Aug-2015.) |
⊢ (𝜑 → 𝑋 ∈ UFL) & ⊢ (𝜑 → 𝑋 = ∪ 𝐵) & ⊢ (𝜑 → 𝐽 = (topGen‘(fi‘𝐵))) & ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥)) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦) ⇒ ⊢ (𝜑 → 𝐽 ∈ Comp) | ||
Theorem | alexsubb 22656* | Biconditional form of the Alexander Subbase Theorem alexsub 22655. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪ 𝐵) → ((topGen‘(fi‘𝐵)) ∈ Comp ↔ ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦))) | ||
Theorem | alexsubALTlem1 22657* | Lemma for alexsubALT 22661. A compact space has a subbase such that every cover taken from it has a finite subcover. (Contributed by Jeff Hankins, 27-Jan-2010.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Comp → ∃𝑥(𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))) | ||
Theorem | alexsubALTlem2 22658* | Lemma for alexsubALT 22661. Every subset of a base which has no finite subcover is a subset of a maximal such collection. (Contributed by Jeff Hankins, 27-Jan-2010.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) → ∃𝑢 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣) | ||
Theorem | alexsubALTlem3 22659* | Lemma for alexsubALT 22661. If a point is covered by a collection taken from the base with no finite subcover, a set from the subbase can be added that covers the point so that the resulting collection has no finite subcover. (Contributed by Jeff Hankins, 28-Jan-2010.) (Revised by Mario Carneiro, 14-Dec-2013.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) → ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛) | ||
Theorem | alexsubALTlem4 22660* | Lemma for alexsubALT 22661. If any cover taken from a subbase has a finite subcover, any cover taken from the corresponding base has a finite subcover. (Contributed by Jeff Hankins, 28-Jan-2010.) (Revised by Mario Carneiro, 14-Dec-2013.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → ∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))) | ||
Theorem | alexsubALT 22661* | The Alexander Subbase Theorem: a space is compact iff it has a subbase such that any cover taken from the subbase has a finite subcover. (Contributed by Jeff Hankins, 24-Jan-2010.) (Revised by Mario Carneiro, 11-Feb-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Comp ↔ ∃𝑥(𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))) | ||
Theorem | ptcmplem1 22662* | Lemma for ptcmp 22668. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) & ⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶Comp) & ⊢ (𝜑 → 𝑋 ∈ (UFL ∩ dom card)) ⇒ ⊢ (𝜑 → (𝑋 = ∪ (ran 𝑆 ∪ {𝑋}) ∧ (∏t‘𝐹) = (topGen‘(fi‘(ran 𝑆 ∪ {𝑋}))))) | ||
Theorem | ptcmplem2 22663* | Lemma for ptcmp 22668. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) & ⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶Comp) & ⊢ (𝜑 → 𝑋 ∈ (UFL ∩ dom card)) & ⊢ (𝜑 → 𝑈 ⊆ ran 𝑆) & ⊢ (𝜑 → 𝑋 = ∪ 𝑈) & ⊢ (𝜑 → ¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧) ⇒ ⊢ (𝜑 → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ∈ dom card) | ||
Theorem | ptcmplem3 22664* | Lemma for ptcmp 22668. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) & ⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶Comp) & ⊢ (𝜑 → 𝑋 ∈ (UFL ∩ dom card)) & ⊢ (𝜑 → 𝑈 ⊆ ran 𝑆) & ⊢ (𝜑 → 𝑋 = ∪ 𝑈) & ⊢ (𝜑 → ¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧) & ⊢ 𝐾 = {𝑢 ∈ (𝐹‘𝑘) ∣ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝑈} ⇒ ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) | ||
Theorem | ptcmplem4 22665* | Lemma for ptcmp 22668. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) & ⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶Comp) & ⊢ (𝜑 → 𝑋 ∈ (UFL ∩ dom card)) & ⊢ (𝜑 → 𝑈 ⊆ ran 𝑆) & ⊢ (𝜑 → 𝑋 = ∪ 𝑈) & ⊢ (𝜑 → ¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧) & ⊢ 𝐾 = {𝑢 ∈ (𝐹‘𝑘) ∣ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝑈} ⇒ ⊢ ¬ 𝜑 | ||
Theorem | ptcmplem5 22666* | Lemma for ptcmp 22668. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) & ⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶Comp) & ⊢ (𝜑 → 𝑋 ∈ (UFL ∩ dom card)) ⇒ ⊢ (𝜑 → (∏t‘𝐹) ∈ Comp) | ||
Theorem | ptcmpg 22667 | Tychonoff's theorem: The product of compact spaces is compact. The choice principles needed are encoded in the last hypothesis: the base set of the product must be well-orderable and satisfy the ultrafilter lemma. Both these assumptions are satisfied if 𝒫 𝒫 𝑋 is well-orderable, so if we assume the Axiom of Choice we can eliminate them (see ptcmp 22668). (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ 𝐽 = (∏t‘𝐹) & ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Comp ∧ 𝑋 ∈ (UFL ∩ dom card)) → 𝐽 ∈ Comp) | ||
Theorem | ptcmp 22668 | Tychonoff's theorem: The product of compact spaces is compact. The proof uses the Axiom of Choice. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Comp) → (∏t‘𝐹) ∈ Comp) | ||
Syntax | ccnext 22669 | Extend class notation with the continuous extension operation. |
class CnExt | ||
Definition | df-cnext 22670* | Define the continuous extension of a given function. (Contributed by Thierry Arnoux, 1-Dec-2017.) |
⊢ CnExt = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑓 ∈ (∪ 𝑘 ↑pm ∪ 𝑗) ↦ ∪ 𝑥 ∈ ((cls‘𝑗)‘dom 𝑓)({𝑥} × ((𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))‘𝑓)))) | ||
Theorem | cnextval 22671* | The function applying continuous extension to a given function 𝑓. (Contributed by Thierry Arnoux, 1-Dec-2017.) |
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽CnExt𝐾) = (𝑓 ∈ (∪ 𝐾 ↑pm ∪ 𝐽) ↦ ∪ 𝑥 ∈ ((cls‘𝐽)‘dom 𝑓)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t dom 𝑓))‘𝑓)))) | ||
Theorem | cnextfval 22672* | The continuous extension of a given function 𝐹. (Contributed by Thierry Arnoux, 1-Dec-2017.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐵 = ∪ 𝐾 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝑋)) → ((𝐽CnExt𝐾)‘𝐹) = ∪ 𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))) | ||
Theorem | cnextrel 22673 | In the general case, a continuous extension is a relation. (Contributed by Thierry Arnoux, 20-Dec-2017.) |
⊢ 𝐶 = ∪ 𝐽 & ⊢ 𝐵 = ∪ 𝐾 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝐶)) → Rel ((𝐽CnExt𝐾)‘𝐹)) | ||
Theorem | cnextfun 22674 | If the target space is Hausdorff, a continuous extension is a function. (Contributed by Thierry Arnoux, 20-Dec-2017.) |
⊢ 𝐶 = ∪ 𝐽 & ⊢ 𝐵 = ∪ 𝐾 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Haus) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝐶)) → Fun ((𝐽CnExt𝐾)‘𝐹)) | ||
Theorem | cnextfvval 22675* | The value of the continuous extension of a given function 𝐹 at a point 𝑋. (Contributed by Thierry Arnoux, 21-Dec-2017.) |
⊢ 𝐶 = ∪ 𝐽 & ⊢ 𝐵 = ∪ 𝐾 & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝐾 ∈ Haus) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐴 ⊆ 𝐶) & ⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑋) = ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹)) | ||
Theorem | cnextf 22676* | Extension by continuity. The extension by continuity is a function. (Contributed by Thierry Arnoux, 25-Dec-2017.) |
⊢ 𝐶 = ∪ 𝐽 & ⊢ 𝐵 = ∪ 𝐾 & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝐾 ∈ Haus) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐴 ⊆ 𝐶) & ⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅) ⇒ ⊢ (𝜑 → ((𝐽CnExt𝐾)‘𝐹):𝐶⟶𝐵) | ||
Theorem | cnextcn 22677* | Extension by continuity. Theorem 1 of [BourbakiTop1] p. I.57. Given a topology 𝐽 on 𝐶, a subset 𝐴 dense in 𝐶, this states a condition for 𝐹 from 𝐴 to a regular space 𝐾 to be extensible by continuity. (Contributed by Thierry Arnoux, 1-Jan-2018.) |
⊢ 𝐶 = ∪ 𝐽 & ⊢ 𝐵 = ∪ 𝐾 & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝐾 ∈ Haus) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐴 ⊆ 𝐶) & ⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅) & ⊢ (𝜑 → 𝐾 ∈ Reg) ⇒ ⊢ (𝜑 → ((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾)) | ||
Theorem | cnextfres1 22678* | 𝐹 and its extension by continuity agree on the domain of 𝐹. (Contributed by Thierry Arnoux, 17-Jan-2018.) |
⊢ 𝐶 = ∪ 𝐽 & ⊢ 𝐵 = ∪ 𝐾 & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝐾 ∈ Haus) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐴 ⊆ 𝐶) & ⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = 𝐶) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅) & ⊢ (𝜑 → 𝐾 ∈ Reg) & ⊢ (𝜑 → 𝐹 ∈ ((𝐽 ↾t 𝐴) Cn 𝐾)) ⇒ ⊢ (𝜑 → (((𝐽CnExt𝐾)‘𝐹) ↾ 𝐴) = 𝐹) | ||
Theorem | cnextfres 22679 | 𝐹 and its extension by continuity agree on the domain of 𝐹. (Contributed by Thierry Arnoux, 29-Aug-2020.) |
⊢ 𝐶 = ∪ 𝐽 & ⊢ 𝐵 = ∪ 𝐾 & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝐾 ∈ Haus) & ⊢ (𝜑 → 𝐴 ⊆ 𝐶) & ⊢ (𝜑 → 𝐹 ∈ ((𝐽 ↾t 𝐴) Cn 𝐾)) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → (((𝐽CnExt𝐾)‘𝐹)‘𝑋) = (𝐹‘𝑋)) | ||
Syntax | ctmd 22680 | Extend class notation with the class of all topological monoids. |
class TopMnd | ||
Syntax | ctgp 22681 | Extend class notation with the class of all topological groups. |
class TopGrp | ||
Definition | df-tmd 22682* | Define the class of all topological monoids. A topological monoid is a monoid whose operation is continuous. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ TopMnd = {𝑓 ∈ (Mnd ∩ TopSp) ∣ [(TopOpen‘𝑓) / 𝑗](+𝑓‘𝑓) ∈ ((𝑗 ×t 𝑗) Cn 𝑗)} | ||
Definition | df-tgp 22683* | Define the class of all topological groups. A topological group is a group whose operation and inverse function are continuous. (Contributed by FL, 18-Apr-2010.) |
⊢ TopGrp = {𝑓 ∈ (Grp ∩ TopMnd) ∣ [(TopOpen‘𝑓) / 𝑗](invg‘𝑓) ∈ (𝑗 Cn 𝑗)} | ||
Theorem | istmd 22684 | The predicate "is a topological monoid". (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ 𝐹 = (+𝑓‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) ⇒ ⊢ (𝐺 ∈ TopMnd ↔ (𝐺 ∈ Mnd ∧ 𝐺 ∈ TopSp ∧ 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽))) | ||
Theorem | tmdmnd 22685 | A topological monoid is a monoid. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ (𝐺 ∈ TopMnd → 𝐺 ∈ Mnd) | ||
Theorem | tmdtps 22686 | A topological monoid is a topological space. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ (𝐺 ∈ TopMnd → 𝐺 ∈ TopSp) | ||
Theorem | istgp 22687 | The predicate "is a topological group". Definition 1 of [BourbakiTop1] p. III.1. (Contributed by FL, 18-Apr-2010.) (Revised by Mario Carneiro, 13-Aug-2015.) |
⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) ⇒ ⊢ (𝐺 ∈ TopGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ TopMnd ∧ 𝐼 ∈ (𝐽 Cn 𝐽))) | ||
Theorem | tgpgrp 22688 | A topological group is a group. (Contributed by FL, 18-Apr-2010.) (Revised by Mario Carneiro, 13-Aug-2015.) |
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp) | ||
Theorem | tgptmd 22689 | A topological group is a topological monoid. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopMnd) | ||
Theorem | tgptps 22690 | A topological group is a topological space. (Contributed by FL, 21-Jun-2010.) (Revised by Mario Carneiro, 13-Aug-2015.) |
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopSp) | ||
Theorem | tmdtopon 22691 | The topology of a topological monoid. (Contributed by Mario Carneiro, 27-Jun-2014.) (Revised by Mario Carneiro, 13-Aug-2015.) |
⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ 𝑋 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ TopMnd → 𝐽 ∈ (TopOn‘𝑋)) | ||
Theorem | tgptopon 22692 | The topology of a topological group. (Contributed by Mario Carneiro, 27-Jun-2014.) (Revised by Mario Carneiro, 13-Aug-2015.) |
⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ 𝑋 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝑋)) | ||
Theorem | tmdcn 22693 | In a topological monoid, the operation 𝐹 representing the functionalization of the operator slot +g is continuous. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ 𝐹 = (+𝑓‘𝐺) ⇒ ⊢ (𝐺 ∈ TopMnd → 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) | ||
Theorem | tgpcn 22694 | In a topological group, the operation 𝐹 representing the functionalization of the operator slot +g is continuous. (Contributed by FL, 21-Jun-2010.) (Revised by Mario Carneiro, 13-Aug-2015.) |
⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ 𝐹 = (+𝑓‘𝐺) ⇒ ⊢ (𝐺 ∈ TopGrp → 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) | ||
Theorem | tgpinv 22695 | In a topological group, the inverse function is continuous. (Contributed by FL, 21-Jun-2010.) (Revised by FL, 27-Jun-2014.) |
⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) ⇒ ⊢ (𝐺 ∈ TopGrp → 𝐼 ∈ (𝐽 Cn 𝐽)) | ||
Theorem | grpinvhmeo 22696 | The inverse function in a topological group is a homeomorphism from the group to itself. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) ⇒ ⊢ (𝐺 ∈ TopGrp → 𝐼 ∈ (𝐽Homeo𝐽)) | ||
Theorem | cnmpt1plusg 22697* | Continuity of the group sum; analogue of cnmpt12f 22276 which cannot be used directly because +g is not a function. (Contributed by Mario Carneiro, 23-Aug-2015.) |
⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TopMnd) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐾 Cn 𝐽)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐾 Cn 𝐽)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 + 𝐵)) ∈ (𝐾 Cn 𝐽)) | ||
Theorem | cnmpt2plusg 22698* | Continuity of the group sum; analogue of cnmpt22f 22285 which cannot be used directly because +g is not a function. (Contributed by Mario Carneiro, 23-Aug-2015.) |
⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ TopMnd) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐾 ×t 𝐿) Cn 𝐽)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐾 ×t 𝐿) Cn 𝐽)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝐴 + 𝐵)) ∈ ((𝐾 ×t 𝐿) Cn 𝐽)) | ||
Theorem | tmdcn2 22699* | Write out the definition of continuity of +g explicitly. (Contributed by Mario Carneiro, 20-Sep-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ∀𝑥 ∈ 𝑢 ∀𝑦 ∈ 𝑣 (𝑥 + 𝑦) ∈ 𝑈)) | ||
Theorem | tgpsubcn 22700 | In a topological group, the "subtraction" (or "division") is continuous. Axiom GT' of [BourbakiTop1] p. III.1. (Contributed by FL, 21-Jun-2010.) (Revised by Mario Carneiro, 19-Mar-2015.) |
⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ (𝐺 ∈ TopGrp → − ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |