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	restabs 23101	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 23102	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 23103	The underlying set of a subspace topology. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝐴 ∩ 𝑋) = ∪ (𝐽 ↾t 𝐴))
Theorem	resttopon2 23104	The underlying set of a subspace topology. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ (TopOn‘(𝐴 ∩ 𝑋)))
Theorem	rest0 23105	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 23106	The only subspace topology induced by the topology {∅}. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 15-Dec-2013.)
⊢ (𝐴 ∈ 𝑉 → ({∅} ↾t 𝐴) = {∅})
Theorem	restsn2 23107	The subspace topology induced by a singleton. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 16-Sep-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐽 ↾t {𝐴}) = 𝒫 {𝐴})
Theorem	restcld 23108*	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 23109	A closed set is closed in the subspace topology. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝐵 ∈ (Clsd‘𝐽) ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ (Clsd‘(𝐽 ↾t 𝐴)))
Theorem	restcldr 23110	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 23111	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 23112	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 23113	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 23114	A subspace of a discrete topology is discrete. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → (𝒫 𝐴 ↾t 𝐵) = 𝒫 𝐵)
Theorem	restfpw 23115	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 23116	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 23117	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 23118	An interior in a subspace topology. Willard in General Topology says that there is no analogue of restcls 23117 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 23119	The limit points of a subset restrict naturally in a subspace. (Contributed by Mario Carneiro, 25-Dec-2016.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (𝐽 ↾t 𝑌)    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → ((limPt‘𝐾)‘𝑆) = (((limPt‘𝐽)‘𝑆) ∩ 𝑌))
Theorem	restperf 23120	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 23121	An open subset of a perfect space is perfect. (Contributed by Mario Carneiro, 25-Dec-2016.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐾 = (𝐽 ↾t 𝑌)    ⇒   ⊢ ((𝐽 ∈ Perf ∧ 𝑌 ∈ 𝐽) → 𝐾 ∈ Perf)
Theorem	resstopn 23122	The topology of a restricted structure. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ 𝐻 = (𝐾 ↾s 𝐴)    &   ⊢ 𝐽 = (TopOpen‘𝐾)    ⇒   ⊢ (𝐽 ↾t 𝐴) = (TopOpen‘𝐻)
Theorem	resstps 23123	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 23124*	Lemma for ordtbas 23128. In a total order, unbounded-above intervals are closed under intersection. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝑋 = dom 𝑅    &   ⊢ 𝐴 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥})    ⇒   ⊢ (𝑅 ∈ TosetRel → (fi‘𝐴) = 𝐴)
Theorem	ordtval 23125*	Value of the order topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝑋 = dom 𝑅    &   ⊢ 𝐴 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥})    &   ⊢ 𝐵 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦})    ⇒   ⊢ (𝑅 ∈ 𝑉 → (ordTop‘𝑅) = (topGen‘(fi‘({𝑋} ∪ (𝐴 ∪ 𝐵)))))
Theorem	ordtuni 23126*	Value of the order topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝑋 = dom 𝑅    &   ⊢ 𝐴 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥})    &   ⊢ 𝐵 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦})    ⇒   ⊢ (𝑅 ∈ 𝑉 → 𝑋 = ∪ ({𝑋} ∪ (𝐴 ∪ 𝐵)))
Theorem	ordtbas2 23127*	Lemma for ordtbas 23128. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝑋 = dom 𝑅    &   ⊢ 𝐴 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑦𝑅𝑥})    &   ⊢ 𝐵 = ran (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑦})    &   ⊢ 𝐶 = ran (𝑎 ∈ 𝑋, 𝑏 ∈ 𝑋 ↦ {𝑦 ∈ 𝑋 ∣ (¬ 𝑦𝑅𝑎 ∧ ¬ 𝑏𝑅𝑦)})    ⇒   ⊢ (𝑅 ∈ TosetRel → (fi‘(𝐴 ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∪ 𝐶))
Theorem	ordtbas 23128*	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 23129	Value of the order topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ (𝑅 ∈ 𝑉 → (ordTop‘𝑅) ∈ (TopOn‘𝑋))
Theorem	ordtopn1 23130*	An upward ray (𝑃, +∞) is open. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋) → {𝑥 ∈ 𝑋 ∣ ¬ 𝑥𝑅𝑃} ∈ (ordTop‘𝑅))
Theorem	ordtopn2 23131*	A downward ray (-∞, 𝑃) is open. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋) → {𝑥 ∈ 𝑋 ∣ ¬ 𝑃𝑅𝑥} ∈ (ordTop‘𝑅))
Theorem	ordtopn3 23132*	An open interval (𝐴, 𝐵) is open. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → {𝑥 ∈ 𝑋 ∣ (¬ 𝑥𝑅𝐴 ∧ ¬ 𝐵𝑅𝑥)} ∈ (ordTop‘𝑅))
Theorem	ordtcld1 23133*	A downward ray (-∞, 𝑃] is closed. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋) → {𝑥 ∈ 𝑋 ∣ 𝑥𝑅𝑃} ∈ (Clsd‘(ordTop‘𝑅)))
Theorem	ordtcld2 23134*	An upward ray [𝑃, +∞) is closed. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋) → {𝑥 ∈ 𝑋 ∣ 𝑃𝑅𝑥} ∈ (Clsd‘(ordTop‘𝑅)))
Theorem	ordtcld3 23135*	A closed interval [𝐴, 𝐵] is closed. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → {𝑥 ∈ 𝑋 ∣ (𝐴𝑅𝑥 ∧ 𝑥𝑅𝐵)} ∈ (Clsd‘(ordTop‘𝑅)))
Theorem	ordttop 23136	The order topology is a topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ (𝑅 ∈ 𝑉 → (ordTop‘𝑅) ∈ Top)
Theorem	ordtcnv 23137	The order dual generates the same topology as the original order. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ (𝑅 ∈ PosetRel → (ordTop‘◡𝑅) = (ordTop‘𝑅))
Theorem	ordtrest 23138	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 23139*	Lemma for ordtrest2 23140. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ 𝑋 = dom 𝑅    &   ⊢ (𝜑 → 𝑅 ∈ TosetRel )    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑋)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝑋 ∣ (𝑥𝑅𝑧 ∧ 𝑧𝑅𝑦)} ⊆ 𝐴)    ⇒   ⊢ (𝜑 → ∀𝑣 ∈ ran (𝑧 ∈ 𝑋 ↦ {𝑤 ∈ 𝑋 ∣ ¬ 𝑤𝑅𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘(𝑅 ∩ (𝐴 × 𝐴))))
Theorem	ordtrest2 23140*	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 23141	The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ (ordTop‘ ≤ ) ∈ (TopOn‘ℝ*)
Theorem	letop 23142	The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ (ordTop‘ ≤ ) ∈ Top
Theorem	letopuni 23143	The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ ℝ* = ∪ (ordTop‘ ≤ )
Theorem	xrstopn 23144	The topology component of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ (ordTop‘ ≤ ) = (TopOpen‘ℝ*𝑠)
Theorem	xrstps 23145	The extended real number structure is a topological space. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ℝ*𝑠 ∈ TopSp
Theorem	leordtvallem1 23146*	Lemma for leordtval 23149. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝐴 = ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞))    ⇒   ⊢ 𝐴 = ran (𝑥 ∈ ℝ* ↦ {𝑦 ∈ ℝ* ∣ ¬ 𝑦 ≤ 𝑥})
Theorem	leordtvallem2 23147*	Lemma for leordtval 23149. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝐴 = ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞))    &   ⊢ 𝐵 = ran (𝑥 ∈ ℝ* ↦ (-∞[,)𝑥))    ⇒   ⊢ 𝐵 = ran (𝑥 ∈ ℝ* ↦ {𝑦 ∈ ℝ* ∣ ¬ 𝑥 ≤ 𝑦})
Theorem	leordtval2 23148	The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝐴 = ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞))    &   ⊢ 𝐵 = ran (𝑥 ∈ ℝ* ↦ (-∞[,)𝑥))    ⇒   ⊢ (ordTop‘ ≤ ) = (topGen‘(fi‘(𝐴 ∪ 𝐵)))
Theorem	leordtval 23149	The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝐴 = ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞))    &   ⊢ 𝐵 = ran (𝑥 ∈ ℝ* ↦ (-∞[,)𝑥))    &   ⊢ 𝐶 = ran (,)    ⇒   ⊢ (ordTop‘ ≤ ) = (topGen‘((𝐴 ∪ 𝐵) ∪ 𝐶))
Theorem	iccordt 23150	A closed interval is closed in the order topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ (𝐴[,]𝐵) ∈ (Clsd‘(ordTop‘ ≤ ))
Theorem	iocpnfordt 23151	An unbounded above open interval is open in the order topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ (𝐴(,]+∞) ∈ (ordTop‘ ≤ )
Theorem	icomnfordt 23152	An unbounded above open interval is open in the order topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ (-∞[,)𝐴) ∈ (ordTop‘ ≤ )
Theorem	iooordt 23153	An open interval is open in the order topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ (𝐴(,)𝐵) ∈ (ordTop‘ ≤ )
Theorem	reordt 23154	The real numbers are an open set in the topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ ℝ ∈ (ordTop‘ ≤ )
Theorem	lecldbas 23155	The set of closed intervals forms a closed subbasis for the topology on the extended reals. Since our definition of a basis is in terms of open sets, we express this by showing that the complements of closed intervals form an open subbasis for the topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ 𝐹 = (𝑥 ∈ ran [,] ↦ (ℝ* ∖ 𝑥))    ⇒   ⊢ (ordTop‘ ≤ ) = (topGen‘(fi‘ran 𝐹))
Theorem	pnfnei 23156*	A neighborhood of +∞ contains an unbounded interval based at a real number. Together with xrtgioo 24744 (which describes neighborhoods of ℝ) and mnfnei 23157, this gives all "negative" topological information ensuring that it is not too fine (and of course iooordt 23153 and similar ensure that it has all the sets we want). (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ ((𝐴 ∈ (ordTop‘ ≤ ) ∧ +∞ ∈ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)
Theorem	mnfnei 23157*	A neighborhood of -∞ contains an unbounded interval based at a real number. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ ((𝐴 ∈ (ordTop‘ ≤ ) ∧ -∞ ∈ 𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴)
Theorem	ordtrestixx 23158*	The restriction of the less than order to an interval gives the same topology as the subspace topology. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ 𝐴 ⊆ ℝ*    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥[,]𝑦) ⊆ 𝐴)    ⇒   ⊢ ((ordTop‘ ≤ ) ↾t 𝐴) = (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))
Theorem	ordtresticc 23159	The restriction of the less than order to a closed interval gives the same topology as the subspace topology. (Contributed by Mario Carneiro, 9-Sep-2015.)
⊢ ((ordTop‘ ≤ ) ↾t (𝐴[,]𝐵)) = (ordTop‘( ≤ ∩ ((𝐴[,]𝐵) × (𝐴[,]𝐵))))
12.1.9  Limits and continuity in topological spaces
Syntax	ccn 23160	Extend class notation with the class of continuous functions between topologies.
class Cn
Syntax	ccnp 23161	Extend class notation with the class of functions between topologies continuous at a given point.
class CnP
Syntax	clm 23162	Extend class notation with a function on topological spaces whose value is the convergence relation for limit sequences in the space.
class ⇝𝑡
Definition	df-cn 23163*	Define a function on two topologies whose value is the set of continuous mappings from the first topology to the second. Based on definition of continuous function in [Munkres] p. 102. See iscn 23171 for the predicate form. (Contributed by NM, 17-Oct-2006.)
⊢ Cn = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑓 ∈ (∪ 𝑘 ↑m ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 (◡𝑓 “ 𝑦) ∈ 𝑗})
Definition	df-cnp 23164*	Define a function on two topologies whose value is the set of continuous mappings at a specified point in the first topology. Based on Theorem 7.2(g) of [Munkres] p. 107. (Contributed by NM, 17-Oct-2006.)
⊢ CnP = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑥 ∈ ∪ 𝑗 ↦ {𝑓 ∈ (∪ 𝑘 ↑m ∪ 𝑗) ∣ ∀𝑦 ∈ 𝑘 ((𝑓‘𝑥) ∈ 𝑦 → ∃𝑔 ∈ 𝑗 (𝑥 ∈ 𝑔 ∧ (𝑓 “ 𝑔) ⊆ 𝑦))}))
Definition	df-lm 23165*	Define a function on topologies whose value is the convergence relation for sequences into the given topological space. Although 𝑓 is typically a sequence (a function from an upperset of integers) with values in the topological space, it need not be. Note, however, that the limit property concerns only values at integers, so that the real-valued function (𝑥 ∈ ℝ ↦ (sin‘(π · 𝑥))) converges to zero (in the standard topology on the reals) with this definition. (Contributed by NM, 7-Sep-2006.)
⊢ ⇝𝑡 = (𝑗 ∈ Top ↦ {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ (∪ 𝑗 ↑pm ℂ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀𝑢 ∈ 𝑗 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))})
Theorem	lmrel 23166	The topological space convergence relation is a relation. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 14-Nov-2013.)
⊢ Rel (⇝𝑡‘𝐽)
Theorem	lmrcl 23167	Reverse closure for the convergence relation. (Contributed by Mario Carneiro, 7-Sep-2015.)
⊢ (𝐹(⇝𝑡‘𝐽)𝑃 → 𝐽 ∈ Top)
Theorem	lmfval 23168*	The relation "sequence 𝑓 converges to point 𝑦 " in a metric space. (Contributed by NM, 7-Sep-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → (⇝𝑡‘𝐽) = {⟨𝑓, 𝑥⟩ ∣ (𝑓 ∈ (𝑋 ↑pm ℂ) ∧ 𝑥 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝑓 ↾ 𝑦):𝑦⟶𝑢))})
Theorem	cnfval 23169*	The set of all continuous functions from topology 𝐽 to topology 𝐾. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 Cn 𝐾) = {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑦 ∈ 𝐾 (◡𝑓 “ 𝑦) ∈ 𝐽})
Theorem	cnpfval 23170*	The function mapping the points in a topology 𝐽 to the set of all functions from 𝐽 to topology 𝐾 continuous at that point. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 CnP 𝐾) = (𝑥 ∈ 𝑋 ↦ {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑤 ∈ 𝐾 ((𝑓‘𝑥) ∈ 𝑤 → ∃𝑣 ∈ 𝐽 (𝑥 ∈ 𝑣 ∧ (𝑓 “ 𝑣) ⊆ 𝑤))}))
Theorem	iscn 23171*	The predicate "the class 𝐹 is a continuous function from topology 𝐽 to topology 𝐾". Definition of continuous function in [Munkres] p. 102. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 (◡𝐹 “ 𝑦) ∈ 𝐽)))
Theorem	cnpval 23172*	The set of all functions from topology 𝐽 to topology 𝐾 that are continuous at a point 𝑃. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) → ((𝐽 CnP 𝐾)‘𝑃) = {𝑓 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑦 ∈ 𝐾 ((𝑓‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝑓 “ 𝑥) ⊆ 𝑦))})
Theorem	iscnp 23173*	The predicate "the class 𝐹 is a continuous function from topology 𝐽 to topology 𝐾 at point 𝑃". Based on Theorem 7.2(g) of [Munkres] p. 107. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦)))))
Theorem	iscn2 23174*	The predicate "the class 𝐹 is a continuous function from topology 𝐽 to topology 𝐾". Definition of continuous function in [Munkres] p. 102. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 (◡𝐹 “ 𝑦) ∈ 𝐽)))
Theorem	iscnp2 23175*	The predicate "the class 𝐹 is a continuous function from topology 𝐽 to topology 𝐾 at point 𝑃". Based on Theorem 7.2(g) of [Munkres] p. 107. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦)))))
Theorem	cntop1 23176	Reverse closure for a continuous function. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top)
Theorem	cntop2 23177	Reverse closure for a continuous function. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top)
Theorem	cnptop1 23178	Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝐽 ∈ Top)
Theorem	cnptop2 23179	Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝐾 ∈ Top)
Theorem	iscnp3 23180*	The predicate "the class 𝐹 is a continuous function from topology 𝐽 to topology 𝐾 at point 𝑃". (Contributed by NM, 15-May-2007.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ (◡𝐹 “ 𝑦))))))
Theorem	cnprcl 23181	Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝑃 ∈ 𝑋)
Theorem	cnf 23182	A continuous function is a mapping. (Contributed by FL, 8-Dec-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋⟶𝑌)
Theorem	cnpf 23183	A continuous function at point 𝑃 is a mapping. (Contributed by FL, 17-Nov-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) → 𝐹:𝑋⟶𝑌)
Theorem	cnpcl 23184	The value of a continuous function from 𝐽 to 𝐾 at point 𝑃 belongs to the underlying set of topology 𝐾. (Contributed by FL, 27-Dec-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐴 ∈ 𝑋) → (𝐹‘𝐴) ∈ 𝑌)
Theorem	cnf2 23185	A continuous function is a mapping. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:𝑋⟶𝑌)
Theorem	cnpf2 23186	A continuous function at point 𝑃 is a mapping. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐹:𝑋⟶𝑌)
Theorem	cnprcl2 23187	Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝑃 ∈ 𝑋)
Theorem	tgcn 23188*	The continuity predicate when the range is given by a basis for a topology. (Contributed by Mario Carneiro, 7-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐾 = (topGen‘𝐵))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽)))
Theorem	tgcnp 23189*	The "continuous at a point" predicate when the range is given by a basis for a topology. (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐾 = (topGen‘𝐵))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → 𝑃 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐵 ((𝐹‘𝑃) ∈ 𝑦 → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝑦)))))
Theorem	subbascn 23190*	The continuity predicate when the range is given by a subbasis for a topology. (Contributed by Mario Carneiro, 7-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐾 = (topGen‘(fi‘𝐵)))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽)))
Theorem	ssidcn 23191	The identity function is a continuous function from one topology to another topology on the same set iff the domain is finer than the codomain. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 21-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) → (( I ↾ 𝑋) ∈ (𝐽 Cn 𝐾) ↔ 𝐾 ⊆ 𝐽))
Theorem	cnpimaex 23192*	Property of a function continuous at a point. (Contributed by FL, 31-Dec-2006.)
⊢ ((𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐴 ∈ 𝐾 ∧ (𝐹‘𝑃) ∈ 𝐴) → ∃𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 ∧ (𝐹 “ 𝑥) ⊆ 𝐴))
Theorem	idcn 23193	A restricted identity function is a continuous function. (Contributed by FL, 27-Dec-2006.) (Proof shortened by Mario Carneiro, 21-Mar-2015.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → ( I ↾ 𝑋) ∈ (𝐽 Cn 𝐽))
Theorem	lmbr 23194*	Express the binary relation "sequence 𝐹 converges to point 𝑃 " in a topological space. Definition 1.4-1 of [Kreyszig] p. 25. The condition 𝐹 ⊆ (ℂ × 𝑋) allows to use objects more general than sequences when convenient; see the comment in df-lm 23165. (Contributed by Mario Carneiro, 14-Nov-2013.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ 𝑃 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶𝑢))))
Theorem	lmbr2 23195*	Express the binary relation "sequence 𝐹 converges to point 𝑃 " in a metric space using an arbitrary upper set of integers. (Contributed by Mario Carneiro, 14-Nov-2013.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ 𝑃 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))))
Theorem	lmbrf 23196*	Express the binary relation "sequence 𝐹 converges to point 𝑃 " in a metric space using an arbitrary upper set of integers. This version of lmbr2 23195 presupposes that 𝐹 is a function. (Contributed by Mario Carneiro, 14-Nov-2013.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:𝑍⟶𝑋)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝐴 ∈ 𝑢))))
Theorem	lmconst 23197	A constant sequence converges to its value. (Contributed by NM, 8-Nov-2007.) (Revised by Mario Carneiro, 14-Nov-2013.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ ℤ) → (𝑍 × {𝑃})(⇝𝑡‘𝐽)𝑃)
Theorem	lmcvg 23198*	Convergence property of a converging sequence. (Contributed by Mario Carneiro, 14-Nov-2013.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑃 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐽)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑈)
Theorem	iscnp4 23199*	The predicate "the class 𝐹 is a continuous function from topology 𝐽 to topology 𝐾 at point 𝑃 " in terms of neighborhoods. (Contributed by FL, 18-Jul-2011.) (Revised by Mario Carneiro, 10-Sep-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝑃)})∃𝑥 ∈ ((nei‘𝐽)‘{𝑃})(𝐹 “ 𝑥) ⊆ 𝑦)))
Theorem	cnpnei 23200*	A condition for continuity at a point in terms of neighborhoods. (Contributed by Jeff Hankins, 7-Sep-2009.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:𝑋⟶𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ ∀𝑦 ∈ ((nei‘𝐾)‘{(𝐹‘𝐴)})(◡𝐹 “ 𝑦) ∈ ((nei‘𝐽)‘{𝐴})))