P. 238 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 23701-23800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	uncmp 23701	The union of two compact sets is compact. (Contributed by Jeff Hankins, 30-Jan-2010.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ ((𝐽 ↾t 𝑆) ∈ Comp ∧ (𝐽 ↾t 𝑇) ∈ Comp)) → 𝐽 ∈ Comp)
Theorem	fiuncmp 23702*	A finite union of compact sets is compact. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝐽 ↾t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp)
Theorem	sscmp 23703	A subset of a compact topology (i.e. a coarser topology) is compact. (Contributed by Mario Carneiro, 20-Mar-2015.)
⊢ 𝑋 = ∪ 𝐾    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾) → 𝐽 ∈ Comp)
Theorem	hauscmplem 23704*	Lemma for hauscmp 23705. (Contributed by Mario Carneiro, 27-Nov-2013.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑂 = {𝑦 ∈ 𝐽 ∣ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))}    &   ⊢ (𝜑 → 𝐽 ∈ Haus)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑋)    &   ⊢ (𝜑 → (𝐽 ↾t 𝑆) ∈ Comp)    &   ⊢ (𝜑 → 𝐴 ∈ (𝑋 ∖ 𝑆))    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))
Theorem	hauscmp 23705	A compact subspace of a T2 space is closed. (Contributed by Jeff Hankins, 16-Jan-2010.) (Proof shortened by Mario Carneiro, 14-Dec-2013.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Haus ∧ 𝑆 ⊆ 𝑋 ∧ (𝐽 ↾t 𝑆) ∈ Comp) → 𝑆 ∈ (Clsd‘𝐽))
Theorem	cmpfi 23706*	If a topology is compact and a collection of closed sets has the finite intersection property, its intersection is nonempty. (Contributed by Jeff Hankins, 25-Aug-2009.) (Proof shortened by Mario Carneiro, 1-Sep-2015.)
⊢ (𝐽 ∈ Top → (𝐽 ∈ Comp ↔ ∀𝑥 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑥) → ∩ 𝑥 ≠ ∅)))
Theorem	cmpfii 23707	In a compact topology, a system of closed sets with nonempty finite intersections has a nonempty intersection. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ ((𝐽 ∈ Comp ∧ 𝑋 ⊆ (Clsd‘𝐽) ∧ ¬ ∅ ∈ (fi‘𝑋)) → ∩ 𝑋 ≠ ∅)
12.1.12  Bolzano-Weierstrass theorem
Theorem	bwth 23708*	The glorious Bolzano-Weierstrass theorem. The first general topology theorem ever proved. The first mention of this theorem can be found in a course by Weierstrass from 1865. In his course Weierstrass called it a lemma. He didn't know how famous this theorem would be. He used a Euclidean space instead of a general compact space. And he was not aware of the Heine-Borel property. But the concepts of neighborhood and limit point were already there although not precisely defined. Cantor was one of his students. He published and used the theorem in an article from 1872. The rest of the general topology followed from that. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) Revised by BL to significantly shorten the proof and avoid infinity, regularity, and choice. (Revised by Brendan Leahy, 26-Dec-2018.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Comp ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin) → ∃𝑥 ∈ 𝑋 𝑥 ∈ ((limPt‘𝐽)‘𝐴))
12.1.13  Connectedness
Syntax	cconn 23709	Extend class notation with the class of all connected topologies.
class Conn
Definition	df-conn 23710	Topologies are connected when only ∅ and ∪ 𝑗 are both open and closed. (Contributed by FL, 17-Nov-2008.)
⊢ Conn = {𝑗 ∈ Top ∣ (𝑗 ∩ (Clsd‘𝑗)) = {∅, ∪ 𝑗}}
Theorem	isconn 23711	The predicate 𝐽 is a connected topology . (Contributed by FL, 17-Nov-2008.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Conn ↔ (𝐽 ∈ Top ∧ (𝐽 ∩ (Clsd‘𝐽)) = {∅, 𝑋}))
Theorem	isconn2 23712	The predicate 𝐽 is a connected topology . (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Conn ↔ (𝐽 ∈ Top ∧ (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, 𝑋}))
Theorem	connclo 23713	The only nonempty clopen set of a connected topology is the whole space. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐽 ∈ Conn)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐽)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → 𝐴 ∈ (Clsd‘𝐽))    ⇒   ⊢ (𝜑 → 𝐴 = 𝑋)
Theorem	conndisj 23714	If a topology is connected, its underlying set can't be partitioned into two nonempty non-overlapping open sets. (Contributed by FL, 16-Nov-2008.) (Proof shortened by Mario Carneiro, 10-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐽 ∈ Conn)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐽)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐽)    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐵) ≠ 𝑋)
Theorem	conntop 23715	A connected topology is a topology. (Contributed by FL, 22-Dec-2008.) (Revised by Mario Carneiro, 14-Dec-2013.)
⊢ (𝐽 ∈ Conn → 𝐽 ∈ Top)
Theorem	indisconn 23716	The indiscrete topology (or trivial topology) on any set is connected. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ {∅, 𝐴} ∈ Conn
Theorem	dfconn2 23717*	An alternate definition of connectedness. (Contributed by Jeff Hankins, 9-Jul-2009.) (Proof shortened by Mario Carneiro, 10-Mar-2015.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Conn ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ 𝑋)))
Theorem	connsuba 23718*	Connectedness for a subspace. See connsub 23719. (Contributed by FL, 29-May-2014.) (Proof shortened by Mario Carneiro, 10-Mar-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((𝐽 ↾t 𝐴) ∈ Conn ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (((𝑥 ∩ 𝐴) ≠ ∅ ∧ (𝑦 ∩ 𝐴) ≠ ∅ ∧ ((𝑥 ∩ 𝑦) ∩ 𝐴) = ∅) → ((𝑥 ∪ 𝑦) ∩ 𝐴) ≠ 𝐴)))
Theorem	connsub 23719*	Two equivalent ways of saying that a subspace topology is connected. (Contributed by Jeff Hankins, 9-Jul-2009.) (Proof shortened by Mario Carneiro, 10-Mar-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋) → ((𝐽 ↾t 𝑆) ∈ Conn ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (((𝑥 ∩ 𝑆) ≠ ∅ ∧ (𝑦 ∩ 𝑆) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ 𝑆)) → ¬ 𝑆 ⊆ (𝑥 ∪ 𝑦))))
Theorem	cnconn 23720	Connectedness is respected by a continuous onto map. (Contributed by Jeff Hankins, 12-Jul-2009.) (Proof shortened by Mario Carneiro, 10-Mar-2015.)
⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ ((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ Conn)
Theorem	nconnsubb 23721	Disconnectedness for a subspace. (Contributed by FL, 29-May-2014.) (Proof shortened by Mario Carneiro, 10-Mar-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐽)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐽)    &   ⊢ (𝜑 → (𝑈 ∩ 𝐴) ≠ ∅)    &   ⊢ (𝜑 → (𝑉 ∩ 𝐴) ≠ ∅)    &   ⊢ (𝜑 → ((𝑈 ∩ 𝑉) ∩ 𝐴) = ∅)    &   ⊢ (𝜑 → 𝐴 ⊆ (𝑈 ∪ 𝑉))    ⇒   ⊢ (𝜑 → ¬ (𝐽 ↾t 𝐴) ∈ Conn)
Theorem	connsubclo 23722	If a clopen set meets a connected subspace, it must contain the entire subspace. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑋)    &   ⊢ (𝜑 → (𝐽 ↾t 𝐴) ∈ Conn)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐽)    &   ⊢ (𝜑 → (𝐵 ∩ 𝐴) ≠ ∅)    &   ⊢ (𝜑 → 𝐵 ∈ (Clsd‘𝐽))    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
Theorem	connima 23723	The image of a connected set is connected. (Contributed by Mario Carneiro, 7-Jul-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑋)    &   ⊢ (𝜑 → (𝐽 ↾t 𝐴) ∈ Conn)    ⇒   ⊢ (𝜑 → (𝐾 ↾t (𝐹 “ 𝐴)) ∈ Conn)
Theorem	conncn 23724	A continuous function from a connected topology with one point in a clopen set must lie entirely within the set. (Contributed by Mario Carneiro, 16-Feb-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐽 ∈ Conn)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝑈 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑈 ∈ (Clsd‘𝐾))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → (𝐹‘𝐴) ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝐹:𝑋⟶𝑈)
Theorem	iunconnlem 23725*	Lemma for iunconn 23726. (Contributed by Mario Carneiro, 11-Jun-2014.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ⊆ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑃 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐽 ↾t 𝐵) ∈ Conn)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐽)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐽)    &   ⊢ (𝜑 → (𝑉 ∩ ∪ 𝑘 ∈ 𝐴 𝐵) ≠ ∅)    &   ⊢ (𝜑 → (𝑈 ∩ 𝑉) ⊆ (𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵))    &   ⊢ (𝜑 → ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑈 ∪ 𝑉))    &   ⊢ Ⅎ𝑘𝜑    ⇒   ⊢ (𝜑 → ¬ 𝑃 ∈ 𝑈)
Theorem	iunconn 23726*	The indexed union of connected overlapping subspaces sharing a common point is connected. (Contributed by Mario Carneiro, 11-Jun-2014.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ⊆ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑃 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐽 ↾t 𝐵) ∈ Conn)    ⇒   ⊢ (𝜑 → (𝐽 ↾t ∪ 𝑘 ∈ 𝐴 𝐵) ∈ Conn)
Theorem	unconn 23727	The union of two connected overlapping subspaces is connected. (Contributed by FL, 29-May-2014.) (Proof shortened by Mario Carneiro, 11-Jun-2014.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) ∧ (𝐴 ∩ 𝐵) ≠ ∅) → (((𝐽 ↾t 𝐴) ∈ Conn ∧ (𝐽 ↾t 𝐵) ∈ Conn) → (𝐽 ↾t (𝐴 ∪ 𝐵)) ∈ Conn))
Theorem	clsconn 23728	The closure of a connected set is connected. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Conn) → (𝐽 ↾t ((cls‘𝐽)‘𝐴)) ∈ Conn)
Theorem	conncompid 23729*	The connected component containing 𝐴 contains 𝐴. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ 𝑆)
Theorem	conncompconn 23730*	The connected component containing 𝐴 is connected. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐽 ↾t 𝑆) ∈ Conn)
Theorem	conncompss 23731*	The connected component containing 𝐴 is a superset of any other connected set containing 𝐴. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}    ⇒   ⊢ ((𝑇 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑇 ∧ (𝐽 ↾t 𝑇) ∈ Conn) → 𝑇 ⊆ 𝑆)
Theorem	conncompcld 23732*	The connected component containing 𝐴 is a closed set. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑋) → 𝑆 ∈ (Clsd‘𝐽))
Theorem	conncompclo 23733*	The connected component containing 𝐴 is a subset of any clopen set containing 𝐴. (Contributed by Mario Carneiro, 20-Sep-2015.)
⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑇 ∈ (𝐽 ∩ (Clsd‘𝐽)) ∧ 𝐴 ∈ 𝑇) → 𝑆 ⊆ 𝑇)
Theorem	t1connperf 23734	A connected T1 space is perfect, unless it is the topology of a singleton. (Contributed by Mario Carneiro, 26-Dec-2016.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Fre ∧ 𝐽 ∈ Conn ∧ ¬ 𝑋 ≈ 1o) → 𝐽 ∈ Perf)
12.1.14  First- and second-countability
Syntax	c1stc 23735	Extend class definition to include the class of all first-countable topologies.
class 1stω
Syntax	c2ndc 23736	Extend class definition to include the class of all second-countable topologies.
class 2ndω
Definition	df-1stc 23737*	Define the class of all first-countable topologies. (Contributed by Jeff Hankins, 22-Aug-2009.)
⊢ 1stω = {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∃𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧)))}
Definition	df-2ndc 23738*	Define the class of all second-countable topologies. (Contributed by Jeff Hankins, 17-Jan-2010.)
⊢ 2ndω = {𝑗 ∣ ∃𝑥 ∈ TopBases (𝑥 ≼ ω ∧ (topGen‘𝑥) = 𝑗)}
Theorem	is1stc 23739*	The predicate "is a first-countable topology." This can be described as "every point has a countable local basis" - that is, every point has a countable collection of open sets containing it such that every open set containing the point has an open set from this collection as a subset. (Contributed by Jeff Hankins, 22-Aug-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ 1stω ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝒫 𝐽(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧)))))
Theorem	is1stc2 23740*	An equivalent way of saying "is a first-countable topology." (Contributed by Jeff Hankins, 22-Aug-2009.) (Revised by Mario Carneiro, 21-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ 1stω ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝒫 𝐽(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))))
Theorem	1stctop 23741	A first-countable topology is a topology. (Contributed by Jeff Hankins, 22-Aug-2009.)
⊢ (𝐽 ∈ 1stω → 𝐽 ∈ Top)
Theorem	1stcclb 23742*	A property of points in a first-countable topology. (Contributed by Jeff Hankins, 22-Aug-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) → ∃𝑥 ∈ 𝒫 𝐽(𝑥 ≼ ω ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑧 ∈ 𝑥 (𝐴 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))))
Theorem	1stcfb 23743*	For any point 𝐴 in a first-countable topology, there is a function 𝑓:ℕ⟶𝐽 enumerating neighborhoods of 𝐴 which is decreasing and forms a local base. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦)))
Theorem	is2ndc 23744*	The property of being second-countable. (Contributed by Jeff Hankins, 17-Jan-2010.) (Revised by Mario Carneiro, 21-Mar-2015.)
⊢ (𝐽 ∈ 2ndω ↔ ∃𝑥 ∈ TopBases (𝑥 ≼ ω ∧ (topGen‘𝑥) = 𝐽))
Theorem	2ndctop 23745	A second-countable topology is a topology. (Contributed by Jeff Hankins, 17-Jan-2010.) (Revised by Mario Carneiro, 21-Mar-2015.)
⊢ (𝐽 ∈ 2ndω → 𝐽 ∈ Top)
Theorem	2ndci 23746	A countable basis generates a second-countable topology. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ ((𝐵 ∈ TopBases ∧ 𝐵 ≼ ω) → (topGen‘𝐵) ∈ 2ndω)
Theorem	2ndcsb 23747*	Having a countable subbase is a sufficient condition for second-countability. (Contributed by Jeff Hankins, 17-Jan-2010.) (Proof shortened by Mario Carneiro, 21-Mar-2015.)
⊢ (𝐽 ∈ 2ndω ↔ ∃𝑥(𝑥 ≼ ω ∧ (topGen‘(fi‘𝑥)) = 𝐽))
Theorem	2ndcredom 23748	A second-countable space has at most the cardinality of the continuum. (Contributed by Mario Carneiro, 9-Apr-2015.)
⊢ (𝐽 ∈ 2ndω → 𝐽 ≼ ℝ)
Theorem	2ndc1stc 23749	A second-countable space is first-countable. (Contributed by Jeff Hankins, 17-Jan-2010.)
⊢ (𝐽 ∈ 2ndω → 𝐽 ∈ 1stω)
Theorem	1stcrestlem 23750*	Lemma for 1stcrest 23751. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ (𝐵 ≼ ω → ran (𝑥 ∈ 𝐵 ↦ 𝐶) ≼ ω)
Theorem	1stcrest 23751	A subspace of a first-countable space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ ((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ 1stω)
Theorem	2ndcrest 23752	A subspace of a second-countable space is second-countable. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ ((𝐽 ∈ 2ndω ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ 2ndω)
Theorem	abrexct 23753*	An image set of a countable set is countable. (Contributed by Thierry Arnoux, 29-Dec-2016.) (Moved to the main part of set.mm by Vincent Gonzalez, 19-Aug-2026.)
⊢ (𝐴 ≼ ω → {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵} ≼ ω)
Theorem	2ndcctbss 23754*	If a topology is second-countable, every base has a countable subset which is a base. Exercise 16B2 in Willard. (Contributed by Jeff Hankins, 28-Jan-2010.) (Proof shortened by Mario Carneiro, 21-Mar-2015.)
⊢ 𝐽 = (topGen‘𝐵)    &   ⊢ 𝑆 = {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣))}    ⇒   ⊢ ((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏)))
Theorem	2ndcdisj 23755*	Any disjoint family of open sets in a second-countable space is countable. (The sets are required to be nonempty because otherwise there could be many empty sets in the family.) (Contributed by Mario Carneiro, 21-Mar-2015.) (Proof shortened by Mario Carneiro, 9-Apr-2015.) (Revised by NM, 17-Jun-2017.)
⊢ ((𝐽 ∈ 2ndω ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω)
Theorem	2ndcdisj2 23756*	Any disjoint collection of open sets in a second-countable space is countable. (Contributed by Mario Carneiro, 21-Mar-2015.) (Proof shortened by Mario Carneiro, 9-Apr-2015.) (Revised by NM, 17-Jun-2017.)
⊢ ((𝐽 ∈ 2ndω ∧ 𝐴 ⊆ 𝐽 ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝑥) → 𝐴 ≼ ω)
Theorem	2ndcomap 23757*	A surjective continuous open map maps second-countable spaces to second-countable spaces. (Contributed by Mario Carneiro, 9-Apr-2015.)
⊢ 𝑌 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐽 ∈ 2ndω)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → ran 𝐹 = 𝑌)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (𝐹 “ 𝑥) ∈ 𝐾)    ⇒   ⊢ (𝜑 → 𝐾 ∈ 2ndω)
Theorem	2ndcsep 23758*	A second-countable topology is separable, which is to say it contains a countable dense subset. (Contributed by Mario Carneiro, 13-Apr-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ 2ndω → ∃𝑥 ∈ 𝒫 𝑋(𝑥 ≼ ω ∧ ((cls‘𝐽)‘𝑥) = 𝑋))
Theorem	dis2ndc 23759	A discrete space is second-countable iff it is countable. (Contributed by Mario Carneiro, 13-Apr-2015.)
⊢ (𝑋 ≼ ω ↔ 𝒫 𝑋 ∈ 2ndω)
Theorem	1stcelcls 23760*	A point belongs to the closure of a subset iff there is a sequence in the subset converging to it. Theorem 1.4-6(a) of [Kreyszig] p. 30. This proof uses countable choice ax-cc 10494. A space satisfying the conclusion of this theorem is called a sequential space, so the theorem can also be stated as "every first-countable space is a sequential space". (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)))
Theorem	1stccnp 23761*	A mapping is continuous at 𝑃 in a first-countable space 𝑋 iff it is sequentially continuous at 𝑃, meaning that the image under 𝐹 of every sequence converging at 𝑃 converges to 𝐹(𝑃). This proof uses ax-cc 10494, but only via 1stcelcls 23760, so it could be refactored into a proof that continuity and sequential continuity are the same in sequential spaces. (Contributed by Mario Carneiro, 7-Sep-2015.)
⊢ (𝜑 → 𝐽 ∈ 1stω)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → 𝑃 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))))
Theorem	1stccn 23762*	A mapping 𝑋⟶𝑌, where 𝑋 is first-countable, is continuous iff it is sequentially continuous, meaning that for any sequence 𝑓(𝑛) converging to 𝑥, its image under 𝐹 converges to 𝐹(𝑥). (Contributed by Mario Carneiro, 7-Sep-2015.)
⊢ (𝜑 → 𝐽 ∈ 1stω)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → 𝐹:𝑋⟶𝑌)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ∀𝑓(𝑓:ℕ⟶𝑋 → ∀𝑥(𝑓(⇝𝑡‘𝐽)𝑥 → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑥)))))
12.1.15  Local topological properties
Syntax	clly 23763	Extend class notation with the "locally 𝐴 " predicate of a topological space.
class Locally 𝐴
Syntax	cnlly 23764	Extend class notation with the "N-locally 𝐴 " predicate of a topological space.
class 𝑛-Locally 𝐴
Definition	df-lly 23765*	Define a space that is locally 𝐴, where 𝐴 is a topological property like "compact", "connected", or "path-connected". A topological space is locally 𝐴 if every neighborhood of a point contains an open subneighborhood that is 𝐴 in the subspace topology. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ Locally 𝐴 = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝑗 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝐴)}
Definition	df-nlly 23766*	Define a space that is n-locally 𝐴, where 𝐴 is a topological property like "compact", "connected", or "path-connected". A topological space is n-locally 𝐴 if every neighborhood of a point contains a subneighborhood that is 𝐴 in the subspace topology. The terminology "n-locally", where 'n' stands for "neighborhood", is not standard, although this is sometimes called "weakly locally 𝐴". The reason for the distinction is that some notions only make sense for arbitrary neighborhoods (such as "locally compact", which is actually 𝑛-Locally Comp in our terminology - open compact sets are not very useful), while others such as "locally connected" are strictly weaker notions if the neighborhoods are not required to be open. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ 𝑛-Locally 𝐴 = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴}
Theorem	islly 23767*	The property of being a locally 𝐴 topological space. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ (𝐽 ∈ Locally 𝐴 ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝐽 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝐽 ↾t 𝑢) ∈ 𝐴)))
Theorem	isnlly 23768*	The property of being an n-locally 𝐴 topological space. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ (𝐽 ∈ 𝑛-Locally 𝐴 ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝐽)‘{𝑦}) ∩ 𝒫 𝑥)(𝐽 ↾t 𝑢) ∈ 𝐴))
Theorem	llyeq 23769	Equality theorem for the Locally 𝐴 predicate. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ (𝐴 = 𝐵 → Locally 𝐴 = Locally 𝐵)
Theorem	nllyeq 23770	Equality theorem for the Locally 𝐴 predicate. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ (𝐴 = 𝐵 → 𝑛-Locally 𝐴 = 𝑛-Locally 𝐵)
Theorem	llytop 23771	A locally 𝐴 space is a topological space. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ (𝐽 ∈ Locally 𝐴 → 𝐽 ∈ Top)
Theorem	nllytop 23772	A locally 𝐴 space is a topological space. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ (𝐽 ∈ 𝑛-Locally 𝐴 → 𝐽 ∈ Top)
Theorem	llyi 23773*	The property of a locally 𝐴 topological space. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ ((𝐽 ∈ Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) → ∃𝑢 ∈ 𝐽 (𝑢 ⊆ 𝑈 ∧ 𝑃 ∈ 𝑢 ∧ (𝐽 ↾t 𝑢) ∈ 𝐴))
Theorem	nllyi 23774*	The property of an n-locally 𝐴 topological space. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ ((𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑃})(𝑢 ⊆ 𝑈 ∧ (𝐽 ↾t 𝑢) ∈ 𝐴))
Theorem	nlly2i 23775*	Eliminate the neighborhood symbol from nllyi 23774. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ ((𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) → ∃𝑠 ∈ 𝒫 𝑈∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ 𝐴))
Theorem	llynlly 23776	A locally 𝐴 space is n-locally 𝐴: the "n-locally" predicate is the weaker notion. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ (𝐽 ∈ Locally 𝐴 → 𝐽 ∈ 𝑛-Locally 𝐴)
Theorem	llyssnlly 23777	A locally 𝐴 space is n-locally 𝐴. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ Locally 𝐴 ⊆ 𝑛-Locally 𝐴
Theorem	llyss 23778	The "locally" predicate respects inclusion. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ (𝐴 ⊆ 𝐵 → Locally 𝐴 ⊆ Locally 𝐵)
Theorem	nllyss 23779	The "n-locally" predicate respects inclusion. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ (𝐴 ⊆ 𝐵 → 𝑛-Locally 𝐴 ⊆ 𝑛-Locally 𝐵)
Theorem	subislly 23780*	The property of a subspace being locally 𝐴. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ ((𝐽 ∈ Top ∧ 𝐵 ∈ 𝑉) → ((𝐽 ↾t 𝐵) ∈ Locally 𝐴 ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ (𝑥 ∩ 𝐵)∃𝑢 ∈ 𝐽 ((𝑢 ∩ 𝐵) ⊆ 𝑥 ∧ 𝑦 ∈ 𝑢 ∧ (𝐽 ↾t (𝑢 ∩ 𝐵)) ∈ 𝐴)))
Theorem	restnlly 23781*	If the property 𝐴 passes to open subspaces, then a space is n-locally 𝐴 iff it is locally 𝐴. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑥 ∈ 𝑗)) → (𝑗 ↾t 𝑥) ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝑛-Locally 𝐴 = Locally 𝐴)
Theorem	restlly 23782*	If the property 𝐴 passes to open subspaces, then a space which is 𝐴 is also locally 𝐴. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑥 ∈ 𝑗)) → (𝑗 ↾t 𝑥) ∈ 𝐴)    &   ⊢ (𝜑 → 𝐴 ⊆ Top)    ⇒   ⊢ (𝜑 → 𝐴 ⊆ Locally 𝐴)
Theorem	islly2 23783*	An alternative expression for 𝐽 ∈ Locally 𝐴 when 𝐴 passes to open subspaces: A space is locally 𝐴 if every point is contained in an open neighborhood with property 𝐴. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑥 ∈ 𝑗)) → (𝑗 ↾t 𝑥) ∈ 𝐴)    &   ⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝜑 → (𝐽 ∈ Locally 𝐴 ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝑋 ∃𝑢 ∈ 𝐽 (𝑦 ∈ 𝑢 ∧ (𝐽 ↾t 𝑢) ∈ 𝐴))))
Theorem	llyrest 23784	An open subspace of a locally 𝐴 space is also locally 𝐴. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ ((𝐽 ∈ Locally 𝐴 ∧ 𝐵 ∈ 𝐽) → (𝐽 ↾t 𝐵) ∈ Locally 𝐴)
Theorem	nllyrest 23785	An open subspace of an n-locally 𝐴 space is also n-locally 𝐴. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ ((𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝐵 ∈ 𝐽) → (𝐽 ↾t 𝐵) ∈ 𝑛-Locally 𝐴)
Theorem	loclly 23786	If 𝐴 is a local property, then both Locally 𝐴 and 𝑛-Locally 𝐴 simplify to 𝐴. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ (Locally 𝐴 = 𝐴 ↔ 𝑛-Locally 𝐴 = 𝐴)
Theorem	llyidm 23787	Idempotence of the "locally" predicate, i.e. being "locally 𝐴 " is a local property. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ Locally Locally 𝐴 = Locally 𝐴
Theorem	nllyidm 23788	Idempotence of the "n-locally" predicate, i.e. being "n-locally 𝐴 " is a local property. (Use loclly 23786 to show 𝑛-Locally 𝑛-Locally 𝐴 = 𝑛-Locally 𝐴.) (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ Locally 𝑛-Locally 𝐴 = 𝑛-Locally 𝐴
Theorem	toplly 23789	A topology is locally a topology. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ Locally Top = Top
Theorem	topnlly 23790	A topology is n-locally a topology. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ 𝑛-Locally Top = Top
Theorem	hauslly 23791	A Hausdorff space is locally Hausdorff. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ (𝐽 ∈ Haus → 𝐽 ∈ Locally Haus)
Theorem	hausnlly 23792	A Hausdorff space is n-locally Hausdorff iff it is locally Hausdorff (both notions are thus referred to as "locally Hausdorff"). (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ (𝐽 ∈ 𝑛-Locally Haus ↔ 𝐽 ∈ Locally Haus)
Theorem	hausllycmp 23793	A compact Hausdorff space is locally compact. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ ((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) → 𝐽 ∈ 𝑛-Locally Comp)
Theorem	cldllycmp 23794	A closed subspace of a locally compact space is also locally compact. (The analogous result for open subspaces follows from the more general nllyrest 23785.) (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ ((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐽 ↾t 𝐴) ∈ 𝑛-Locally Comp)
Theorem	lly1stc 23795	First-countability is a local property (unlike second-countability). (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ Locally 1stω = 1stω
Theorem	dislly 23796*	The discrete space 𝒫 𝑋 is locally 𝐴 if and only if every singleton space has property 𝐴. (Contributed by Mario Carneiro, 20-Mar-2015.)
⊢ (𝑋 ∈ 𝑉 → (𝒫 𝑋 ∈ Locally 𝐴 ↔ ∀𝑥 ∈ 𝑋 𝒫 {𝑥} ∈ 𝐴))
Theorem	disllycmp 23797	A discrete space is locally compact. (Contributed by Mario Carneiro, 20-Mar-2015.)
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ Locally Comp)
Theorem	dis1stc 23798	A discrete space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ 1stω)
Theorem	hausmapdom 23799	If 𝑋 is a first-countable Hausdorff space, then the cardinality of the closure of a set 𝐴 is bounded by ℕ to the power 𝐴. In particular, a first-countable Hausdorff space with a dense subset 𝐴 has cardinality at most 𝐴↑ℕ, and a separable first-countable Hausdorff space has cardinality at most 𝒫 ℕ. (Compare hauspwpwdom 24287 to see a weaker result if the assumption of first-countability is omitted.) (Contributed by Mario Carneiro, 9-Apr-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋) → ((cls‘𝐽)‘𝐴) ≼ (𝐴 ↑m ℕ))
Theorem	hauspwdom 23800	Simplify the cardinal 𝐴↑ℕ of hausmapdom 23799 to 𝒫 𝐵 = 2↑𝐵 when 𝐵 is an infinite cardinal greater than 𝐴. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → ((cls‘𝐽)‘𝐴) ≼ 𝒫 𝐵)