Home | Metamath
Proof Explorer Theorem List (p. 208 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 | isclo 20701* | A set 𝐴 is clopen iff for every point 𝑥 in the space there is a neighborhood 𝑦 such that all the points in 𝑦 are in 𝐴 iff 𝑥 is. (Contributed by Mario Carneiro, 10-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (𝐴 ∈ (𝐽 ∩ (Clsd‘𝐽)) ↔ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)))) | ||
Theorem | isclo2 20702* | A set 𝐴 is clopen iff for every point 𝑥 in the space there is a neighborhood 𝑦 of 𝑥 which is either disjoint from 𝐴 or contained in 𝐴. (Contributed by Mario Carneiro, 7-Jul-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (𝐴 ∈ (𝐽 ∩ (Clsd‘𝐽)) ↔ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ∈ 𝐴 → 𝑦 ⊆ 𝐴)))) | ||
Theorem | discld 20703 | The open sets of a discrete topology are closed and its closed sets are open. (Contributed by FL, 7-Jun-2007.) (Revised by Mario Carneiro, 7-Apr-2015.) |
⊢ (𝐴 ∈ 𝑉 → (Clsd‘𝒫 𝐴) = 𝒫 𝐴) | ||
Theorem | sn0cld 20704 | The closed sets of the topology {∅}. (Contributed by FL, 5-Jan-2009.) |
⊢ (Clsd‘{∅}) = {∅} | ||
Theorem | indiscld 20705 | The closed sets of an indiscrete topology. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 14-Aug-2015.) |
⊢ (Clsd‘{∅, 𝐴}) = {∅, 𝐴} | ||
Theorem | mretopd 20706* | A Moore collection which is closed under finite unions called topological; such a collection is the closed sets of a canonically associated topology. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ (𝜑 → 𝑀 ∈ (Moore‘𝐵)) & ⊢ (𝜑 → ∅ ∈ 𝑀) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀) → (𝑥 ∪ 𝑦) ∈ 𝑀) & ⊢ 𝐽 = {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ 𝑀} ⇒ ⊢ (𝜑 → (𝐽 ∈ (TopOn‘𝐵) ∧ 𝑀 = (Clsd‘𝐽))) | ||
Theorem | toponmre 20707 | The topologies over a given base set form a Moore collection: the intersection of any family of them is a topology, including the empty (relative) intersection which gives the discrete topology distop 20610. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by Mario Carneiro, 5-May-2015.) |
⊢ (𝐵 ∈ 𝑉 → (TopOn‘𝐵) ∈ (Moore‘𝒫 𝐵)) | ||
Theorem | cldmreon 20708 | The closed sets of a topology over a set are a Moore collection over the same set. (Contributed by Stefan O'Rear, 31-Jan-2015.) |
⊢ (𝐽 ∈ (TopOn‘𝐵) → (Clsd‘𝐽) ∈ (Moore‘𝐵)) | ||
Theorem | iscldtop 20709* | A family is the closed sets of a topology iff it is a Moore collection and closed under finite union. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
⊢ (𝐾 ∈ (Clsd “ (TopOn‘𝐵)) ↔ (𝐾 ∈ (Moore‘𝐵) ∧ ∅ ∈ 𝐾 ∧ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝐾 (𝑥 ∪ 𝑦) ∈ 𝐾)) | ||
Theorem | mreclatdemoBAD 20710 | The closed subspaces of a topology-bearing module form a complete lattice. Demonstration for mreclatBAD 17010. (Contributed by Stefan O'Rear, 31-Jan-2015.) TODO (df-riota 6511 update): This proof uses the old df-clat 16931 and references the required instance of mreclatBAD 17010 as a hypothesis. When mreclatBAD 17010 is corrected to become mreclat, delete this theorem and uncomment the mreclatdemo below. |
⊢ (((LSubSp‘𝑊) ∩ (Clsd‘(TopOpen‘𝑊))) ∈ (Moore‘∪ (TopOpen‘𝑊)) → (toInc‘((LSubSp‘𝑊) ∩ (Clsd‘(TopOpen‘𝑊)))) ∈ CLat) ⇒ ⊢ (𝑊 ∈ (TopSp ∩ LMod) → (toInc‘((LSubSp‘𝑊) ∩ (Clsd‘(TopOpen‘𝑊)))) ∈ CLat) | ||
Syntax | cnei 20711 | Extend class notation with neighborhood relation for topologies. |
class nei | ||
Definition | df-nei 20712* | Define a function on topologies whose value is a map from a subset to its neighborhoods. (Contributed by NM, 11-Feb-2007.) |
⊢ nei = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ {𝑦 ∈ 𝒫 ∪ 𝑗 ∣ ∃𝑔 ∈ 𝑗 (𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦)})) | ||
Theorem | neifval 20713* | The neighborhood function on the subsets of a topology's base set. (Contributed by NM, 11-Feb-2007.) (Revised by Mario Carneiro, 11-Nov-2013.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (nei‘𝐽) = (𝑥 ∈ 𝒫 𝑋 ↦ {𝑣 ∈ 𝒫 𝑋 ∣ ∃𝑔 ∈ 𝐽 (𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣)})) | ||
Theorem | neif 20714 | The neighborhood function is a function of the subsets of a topology's base set. (Contributed by NM, 12-Feb-2007.) (Revised by Mario Carneiro, 11-Nov-2013.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (nei‘𝐽) Fn 𝒫 𝑋) | ||
Theorem | neiss2 20715 | A set with a neighborhood is a subset of the topology's base set. (This theorem depends on a function's value being empty outside of its domain, but it will make later theorems simpler to state.) (Contributed by NM, 12-Feb-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) → 𝑆 ⊆ 𝑋) | ||
Theorem | neival 20716* | The set of neighborhoods of a subset of the base set of a topology. (Contributed by NM, 11-Feb-2007.) (Revised by Mario Carneiro, 11-Nov-2013.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((nei‘𝐽)‘𝑆) = {𝑣 ∈ 𝒫 𝑋 ∣ ∃𝑔 ∈ 𝐽 (𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣)}) | ||
Theorem | isnei 20717* | The predicate "𝑁 is a neighborhood of 𝑆." (Contributed by FL, 25-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑁 ∈ ((nei‘𝐽)‘𝑆) ↔ (𝑁 ⊆ 𝑋 ∧ ∃𝑔 ∈ 𝐽 (𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁)))) | ||
Theorem | neiint 20718 | An intuitive definition of a neighborhood in terms of interior. (Contributed by Szymon Jaroszewicz, 18-Dec-2007.) (Revised by Mario Carneiro, 11-Nov-2013.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑁 ⊆ 𝑋) → (𝑁 ∈ ((nei‘𝐽)‘𝑆) ↔ 𝑆 ⊆ ((int‘𝐽)‘𝑁))) | ||
Theorem | isneip 20719* | The predicate "𝑁 is a neighborhood of point 𝑃." (Contributed by NM, 26-Feb-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) ↔ (𝑁 ⊆ 𝑋 ∧ ∃𝑔 ∈ 𝐽 (𝑃 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁)))) | ||
Theorem | neii1 20720 | A neighborhood is included in the topology's base set. (Contributed by NM, 12-Feb-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) → 𝑁 ⊆ 𝑋) | ||
Theorem | neisspw 20721 | The neighborhoods of any set are subsets of the base set. (Contributed by Stefan O'Rear, 6-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → ((nei‘𝐽)‘𝑆) ⊆ 𝒫 𝑋) | ||
Theorem | neii2 20722* | Property of a neighborhood. (Contributed by NM, 12-Feb-2007.) |
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) → ∃𝑔 ∈ 𝐽 (𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁)) | ||
Theorem | neiss 20723 | Any neighborhood of a set 𝑆 is also a neighborhood of any subset 𝑅 ⊆ 𝑆. Theorem of [BourbakiTop1] p. I.2. (Contributed by FL, 25-Sep-2006.) |
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆) ∧ 𝑅 ⊆ 𝑆) → 𝑁 ∈ ((nei‘𝐽)‘𝑅)) | ||
Theorem | ssnei 20724 | A set is included in its neighborhoods. Proposition Viii of [BourbakiTop1] p. I.3 . (Contributed by FL, 16-Nov-2006.) |
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) → 𝑆 ⊆ 𝑁) | ||
Theorem | elnei 20725 | A point belongs to any of its neighborhoods. Proposition Viii of [BourbakiTop1] p. I.3. (Contributed by FL, 28-Sep-2006.) |
⊢ ((𝐽 ∈ Top ∧ 𝑃 ∈ 𝐴 ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑃 ∈ 𝑁) | ||
Theorem | 0nnei 20726 | The empty set is not a neighborhood of a nonempty set. (Contributed by FL, 18-Sep-2007.) |
⊢ ((𝐽 ∈ Top ∧ 𝑆 ≠ ∅) → ¬ ∅ ∈ ((nei‘𝐽)‘𝑆)) | ||
Theorem | neips 20727* | A neighborhood of a set is a neighborhood of every point in the set. Proposition of [BourbakiTop1] p. I.2. (Contributed by FL, 16-Nov-2006.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → (𝑁 ∈ ((nei‘𝐽)‘𝑆) ↔ ∀𝑝 ∈ 𝑆 𝑁 ∈ ((nei‘𝐽)‘{𝑝}))) | ||
Theorem | opnneissb 20728 | An open set is a neighborhood of any of its subsets. (Contributed by FL, 2-Oct-2006.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑋) → (𝑆 ⊆ 𝑁 ↔ 𝑁 ∈ ((nei‘𝐽)‘𝑆))) | ||
Theorem | opnssneib 20729 | Any superset of an open set is a neighborhood of it. (Contributed by NM, 14-Feb-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽 ∧ 𝑁 ⊆ 𝑋) → (𝑆 ⊆ 𝑁 ↔ 𝑁 ∈ ((nei‘𝐽)‘𝑆))) | ||
Theorem | ssnei2 20730 | Any subset of 𝑋 containing a neighborhood of a set is a neighborhood of this set. Proposition Vi of [BourbakiTop1] p. I.3. (Contributed by FL, 2-Oct-2006.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) ∧ (𝑁 ⊆ 𝑀 ∧ 𝑀 ⊆ 𝑋)) → 𝑀 ∈ ((nei‘𝐽)‘𝑆)) | ||
Theorem | neindisj 20731 | Any neighborhood of an element in the closure of a subset intersects the subset. Part of proof of Theorem 6.6 of [Munkres] p. 97. (Contributed by NM, 26-Feb-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ (𝑃 ∈ ((cls‘𝐽)‘𝑆) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃}))) → (𝑁 ∩ 𝑆) ≠ ∅) | ||
Theorem | opnneiss 20732 | An open set is a neighborhood of any of its subsets. (Contributed by NM, 13-Feb-2007.) |
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘𝑆)) | ||
Theorem | opnneip 20733 | An open set is a neighborhood of any of its members. (Contributed by NM, 8-Mar-2007.) |
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑃 ∈ 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) | ||
Theorem | opnnei 20734* | A set is open iff it is a neighborhood of all of its points. (Contributed by Jeff Hankins, 15-Sep-2009.) |
⊢ (𝐽 ∈ Top → (𝑆 ∈ 𝐽 ↔ ∀𝑥 ∈ 𝑆 𝑆 ∈ ((nei‘𝐽)‘{𝑥}))) | ||
Theorem | tpnei 20735 | The underlying set of a topology is a neighborhood of any of its subsets. Special case of opnneiss 20732. (Contributed by FL, 2-Oct-2006.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (𝑆 ⊆ 𝑋 ↔ 𝑋 ∈ ((nei‘𝐽)‘𝑆))) | ||
Theorem | neiuni 20736 | The union of the neighborhoods of a set equals the topology's underlying set. (Contributed by FL, 18-Sep-2007.) (Revised by Mario Carneiro, 9-Apr-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑋 = ∪ ((nei‘𝐽)‘𝑆)) | ||
Theorem | neindisj2 20737* | A point 𝑃 belongs to the closure of a set 𝑆 iff every neighborhood of 𝑃 meets 𝑆. (Contributed by FL, 15-Sep-2013.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ∀𝑛 ∈ ((nei‘𝐽)‘{𝑃})(𝑛 ∩ 𝑆) ≠ ∅)) | ||
Theorem | topssnei 20738 | A finer topology has more neighborhoods. (Contributed by Mario Carneiro, 9-Apr-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑋 = 𝑌) ∧ 𝐽 ⊆ 𝐾) → ((nei‘𝐽)‘𝑆) ⊆ ((nei‘𝐾)‘𝑆)) | ||
Theorem | innei 20739 | The intersection of two neighborhoods of a set is also a neighborhood of the set. Proposition Vii of [BourbakiTop1] p. I.3 . (Contributed by FL, 28-Sep-2006.) |
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆) ∧ 𝑀 ∈ ((nei‘𝐽)‘𝑆)) → (𝑁 ∩ 𝑀) ∈ ((nei‘𝐽)‘𝑆)) | ||
Theorem | opnneiid 20740 | Only an open set is a neighborhood of itself. (Contributed by FL, 2-Oct-2006.) |
⊢ (𝐽 ∈ Top → (𝑁 ∈ ((nei‘𝐽)‘𝑁) ↔ 𝑁 ∈ 𝐽)) | ||
Theorem | neissex 20741* | For any neighborhood 𝑁 of 𝑆, there is a neighborhood 𝑥 of 𝑆 such that 𝑁 is a neighborhood of all subsets of 𝑥. Proposition Viv of [BourbakiTop1] p. I.3 . (Contributed by FL, 2-Oct-2006.) |
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) → ∃𝑥 ∈ ((nei‘𝐽)‘𝑆)∀𝑦(𝑦 ⊆ 𝑥 → 𝑁 ∈ ((nei‘𝐽)‘𝑦))) | ||
Theorem | 0nei 20742 | The empty set is a neighborhood of itself. (Contributed by FL, 10-Dec-2006.) |
⊢ (𝐽 ∈ Top → ∅ ∈ ((nei‘𝐽)‘∅)) | ||
Theorem | neipeltop 20743* | Lemma for neiptopreu 20747. (Contributed by Thierry Arnoux, 6-Jan-2018.) |
⊢ 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} ⇒ ⊢ (𝐶 ∈ 𝐽 ↔ (𝐶 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝐶 𝐶 ∈ (𝑁‘𝑝))) | ||
Theorem | neiptopuni 20744* | Lemma for neiptopreu 20747. (Contributed by Thierry Arnoux, 6-Jan-2018.) |
⊢ 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} & ⊢ (𝜑 → 𝑁:𝑋⟶𝒫 𝒫 𝑋) & ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) & ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝)) & ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎) & ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞)) & ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝)) ⇒ ⊢ (𝜑 → 𝑋 = ∪ 𝐽) | ||
Theorem | neiptoptop 20745* | Lemma for neiptopreu 20747. (Contributed by Thierry Arnoux, 7-Jan-2018.) |
⊢ 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} & ⊢ (𝜑 → 𝑁:𝑋⟶𝒫 𝒫 𝑋) & ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) & ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝)) & ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎) & ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞)) & ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝)) ⇒ ⊢ (𝜑 → 𝐽 ∈ Top) | ||
Theorem | neiptopnei 20746* | Lemma for neiptopreu 20747. (Contributed by Thierry Arnoux, 7-Jan-2018.) |
⊢ 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} & ⊢ (𝜑 → 𝑁:𝑋⟶𝒫 𝒫 𝑋) & ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) & ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝)) & ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎) & ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞)) & ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝)) ⇒ ⊢ (𝜑 → 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝐽)‘{𝑝}))) | ||
Theorem | neiptopreu 20747* | If, to each element 𝑃 of a set 𝑋, we associate a set (𝑁‘𝑃) fulfilling the properties Vi, Vii, Viii and property Viv of [BourbakiTop1] p. I.2. , corresponding to ssnei 20724, innei 20739, elnei 20725 and neissex 20741, then there is a unique topology 𝑗 such that for any point 𝑝, (𝑁‘𝑝) is the set of neighborhoods of 𝑝. Proposition 2 of [BourbakiTop1] p. I.3. This can be used to build a topology from a set of neighborhoods. Note that the additional condition that 𝑋 is a neighborhood of all points was added. (Contributed by Thierry Arnoux, 6-Jan-2018.) |
⊢ 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} & ⊢ (𝜑 → 𝑁:𝑋⟶𝒫 𝒫 𝑋) & ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) & ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝)) & ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎) & ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞)) & ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝)) ⇒ ⊢ (𝜑 → ∃!𝑗 ∈ (TopOn‘𝑋)𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝}))) | ||
Syntax | clp 20748 | Extend class notation with the limit point function for topologies. |
class limPt | ||
Syntax | cperf 20749 | Extend class notation with the class of all perfect spaces. |
class Perf | ||
Definition | df-lp 20750* | Define a function on topologies whose value is the set of limit points of the subsets of the base set. See lpval 20753. (Contributed by NM, 10-Feb-2007.) |
⊢ limPt = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ {𝑦 ∣ 𝑦 ∈ ((cls‘𝑗)‘(𝑥 ∖ {𝑦}))})) | ||
Definition | df-perf 20751 | Define the class of all perfect spaces. A perfect space is one for which every point in the set is a limit point of the whole space. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ Perf = {𝑗 ∈ Top ∣ ((limPt‘𝑗)‘∪ 𝑗) = ∪ 𝑗} | ||
Theorem | lpfval 20752* | The limit point function on the subsets of a topology's base set. (Contributed by NM, 10-Feb-2007.) (Revised by Mario Carneiro, 11-Nov-2013.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (limPt‘𝐽) = (𝑥 ∈ 𝒫 𝑋 ↦ {𝑦 ∣ 𝑦 ∈ ((cls‘𝐽)‘(𝑥 ∖ {𝑦}))})) | ||
Theorem | lpval 20753* | The set of limit points of a subset of the base set of a topology. Alternate definition of limit point in [Munkres] p. 97. (Contributed by NM, 10-Feb-2007.) (Revised by Mario Carneiro, 11-Nov-2013.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((limPt‘𝐽)‘𝑆) = {𝑥 ∣ 𝑥 ∈ ((cls‘𝐽)‘(𝑆 ∖ {𝑥}))}) | ||
Theorem | islp 20754 | The predicate "𝑃 is a limit point of 𝑆." (Contributed by NM, 10-Feb-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((limPt‘𝐽)‘𝑆) ↔ 𝑃 ∈ ((cls‘𝐽)‘(𝑆 ∖ {𝑃})))) | ||
Theorem | lpsscls 20755 | The limit points of a subset are included in the subset's closure. (Contributed by NM, 26-Feb-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((limPt‘𝐽)‘𝑆) ⊆ ((cls‘𝐽)‘𝑆)) | ||
Theorem | lpss 20756 | The limit points of a subset are included in the base set. (Contributed by NM, 9-Nov-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((limPt‘𝐽)‘𝑆) ⊆ 𝑋) | ||
Theorem | lpdifsn 20757 | 𝑃 is a limit point of 𝑆 iff it is a limit point of 𝑆 ∖ {𝑃}. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((limPt‘𝐽)‘𝑆) ↔ 𝑃 ∈ ((limPt‘𝐽)‘(𝑆 ∖ {𝑃})))) | ||
Theorem | lpss3 20758 | Subset relationship for limit points. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆) → ((limPt‘𝐽)‘𝑇) ⊆ ((limPt‘𝐽)‘𝑆)) | ||
Theorem | islp2 20759* | The predicate "𝑃 is a limit point of 𝑆," in terms of neighborhoods. Definition of limit point in [Munkres] p. 97. Although Munkres uses open neighborhoods, it also works for our more general neighborhoods. (Contributed by NM, 26-Feb-2007.) (Proof shortened by Mario Carneiro, 25-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑃 ∈ ((limPt‘𝐽)‘𝑆) ↔ ∀𝑛 ∈ ((nei‘𝐽)‘{𝑃})(𝑛 ∩ (𝑆 ∖ {𝑃})) ≠ ∅)) | ||
Theorem | islp3 20760* | The predicate "𝑃 is a limit point of 𝑆 " in terms of open sets. see islp2 20759, elcls 20687, islp 20754. (Contributed by FL, 31-Jul-2009.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑃 ∈ ((limPt‘𝐽)‘𝑆) ↔ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → (𝑥 ∩ (𝑆 ∖ {𝑃})) ≠ ∅))) | ||
Theorem | maxlp 20761 | A point is a limit point of the whole space iff the singleton of the point is not open. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (𝑃 ∈ ((limPt‘𝐽)‘𝑋) ↔ (𝑃 ∈ 𝑋 ∧ ¬ {𝑃} ∈ 𝐽))) | ||
Theorem | clslp 20762 | The closure of a subset of a topological space is the subset together with its limit points. Theorem 6.6 of [Munkres] p. 97. (Contributed by NM, 26-Feb-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) = (𝑆 ∪ ((limPt‘𝐽)‘𝑆))) | ||
Theorem | islpi 20763 | A point belonging to a set's closure but not the set itself is a limit point. (Contributed by NM, 8-Nov-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ (𝑃 ∈ ((cls‘𝐽)‘𝑆) ∧ ¬ 𝑃 ∈ 𝑆)) → 𝑃 ∈ ((limPt‘𝐽)‘𝑆)) | ||
Theorem | cldlp 20764 | A subset of a topological space is closed iff it contains all its limit points. Corollary 6.7 of [Munkres] p. 97. (Contributed by NM, 26-Feb-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ (Clsd‘𝐽) ↔ ((limPt‘𝐽)‘𝑆) ⊆ 𝑆)) | ||
Theorem | isperf 20765 | Definition of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Perf ↔ (𝐽 ∈ Top ∧ ((limPt‘𝐽)‘𝑋) = 𝑋)) | ||
Theorem | isperf2 20766 | Definition of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Perf ↔ (𝐽 ∈ Top ∧ 𝑋 ⊆ ((limPt‘𝐽)‘𝑋))) | ||
Theorem | isperf3 20767* | A perfect space is a topology which has no open singletons. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Perf ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝑋 ¬ {𝑥} ∈ 𝐽)) | ||
Theorem | perflp 20768 | The limit points of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Perf → ((limPt‘𝐽)‘𝑋) = 𝑋) | ||
Theorem | perfi 20769 | Property of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Perf ∧ 𝑃 ∈ 𝑋) → ¬ {𝑃} ∈ 𝐽) | ||
Theorem | perftop 20770 | A perfect space is a topology. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ (𝐽 ∈ Perf → 𝐽 ∈ Top) | ||
Theorem | restrcl 20771 | Reverse closure for the subspace topology. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 1-May-2015.) |
⊢ ((𝐽 ↾t 𝐴) ∈ Top → (𝐽 ∈ V ∧ 𝐴 ∈ V)) | ||
Theorem | restbas 20772 | A subspace topology basis is a basis. 𝑌 is normally a subset of the base set of 𝐽. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ (𝐵 ∈ TopBases → (𝐵 ↾t 𝐴) ∈ TopBases) | ||
Theorem | tgrest 20773 | A subspace can be generated by restricted sets from a basis for the original topology. (Contributed by Mario Carneiro, 19-Mar-2015.) (Proof shortened by Mario Carneiro, 30-Aug-2015.) |
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (topGen‘(𝐵 ↾t 𝐴)) = ((topGen‘𝐵) ↾t 𝐴)) | ||
Theorem | resttop 20774 | A subspace topology is a topology. Definition of subspace topology in [Munkres] p. 89. 𝐴 is normally a subset of the base set of 𝐽. (Contributed by FL, 15-Apr-2007.) (Revised by Mario Carneiro, 1-May-2015.) |
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ Top) | ||
Theorem | resttopon 20775 | A subspace topology is a topology on the base set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴)) | ||
Theorem | restuni 20776 | The underlying set of a subspace topology. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 13-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → 𝐴 = ∪ (𝐽 ↾t 𝐴)) | ||
Theorem | stoig 20777 | The topological space built with a subspace topology. (Contributed by FL, 5-Jan-2009.) (Proof shortened by Mario Carneiro, 1-May-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → {〈(Base‘ndx), 𝐴〉, 〈(TopSet‘ndx), (𝐽 ↾t 𝐴)〉} ∈ TopSp) | ||
Theorem | restco 20778 | Composition of subspaces. (Contributed by Mario Carneiro, 15-Dec-2013.) (Revised by Mario Carneiro, 1-May-2015.) |
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → ((𝐽 ↾t 𝐴) ↾t 𝐵) = (𝐽 ↾t (𝐴 ∩ 𝐵))) | ||
Theorem | restabs 20779 | Equivalence of being a subspace of a subspace and being a subspace of the original. (Contributed by Jeff Hankins, 11-Jul-2009.) (Proof shortened by Mario Carneiro, 1-May-2015.) |
⊢ ((𝐽 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑇 ∧ 𝑇 ∈ 𝑊) → ((𝐽 ↾t 𝑇) ↾t 𝑆) = (𝐽 ↾t 𝑆)) | ||
Theorem | restin 20780 | When the subspace region is not a subset of the base of the topology, the resulting set is the same as the subspace restricted to the base. (Contributed by Mario Carneiro, 15-Dec-2013.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝐽 ↾t 𝐴) = (𝐽 ↾t (𝐴 ∩ 𝑋))) | ||
Theorem | restuni2 20781 | The underlying set of a subspace topology. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝐴 ∩ 𝑋) = ∪ (𝐽 ↾t 𝐴)) | ||
Theorem | resttopon2 20782 | The underlying set of a subspace topology. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ (TopOn‘(𝐴 ∩ 𝑋))) | ||
Theorem | rest0 20783 | The subspace topology induced by the topology 𝐽 on the empty set. (Contributed by FL, 22-Dec-2008.) (Revised by Mario Carneiro, 1-May-2015.) |
⊢ (𝐽 ∈ Top → (𝐽 ↾t ∅) = {∅}) | ||
Theorem | restsn 20784 | The only subspace topology induced by the topology {∅}. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) |
⊢ (𝐴 ∈ 𝑉 → ({∅} ↾t 𝐴) = {∅}) | ||
Theorem | restsn2 20785 | The subspace topology induced by a singleton. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 16-Sep-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐽 ↾t {𝐴}) = 𝒫 {𝐴}) | ||
Theorem | restcld 20786* | A closed set of a subspace topology is a closed set of the original topology intersected with the subset. (Contributed by FL, 11-Jul-2009.) (Proof shortened by Mario Carneiro, 15-Dec-2013.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝐴 ∈ (Clsd‘(𝐽 ↾t 𝑆)) ↔ ∃𝑥 ∈ (Clsd‘𝐽)𝐴 = (𝑥 ∩ 𝑆))) | ||
Theorem | restcldi 20787 | A closed set is closed in the subspace topology. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝐵 ∈ (Clsd‘𝐽) ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ (Clsd‘(𝐽 ↾t 𝐴))) | ||
Theorem | restcldr 20788 | A set which is closed in the subspace topology induced by a closed set is closed in the original topology. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝐴 ∈ (Clsd‘𝐽) ∧ 𝐵 ∈ (Clsd‘(𝐽 ↾t 𝐴))) → 𝐵 ∈ (Clsd‘𝐽)) | ||
Theorem | restopnb 20789 | If 𝐵 is an open subset of the subspace base set 𝐴, then any subset of 𝐵 is open iff it is open in 𝐴. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ (((𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝐵 ∈ 𝐽 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐶 ⊆ 𝐵)) → (𝐶 ∈ 𝐽 ↔ 𝐶 ∈ (𝐽 ↾t 𝐴))) | ||
Theorem | ssrest 20790 | If 𝐾 is a finer topology than 𝐽, then the subspace topologies induced by 𝐴 maintain this relationship. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 1-May-2015.) |
⊢ ((𝐾 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐾) → (𝐽 ↾t 𝐴) ⊆ (𝐾 ↾t 𝐴)) | ||
Theorem | restopn2 20791 | The if 𝐴 is open, then 𝐵 is open in 𝐴 iff it is an open subset of 𝐴. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽) → (𝐵 ∈ (𝐽 ↾t 𝐴) ↔ (𝐵 ∈ 𝐽 ∧ 𝐵 ⊆ 𝐴))) | ||
Theorem | restdis 20792 | A subspace of a discrete topology is discrete. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → (𝒫 𝐴 ↾t 𝐵) = 𝒫 𝐵) | ||
Theorem | restfpw 20793 | The restriction of the set of finite subsets of 𝐴 is the set of finite subsets of 𝐵. (Contributed by Mario Carneiro, 18-Sep-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → ((𝒫 𝐴 ∩ Fin) ↾t 𝐵) = (𝒫 𝐵 ∩ Fin)) | ||
Theorem | neitr 20794 | The neighborhood of a trace is the trace of the neighborhood. (Contributed by Thierry Arnoux, 17-Jan-2018.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝐴) → ((nei‘(𝐽 ↾t 𝐴))‘𝐵) = (((nei‘𝐽)‘𝐵) ↾t 𝐴)) | ||
Theorem | restcls 20795 | A closure in a subspace topology. (Contributed by Jeff Hankins, 22-Jan-2010.) (Revised by Mario Carneiro, 15-Dec-2013.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (𝐽 ↾t 𝑌) ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → ((cls‘𝐾)‘𝑆) = (((cls‘𝐽)‘𝑆) ∩ 𝑌)) | ||
Theorem | restntr 20796 | An interior in a subspace topology. Willard in General Topology says that there is no analogue of restcls 20795 for interiors. In some sense, that is true. (Contributed by Jeff Hankins, 23-Jan-2010.) (Revised by Mario Carneiro, 15-Dec-2013.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (𝐽 ↾t 𝑌) ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → ((int‘𝐾)‘𝑆) = (((int‘𝐽)‘(𝑆 ∪ (𝑋 ∖ 𝑌))) ∩ 𝑌)) | ||
Theorem | restlp 20797 | The limit points of a subset restrict naturally in a subspace. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (𝐽 ↾t 𝑌) ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → ((limPt‘𝐾)‘𝑆) = (((limPt‘𝐽)‘𝑆) ∩ 𝑌)) | ||
Theorem | restperf 20798 | Perfection of a subspace. Note that the term "perfect set" is reserved for closed sets which are perfect in the subspace topology. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (𝐽 ↾t 𝑌) ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋) → (𝐾 ∈ Perf ↔ 𝑌 ⊆ ((limPt‘𝐽)‘𝑌))) | ||
Theorem | perfopn 20799 | An open subset of a perfect space is perfect. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (𝐽 ↾t 𝑌) ⇒ ⊢ ((𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽) → 𝐾 ∈ Perf) | ||
Theorem | resstopn 20800 | The topology of a restricted structure. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝐻 = (𝐾 ↾s 𝐴) & ⊢ 𝐽 = (TopOpen‘𝐾) ⇒ ⊢ (𝐽 ↾t 𝐴) = (TopOpen‘𝐻) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |