![]() |
Metamath
Proof Explorer Theorem List (p. 236 of 478) | < 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-30149) |
![]() (30150-31672) |
![]() (31673-47754) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fclsopni 23501 | 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 23502 | 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 23503 | 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 23504 | 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 23505* | 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 23506* | 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 23507* | 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 23508 | 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 23509 | 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 23510 | 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 23511* | 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 23512 | 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 23513* | 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 23514* | A filter converges to a point iff every finer filter clusters there. Along with fclsfnflim 23513, 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 23515 | Forward direction of fclscmp 23516. 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 23516* | 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 23517 | 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 23518* | 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 23519 | 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 23520* | 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 23521* | 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 23522 | 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 23523 | 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 23524 | 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 23525 | 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 23526 | Lemma for cnpfcf 23527. 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 23527* | 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 23528* | 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 23529 | 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 23530* | Lemma for alexsub 23531. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ (𝜑 → 𝑋 ∈ UFL) & ⊢ (𝜑 → 𝑋 = ∪ 𝐵) & ⊢ (𝜑 → 𝐽 = (topGen‘(fi‘𝐵))) & ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥)) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦) & ⊢ (𝜑 → 𝐹 ∈ (UFil‘𝑋)) & ⊢ (𝜑 → (𝐽 fLim 𝐹) = ∅) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | alexsub 23531* | 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 23537 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 23532* | Biconditional form of the Alexander Subbase Theorem alexsub 23531. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪ 𝐵) → ((topGen‘(fi‘𝐵)) ∈ Comp ↔ ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦))) | ||
Theorem | alexsubALTlem1 23533* | Lemma for alexsubALT 23537. 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 23534* | Lemma for alexsubALT 23537. 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 23535* | Lemma for alexsubALT 23537. 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 23536* | Lemma for alexsubALT 23537. 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 23537* | 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 23538* | Lemma for ptcmp 23544. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) & ⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶Comp) & ⊢ (𝜑 → 𝑋 ∈ (UFL ∩ dom card)) ⇒ ⊢ (𝜑 → (𝑋 = ∪ (ran 𝑆 ∪ {𝑋}) ∧ (∏t‘𝐹) = (topGen‘(fi‘(ran 𝑆 ∪ {𝑋}))))) | ||
Theorem | ptcmplem2 23539* | Lemma for ptcmp 23544. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) & ⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶Comp) & ⊢ (𝜑 → 𝑋 ∈ (UFL ∩ dom card)) & ⊢ (𝜑 → 𝑈 ⊆ ran 𝑆) & ⊢ (𝜑 → 𝑋 = ∪ 𝑈) & ⊢ (𝜑 → ¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧) ⇒ ⊢ (𝜑 → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ∈ dom card) | ||
Theorem | ptcmplem3 23540* | Lemma for ptcmp 23544. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) & ⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶Comp) & ⊢ (𝜑 → 𝑋 ∈ (UFL ∩ dom card)) & ⊢ (𝜑 → 𝑈 ⊆ ran 𝑆) & ⊢ (𝜑 → 𝑋 = ∪ 𝑈) & ⊢ (𝜑 → ¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧) & ⊢ 𝐾 = {𝑢 ∈ (𝐹‘𝑘) ∣ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝑈} ⇒ ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) | ||
Theorem | ptcmplem4 23541* | Lemma for ptcmp 23544. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) & ⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶Comp) & ⊢ (𝜑 → 𝑋 ∈ (UFL ∩ dom card)) & ⊢ (𝜑 → 𝑈 ⊆ ran 𝑆) & ⊢ (𝜑 → 𝑋 = ∪ 𝑈) & ⊢ (𝜑 → ¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧) & ⊢ 𝐾 = {𝑢 ∈ (𝐹‘𝑘) ∣ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝑈} ⇒ ⊢ ¬ 𝜑 | ||
Theorem | ptcmplem5 23542* | Lemma for ptcmp 23544. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝑆 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) & ⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶Comp) & ⊢ (𝜑 → 𝑋 ∈ (UFL ∩ dom card)) ⇒ ⊢ (𝜑 → (∏t‘𝐹) ∈ Comp) | ||
Theorem | ptcmpg 23543 | 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 23544). (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ 𝐽 = (∏t‘𝐹) & ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Comp ∧ 𝑋 ∈ (UFL ∩ dom card)) → 𝐽 ∈ Comp) | ||
Theorem | ptcmp 23544 | 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 23545 | Extend class notation with the continuous extension operation. |
class CnExt | ||
Definition | df-cnext 23546* | 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 23547* | 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 23548* | The continuous extension of a given function 𝐹. (Contributed by Thierry Arnoux, 1-Dec-2017.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐵 = ∪ 𝐾 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝑋)) → ((𝐽CnExt𝐾)‘𝐹) = ∪ 𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹))) | ||
Theorem | cnextrel 23549 | In the general case, a continuous extension is a relation. (Contributed by Thierry Arnoux, 20-Dec-2017.) |
⊢ 𝐶 = ∪ 𝐽 & ⊢ 𝐵 = ∪ 𝐾 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝐶)) → Rel ((𝐽CnExt𝐾)‘𝐹)) | ||
Theorem | cnextfun 23550 | 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 23551* | 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 23552* | 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 23553* | 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 23554* | 𝐹 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 23555 | 𝐹 and its extension by continuity agree on the domain of 𝐹. (Contributed by Thierry Arnoux, 29-Aug-2020.) |
⊢ 𝐶 = ∪ 𝐽 & ⊢ 𝐵 = ∪ 𝐾 & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝐾 ∈ Haus) & ⊢ (𝜑 → 𝐴 ⊆ 𝐶) & ⊢ (𝜑 → 𝐹 ∈ ((𝐽 ↾t 𝐴) Cn 𝐾)) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → (((𝐽CnExt𝐾)‘𝐹)‘𝑋) = (𝐹‘𝑋)) | ||
Syntax | ctmd 23556 | Extend class notation with the class of all topological monoids. |
class TopMnd | ||
Syntax | ctgp 23557 | Extend class notation with the class of all topological groups. |
class TopGrp | ||
Definition | df-tmd 23558* | 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 23559* | 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 23560 | The predicate "is a topological monoid". (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ 𝐹 = (+𝑓‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) ⇒ ⊢ (𝐺 ∈ TopMnd ↔ (𝐺 ∈ Mnd ∧ 𝐺 ∈ TopSp ∧ 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽))) | ||
Theorem | tmdmnd 23561 | A topological monoid is a monoid. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ (𝐺 ∈ TopMnd → 𝐺 ∈ Mnd) | ||
Theorem | tmdtps 23562 | A topological monoid is a topological space. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ (𝐺 ∈ TopMnd → 𝐺 ∈ TopSp) | ||
Theorem | istgp 23563 | 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 23564 | A topological group is a group. (Contributed by FL, 18-Apr-2010.) (Revised by Mario Carneiro, 13-Aug-2015.) |
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp) | ||
Theorem | tgptmd 23565 | A topological group is a topological monoid. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopMnd) | ||
Theorem | tgptps 23566 | A topological group is a topological space. (Contributed by FL, 21-Jun-2010.) (Revised by Mario Carneiro, 13-Aug-2015.) |
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopSp) | ||
Theorem | tmdtopon 23567 | 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 23568 | 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 23569 | 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 23570 | 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 23571 | 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 23572 | 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 23573* | Continuity of the group sum; analogue of cnmpt12f 23152 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 23574* | Continuity of the group sum; analogue of cnmpt22f 23161 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 23575* | Write out the definition of continuity of +g explicitly. (Contributed by Mario Carneiro, 20-Sep-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (((𝐺 ∈ TopMnd ∧ 𝑈 ∈ 𝐽) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 + 𝑌) ∈ 𝑈)) → ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ 𝑌 ∈ 𝑣 ∧ ∀𝑥 ∈ 𝑢 ∀𝑦 ∈ 𝑣 (𝑥 + 𝑦) ∈ 𝑈)) | ||
Theorem | tgpsubcn 23576 | 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 23577 | 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 23578* | 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 23579* | 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 23580 | 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 24314 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 23581* | 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 𝐽)) | ||
Theorem | tmdgsum2 23582* | For any neighborhood 𝑈 of 𝑛𝑋, there is a neighborhood 𝑢 of 𝑋 such that any sum of 𝑛 elements in 𝑢 sums to an element of 𝑈. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐺 ∈ TopMnd) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝑈 ∈ 𝐽) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → ((♯‘𝐴) · 𝑋) ∈ 𝑈) ⇒ ⊢ (𝜑 → ∃𝑢 ∈ 𝐽 (𝑋 ∈ 𝑢 ∧ ∀𝑓 ∈ (𝑢 ↑m 𝐴)(𝐺 Σg 𝑓) ∈ 𝑈)) | ||
Theorem | oppgtmd 23583 | The opposite of a topological monoid is a topological monoid. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ 𝑂 = (oppg‘𝐺) ⇒ ⊢ (𝐺 ∈ TopMnd → 𝑂 ∈ TopMnd) | ||
Theorem | oppgtgp 23584 | The opposite of a topological group is a topological group. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝑂 = (oppg‘𝐺) ⇒ ⊢ (𝐺 ∈ TopGrp → 𝑂 ∈ TopGrp) | ||
Theorem | distgp 23585 | Any group equipped with the discrete topology is a topological group. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐽 = 𝒫 𝐵) → 𝐺 ∈ TopGrp) | ||
Theorem | indistgp 23586 | Any group equipped with the indiscrete topology is a topological group. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐽 = {∅, 𝐵}) → 𝐺 ∈ TopGrp) | ||
Theorem | efmndtmd 23587 | The monoid of endofunctions on a set 𝐴 is a topological monoid. Formerly part of proof for symgtgp 23592. (Contributed by AV, 23-Feb-2024.) |
⊢ 𝑀 = (EndoFMnd‘𝐴) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝑀 ∈ TopMnd) | ||
Theorem | tmdlactcn 23588* | The left group action of element 𝐴 in a topological monoid 𝐺 is a continuous function. (Contributed by FL, 18-Mar-2008.) (Revised by Mario Carneiro, 14-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ (𝐴 + 𝑥)) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) ⇒ ⊢ ((𝐺 ∈ TopMnd ∧ 𝐴 ∈ 𝑋) → 𝐹 ∈ (𝐽 Cn 𝐽)) | ||
Theorem | tgplacthmeo 23589* | The left group action of element 𝐴 in a topological group 𝐺 is a homeomorphism from the group to itself. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ (𝐴 + 𝑥)) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) ⇒ ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → 𝐹 ∈ (𝐽Homeo𝐽)) | ||
Theorem | submtmd 23590 | A submonoid of a topological monoid is a topological monoid. (Contributed by Mario Carneiro, 6-Oct-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ ((𝐺 ∈ TopMnd ∧ 𝑆 ∈ (SubMnd‘𝐺)) → 𝐻 ∈ TopMnd) | ||
Theorem | subgtgp 23591 | A subgroup of a topological group is a topological group. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ TopGrp) | ||
Theorem | symgtgp 23592 | The symmetric group is a topological group. (Contributed by Mario Carneiro, 2-Sep-2015.) (Proof shortened by AV, 30-Mar-2024.) |
⊢ 𝐺 = (SymGrp‘𝐴) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐺 ∈ TopGrp) | ||
Theorem | subgntr 23593 | A subgroup of a topological group with nonempty interior is open. Alternatively, dual to clssubg 23595, the interior of a subgroup is either a subgroup, or empty. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘𝐺) ⇒ ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ ((int‘𝐽)‘𝑆)) → 𝑆 ∈ 𝐽) | ||
Theorem | opnsubg 23594 | An open subgroup of a topological group is also closed. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘𝐺) ⇒ ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑆 ∈ 𝐽) → 𝑆 ∈ (Clsd‘𝐽)) | ||
Theorem | clssubg 23595 | The closure of a subgroup in a topological group is a subgroup. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘𝐺) ⇒ ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ((cls‘𝐽)‘𝑆) ∈ (SubGrp‘𝐺)) | ||
Theorem | clsnsg 23596 | The closure of a normal subgroup is a normal subgroup. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘𝐺) ⇒ ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (NrmSGrp‘𝐺)) → ((cls‘𝐽)‘𝑆) ∈ (NrmSGrp‘𝐺)) | ||
Theorem | cldsubg 23597 | A subgroup of finite index is closed iff it is open. (Contributed by Mario Carneiro, 20-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ 𝑅 = (𝐺 ~QG 𝑆) & ⊢ 𝑋 = (Base‘𝐺) ⇒ ⊢ ((𝐺 ∈ TopGrp ∧ 𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑋 / 𝑅) ∈ Fin) → (𝑆 ∈ (Clsd‘𝐽) ↔ 𝑆 ∈ 𝐽)) | ||
Theorem | tgpconncompeqg 23598* | The connected component containing 𝐴 is the left coset of the identity component containing 𝐴. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} & ⊢ ∼ = (𝐺 ~QG 𝑆) ⇒ ⊢ ((𝐺 ∈ TopGrp ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}) | ||
Theorem | tgpconncomp 23599* | The identity component, the connected component containing the identity element, is a closed (conncompcld 22920) normal subgroup. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⇒ ⊢ (𝐺 ∈ TopGrp → 𝑆 ∈ (NrmSGrp‘𝐺)) | ||
Theorem | tgpconncompss 23600* | The identity component is a subset of any open subgroup. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ ( 0 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)} ⇒ ⊢ ((𝐺 ∈ TopGrp ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ 𝐽) → 𝑆 ⊆ 𝑇) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |