P. 232 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 23101-23200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	elnei 23101	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 23102	The empty set is not a neighborhood of a nonempty set. (Contributed by FL, 18-Sep-2007.)
⊢ ((𝐽 ∈ Top ∧ 𝑆 ≠ ∅) → ¬ ∅ ∈ ((nei‘𝐽)‘𝑆))
Theorem	neips 23103*	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 23104	An open set is a neighborhood of any of its subsets. (Contributed by FL, 2-Oct-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑋) → (𝑆 ⊆ 𝑁 ↔ 𝑁 ∈ ((nei‘𝐽)‘𝑆)))
Theorem	opnssneib 23105	Any superset of an open set is a neighborhood of it. (Contributed by NM, 14-Feb-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽 ∧ 𝑁 ⊆ 𝑋) → (𝑆 ⊆ 𝑁 ↔ 𝑁 ∈ ((nei‘𝐽)‘𝑆)))
Theorem	ssnei2 23106	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 23107	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 23108	An open set is a neighborhood of any of its subsets. (Contributed by NM, 13-Feb-2007.)
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘𝑆))
Theorem	opnneip 23109	An open set is a neighborhood of any of its members. (Contributed by NM, 8-Mar-2007.)
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑃 ∈ 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃}))
Theorem	opnnei 23110*	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 23111	The underlying set of a topology is a neighborhood of any of its subsets. Special case of opnneiss 23108. (Contributed by FL, 2-Oct-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Top → (𝑆 ⊆ 𝑋 ↔ 𝑋 ∈ ((nei‘𝐽)‘𝑆)))
Theorem	neiuni 23112	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 23113*	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 23114	A finer topology has more neighborhoods. (Contributed by Mario Carneiro, 9-Apr-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑋 = 𝑌) ∧ 𝐽 ⊆ 𝐾) → ((nei‘𝐽)‘𝑆) ⊆ ((nei‘𝐾)‘𝑆))
Theorem	innei 23115	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 23116	Only an open set is a neighborhood of itself. (Contributed by FL, 2-Oct-2006.)
⊢ (𝐽 ∈ Top → (𝑁 ∈ ((nei‘𝐽)‘𝑁) ↔ 𝑁 ∈ 𝐽))
Theorem	neissex 23117*	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 23118	The empty set is a neighborhood of itself. (Contributed by FL, 10-Dec-2006.)
⊢ (𝐽 ∈ Top → ∅ ∈ ((nei‘𝐽)‘∅))
Theorem	neipeltop 23119*	Lemma for neiptopreu 23123. (Contributed by Thierry Arnoux, 6-Jan-2018.)
⊢ 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)}    ⇒   ⊢ (𝐶 ∈ 𝐽 ↔ (𝐶 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝐶 𝐶 ∈ (𝑁‘𝑝)))
Theorem	neiptopuni 23120*	Lemma for neiptopreu 23123. (Contributed by Thierry Arnoux, 6-Jan-2018.)
⊢ 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)}    &   ⊢ (𝜑 → 𝑁:𝑋⟶𝒫 𝒫 𝑋)    &   ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝))    &   ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝))    &   ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎)    &   ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞))    &   ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝))    ⇒   ⊢ (𝜑 → 𝑋 = ∪ 𝐽)
Theorem	neiptoptop 23121*	Lemma for neiptopreu 23123. (Contributed by Thierry Arnoux, 7-Jan-2018.)
⊢ 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)}    &   ⊢ (𝜑 → 𝑁:𝑋⟶𝒫 𝒫 𝑋)    &   ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝))    &   ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝))    &   ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎)    &   ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞))    &   ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝))    ⇒   ⊢ (𝜑 → 𝐽 ∈ Top)
Theorem	neiptopnei 23122*	Lemma for neiptopreu 23123. (Contributed by Thierry Arnoux, 7-Jan-2018.)
⊢ 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)}    &   ⊢ (𝜑 → 𝑁:𝑋⟶𝒫 𝒫 𝑋)    &   ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝))    &   ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝))    &   ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎)    &   ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞))    &   ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝))    ⇒   ⊢ (𝜑 → 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝐽)‘{𝑝})))
Theorem	neiptopreu 23123*	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 23100, innei 23115, elnei 23101 and neissex 23117, 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 23115 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 9321 includes the empty intersection, remove that extra hypothesis. (Contributed by Thierry Arnoux, 6-Jan-2018.)
⊢ 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)}    &   ⊢ (𝜑 → 𝑁:𝑋⟶𝒫 𝒫 𝑋)    &   ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝))    &   ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝))    &   ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎)    &   ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞))    &   ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝))    ⇒   ⊢ (𝜑 → ∃!𝑗 ∈ (TopOn‘𝑋)𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝})))
12.1.6  Limit points and perfect sets
Syntax	clp 23124	Extend class notation with the limit point function for topologies.
class limPt
Syntax	cperf 23125	Extend class notation with the class of all perfect spaces.
class Perf
Definition	df-lp 23126*	Define a function on topologies whose value is the set of limit points of the subsets of the base set. See lpval 23129. (Contributed by NM, 10-Feb-2007.)
⊢ limPt = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ {𝑦 ∣ 𝑦 ∈ ((cls‘𝑗)‘(𝑥 ∖ {𝑦}))}))
Definition	df-perf 23127	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 23128*	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 23129*	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 23130	The predicate "the class 𝑃 is a limit point of 𝑆". (Contributed by NM, 10-Feb-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((limPt‘𝐽)‘𝑆) ↔ 𝑃 ∈ ((cls‘𝐽)‘(𝑆 ∖ {𝑃}))))
Theorem	lpsscls 23131	The limit points of a subset are included in the subset's closure. (Contributed by NM, 26-Feb-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((limPt‘𝐽)‘𝑆) ⊆ ((cls‘𝐽)‘𝑆))
Theorem	lpss 23132	The limit points of a subset are included in the base set. (Contributed by NM, 9-Nov-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((limPt‘𝐽)‘𝑆) ⊆ 𝑋)
Theorem	lpdifsn 23133	𝑃 is a limit point of 𝑆 iff it is a limit point of 𝑆 ∖ {𝑃}. (Contributed by Mario Carneiro, 25-Dec-2016.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((limPt‘𝐽)‘𝑆) ↔ 𝑃 ∈ ((limPt‘𝐽)‘(𝑆 ∖ {𝑃}))))
Theorem	lpss3 23134	Subset relationship for limit points. (Contributed by Mario Carneiro, 25-Dec-2016.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆) → ((limPt‘𝐽)‘𝑇) ⊆ ((limPt‘𝐽)‘𝑆))
Theorem	islp2 23135*	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 23136*	The predicate "𝑃 is a limit point of 𝑆 " in terms of open sets. see islp2 23135, elcls 23063, islp 23130. (Contributed by FL, 31-Jul-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑃 ∈ ((limPt‘𝐽)‘𝑆) ↔ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → (𝑥 ∩ (𝑆 ∖ {𝑃})) ≠ ∅)))
Theorem	maxlp 23137	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 23138	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 23139	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 23140	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 23141	Definition of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Perf ↔ (𝐽 ∈ Top ∧ ((limPt‘𝐽)‘𝑋) = 𝑋))
Theorem	isperf2 23142	Definition of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Perf ↔ (𝐽 ∈ Top ∧ 𝑋 ⊆ ((limPt‘𝐽)‘𝑋)))
Theorem	isperf3 23143*	A perfect space is a topology which has no open singletons. (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Perf ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝑋 ¬ {𝑥} ∈ 𝐽))
Theorem	perflp 23144	The limit points of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Perf → ((limPt‘𝐽)‘𝑋) = 𝑋)
Theorem	perfi 23145	Property of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Perf ∧ 𝑃 ∈ 𝑋) → ¬ {𝑃} ∈ 𝐽)
Theorem	perftop 23146	A perfect space is a topology. (Contributed by Mario Carneiro, 25-Dec-2016.)
⊢ (𝐽 ∈ Perf → 𝐽 ∈ Top)
12.1.7  Subspace topologies
Theorem	restrcl 23147	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 23148	A subspace topology basis is a basis. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ (𝐵 ∈ TopBases → (𝐵 ↾t 𝐴) ∈ TopBases)
Theorem	tgrest 23149	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 23150	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 23151	A subspace topology is a topology on the base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴))
Theorem	restuni 23152	The underlying set of a subspace topology. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 13-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → 𝐴 = ∪ (𝐽 ↾t 𝐴))
Theorem	stoig 23153	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 23154	Composition of subspaces. (Contributed by Mario Carneiro, 15-Dec-2013.) (Revised by Mario Carneiro, 1-May-2015.)
⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → ((𝐽 ↾t 𝐴) ↾t 𝐵) = (𝐽 ↾t (𝐴 ∩ 𝐵)))
Theorem	restabs 23155	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 23156	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 23157	The underlying set of a subspace topology. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝐴 ∩ 𝑋) = ∪ (𝐽 ↾t 𝐴))
Theorem	resttopon2 23158	The underlying set of a subspace topology. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ (TopOn‘(𝐴 ∩ 𝑋)))
Theorem	rest0 23159	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 23160	The only subspace topology induced by the topology {∅}. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 15-Dec-2013.)
⊢ (𝐴 ∈ 𝑉 → ({∅} ↾t 𝐴) = {∅})
Theorem	restsn2 23161	The subspace topology induced by a singleton. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 16-Sep-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐽 ↾t {𝐴}) = 𝒫 {𝐴})
Theorem	restcld 23162*	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 23163	A closed set is closed in the subspace topology. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝐵 ∈ (Clsd‘𝐽) ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ (Clsd‘(𝐽 ↾t 𝐴)))
Theorem	restcldr 23164	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 23165	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 23166	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 23167	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 23168	A subspace of a discrete topology is discrete. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → (𝒫 𝐴 ↾t 𝐵) = 𝒫 𝐵)
Theorem	restfpw 23169	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 23170	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 23171	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 23172	An interior in a subspace topology. Willard in General Topology says that there is no analogue of restcls 23171 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 23173	The limit points of a subset restrict naturally in a subspace. (Contributed by Mario Carneiro, 25-Dec-2016.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (𝐽 ↾t 𝑌)    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → ((limPt‘𝐾)‘𝑆) = (((limPt‘𝐽)‘𝑆) ∩ 𝑌))
Theorem	restperf 23174	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 23175	An open subset of a perfect space is perfect. (Contributed by Mario Carneiro, 25-Dec-2016.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (𝐽 ↾t 𝑌)    ⇒   ⊢ ((𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽) → 𝐾 ∈ Perf)
Theorem	resstopn 23176	The topology of a restricted structure. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ 𝐻 = (𝐾 ↾s 𝐴)    &   ⊢ 𝐽 = (TopOpen‘𝐾)    ⇒   ⊢ (𝐽 ↾t 𝐴) = (TopOpen‘𝐻)
Theorem	resstps 23177	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)
12.1.8  Order topology
Theorem	ordtbaslem 23178*	Lemma for ordtbas 23182. In a total order, unbounded-above intervals are closed under intersection. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝑋 = dom 𝑅    &   ⊢ 𝐴 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥})    ⇒   ⊢ (𝑅 ∈ TosetRel → (fi‘𝐴) = 𝐴)
Theorem	ordtval 23179*	Value of the order topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝑋 = dom 𝑅    &   ⊢ 𝐴 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥})    &   ⊢ 𝐵 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦})    ⇒   ⊢ (𝑅 ∈ 𝑉 → (ordTop‘𝑅) = (topGen‘(fi‘({𝑋} ∪ (𝐴 ∪ 𝐵)))))
Theorem	ordtuni 23180*	Value of the order topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝑋 = dom 𝑅    &   ⊢ 𝐴 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥})    &   ⊢ 𝐵 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦})    ⇒   ⊢ (𝑅 ∈ 𝑉 → 𝑋 = ∪ ({𝑋} ∪ (𝐴 ∪ 𝐵)))
Theorem	ordtbas2 23181*	Lemma for ordtbas 23182. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝑋 = dom 𝑅    &   ⊢ 𝐴 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥})    &   ⊢ 𝐵 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦})    &   ⊢ 𝐶 = ran (𝑎 ∈ 𝑋, 𝑏 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑏𝑅𝑦)})    ⇒   ⊢ (𝑅 ∈ TosetRel → (fi‘(𝐴 ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∪ 𝐶))
Theorem	ordtbas 23182*	In a total order, the finite intersections of the open rays generates the set of open intervals, but no more - these four collections form a subbasis for the order topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝑋 = dom 𝑅    &   ⊢ 𝐴 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥})    &   ⊢ 𝐵 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦})    &   ⊢ 𝐶 = ran (𝑎 ∈ 𝑋, 𝑏 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑏𝑅𝑦)})    ⇒   ⊢ (𝑅 ∈ TosetRel → (fi‘({𝑋} ∪ (𝐴 ∪ 𝐵))) = (({𝑋} ∪ (𝐴 ∪ 𝐵)) ∪ 𝐶))
Theorem	ordttopon 23183	Value of the order topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ (𝑅 ∈ 𝑉 → (ordTop‘𝑅) ∈ (TopOn‘𝑋))
Theorem	ordtopn1 23184*	An upward ray (𝑃, +∞) is open. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋) → {𝑥 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑃} ∈ (ordTop‘𝑅))
Theorem	ordtopn2 23185*	A downward ray (-∞, 𝑃) is open. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋) → {𝑥 ∈ 𝑋 ∣ ¬ 𝑃𝑅𝑥} ∈ (ordTop‘𝑅))
Theorem	ordtopn3 23186*	An open interval (𝐴, 𝐵) is open. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → {𝑥 ∈ 𝑋 ∣ (¬ 𝑥𝑅𝐴 ∧ ¬ 𝐵𝑅𝑥)} ∈ (ordTop‘𝑅))
Theorem	ordtcld1 23187*	A downward ray (-∞, 𝑃] is closed. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋) → {𝑥 ∈ 𝑋 ∣ 𝑥𝑅𝑃} ∈ (Clsd‘(ordTop‘𝑅)))
Theorem	ordtcld2 23188*	An upward ray [𝑃, +∞) is closed. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋) → {𝑥 ∈ 𝑋 ∣ 𝑃𝑅𝑥} ∈ (Clsd‘(ordTop‘𝑅)))
Theorem	ordtcld3 23189*	A closed interval [𝐴, 𝐵] is closed. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → {𝑥 ∈ 𝑋 ∣ (𝐴𝑅𝑥 ∧ 𝑥𝑅𝐵)} ∈ (Clsd‘(ordTop‘𝑅)))
Theorem	ordttop 23190	The order topology is a topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ (𝑅 ∈ 𝑉 → (ordTop‘𝑅) ∈ Top)
Theorem	ordtcnv 23191	The order dual generates the same topology as the original order. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ (𝑅 ∈ PosetRel → (ordTop‘◡𝑅) = (ordTop‘𝑅))
Theorem	ordtrest 23192	The subspace topology of an order topology is in general finer than the topology generated by the restricted order, but we do have inclusion in one direction. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑉) → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) ⊆ ((ordTop‘𝑅) ↾t 𝐴))
Theorem	ordtrest2lem 23193*	Lemma for ordtrest2 23194. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ 𝑋 = dom 𝑅    &   ⊢ (𝜑 → 𝑅 ∈ TosetRel )    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑋)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝑋 ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑅𝑦)} ⊆ 𝐴)    ⇒   ⊢ (𝜑 → ∀𝑣 ∈ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))))
Theorem	ordtrest2 23194*	An interval-closed set 𝐴 in a total order has the same subspace topology as the restricted order topology. (An interval-closed set is the same thing as an open or half-open or closed interval in ℝ, but in other sets like ℚ there are interval-closed sets like (π, +∞) ∩ ℚ that are not intervals.) (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ 𝑋 = dom 𝑅    &   ⊢ (𝜑 → 𝑅 ∈ TosetRel )    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑋)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝑋 ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑅𝑦)} ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))) = ((ordTop‘𝑅) ↾t 𝐴))
Theorem	letopon 23195	The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ (ordTop‘ ≤ ) ∈ (TopOn‘ℝ*)
Theorem	letop 23196	The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ (ordTop‘ ≤ ) ∈ Top
Theorem	letopuni 23197	The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ ℝ* = ∪ (ordTop‘ ≤ )
Theorem	xrstopn 23198	The topology component of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ (ordTop‘ ≤ ) = (TopOpen‘ℝ*𝑠)
Theorem	xrstps 23199	The extended real number structure is a topological space. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ℝ*𝑠 ∈ TopSp
Theorem	leordtvallem1 23200*	Lemma for leordtval 23203. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝐴 = ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞))    ⇒   ⊢ 𝐴 = ran (𝑥 ∈ ℝ* ↦ {𝑦 ∈ ℝ* ∣ ¬ 𝑦 ≤ 𝑥})