![]() |
Metamath
Proof Explorer Theorem List (p. 227 of 454) | < 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-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | flftg 22601* | Limit points of a function can be defined using topological bases. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ 𝐽 = (topGen‘𝐵) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐵 (𝐴 ∈ 𝑜 → ∃𝑠 ∈ 𝐿 (𝐹 “ 𝑠) ⊆ 𝑜)))) | ||
Theorem | hausflf 22602* | 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 22603 | 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 22604 | Forward direction of cnpflf 22606. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
⊢ ((𝐴 ∈ (𝐽 fLim 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝐿)‘𝐹)) | ||
Theorem | cnpflf2 22605 | 𝐹 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 22606* | 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 22607* | 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 22608* | 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 22609 | A continuous function preserves filter limits. (Contributed by Mario Carneiro, 18-Sep-2015.) |
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐴))) → (𝐺‘𝐴) ∈ ((𝐾 fLimf 𝐿)‘(𝐺 ∘ 𝐹))) | ||
Theorem | lmflf 22610 | 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 22611* | 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 22612* | 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 22613* | 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 22614* | 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 22615 | 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 22616 | 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 22617 | Reverse closure for the cluster point predicate. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → (𝐽 ∈ (TopOn‘𝑋) ↔ 𝐹 ∈ (Fil‘𝑋))) | ||
Theorem | isfcls2 22618* | A cluster point of a filter. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fClus 𝐹) ↔ ∀𝑠 ∈ 𝐹 𝐴 ∈ ((cls‘𝐽)‘𝑠))) | ||
Theorem | fclsopn 22619* | 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 22620 | 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 22621 | 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 22622 | 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 22623 | 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 22624* | 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 22625* | 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 22626* | 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 22627 | 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 22628 | 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 22629 | 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 22630* | 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 22631 | 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 22632* | 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 22633* | A filter converges to a point iff every finer filter clusters there. Along with fclsfnflim 22632, 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 22634 | Forward direction of fclscmp 22635. 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 22635* | 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 22636 | 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 22637* | 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 22638 | 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 22639* | 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 22640* | 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 22641 | 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 22642 | 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 22643 | 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 22644 | 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 22645 | Lemma for cnpfcf 22646. 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 22646* | 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 22647* | 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 22648 | 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 22649* | Lemma for alexsub 22650. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ (𝜑 → 𝑋 ∈ UFL) & ⊢ (𝜑 → 𝑋 = ∪ 𝐵) & ⊢ (𝜑 → 𝐽 = (topGen‘(fi‘𝐵))) & ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥)) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦) & ⊢ (𝜑 → 𝐹 ∈ (UFil‘𝑋)) & ⊢ (𝜑 → (𝐽 fLim 𝐹) = ∅) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | alexsub 22650* | 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 22656 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 22651* | Biconditional form of the Alexander Subbase Theorem alexsub 22650. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪ 𝐵) → ((topGen‘(fi‘𝐵)) ∈ Comp ↔ ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦))) | ||
Theorem | alexsubALTlem1 22652* | Lemma for alexsubALT 22656. 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 22653* | Lemma for alexsubALT 22656. 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 22654* | Lemma for alexsubALT 22656. 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 22655* | Lemma for alexsubALT 22656. 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 22656* | 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 22657* | Lemma for ptcmp 22663. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) & ⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶Comp) & ⊢ (𝜑 → 𝑋 ∈ (UFL ∩ dom card)) ⇒ ⊢ (𝜑 → (𝑋 = ∪ (ran 𝑆 ∪ {𝑋}) ∧ (∏t‘𝐹) = (topGen‘(fi‘(ran 𝑆 ∪ {𝑋}))))) | ||
Theorem | ptcmplem2 22658* | Lemma for ptcmp 22663. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) & ⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶Comp) & ⊢ (𝜑 → 𝑋 ∈ (UFL ∩ dom card)) & ⊢ (𝜑 → 𝑈 ⊆ ran 𝑆) & ⊢ (𝜑 → 𝑋 = ∪ 𝑈) & ⊢ (𝜑 → ¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧) ⇒ ⊢ (𝜑 → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ∈ dom card) | ||
Theorem | ptcmplem3 22659* | Lemma for ptcmp 22663. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) & ⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶Comp) & ⊢ (𝜑 → 𝑋 ∈ (UFL ∩ dom card)) & ⊢ (𝜑 → 𝑈 ⊆ ran 𝑆) & ⊢ (𝜑 → 𝑋 = ∪ 𝑈) & ⊢ (𝜑 → ¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧) & ⊢ 𝐾 = {𝑢 ∈ (𝐹‘𝑘) ∣ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝑈} ⇒ ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) | ||
Theorem | ptcmplem4 22660* | Lemma for ptcmp 22663. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) & ⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶Comp) & ⊢ (𝜑 → 𝑋 ∈ (UFL ∩ dom card)) & ⊢ (𝜑 → 𝑈 ⊆ ran 𝑆) & ⊢ (𝜑 → 𝑋 = ∪ 𝑈) & ⊢ (𝜑 → ¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧) & ⊢ 𝐾 = {𝑢 ∈ (𝐹‘𝑘) ∣ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝑈} ⇒ ⊢ ¬ 𝜑 | ||
Theorem | ptcmplem5 22661* | Lemma for ptcmp 22663. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) & ⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶Comp) & ⊢ (𝜑 → 𝑋 ∈ (UFL ∩ dom card)) ⇒ ⊢ (𝜑 → (∏t‘𝐹) ∈ Comp) | ||
Theorem | ptcmpg 22662 | 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 22663). (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ 𝐽 = (∏t‘𝐹) & ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Comp ∧ 𝑋 ∈ (UFL ∩ dom card)) → 𝐽 ∈ Comp) | ||
Theorem | ptcmp 22663 | 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 22664 | Extend class notation with the continuous extension operation. |
class CnExt | ||
Definition | df-cnext 22665* | 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 22666* | 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 22667* | The continuous extension of a given function 𝐹. (Contributed by Thierry Arnoux, 1-Dec-2017.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐵 = ∪ 𝐾 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝑋)) → ((𝐽CnExt𝐾)‘𝐹) = ∪ 𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))) | ||
Theorem | cnextrel 22668 | In the general case, a continuous extension is a relation. (Contributed by Thierry Arnoux, 20-Dec-2017.) |
⊢ 𝐶 = ∪ 𝐽 & ⊢ 𝐵 = ∪ 𝐾 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝐶)) → Rel ((𝐽CnExt𝐾)‘𝐹)) | ||
Theorem | cnextfun 22669 | 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 22670* | 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 22671* | 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 22672* | 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 22673* | 𝐹 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 22674 | 𝐹 and its extension by continuity agree on the domain of 𝐹. (Contributed by Thierry Arnoux, 29-Aug-2020.) |
⊢ 𝐶 = ∪ 𝐽 & ⊢ 𝐵 = ∪ 𝐾 & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝐾 ∈ Haus) & ⊢ (𝜑 → 𝐴 ⊆ 𝐶) & ⊢ (𝜑 → 𝐹 ∈ ((𝐽 ↾t 𝐴) Cn 𝐾)) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → (((𝐽CnExt𝐾)‘𝐹)‘𝑋) = (𝐹‘𝑋)) | ||
Syntax | ctmd 22675 | Extend class notation with the class of all topological monoids. |
class TopMnd | ||
Syntax | ctgp 22676 | Extend class notation with the class of all topological groups. |
class TopGrp | ||
Definition | df-tmd 22677* | 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 22678* | 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 22679 | The predicate "is a topological monoid". (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ 𝐹 = (+𝑓‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) ⇒ ⊢ (𝐺 ∈ TopMnd ↔ (𝐺 ∈ Mnd ∧ 𝐺 ∈ TopSp ∧ 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽))) | ||
Theorem | tmdmnd 22680 | A topological monoid is a monoid. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ (𝐺 ∈ TopMnd → 𝐺 ∈ Mnd) | ||
Theorem | tmdtps 22681 | A topological monoid is a topological space. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ (𝐺 ∈ TopMnd → 𝐺 ∈ TopSp) | ||
Theorem | istgp 22682 | 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 22683 | A topological group is a group. (Contributed by FL, 18-Apr-2010.) (Revised by Mario Carneiro, 13-Aug-2015.) |
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp) | ||
Theorem | tgptmd 22684 | A topological group is a topological monoid. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopMnd) | ||
Theorem | tgptps 22685 | A topological group is a topological space. (Contributed by FL, 21-Jun-2010.) (Revised by Mario Carneiro, 13-Aug-2015.) |
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopSp) | ||
Theorem | tmdtopon 22686 | 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 22687 | 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 22688 | 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 22689 | 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 22690 | 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 22691 | 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 22692* | Continuity of the group sum; analogue of cnmpt12f 22271 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 22693* | Continuity of the group sum; analogue of cnmpt22f 22280 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 22694* | Write out the definition of continuity of +g explicitly. (Contributed by Mario Carneiro, 20-Sep-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ∀𝑥 ∈ 𝑢 ∀𝑦 ∈ 𝑣 (𝑥 + 𝑦) ∈ 𝑈)) | ||
Theorem | tgpsubcn 22695 | 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 𝐽)) | ||
Theorem | istgp2 22696 | A group with a topology is a topological group iff the subtraction operation is continuous. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ (𝐺 ∈ TopGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ TopSp ∧ − ∈ ((𝐽 ×t 𝐽) Cn 𝐽))) | ||
Theorem | tmdmulg 22697* | In a topological monoid, the n-times group multiple function is continuous. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ ((𝐺 ∈ TopMnd ∧ 𝑁 ∈ ℕ0) → (𝑥 ∈ 𝐵 ↦ (𝑁 · 𝑥)) ∈ (𝐽 Cn 𝐽)) | ||
Theorem | tgpmulg 22698* | In a topological group, the n-times group multiple function is continuous. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ ((𝐺 ∈ TopGrp ∧ 𝑁 ∈ ℤ) → (𝑥 ∈ 𝐵 ↦ (𝑁 · 𝑥)) ∈ (𝐽 Cn 𝐽)) | ||
Theorem | tgpmulg2 22699 | In a topological monoid, the group multiple function is jointly continuous (although this is not saying much as one of the factors is discrete). Use zdis 23421 to write the left topology as a subset of the complex numbers. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ (𝐺 ∈ TopGrp → · ∈ ((𝒫 ℤ ×t 𝐽) Cn 𝐽)) | ||
Theorem | tmdgsum 22700* | In a topological monoid, the group sum operation is a continuous function from the function space to the base topology. This theorem is not true when 𝐴 is infinite, because in this case for any basic open set of the domain one of the factors will be the whole space, so by varying the value of the functions to sum at this index, one can achieve any desired sum. (Contributed by Mario Carneiro, 19-Sep-2015.) (Proof shortened by AV, 24-Jul-2019.) |
⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd ∧ 𝐴 ∈ Fin) → (𝑥 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑥)) ∈ ((𝐽 ↑ko 𝒫 𝐴) Cn 𝐽)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |