Home | Metamath
Proof Explorer Theorem List (p. 218 of 450) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28697) |
Hilbert Space Explorer
(28698-30220) |
Users' Mathboxes
(30221-44913) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | indiscld 21701 | The closed sets of an indiscrete topology. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 14-Aug-2015.) |
⊢ (Clsd‘{∅, 𝐴}) = {∅, 𝐴} | ||
Theorem | mretopd 21702* | 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 21703 | 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 21605. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by Mario Carneiro, 5-May-2015.) |
⊢ (𝐵 ∈ 𝑉 → (TopOn‘𝐵) ∈ (Moore‘𝒫 𝐵)) | ||
Theorem | cldmreon 21704 | 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 21705* | 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 21706 | The closed subspaces of a topology-bearing module form a complete lattice. Demonstration for mreclatBAD 17799. (Contributed by Stefan O'Rear, 31-Jan-2015.) TODO (df-riota 7116 update): This proof uses the old df-clat 17720 and references the required instance of mreclatBAD 17799 as a hypothesis. When mreclatBAD 17799 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 21707 | Extend class notation with neighborhood relation for topologies. |
class nei | ||
Definition | df-nei 21708* | 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 21709* | Value of the neighborhood function on the subsets of the base set of a topology. (Contributed by NM, 11-Feb-2007.) (Revised by Mario Carneiro, 11-Nov-2013.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (nei‘𝐽) = (𝑥 ∈ 𝒫 𝑋 ↦ {𝑣 ∈ 𝒫 𝑋 ∣ ∃𝑔 ∈ 𝐽 (𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣)})) | ||
Theorem | neif 21710 | The neighborhood function is a function from the set of the subsets of the base set of a topology. (Contributed by NM, 12-Feb-2007.) (Revised by Mario Carneiro, 11-Nov-2013.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (nei‘𝐽) Fn 𝒫 𝑋) | ||
Theorem | neiss2 21711 | A set with a neighborhood is a subset of the base set of a topology. (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 21712* | Value of 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 21713* | The predicate "the class 𝑁 is a neighborhood of 𝑆". (Contributed by FL, 25-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑁 ∈ ((nei‘𝐽)‘𝑆) ↔ (𝑁 ⊆ 𝑋 ∧ ∃𝑔 ∈ 𝐽 (𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁)))) | ||
Theorem | neiint 21714 | 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 21715* | The predicate "the class 𝑁 is a neighborhood of point 𝑃". (Contributed by NM, 26-Feb-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) ↔ (𝑁 ⊆ 𝑋 ∧ ∃𝑔 ∈ 𝐽 (𝑃 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁)))) | ||
Theorem | neii1 21716 | A neighborhood is included in the topology's base set. (Contributed by NM, 12-Feb-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) → 𝑁 ⊆ 𝑋) | ||
Theorem | neisspw 21717 | The neighborhoods of any set are subsets of the base set. (Contributed by Stefan O'Rear, 6-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → ((nei‘𝐽)‘𝑆) ⊆ 𝒫 𝑋) | ||
Theorem | neii2 21718* | Property of a neighborhood. (Contributed by NM, 12-Feb-2007.) |
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) → ∃𝑔 ∈ 𝐽 (𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁)) | ||
Theorem | neiss 21719 | Any neighborhood of a set 𝑆 is also a neighborhood of any subset 𝑅 ⊆ 𝑆. Similar to Proposition 1 of [BourbakiTop1] p. I.2. (Contributed by FL, 25-Sep-2006.) |
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆) ∧ 𝑅 ⊆ 𝑆) → 𝑁 ∈ ((nei‘𝐽)‘𝑅)) | ||
Theorem | ssnei 21720 | A set is included in any of its neighborhoods. Generalization to subsets of elnei 21721. (Contributed by FL, 16-Nov-2006.) |
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) → 𝑆 ⊆ 𝑁) | ||
Theorem | elnei 21721 | A point belongs to any of its neighborhoods. Property Viii of [BourbakiTop1] p. I.3. (Contributed by FL, 28-Sep-2006.) |
⊢ ((𝐽 ∈ Top ∧ 𝑃 ∈ 𝐴 ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑃 ∈ 𝑁) | ||
Theorem | 0nnei 21722 | The empty set is not a neighborhood of a nonempty set. (Contributed by FL, 18-Sep-2007.) |
⊢ ((𝐽 ∈ Top ∧ 𝑆 ≠ ∅) → ¬ ∅ ∈ ((nei‘𝐽)‘𝑆)) | ||
Theorem | neips 21723* | A neighborhood of a set is a neighborhood of every point in the set. Proposition 1 of [BourbakiTop1] p. I.2. (Contributed by FL, 16-Nov-2006.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → (𝑁 ∈ ((nei‘𝐽)‘𝑆) ↔ ∀𝑝 ∈ 𝑆 𝑁 ∈ ((nei‘𝐽)‘{𝑝}))) | ||
Theorem | opnneissb 21724 | An open set is a neighborhood of any of its subsets. (Contributed by FL, 2-Oct-2006.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑋) → (𝑆 ⊆ 𝑁 ↔ 𝑁 ∈ ((nei‘𝐽)‘𝑆))) | ||
Theorem | opnssneib 21725 | Any superset of an open set is a neighborhood of it. (Contributed by NM, 14-Feb-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽 ∧ 𝑁 ⊆ 𝑋) → (𝑆 ⊆ 𝑁 ↔ 𝑁 ∈ ((nei‘𝐽)‘𝑆))) | ||
Theorem | ssnei2 21726 | Any subset 𝑀 of 𝑋 containing a neighborhood 𝑁 of a set 𝑆 is a neighborhood of this set. Generalization to subsets of Property Vi of [BourbakiTop1] p. I.3. (Contributed by FL, 2-Oct-2006.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) ∧ (𝑁 ⊆ 𝑀 ∧ 𝑀 ⊆ 𝑋)) → 𝑀 ∈ ((nei‘𝐽)‘𝑆)) | ||
Theorem | neindisj 21727 | 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 21728 | An open set is a neighborhood of any of its subsets. (Contributed by NM, 13-Feb-2007.) |
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘𝑆)) | ||
Theorem | opnneip 21729 | An open set is a neighborhood of any of its members. (Contributed by NM, 8-Mar-2007.) |
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑃 ∈ 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) | ||
Theorem | opnnei 21730* | 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 21731 | The underlying set of a topology is a neighborhood of any of its subsets. Special case of opnneiss 21728. (Contributed by FL, 2-Oct-2006.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (𝑆 ⊆ 𝑋 ↔ 𝑋 ∈ ((nei‘𝐽)‘𝑆))) | ||
Theorem | neiuni 21732 | 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 21733* | 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 21734 | A finer topology has more neighborhoods. (Contributed by Mario Carneiro, 9-Apr-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑋 = 𝑌) ∧ 𝐽 ⊆ 𝐾) → ((nei‘𝐽)‘𝑆) ⊆ ((nei‘𝐾)‘𝑆)) | ||
Theorem | innei 21735 | The intersection of two neighborhoods of a set is also a neighborhood of the set. Generalization to subsets of Property Vii of [BourbakiTop1] p. I.3 for binary intersections. (Contributed by FL, 28-Sep-2006.) |
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆) ∧ 𝑀 ∈ ((nei‘𝐽)‘𝑆)) → (𝑁 ∩ 𝑀) ∈ ((nei‘𝐽)‘𝑆)) | ||
Theorem | opnneiid 21736 | Only an open set is a neighborhood of itself. (Contributed by FL, 2-Oct-2006.) |
⊢ (𝐽 ∈ Top → (𝑁 ∈ ((nei‘𝐽)‘𝑁) ↔ 𝑁 ∈ 𝐽)) | ||
Theorem | neissex 21737* | For any neighborhood 𝑁 of 𝑆, there is a neighborhood 𝑥 of 𝑆 such that 𝑁 is a neighborhood of all subsets of 𝑥. Generalization to subsets of Property Viv of [BourbakiTop1] p. I.3. (Contributed by FL, 2-Oct-2006.) |
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) → ∃𝑥 ∈ ((nei‘𝐽)‘𝑆)∀𝑦(𝑦 ⊆ 𝑥 → 𝑁 ∈ ((nei‘𝐽)‘𝑦))) | ||
Theorem | 0nei 21738 | The empty set is a neighborhood of itself. (Contributed by FL, 10-Dec-2006.) |
⊢ (𝐽 ∈ Top → ∅ ∈ ((nei‘𝐽)‘∅)) | ||
Theorem | neipeltop 21739* | Lemma for neiptopreu 21743. (Contributed by Thierry Arnoux, 6-Jan-2018.) |
⊢ 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} ⇒ ⊢ (𝐶 ∈ 𝐽 ↔ (𝐶 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝐶 𝐶 ∈ (𝑁‘𝑝))) | ||
Theorem | neiptopuni 21740* | Lemma for neiptopreu 21743. (Contributed by Thierry Arnoux, 6-Jan-2018.) |
⊢ 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} & ⊢ (𝜑 → 𝑁:𝑋⟶𝒫 𝒫 𝑋) & ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) & ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝)) & ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎) & ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞)) & ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝)) ⇒ ⊢ (𝜑 → 𝑋 = ∪ 𝐽) | ||
Theorem | neiptoptop 21741* | Lemma for neiptopreu 21743. (Contributed by Thierry Arnoux, 7-Jan-2018.) |
⊢ 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} & ⊢ (𝜑 → 𝑁:𝑋⟶𝒫 𝒫 𝑋) & ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) & ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝)) & ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎) & ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞)) & ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝)) ⇒ ⊢ (𝜑 → 𝐽 ∈ Top) | ||
Theorem | neiptopnei 21742* | Lemma for neiptopreu 21743. (Contributed by Thierry Arnoux, 7-Jan-2018.) |
⊢ 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} & ⊢ (𝜑 → 𝑁:𝑋⟶𝒫 𝒫 𝑋) & ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) & ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝)) & ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎) & ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞)) & ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝)) ⇒ ⊢ (𝜑 → 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝐽)‘{𝑝}))) | ||
Theorem | neiptopreu 21743* | If, to each element 𝑃 of a set 𝑋, we associate a set (𝑁‘𝑃) fulfilling Properties Vi, Vii, Viii and Property Viv of [BourbakiTop1] p. I.2. , corresponding to ssnei 21720, innei 21735, elnei 21721 and neissex 21737, 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 innei 21735 uses binary intersections whereas Property Vii mentions finite intersections (which includes the empty intersection of subsets of 𝑋, which is equal to 𝑋), so we add the hypothesis that 𝑋 is a neighborhood of all points. TODO: when df-fi 8877 includes the empty intersection, remove that extra hypothesis. (Contributed by Thierry Arnoux, 6-Jan-2018.) |
⊢ 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} & ⊢ (𝜑 → 𝑁:𝑋⟶𝒫 𝒫 𝑋) & ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) & ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝)) & ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎) & ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞)) & ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝)) ⇒ ⊢ (𝜑 → ∃!𝑗 ∈ (TopOn‘𝑋)𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝}))) | ||
Syntax | clp 21744 | Extend class notation with the limit point function for topologies. |
class limPt | ||
Syntax | cperf 21745 | Extend class notation with the class of all perfect spaces. |
class Perf | ||
Definition | df-lp 21746* | Define a function on topologies whose value is the set of limit points of the subsets of the base set. See lpval 21749. (Contributed by NM, 10-Feb-2007.) |
⊢ limPt = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ {𝑦 ∣ 𝑦 ∈ ((cls‘𝑗)‘(𝑥 ∖ {𝑦}))})) | ||
Definition | df-perf 21747 | 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 21748* | 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 21749* | 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 21750 | The predicate "the class 𝑃 is a limit point of 𝑆". (Contributed by NM, 10-Feb-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((limPt‘𝐽)‘𝑆) ↔ 𝑃 ∈ ((cls‘𝐽)‘(𝑆 ∖ {𝑃})))) | ||
Theorem | lpsscls 21751 | The limit points of a subset are included in the subset's closure. (Contributed by NM, 26-Feb-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((limPt‘𝐽)‘𝑆) ⊆ ((cls‘𝐽)‘𝑆)) | ||
Theorem | lpss 21752 | The limit points of a subset are included in the base set. (Contributed by NM, 9-Nov-2007.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((limPt‘𝐽)‘𝑆) ⊆ 𝑋) | ||
Theorem | lpdifsn 21753 | 𝑃 is a limit point of 𝑆 iff it is a limit point of 𝑆 ∖ {𝑃}. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((limPt‘𝐽)‘𝑆) ↔ 𝑃 ∈ ((limPt‘𝐽)‘(𝑆 ∖ {𝑃})))) | ||
Theorem | lpss3 21754 | Subset relationship for limit points. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆) → ((limPt‘𝐽)‘𝑇) ⊆ ((limPt‘𝐽)‘𝑆)) | ||
Theorem | islp2 21755* | 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 21756* | The predicate "𝑃 is a limit point of 𝑆 " in terms of open sets. see islp2 21755, elcls 21683, islp 21750. (Contributed by FL, 31-Jul-2009.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑃 ∈ ((limPt‘𝐽)‘𝑆) ↔ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → (𝑥 ∩ (𝑆 ∖ {𝑃})) ≠ ∅))) | ||
Theorem | maxlp 21757 | 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 21758 | 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 21759 | 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 21760 | 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 21761 | Definition of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Perf ↔ (𝐽 ∈ Top ∧ ((limPt‘𝐽)‘𝑋) = 𝑋)) | ||
Theorem | isperf2 21762 | Definition of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Perf ↔ (𝐽 ∈ Top ∧ 𝑋 ⊆ ((limPt‘𝐽)‘𝑋))) | ||
Theorem | isperf3 21763* | A perfect space is a topology which has no open singletons. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Perf ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝑋 ¬ {𝑥} ∈ 𝐽)) | ||
Theorem | perflp 21764 | The limit points of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Perf → ((limPt‘𝐽)‘𝑋) = 𝑋) | ||
Theorem | perfi 21765 | Property of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Perf ∧ 𝑃 ∈ 𝑋) → ¬ {𝑃} ∈ 𝐽) | ||
Theorem | perftop 21766 | A perfect space is a topology. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ (𝐽 ∈ Perf → 𝐽 ∈ Top) | ||
Theorem | restrcl 21767 | 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 21768 | A subspace topology basis is a basis. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ (𝐵 ∈ TopBases → (𝐵 ↾t 𝐴) ∈ TopBases) | ||
Theorem | tgrest 21769 | 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 21770 | 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 21771 | A subspace topology is a topology on the base set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴)) | ||
Theorem | restuni 21772 | The underlying set of a subspace topology. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 13-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → 𝐴 = ∪ (𝐽 ↾t 𝐴)) | ||
Theorem | stoig 21773 | 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 21774 | Composition of subspaces. (Contributed by Mario Carneiro, 15-Dec-2013.) (Revised by Mario Carneiro, 1-May-2015.) |
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → ((𝐽 ↾t 𝐴) ↾t 𝐵) = (𝐽 ↾t (𝐴 ∩ 𝐵))) | ||
Theorem | restabs 21775 | 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 21776 | 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 21777 | The underlying set of a subspace topology. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝐴 ∩ 𝑋) = ∪ (𝐽 ↾t 𝐴)) | ||
Theorem | resttopon2 21778 | The underlying set of a subspace topology. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ (TopOn‘(𝐴 ∩ 𝑋))) | ||
Theorem | rest0 21779 | 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 21780 | The only subspace topology induced by the topology {∅}. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) |
⊢ (𝐴 ∈ 𝑉 → ({∅} ↾t 𝐴) = {∅}) | ||
Theorem | restsn2 21781 | The subspace topology induced by a singleton. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 16-Sep-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐽 ↾t {𝐴}) = 𝒫 {𝐴}) | ||
Theorem | restcld 21782* | 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 21783 | A closed set is closed in the subspace topology. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝐵 ∈ (Clsd‘𝐽) ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ (Clsd‘(𝐽 ↾t 𝐴))) | ||
Theorem | restcldr 21784 | 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 21785 | 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 21786 | 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 21787 | 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 21788 | A subspace of a discrete topology is discrete. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → (𝒫 𝐴 ↾t 𝐵) = 𝒫 𝐵) | ||
Theorem | restfpw 21789 | 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 21790 | 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 21791 | 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 21792 | An interior in a subspace topology. Willard in General Topology says that there is no analogue of restcls 21791 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 21793 | The limit points of a subset restrict naturally in a subspace. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (𝐽 ↾t 𝑌) ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → ((limPt‘𝐾)‘𝑆) = (((limPt‘𝐽)‘𝑆) ∩ 𝑌)) | ||
Theorem | restperf 21794 | 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 21795 | An open subset of a perfect space is perfect. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (𝐽 ↾t 𝑌) ⇒ ⊢ ((𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽) → 𝐾 ∈ Perf) | ||
Theorem | resstopn 21796 | The topology of a restricted structure. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝐻 = (𝐾 ↾s 𝐴) & ⊢ 𝐽 = (TopOpen‘𝐾) ⇒ ⊢ (𝐽 ↾t 𝐴) = (TopOpen‘𝐻) | ||
Theorem | resstps 21797 | A restricted topological space is a topological space. Note that this theorem would not be true if TopSp was defined directly in terms of the TopSet slot instead of the TopOpen derived function. (Contributed by Mario Carneiro, 13-Aug-2015.) |
⊢ ((𝐾 ∈ TopSp ∧ 𝐴 ∈ 𝑉) → (𝐾 ↾s 𝐴) ∈ TopSp) | ||
Theorem | ordtbaslem 21798* | Lemma for ordtbas 21802. In a total order, unbounded-above intervals are closed under intersection. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 & ⊢ 𝐴 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) ⇒ ⊢ (𝑅 ∈ TosetRel → (fi‘𝐴) = 𝐴) | ||
Theorem | ordtval 21799* | Value of the order topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 & ⊢ 𝐴 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) & ⊢ 𝐵 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}) ⇒ ⊢ (𝑅 ∈ 𝑉 → (ordTop‘𝑅) = (topGen‘(fi‘({𝑋} ∪ (𝐴 ∪ 𝐵))))) | ||
Theorem | ordtuni 21800* | Value of the order topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 & ⊢ 𝐴 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥}) & ⊢ 𝐵 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦}) ⇒ ⊢ (𝑅 ∈ 𝑉 → 𝑋 = ∪ ({𝑋} ∪ (𝐴 ∪ 𝐵))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |