Home | Metamath
Proof Explorer Theorem List (p. 211 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | iscmp 21001* | The predicate "is a compact topology". (Contributed by FL, 22-Dec-2008.) (Revised by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))) | ||
Theorem | cmpcov 21002* | An open cover of a compact topology has a finite subcover. (Contributed by Jeff Hankins, 29-Jun-2009.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Comp ∧ 𝑆 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑆) → ∃𝑠 ∈ (𝒫 𝑆 ∩ Fin)𝑋 = ∪ 𝑠) | ||
Theorem | cmpcov2 21003* | Rewrite cmpcov 21002 for the cover {𝑦 ∈ 𝐽 ∣ 𝜑}. (Contributed by Mario Carneiro, 11-Sep-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Comp ∧ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝜑)) → ∃𝑠 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = ∪ 𝑠 ∧ ∀𝑦 ∈ 𝑠 𝜑)) | ||
Theorem | cmpcovf 21004* | Combine cmpcov 21002 with ac6sfi 8089 to show the existence of a function that indexes the elements that are generating the open cover. (Contributed by Mario Carneiro, 14-Sep-2014.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ (𝑧 = (𝑓‘𝑦) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐽 ∈ Comp ∧ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝐴 𝜑)) → ∃𝑠 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = ∪ 𝑠 ∧ ∃𝑓(𝑓:𝑠⟶𝐴 ∧ ∀𝑦 ∈ 𝑠 𝜓))) | ||
Theorem | cncmp 21005 | Compactness is respected by a continuous onto map. (Contributed by Jeff Hankins, 12-Jul-2009.) (Proof shortened by Mario Carneiro, 22-Aug-2015.) |
⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ ((𝐽 ∈ Comp ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ Comp) | ||
Theorem | fincmp 21006 | A finite topology is compact. (Contributed by FL, 22-Dec-2008.) |
⊢ (𝐽 ∈ (Top ∩ Fin) → 𝐽 ∈ Comp) | ||
Theorem | 0cmp 21007 | The singleton of the empty set is compact. (Contributed by FL, 2-Aug-2009.) |
⊢ {∅} ∈ Comp | ||
Theorem | cmptop 21008 | A compact topology is a topology. (Contributed by Jeff Hankins, 29-Jun-2009.) |
⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top) | ||
Theorem | rncmp 21009 | The image of a compact set under a continuous function is compact. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ ((𝐽 ∈ Comp ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐾 ↾t ran 𝐹) ∈ Comp) | ||
Theorem | imacmp 21010 | The image of a compact set under a continuous function is compact. (Contributed by Mario Carneiro, 18-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ (𝐽 ↾t 𝐴) ∈ Comp) → (𝐾 ↾t (𝐹 “ 𝐴)) ∈ Comp) | ||
Theorem | discmp 21011 | A discrete topology is compact iff the base set is finite. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Comp) | ||
Theorem | cmpsublem 21012* | Lemma for cmpsub 21013. (Contributed by Jeff Hankins, 28-Jun-2009.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑) → ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡))) | ||
Theorem | cmpsub 21013* | Two equivalent ways of describing a compact subset of a topological space. Inspired by Sue E. Goodman's Beginning Topology. (Contributed by Jeff Hankins, 22-Jun-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝐽 ↾t 𝑆) ∈ Comp ↔ ∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑))) | ||
Theorem | tgcmp 21014* | A topology generated by a basis is compact iff open covers drawn from the basis have finite subcovers. (See also alexsub 21659, which further specializes to subbases, assuming the ultrafilter lemma.) (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) → ((topGen‘𝐵) ∈ Comp ↔ ∀𝑦 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))) | ||
Theorem | cmpcld 21015 | A closed subset of a compact space is compact. (Contributed by Jeff Hankins, 29-Jun-2009.) |
⊢ ((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) → (𝐽 ↾t 𝑆) ∈ Comp) | ||
Theorem | uncmp 21016 | The union of two compact sets is compact. (Contributed by Jeff Hankins, 30-Jan-2010.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ ((𝐽 ↾t 𝑆) ∈ Comp ∧ (𝐽 ↾t 𝑇) ∈ Comp)) → 𝐽 ∈ Comp) | ||
Theorem | fiuncmp 21017* | A finite union of compact sets is compact. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝐽 ↾t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp) | ||
Theorem | sscmp 21018 | A subset of a compact topology (i.e. a coarser topology) is compact. (Contributed by Mario Carneiro, 20-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐾 ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾) → 𝐽 ∈ Comp) | ||
Theorem | hauscmplem 21019* | Lemma for hauscmp 21020. (Contributed by Mario Carneiro, 27-Nov-2013.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑂 = {𝑦 ∈ 𝐽 ∣ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))} & ⊢ (𝜑 → 𝐽 ∈ Haus) & ⊢ (𝜑 → 𝑆 ⊆ 𝑋) & ⊢ (𝜑 → (𝐽 ↾t 𝑆) ∈ Comp) & ⊢ (𝜑 → 𝐴 ∈ (𝑋 ∖ 𝑆)) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆))) | ||
Theorem | hauscmp 21020 | A compact subspace of a T2 space is closed. (Contributed by Jeff Hankins, 16-Jan-2010.) (Proof shortened by Mario Carneiro, 14-Dec-2013.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Haus ∧ 𝑆 ⊆ 𝑋 ∧ (𝐽 ↾t 𝑆) ∈ Comp) → 𝑆 ∈ (Clsd‘𝐽)) | ||
Theorem | cmpfi 21021* | If a topology is compact and a collection of closed sets has the finite intersection property, its intersection is nonempty. (Contributed by Jeff Hankins, 25-Aug-2009.) (Proof shortened by Mario Carneiro, 1-Sep-2015.) |
⊢ (𝐽 ∈ Top → (𝐽 ∈ Comp ↔ ∀𝑥 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑥) → ∩ 𝑥 ≠ ∅))) | ||
Theorem | cmpfii 21022 | In a compact topology, a system of closed sets with nonempty finite intersections has a nonempty intersection. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ ((𝐽 ∈ Comp ∧ 𝑋 ⊆ (Clsd‘𝐽) ∧ ¬ ∅ ∈ (fi‘𝑋)) → ∩ 𝑋 ≠ ∅) | ||
Theorem | bwth 21023* | The glorious Bolzano-Weierstrass theorem. The first general topology theorem ever proved. The first mention of this theorem can be found in a course by Weierstrass from 1865. In his course Weierstrass called it a lemma. He didn't know how famous this theorem would be. He used a Euclidean space instead of a general compact space. And he was not aware of the Heine-Borel property. But the concepts of neighborhood and limit point were already there although not precisely defined. Cantor was one of his students. He published and used the theorem in an article from 1872. The rest of the general topology followed from that. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) Revised by BL to significantly shorten the proof and avoid infinity, regularity, and choice. (Revised by Brendan Leahy, 26-Dec-2018.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Comp ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin) → ∃𝑥 ∈ 𝑋 𝑥 ∈ ((limPt‘𝐽)‘𝐴)) | ||
Syntax | ccon 21024 | Extend class notation with the class of all connected topologies. |
class Con | ||
Definition | df-con 21025 | Topologies are connected when only ∅ and ∪ 𝑗 are both open and closed. (Contributed by FL, 17-Nov-2008.) |
⊢ Con = {𝑗 ∈ Top ∣ (𝑗 ∩ (Clsd‘𝑗)) = {∅, ∪ 𝑗}} | ||
Theorem | iscon 21026 | The predicate 𝐽 is a connected topology . (Contributed by FL, 17-Nov-2008.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Con ↔ (𝐽 ∈ Top ∧ (𝐽 ∩ (Clsd‘𝐽)) = {∅, 𝑋})) | ||
Theorem | iscon2 21027 | The predicate 𝐽 is a connected topology . (Contributed by Mario Carneiro, 10-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Con ↔ (𝐽 ∈ Top ∧ (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, 𝑋})) | ||
Theorem | conclo 21028 | The only nonempty clopen set of a connected topology is the whole space. (Contributed by Mario Carneiro, 10-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ (𝜑 → 𝐽 ∈ Con) & ⊢ (𝜑 → 𝐴 ∈ 𝐽) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → 𝐴 ∈ (Clsd‘𝐽)) ⇒ ⊢ (𝜑 → 𝐴 = 𝑋) | ||
Theorem | conndisj 21029 | If a topology is connected, its underlying set can't be partitioned into two nonempty non-overlapping open sets. (Contributed by FL, 16-Nov-2008.) (Proof shortened by Mario Carneiro, 10-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ (𝜑 → 𝐽 ∈ Con) & ⊢ (𝜑 → 𝐴 ∈ 𝐽) & ⊢ (𝜑 → 𝐴 ≠ ∅) & ⊢ (𝜑 → 𝐵 ∈ 𝐽) & ⊢ (𝜑 → 𝐵 ≠ ∅) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) ⇒ ⊢ (𝜑 → (𝐴 ∪ 𝐵) ≠ 𝑋) | ||
Theorem | contop 21030 | A connected topology is a topology. (Contributed by FL, 22-Dec-2008.) (Revised by Mario Carneiro, 14-Dec-2013.) |
⊢ (𝐽 ∈ Con → 𝐽 ∈ Top) | ||
Theorem | indiscon 21031 | The indiscrete topology (or trivial topology) on any set is connected. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 14-Aug-2015.) |
⊢ {∅, 𝐴} ∈ Con | ||
Theorem | dfcon2 21032* | An alternate definition of connectedness. (Contributed by Jeff Hankins, 9-Jul-2009.) (Proof shortened by Mario Carneiro, 10-Mar-2015.) |
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Con ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ 𝑋))) | ||
Theorem | consuba 21033* | Connectedness for a subspace. See connsub 21034. (Contributed by FL, 29-May-2014.) (Proof shortened by Mario Carneiro, 10-Mar-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((𝐽 ↾t 𝐴) ∈ Con ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (((𝑥 ∩ 𝐴) ≠ ∅ ∧ (𝑦 ∩ 𝐴) ≠ ∅ ∧ ((𝑥 ∩ 𝑦) ∩ 𝐴) = ∅) → ((𝑥 ∪ 𝑦) ∩ 𝐴) ≠ 𝐴))) | ||
Theorem | connsub 21034* | Two equivalent ways of saying that a subspace topology is connected. (Contributed by Jeff Hankins, 9-Jul-2009.) (Proof shortened by Mario Carneiro, 10-Mar-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋) → ((𝐽 ↾t 𝑆) ∈ Con ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (((𝑥 ∩ 𝑆) ≠ ∅ ∧ (𝑦 ∩ 𝑆) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ 𝑆)) → ¬ 𝑆 ⊆ (𝑥 ∪ 𝑦)))) | ||
Theorem | cnconn 21035 | Connectedness is respected by a continuous onto map. (Contributed by Jeff Hankins, 12-Jul-2009.) (Proof shortened by Mario Carneiro, 10-Mar-2015.) |
⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ ((𝐽 ∈ Con ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ Con) | ||
Theorem | nconsubb 21036 | Disconnectedness for a subspace. (Contributed by FL, 29-May-2014.) (Proof shortened by Mario Carneiro, 10-Mar-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) & ⊢ (𝜑 → 𝑈 ∈ 𝐽) & ⊢ (𝜑 → 𝑉 ∈ 𝐽) & ⊢ (𝜑 → (𝑈 ∩ 𝐴) ≠ ∅) & ⊢ (𝜑 → (𝑉 ∩ 𝐴) ≠ ∅) & ⊢ (𝜑 → ((𝑈 ∩ 𝑉) ∩ 𝐴) = ∅) & ⊢ (𝜑 → 𝐴 ⊆ (𝑈 ∪ 𝑉)) ⇒ ⊢ (𝜑 → ¬ (𝐽 ↾t 𝐴) ∈ Con) | ||
Theorem | consubclo 21037 | If a clopen set meets a connected subspace, it must contain the entire subspace. (Contributed by Mario Carneiro, 10-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) & ⊢ (𝜑 → (𝐽 ↾t 𝐴) ∈ Con) & ⊢ (𝜑 → 𝐵 ∈ 𝐽) & ⊢ (𝜑 → (𝐵 ∩ 𝐴) ≠ ∅) & ⊢ (𝜑 → 𝐵 ∈ (Clsd‘𝐽)) ⇒ ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | ||
Theorem | conima 21038 | The image of a connected set is connected. (Contributed by Mario Carneiro, 7-Jul-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) & ⊢ (𝜑 → (𝐽 ↾t 𝐴) ∈ Con) ⇒ ⊢ (𝜑 → (𝐾 ↾t (𝐹 “ 𝐴)) ∈ Con) | ||
Theorem | concn 21039 | A continuous function from a connected topology with one point in a clopen set must lie entirely within the set. (Contributed by Mario Carneiro, 16-Feb-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ (𝜑 → 𝐽 ∈ Con) & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝑈 ∈ 𝐾) & ⊢ (𝜑 → 𝑈 ∈ (Clsd‘𝐾)) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → (𝐹‘𝐴) ∈ 𝑈) ⇒ ⊢ (𝜑 → 𝐹:𝑋⟶𝑈) | ||
Theorem | iunconlem 21040* | Lemma for iuncon 21041. (Contributed by Mario Carneiro, 11-Jun-2014.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ⊆ 𝑋) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑃 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐽 ↾t 𝐵) ∈ Con) & ⊢ (𝜑 → 𝑈 ∈ 𝐽) & ⊢ (𝜑 → 𝑉 ∈ 𝐽) & ⊢ (𝜑 → (𝑉 ∩ ∪ 𝑘 ∈ 𝐴 𝐵) ≠ ∅) & ⊢ (𝜑 → (𝑈 ∩ 𝑉) ⊆ (𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵)) & ⊢ (𝜑 → ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑈 ∪ 𝑉)) & ⊢ Ⅎ𝑘𝜑 ⇒ ⊢ (𝜑 → ¬ 𝑃 ∈ 𝑈) | ||
Theorem | iuncon 21041* | The indexed union of connected overlapping subspaces sharing a common point is connected. (Contributed by Mario Carneiro, 11-Jun-2014.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ⊆ 𝑋) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑃 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐽 ↾t 𝐵) ∈ Con) ⇒ ⊢ (𝜑 → (𝐽 ↾t ∪ 𝑘 ∈ 𝐴 𝐵) ∈ Con) | ||
Theorem | uncon 21042 | The union of two connected overlapping subspaces is connected. (Contributed by FL, 29-May-2014.) (Proof shortened by Mario Carneiro, 11-Jun-2014.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) ∧ (𝐴 ∩ 𝐵) ≠ ∅) → (((𝐽 ↾t 𝐴) ∈ Con ∧ (𝐽 ↾t 𝐵) ∈ Con) → (𝐽 ↾t (𝐴 ∪ 𝐵)) ∈ Con)) | ||
Theorem | clscon 21043 | The closure of a connected set is connected. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Con) → (𝐽 ↾t ((cls‘𝐽)‘𝐴)) ∈ Con) | ||
Theorem | concompid 21044* | The connected component containing 𝐴 contains 𝐴. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Con)} ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ 𝑆) | ||
Theorem | concompcon 21045* | The connected component containing 𝐴 is connected. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Con)} ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐽 ↾t 𝑆) ∈ Con) | ||
Theorem | concompss 21046* | The connected component containing 𝐴 is a superset of any other connected set containing 𝐴. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Con)} ⇒ ⊢ ((𝑇 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑇 ∧ (𝐽 ↾t 𝑇) ∈ Con) → 𝑇 ⊆ 𝑆) | ||
Theorem | concompcld 21047* | The connected component containing 𝐴 is a closed set. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Con)} ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑋) → 𝑆 ∈ (Clsd‘𝐽)) | ||
Theorem | concompclo 21048* | The connected component containing 𝐴 is a subset of any clopen set containing 𝐴. (Contributed by Mario Carneiro, 20-Sep-2015.) |
⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Con)} ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑇 ∈ (𝐽 ∩ (Clsd‘𝐽)) ∧ 𝐴 ∈ 𝑇) → 𝑆 ⊆ 𝑇) | ||
Theorem | t1conperf 21049 | A connected T1 space is perfect, unless it is the topology of a singleton. (Contributed by Mario Carneiro, 26-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Fre ∧ 𝐽 ∈ Con ∧ ¬ 𝑋 ≈ 1𝑜) → 𝐽 ∈ Perf) | ||
Syntax | c1stc 21050 | Extend class definition to include the class of all first-countable topologies. |
class 1st𝜔 | ||
Syntax | c2ndc 21051 | Extend class definition to include the class of all second-countable topologies. |
class 2nd𝜔 | ||
Definition | df-1stc 21052* | Define the class of all first-countable topologies. (Contributed by Jeff Hankins, 22-Aug-2009.) |
⊢ 1st𝜔 = {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∃𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧)))} | ||
Definition | df-2ndc 21053* | Define the class of all second-countable topologies. (Contributed by Jeff Hankins, 17-Jan-2010.) |
⊢ 2nd𝜔 = {𝑗 ∣ ∃𝑥 ∈ TopBases (𝑥 ≼ ω ∧ (topGen‘𝑥) = 𝑗)} | ||
Theorem | is1stc 21054* | The predicate "is a first-countable topology." This can be described as "every point has a countable local basis" - that is, every point has a countable collection of open sets containing it such that every open set containing the point has an open set from this collection as a subset. (Contributed by Jeff Hankins, 22-Aug-2009.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ 1st𝜔 ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝒫 𝐽(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧))))) | ||
Theorem | is1stc2 21055* | An equivalent way of saying "is a first-countable topology." (Contributed by Jeff Hankins, 22-Aug-2009.) (Revised by Mario Carneiro, 21-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ 1st𝜔 ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝒫 𝐽(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))) | ||
Theorem | 1stctop 21056 | A first-countable topology is a topology. (Contributed by Jeff Hankins, 22-Aug-2009.) |
⊢ (𝐽 ∈ 1st𝜔 → 𝐽 ∈ Top) | ||
Theorem | 1stcclb 21057* | A property of points in a first-countable topology. (Contributed by Jeff Hankins, 22-Aug-2009.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) → ∃𝑥 ∈ 𝒫 𝐽(𝑥 ≼ ω ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑧 ∈ 𝑥 (𝐴 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦)))) | ||
Theorem | 1stcfb 21058* | For any point 𝐴 in a first-countable topology, there is a function 𝑓:ℕ⟶𝐽 enumerating neighborhoods of 𝐴 which is decreasing and forms a local base. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑋) → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦))) | ||
Theorem | is2ndc 21059* | The property of being second-countable. (Contributed by Jeff Hankins, 17-Jan-2010.) (Revised by Mario Carneiro, 21-Mar-2015.) |
⊢ (𝐽 ∈ 2nd𝜔 ↔ ∃𝑥 ∈ TopBases (𝑥 ≼ ω ∧ (topGen‘𝑥) = 𝐽)) | ||
Theorem | 2ndctop 21060 | A second-countable topology is a topology. (Contributed by Jeff Hankins, 17-Jan-2010.) (Revised by Mario Carneiro, 21-Mar-2015.) |
⊢ (𝐽 ∈ 2nd𝜔 → 𝐽 ∈ Top) | ||
Theorem | 2ndci 21061 | A countable basis generates a second-countable topology. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ ((𝐵 ∈ TopBases ∧ 𝐵 ≼ ω) → (topGen‘𝐵) ∈ 2nd𝜔) | ||
Theorem | 2ndcsb 21062* | Having a countable subbase is a sufficient condition for second-countability. (Contributed by Jeff Hankins, 17-Jan-2010.) (Proof shortened by Mario Carneiro, 21-Mar-2015.) |
⊢ (𝐽 ∈ 2nd𝜔 ↔ ∃𝑥(𝑥 ≼ ω ∧ (topGen‘(fi‘𝑥)) = 𝐽)) | ||
Theorem | 2ndcredom 21063 | A second-countable space has at most the cardinality of the continuum. (Contributed by Mario Carneiro, 9-Apr-2015.) |
⊢ (𝐽 ∈ 2nd𝜔 → 𝐽 ≼ ℝ) | ||
Theorem | 2ndc1stc 21064 | A second-countable space is first-countable. (Contributed by Jeff Hankins, 17-Jan-2010.) |
⊢ (𝐽 ∈ 2nd𝜔 → 𝐽 ∈ 1st𝜔) | ||
Theorem | 1stcrestlem 21065* | Lemma for 1stcrest 21066. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ (𝐵 ≼ ω → ran (𝑥 ∈ 𝐵 ↦ 𝐶) ≼ ω) | ||
Theorem | 1stcrest 21066 | A subspace of a first-countable space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ ((𝐽 ∈ 1st𝜔 ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ 1st𝜔) | ||
Theorem | 2ndcrest 21067 | A subspace of a second-countable space is second-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ ((𝐽 ∈ 2nd𝜔 ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ 2nd𝜔) | ||
Theorem | 2ndcctbss 21068* | If a topology is second-countable, every base has a countable subset which is a base. Exercise 16B2 in Willard. (Contributed by Jeff Hankins, 28-Jan-2010.) (Proof shortened by Mario Carneiro, 21-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐵 & ⊢ 𝐽 = (topGen‘𝐵) & ⊢ 𝑆 = {〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣))} ⇒ ⊢ ((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2nd𝜔) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏))) | ||
Theorem | 2ndcdisj 21069* | Any disjoint family of open sets in a second-countable space is countable. (The sets are required to be nonempty because otherwise there could be many empty sets in the family.) (Contributed by Mario Carneiro, 21-Mar-2015.) (Proof shortened by Mario Carneiro, 9-Apr-2015.) (Revised by NM, 17-Jun-2017.) |
⊢ ((𝐽 ∈ 2nd𝜔 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω) | ||
Theorem | 2ndcdisj2 21070* | Any disjoint collection of open sets in a second-countable space is countable. (Contributed by Mario Carneiro, 21-Mar-2015.) (Proof shortened by Mario Carneiro, 9-Apr-2015.) (Revised by NM, 17-Jun-2017.) |
⊢ ((𝐽 ∈ 2nd𝜔 ∧ 𝐴 ⊆ 𝐽 ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝑥) → 𝐴 ≼ ω) | ||
Theorem | 2ndcomap 21071* | A surjective continuous open map maps second-countable spaces to second-countable spaces. (Contributed by Mario Carneiro, 9-Apr-2015.) |
⊢ 𝑌 = ∪ 𝐾 & ⊢ (𝜑 → 𝐽 ∈ 2nd𝜔) & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → ran 𝐹 = 𝑌) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (𝐹 “ 𝑥) ∈ 𝐾) ⇒ ⊢ (𝜑 → 𝐾 ∈ 2nd𝜔) | ||
Theorem | 2ndcsep 21072* | A second-countable topology is separable, which is to say it contains a countable dense subset. (Contributed by Mario Carneiro, 13-Apr-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ 2nd𝜔 → ∃𝑥 ∈ 𝒫 𝑋(𝑥 ≼ ω ∧ ((cls‘𝐽)‘𝑥) = 𝑋)) | ||
Theorem | dis2ndc 21073 | A discrete space is second-countable iff it is countable. (Contributed by Mario Carneiro, 13-Apr-2015.) |
⊢ (𝑋 ≼ ω ↔ 𝒫 𝑋 ∈ 2nd𝜔) | ||
Theorem | 1stcelcls 21074* | 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 9140. A space satisfying the conclusion of this theorem is called a sequential space, so the theorem can also be stated as "every first-countable space is a sequential space". (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ 1st𝜔 ∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃))) | ||
Theorem | 1stccnp 21075* | A mapping is continuous at 𝑃 in a first-countable space 𝑋 iff it is sequentially continuous at 𝑃, meaning that the image under 𝐹 of every sequence converging at 𝑃 converges to 𝐹(𝑃). This proof uses ax-cc 9140, but only via 1stcelcls 21074, so it could be refactored into a proof that continuity and sequential continuity are the same in sequential spaces. (Contributed by Mario Carneiro, 7-Sep-2015.) |
⊢ (𝜑 → 𝐽 ∈ 1st𝜔) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝑃 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃))))) | ||
Theorem | 1stccn 21076* | A mapping 𝑋⟶𝑌, where 𝑋 is first-countable, is continuous iff it is sequentially continuous, meaning that for any sequence 𝑓(𝑛) converging to 𝑥, its image under 𝐹 converges to 𝐹(𝑥). (Contributed by Mario Carneiro, 7-Sep-2015.) |
⊢ (𝜑 → 𝐽 ∈ 1st𝜔) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝐹:𝑋⟶𝑌) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ∀𝑓(𝑓:ℕ⟶𝑋 → ∀𝑥(𝑓(⇝𝑡‘𝐽)𝑥 → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑥))))) | ||
Syntax | clly 21077 | Extend class notation with the "locally 𝐴 " predicate of a topological space. |
class Locally 𝐴 | ||
Syntax | cnlly 21078 | Extend class notation with the "N-locally 𝐴 " predicate of a topological space. |
class 𝑛-Locally 𝐴 | ||
Definition | df-lly 21079* | Define a space that is locally 𝐴, where 𝐴 is a topological property like "compact", "connected", or "path-connected". A topological space is locally 𝐴 if every neighborhood of a point contains an open sub-neighborhood that is 𝐴 in the subspace topology. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ Locally 𝐴 = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝑗 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝐴)} | ||
Definition | df-nlly 21080* |
Define a space that is n-locally 𝐴, where 𝐴 is a topological
property like "compact", "connected", or
"path-connected". A
topological space is n-locally 𝐴 if every neighborhood of a point
contains a sub-neighborhood that is 𝐴 in the subspace topology.
The terminology "n-locally", where 'n' stands for "neighborhood", is not standard, although this is sometimes called "weakly locally 𝐴". The reason for the distinction is that some notions only make sense for arbitrary neighborhoods (such as "locally compact", which is actually 𝑛-Locally Comp in our terminology - open compact sets are not very useful), while others such as "locally connected" are strictly weaker notions if the neighborhoods are not required to be open. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ 𝑛-Locally 𝐴 = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴} | ||
Theorem | islly 21081* | The property of being a locally 𝐴 topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ (𝐽 ∈ Locally 𝐴 ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝐽 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝐽 ↾t 𝑢) ∈ 𝐴))) | ||
Theorem | isnlly 21082* | The property of being an n-locally 𝐴 topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ (𝐽 ∈ 𝑛-Locally 𝐴 ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝐽)‘{𝑦}) ∩ 𝒫 𝑥)(𝐽 ↾t 𝑢) ∈ 𝐴)) | ||
Theorem | llyeq 21083 | Equality theorem for the Locally 𝐴 predicate. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ (𝐴 = 𝐵 → Locally 𝐴 = Locally 𝐵) | ||
Theorem | nllyeq 21084 | Equality theorem for the Locally 𝐴 predicate. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ (𝐴 = 𝐵 → 𝑛-Locally 𝐴 = 𝑛-Locally 𝐵) | ||
Theorem | llytop 21085 | A locally 𝐴 space is a topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ (𝐽 ∈ Locally 𝐴 → 𝐽 ∈ Top) | ||
Theorem | nllytop 21086 | A locally 𝐴 space is a topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ (𝐽 ∈ 𝑛-Locally 𝐴 → 𝐽 ∈ Top) | ||
Theorem | llyi 21087* | The property of a locally 𝐴 topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ ((𝐽 ∈ Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) → ∃𝑢 ∈ 𝐽 (𝑢 ⊆ 𝑈 ∧ 𝑃 ∈ 𝑢 ∧ (𝐽 ↾t 𝑢) ∈ 𝐴)) | ||
Theorem | nllyi 21088* | The property of an n-locally 𝐴 topological space. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ ((𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑃})(𝑢 ⊆ 𝑈 ∧ (𝐽 ↾t 𝑢) ∈ 𝐴)) | ||
Theorem | nlly2i 21089* | Eliminate the neighborhood symbol from nllyi 21088. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ ((𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) → ∃𝑠 ∈ 𝒫 𝑈∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ 𝐴)) | ||
Theorem | llynlly 21090 | A locally 𝐴 space is n-locally 𝐴: the "n-locally" predicate is the weaker notion. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ (𝐽 ∈ Locally 𝐴 → 𝐽 ∈ 𝑛-Locally 𝐴) | ||
Theorem | llyssnlly 21091 | A locally 𝐴 space is n-locally 𝐴. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ Locally 𝐴 ⊆ 𝑛-Locally 𝐴 | ||
Theorem | llyss 21092 | The "locally" predicate respects inclusion. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ (𝐴 ⊆ 𝐵 → Locally 𝐴 ⊆ Locally 𝐵) | ||
Theorem | nllyss 21093 | The "n-locally" predicate respects inclusion. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ (𝐴 ⊆ 𝐵 → 𝑛-Locally 𝐴 ⊆ 𝑛-Locally 𝐵) | ||
Theorem | subislly 21094* | The property of a subspace being locally 𝐴. (Contributed by Mario Carneiro, 10-Mar-2015.) |
⊢ ((𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉) → ((𝐽 ↾t 𝐵) ∈ Locally 𝐴 ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ (𝑥 ∩ 𝐵)∃𝑢 ∈ 𝐽 ((𝑢 ∩ 𝐵) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝐽 ↾t (𝑢 ∩ 𝐵)) ∈ 𝐴))) | ||
Theorem | restnlly 21095* | If the property 𝐴 passes to open subspaces, then a space is n-locally 𝐴 iff it is locally 𝐴. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑥 ∈ 𝑗)) → (𝑗 ↾t 𝑥) ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝑛-Locally 𝐴 = Locally 𝐴) | ||
Theorem | restlly 21096* | If the property 𝐴 passes to open subspaces, then a space which is 𝐴 is also locally 𝐴. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑥 ∈ 𝑗)) → (𝑗 ↾t 𝑥) ∈ 𝐴) & ⊢ (𝜑 → 𝐴 ⊆ Top) ⇒ ⊢ (𝜑 → 𝐴 ⊆ Locally 𝐴) | ||
Theorem | islly2 21097* | An alternative expression for 𝐽 ∈ Locally 𝐴 when 𝐴 passes to open subspaces: A space is locally 𝐴 if every point is contained in an open neighborhood with property 𝐴. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑥 ∈ 𝑗)) → (𝑗 ↾t 𝑥) ∈ 𝐴) & ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝜑 → (𝐽 ∈ Locally 𝐴 ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝑋 ∃𝑢 ∈ 𝐽 (𝑦 ∈ 𝑢 ∧ (𝐽 ↾t 𝑢) ∈ 𝐴)))) | ||
Theorem | llyrest 21098 | An open subspace of a locally 𝐴 space is also locally 𝐴. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ ((𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽) → (𝐽 ↾t 𝐵) ∈ Locally 𝐴) | ||
Theorem | nllyrest 21099 | An open subspace of an n-locally 𝐴 space is also n-locally 𝐴. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ ((𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽) → (𝐽 ↾t 𝐵) ∈ 𝑛-Locally 𝐴) | ||
Theorem | loclly 21100 | If 𝐴 is a local property, then both Locally 𝐴 and 𝑛-Locally 𝐴 simplify to 𝐴. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ (Locally 𝐴 = 𝐴 ↔ 𝑛-Locally 𝐴 = 𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |