P. 341 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34001-34100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	iscref 34001*	The property that every open cover has an 𝐴 refinement for the topological space 𝐽. (Contributed by Thierry Arnoux, 7-Jan-2020.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ CovHasRef𝐴 ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝐽 ∩ 𝐴)𝑧Ref𝑦)))
Theorem	crefeq 34002	Equality theorem for the "every open cover has an A refinement" predicate. (Contributed by Thierry Arnoux, 7-Jan-2020.)
⊢ (𝐴 = 𝐵 → CovHasRef𝐴 = CovHasRef𝐵)
Theorem	creftop 34003	A space where every open cover has an 𝐴 refinement is a topological space. (Contributed by Thierry Arnoux, 7-Jan-2020.)
⊢ (𝐽 ∈ CovHasRef𝐴 → 𝐽 ∈ Top)
Theorem	crefi 34004*	The property that every open cover has an 𝐴 refinement for the topological space 𝐽. (Contributed by Thierry Arnoux, 7-Jan-2020.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ CovHasRef𝐴 ∧ 𝐶 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝐶) → ∃𝑧 ∈ (𝒫 𝐽 ∩ 𝐴)𝑧Ref𝐶)
Theorem	crefdf 34005*	A formulation of crefi 34004 easier to use for definitions. (Contributed by Thierry Arnoux, 7-Jan-2020.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐵 = CovHasRef𝐴    &   ⊢ (𝑧 ∈ 𝐴 → 𝜑)    ⇒   ⊢ ((𝐽 ∈ 𝐵 ∧ 𝐶 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝐶) → ∃𝑧 ∈ 𝒫 𝐽(𝜑 ∧ 𝑧Ref𝐶))
Theorem	crefss 34006	The "every open cover has an 𝐴 refinement" predicate respects inclusion. (Contributed by Thierry Arnoux, 7-Jan-2020.)
⊢ (𝐴 ⊆ 𝐵 → CovHasRef𝐴 ⊆ CovHasRef𝐵)
Theorem	cmpcref 34007	Equivalent definition of compact space in terms of open cover refinements. Compact spaces are topologies with finite open cover refinements. (Contributed by Thierry Arnoux, 7-Jan-2020.)
⊢ Comp = CovHasRefFin
Theorem	cmpfiref 34008*	Every open cover of a Compact space has a finite refinement. (Contributed by Thierry Arnoux, 1-Feb-2020.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Comp ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈) → ∃𝑣 ∈ 𝒫 𝐽(𝑣 ∈ Fin ∧ 𝑣Ref𝑈))
21.3.14.5  Lindelöf spaces
Syntax	cldlf 34009	Extend class notation with the class of all Lindelöf spaces.
class Ldlf
Definition	df-ldlf 34010	Definition of a Lindelöf space. A Lindelöf space is a topological space in which every open cover has a countable subcover. Definition 1 of [BourbakiTop2] p. 195. (Contributed by Thierry Arnoux, 30-Jan-2020.)
⊢ Ldlf = CovHasRef{𝑥 ∣ 𝑥 ≼ ω}
Theorem	ldlfcntref 34011*	Every open cover of a Lindelöf space has a countable refinement. (Contributed by Thierry Arnoux, 1-Feb-2020.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Ldlf ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈) → ∃𝑣 ∈ 𝒫 𝐽(𝑣 ≼ ω ∧ 𝑣Ref𝑈))
21.3.14.6  Paracompact spaces
Syntax	cpcmp 34012	Extend class notation with the class of all paracompact topologies.
class Paracomp
Definition	df-pcmp 34013	Definition of a paracompact topology. A topology is said to be paracompact iff every open cover has an open refinement that is locally finite. The definition 6 of [BourbakiTop1] p. I.69. also requires the topology to be Hausdorff, but this is dropped here. (Contributed by Thierry Arnoux, 7-Jan-2020.)
⊢ Paracomp = {𝑗 ∣ 𝑗 ∈ CovHasRef(LocFin‘𝑗)}
Theorem	ispcmp 34014	The predicate "is a paracompact topology". (Contributed by Thierry Arnoux, 7-Jan-2020.)
⊢ (𝐽 ∈ Paracomp ↔ 𝐽 ∈ CovHasRef(LocFin‘𝐽))
Theorem	cmppcmp 34015	Every compact space is paracompact. (Contributed by Thierry Arnoux, 7-Jan-2020.)
⊢ (𝐽 ∈ Comp → 𝐽 ∈ Paracomp)
Theorem	dispcmp 34016	Every discrete space is paracompact. (Contributed by Thierry Arnoux, 7-Jan-2020.)
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ Paracomp)
Theorem	pcmplfin 34017*	Given a paracompact topology 𝐽 and an open cover 𝑈, there exists an open refinement 𝑣 that is locally finite. (Contributed by Thierry Arnoux, 31-Jan-2020.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Paracomp ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈) → ∃𝑣 ∈ 𝒫 𝐽(𝑣 ∈ (LocFin‘𝐽) ∧ 𝑣Ref𝑈))
Theorem	pcmplfinf 34018*	Given a paracompact topology 𝐽 and an open cover 𝑈, there exists an open refinement ran 𝑓 that is locally finite, using the same index as the original cover 𝑈. (Contributed by Thierry Arnoux, 31-Jan-2020.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Paracomp ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈) → ∃𝑓(𝑓:𝑈⟶𝐽 ∧ ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)))
21.3.14.7  Spectrum of a ring The prime ideals of a ring 𝑅 can be endowed with the Zariski topology. This is done by defining a function 𝑉 which maps ideals of 𝑅 to closed sets (see for example zarcls0 34025 for the definition of 𝑉). The closed sets of the topology are in the range of 𝑉 (see zartopon 34034). The correspondence with the open sets is made in zarcls 34031. As proved in zart0 34036, the Zariski topology is T0 , but generally not T1 .
Syntax	crspec 34019	Extend class notation with the spectrum of a ring.
class Spec
Definition	df-rspec 34020	Define the spectrum of a ring. (Contributed by Thierry Arnoux, 21-Jan-2024.)
⊢ Spec = (𝑟 ∈ Ring ↦ ((IDLsrg‘𝑟) ↾s (PrmIdeal‘𝑟)))
Theorem	rspecval 34021	Value of the spectrum of the ring 𝑅. Notation 1.1.1 of [EGA] p. 80. (Contributed by Thierry Arnoux, 2-Jun-2024.)
⊢ (𝑅 ∈ Ring → (Spec‘𝑅) = ((IDLsrg‘𝑅) ↾s (PrmIdeal‘𝑅)))
Theorem	rspecbas 34022	The prime ideals form the base of the spectrum of a ring. (Contributed by Thierry Arnoux, 2-Jun-2024.)
⊢ 𝑆 = (Spec‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (PrmIdeal‘𝑅) = (Base‘𝑆))
Theorem	rspectset 34023*	Topology component of the spectrum of a ring. (Contributed by Thierry Arnoux, 2-Jun-2024.)
⊢ 𝑆 = (Spec‘𝑅)    &   ⊢ 𝐼 = (LIdeal‘𝑅)    &   ⊢ 𝐽 = ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})    ⇒   ⊢ (𝑅 ∈ Ring → 𝐽 = (TopSet‘𝑆))
Theorem	rspectopn 34024*	The topology component of the spectrum of a ring. (Contributed by Thierry Arnoux, 4-Jun-2024.)
⊢ 𝑆 = (Spec‘𝑅)    &   ⊢ 𝐼 = (LIdeal‘𝑅)    &   ⊢ 𝑃 = (PrmIdeal‘𝑅)    &   ⊢ 𝐽 = ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗})    ⇒   ⊢ (𝑅 ∈ Ring → 𝐽 = (TopOpen‘𝑆))
Theorem	zarcls0 34025*	The closure of the identity ideal in the Zariski topology. Proposition 1.1.2(i) of [EGA] p. 80. (Contributed by Thierry Arnoux, 16-Jun-2024.)
⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗})    &   ⊢ 𝑃 = (PrmIdeal‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝑅 ∈ Ring → (𝑉‘{ 0 }) = 𝑃)
Theorem	zarcls1 34026*	The unit ideal 𝐵 is the only ideal whose closure in the Zariski topology is the empty set. Stronger form of the Proposition 1.1.2(i) of [EGA] p. 80. (Contributed by Thierry Arnoux, 16-Jun-2024.)
⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗})    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → ((𝑉‘𝐼) = ∅ ↔ 𝐼 = 𝐵))
Theorem	zarclsun 34027*	The union of two closed sets of the Zariski topology is closed. (Contributed by Thierry Arnoux, 16-Jun-2024.)
⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗})    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ ran 𝑉 ∧ 𝑌 ∈ ran 𝑉) → (𝑋 ∪ 𝑌) ∈ ran 𝑉)
Theorem	zarclsiin 34028*	In a Zariski topology, the intersection of the closures of a family of ideals is the closure of the span of their union. (Contributed by Thierry Arnoux, 16-Jun-2024.)
⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗})    &   ⊢ 𝐾 = (RSpan‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) → ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙) = (𝑉‘(𝐾‘∪ 𝑇)))
Theorem	zarclsint 34029*	The intersection of a family of closed sets is closed in the Zariski topology. (Contributed by Thierry Arnoux, 16-Jun-2024.)
⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗})    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ∧ 𝑆 ≠ ∅) → ∩ 𝑆 ∈ ran 𝑉)
Theorem	zarclssn 34030*	The closed points of Zariski topology are the maximal ideals. (Contributed by Thierry Arnoux, 16-Jun-2024.)
⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗})    &   ⊢ 𝐵 = (LIdeal‘𝑅)    ⇒   ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ({𝑀} = (𝑉‘𝑀) ↔ 𝑀 ∈ (MaxIdeal‘𝑅)))
Theorem	zarcls 34031*	The open sets of the Zariski topology are the complements of the closed sets. (Contributed by Thierry Arnoux, 16-Jun-2024.)
⊢ 𝑆 = (Spec‘𝑅)    &   ⊢ 𝐽 = (TopOpen‘𝑆)    &   ⊢ 𝑃 = (PrmIdeal‘𝑅)    &   ⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗})    ⇒   ⊢ (𝑅 ∈ Ring → 𝐽 = {𝑠 ∈ 𝒫 𝑃 ∣ (𝑃 ∖ 𝑠) ∈ ran 𝑉})
Theorem	zartopn 34032*	The Zariski topology is a topology, and its closed sets are images by 𝑉 of the ideals of 𝑅. (Contributed by Thierry Arnoux, 16-Jun-2024.)
⊢ 𝑆 = (Spec‘𝑅)    &   ⊢ 𝐽 = (TopOpen‘𝑆)    &   ⊢ 𝑃 = (PrmIdeal‘𝑅)    &   ⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗})    ⇒   ⊢ (𝑅 ∈ CRing → (𝐽 ∈ (TopOn‘𝑃) ∧ ran 𝑉 = (Clsd‘𝐽)))
Theorem	zartop 34033	The Zariski topology is a topology. Proposition 1.1.2 of [EGA] p. 80. (Contributed by Thierry Arnoux, 16-Jun-2024.)
⊢ 𝑆 = (Spec‘𝑅)    &   ⊢ 𝐽 = (TopOpen‘𝑆)    ⇒   ⊢ (𝑅 ∈ CRing → 𝐽 ∈ Top)
Theorem	zartopon 34034	The points of the Zariski topology are the prime ideals. (Contributed by Thierry Arnoux, 16-Jun-2024.)
⊢ 𝑆 = (Spec‘𝑅)    &   ⊢ 𝐽 = (TopOpen‘𝑆)    &   ⊢ 𝑃 = (PrmIdeal‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → 𝐽 ∈ (TopOn‘𝑃))
Theorem	zar0ring 34035	The Zariski Topology of the trivial ring. (Contributed by Thierry Arnoux, 1-Jul-2024.)
⊢ 𝑆 = (Spec‘𝑅)    &   ⊢ 𝐽 = (TopOpen‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Ring ∧ (♯‘𝐵) = 1) → 𝐽 = {∅})
Theorem	zart0 34036	The Zariski topology is T0 . Corollary 1.1.8 of [EGA] p. 81. (Contributed by Thierry Arnoux, 16-Jun-2024.)
⊢ 𝑆 = (Spec‘𝑅)    &   ⊢ 𝐽 = (TopOpen‘𝑆)    ⇒   ⊢ (𝑅 ∈ CRing → 𝐽 ∈ Kol2)
Theorem	zarmxt1 34037	The Zariski topology restricted to maximal ideals is T1 . (Contributed by Thierry Arnoux, 16-Jun-2024.)
⊢ 𝑆 = (Spec‘𝑅)    &   ⊢ 𝐽 = (TopOpen‘𝑆)    &   ⊢ 𝑀 = (MaxIdeal‘𝑅)    &   ⊢ 𝑇 = (𝐽 ↾t 𝑀)    ⇒   ⊢ (𝑅 ∈ CRing → 𝑇 ∈ Fre)
Theorem	zarcmplem 34038*	Lemma for zarcmp 34039. (Contributed by Thierry Arnoux, 2-Jul-2024.)
⊢ 𝑆 = (Spec‘𝑅)    &   ⊢ 𝐽 = (TopOpen‘𝑆)    &   ⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗})    ⇒   ⊢ (𝑅 ∈ CRing → 𝐽 ∈ Comp)
Theorem	zarcmp 34039	The Zariski topology is compact. Proposition 1.1.10(ii) of [EGA], p. 82. (Contributed by Thierry Arnoux, 2-Jul-2024.)
⊢ 𝑆 = (Spec‘𝑅)    &   ⊢ 𝐽 = (TopOpen‘𝑆)    ⇒   ⊢ (𝑅 ∈ CRing → 𝐽 ∈ Comp)
Theorem	rspectps 34040	The spectrum of a ring 𝑅 is a topological space. (Contributed by Thierry Arnoux, 16-Jun-2024.)
⊢ 𝑆 = (Spec‘𝑅)    ⇒   ⊢ (𝑅 ∈ CRing → 𝑆 ∈ TopSp)
Theorem	rhmpreimacnlem 34041*	Lemma for rhmpreimacn 34042. (Contributed by Thierry Arnoux, 7-Jul-2024.)
⊢ 𝑇 = (Spec‘𝑅)    &   ⊢ 𝑈 = (Spec‘𝑆)    &   ⊢ 𝐴 = (PrmIdeal‘𝑅)    &   ⊢ 𝐵 = (PrmIdeal‘𝑆)    &   ⊢ 𝐽 = (TopOpen‘𝑇)    &   ⊢ 𝐾 = (TopOpen‘𝑈)    &   ⊢ 𝐺 = (𝑖 ∈ 𝐵 ↦ (◡𝐹 “ 𝑖))    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))    &   ⊢ (𝜑 → ran 𝐹 = (Base‘𝑆))    &   ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅))    &   ⊢ 𝑉 = (𝑗 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑗 ⊆ 𝑘})    &   ⊢ 𝑊 = (𝑗 ∈ (LIdeal‘𝑆) ↦ {𝑘 ∈ 𝐵 ∣ 𝑗 ⊆ 𝑘})    ⇒   ⊢ (𝜑 → (𝑊‘(𝐹 “ 𝐼)) = (◡𝐺 “ (𝑉‘𝐼)))
Theorem	rhmpreimacn 34042*	The function mapping a prime ideal to its preimage by a surjective ring homomorphism is continuous, when considering the Zariski topology. Corollary 1.2.3 of [EGA], p. 83. Notice that the direction of the continuous map 𝐺 is reverse: the original ring homomorphism 𝐹 goes from 𝑅 to 𝑆, but the continuous map 𝐺 goes from 𝐵 to 𝐴. This mapping is also called "induced map on prime spectra" or "pullback on primes". (Contributed by Thierry Arnoux, 8-Jul-2024.)
⊢ 𝑇 = (Spec‘𝑅)    &   ⊢ 𝑈 = (Spec‘𝑆)    &   ⊢ 𝐴 = (PrmIdeal‘𝑅)    &   ⊢ 𝐵 = (PrmIdeal‘𝑆)    &   ⊢ 𝐽 = (TopOpen‘𝑇)    &   ⊢ 𝐾 = (TopOpen‘𝑈)    &   ⊢ 𝐺 = (𝑖 ∈ 𝐵 ↦ (◡𝐹 “ 𝑖))    &   ⊢ (𝜑 → 𝑅 ∈ CRing)    &   ⊢ (𝜑 → 𝑆 ∈ CRing)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))    &   ⊢ (𝜑 → ran 𝐹 = (Base‘𝑆))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽))
21.3.14.8  Pseudometrics
Syntax	cmetid 34043	Extend class notation with the class of metric identifications.
class ~Met
Syntax	cpstm 34044	Extend class notation with the metric induced by a pseudometric.
class pstoMet
Definition	df-metid 34045*	Define the metric identification relation for a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ ~Met = (𝑑 ∈ ∪ ran PsMet ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0)})
Definition	df-pstm 34046*	Define the metric induced by a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ pstoMet = (𝑑 ∈ ∪ ran PsMet ↦ (𝑎 ∈ (dom dom 𝑑 / (~Met‘𝑑)), 𝑏 ∈ (dom dom 𝑑 / (~Met‘𝑑)) ↦ ∪ {𝑧 ∣ ∃𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝑧 = (𝑥𝑑𝑦)}))
Theorem	metidval 34047*	Value of the metric identification relation. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ (𝐷 ∈ (PsMet‘𝑋) → (~Met‘𝐷) = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑥𝐷𝑦) = 0)})
Theorem	metidss 34048	As a relation, the metric identification is a subset of a Cartesian product. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ (𝐷 ∈ (PsMet‘𝑋) → (~Met‘𝐷) ⊆ (𝑋 × 𝑋))
Theorem	metidv 34049	𝐴 and 𝐵 identify by the metric 𝐷 if their distance is zero. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴(~Met‘𝐷)𝐵 ↔ (𝐴𝐷𝐵) = 0))
Theorem	metideq 34050	Basic property of the metric identification relation. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐴𝐷𝐸) = (𝐵𝐷𝐹))
Theorem	metider 34051	The metric identification is an equivalence relation. (Contributed by Thierry Arnoux, 11-Feb-2018.)
⊢ (𝐷 ∈ (PsMet‘𝑋) → (~Met‘𝐷) Er 𝑋)
Theorem	pstmval 34052*	Value of the metric induced by a pseudometric 𝐷. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ ∼ = (~Met‘𝐷)    ⇒   ⊢ (𝐷 ∈ (PsMet‘𝑋) → (pstoMet‘𝐷) = (𝑎 ∈ (𝑋 / ∼ ), 𝑏 ∈ (𝑋 / ∼ ) ↦ ∪ {𝑧 ∣ ∃𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝑧 = (𝑥𝐷𝑦)}))
Theorem	pstmfval 34053	Function value of the metric induced by a pseudometric 𝐷 (Contributed by Thierry Arnoux, 11-Feb-2018.)
⊢ ∼ = (~Met‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ([𝐴] ∼ (pstoMet‘𝐷)[𝐵] ∼ ) = (𝐴𝐷𝐵))
Theorem	pstmxmet 34054	The metric induced by a pseudometric is a full-fledged metric on the equivalence classes of the metric identification. (Contributed by Thierry Arnoux, 11-Feb-2018.)
⊢ ∼ = (~Met‘𝐷)    ⇒   ⊢ (𝐷 ∈ (PsMet‘𝑋) → (pstoMet‘𝐷) ∈ (∞Met‘(𝑋 / ∼ )))
21.3.14.9  Continuity - misc additions
Theorem	hauseqcn 34055	In a Hausdorff topology, two continuous functions which agree on a dense set agree everywhere. (Contributed by Thierry Arnoux, 28-Dec-2017.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐾 ∈ Haus)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → (𝐹 ↾ 𝐴) = (𝐺 ↾ 𝐴))    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑋)    &   ⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = 𝑋)    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
21.3.14.10  Topology of the closed unit interval
Theorem	elunitge0 34056	An element of the closed unit interval is positive. Useful lemma for manipulating probabilities within the closed unit interval. (Contributed by Thierry Arnoux, 20-Dec-2016.)
⊢ (𝐴 ∈ (0[,]1) → 0 ≤ 𝐴)
Theorem	unitssxrge0 34057	The closed unit interval is a subset of the set of the extended nonnegative reals. Useful lemma for manipulating probabilities within the closed unit interval. (Contributed by Thierry Arnoux, 12-Dec-2016.)
⊢ (0[,]1) ⊆ (0[,]+∞)
Theorem	unitdivcld 34058	Necessary conditions for a quotient to be in the closed unit interval. (somewhat too strong, it would be sufficient that A and B are in RR+) (Contributed by Thierry Arnoux, 20-Dec-2016.)
⊢ ((𝐴 ∈ (0[,]1) ∧ 𝐵 ∈ (0[,]1) ∧ 𝐵 ≠ 0) → (𝐴 ≤ 𝐵 ↔ (𝐴 / 𝐵) ∈ (0[,]1)))
Theorem	iistmd 34059	The closed unit interval forms a topological monoid under multiplication. (Contributed by Thierry Arnoux, 25-Mar-2017.)
⊢ 𝐼 = ((mulGrp‘ℂfld) ↾s (0[,]1))    ⇒   ⊢ 𝐼 ∈ TopMnd
21.3.14.11  Topology of ` ( RR X. RR ) `
Theorem	unicls 34060	The union of the closed set is the underlying set of the topology. (Contributed by Thierry Arnoux, 21-Sep-2017.)
⊢ 𝐽 ∈ Top    &   ⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ∪ (Clsd‘𝐽) = 𝑋
Theorem	tpr2tp 34061	The usual topology on (ℝ × ℝ) is the product topology of the usual topology on ℝ. (Contributed by Thierry Arnoux, 21-Sep-2017.)
⊢ 𝐽 = (topGen‘ran (,))    ⇒   ⊢ (𝐽 ×t 𝐽) ∈ (TopOn‘(ℝ × ℝ))
Theorem	tpr2uni 34062	The usual topology on (ℝ × ℝ) is the product topology of the usual topology on ℝ. (Contributed by Thierry Arnoux, 21-Sep-2017.)
⊢ 𝐽 = (topGen‘ran (,))    ⇒   ⊢ ∪ (𝐽 ×t 𝐽) = (ℝ × ℝ)
Theorem	xpinpreima 34063	Rewrite the cartesian product of two sets as the intersection of their preimage by 1st and 2nd, the projections on the first and second elements. (Contributed by Thierry Arnoux, 22-Sep-2017.)
⊢ (𝐴 × 𝐵) = ((◡(1st ↾ (V × V)) “ 𝐴) ∩ (◡(2nd ↾ (V × V)) “ 𝐵))
Theorem	xpinpreima2 34064	Rewrite the cartesian product of two sets as the intersection of their preimage by 1st and 2nd, the projections on the first and second elements. (Contributed by Thierry Arnoux, 22-Sep-2017.)
⊢ ((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) → (𝐴 × 𝐵) = ((◡(1st ↾ (𝐸 × 𝐹)) “ 𝐴) ∩ (◡(2nd ↾ (𝐸 × 𝐹)) “ 𝐵)))
Theorem	sqsscirc1 34065	The complex square of side 𝐷 is a subset of the complex circle of radius 𝐷. (Contributed by Thierry Arnoux, 25-Sep-2017.)
⊢ ((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ+) → ((𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2)) → (√‘((𝑋↑2) + (𝑌↑2))) < 𝐷))
Theorem	sqsscirc2 34066	The complex square of side 𝐷 is a subset of the complex disc of radius 𝐷. (Contributed by Thierry Arnoux, 25-Sep-2017.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝐷 ∈ ℝ+) → (((abs‘(ℜ‘(𝐵 − 𝐴))) < (𝐷 / 2) ∧ (abs‘(ℑ‘(𝐵 − 𝐴))) < (𝐷 / 2)) → (abs‘(𝐵 − 𝐴)) < 𝐷))
Theorem	cnre2csqlem 34067*	Lemma for cnre2csqima 34068. (Contributed by Thierry Arnoux, 27-Sep-2017.)
⊢ (𝐺 ↾ (ℝ × ℝ)) = (𝐻 ∘ 𝐹)    &   ⊢ 𝐹 Fn (ℝ × ℝ)    &   ⊢ 𝐺 Fn V    &   ⊢ (𝑥 ∈ (ℝ × ℝ) → (𝐺‘𝑥) ∈ ℝ)    &   ⊢ ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹) → (𝐻‘(𝑥 − 𝑦)) = ((𝐻‘𝑥) − (𝐻‘𝑦)))    ⇒   ⊢ ((𝑋 ∈ (ℝ × ℝ) ∧ 𝑌 ∈ (ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (𝑌 ∈ (◡(𝐺 ↾ (ℝ × ℝ)) “ (((𝐺‘𝑋) − 𝐷)(,)((𝐺‘𝑋) + 𝐷))) → (abs‘(𝐻‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷))
Theorem	cnre2csqima 34068*	Image of a centered square by the canonical bijection from (ℝ × ℝ) to ℂ. (Contributed by Thierry Arnoux, 27-Sep-2017.)
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦)))    ⇒   ⊢ ((𝑋 ∈ (ℝ × ℝ) ∧ 𝑌 ∈ (ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (𝑌 ∈ ((((1st ‘𝑋) − 𝐷)(,)((1st ‘𝑋) + 𝐷)) × (((2nd ‘𝑋) − 𝐷)(,)((2nd ‘𝑋) + 𝐷))) → ((abs‘(ℜ‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷 ∧ (abs‘(ℑ‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷)))
Theorem	tpr2rico 34069*	For any point of an open set of the usual topology on (ℝ × ℝ) there is an open square which contains that point and is entirely in the open set. This is square is actually a ball by the (𝑙↑+∞) norm 𝑋. (Contributed by Thierry Arnoux, 21-Sep-2017.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ 𝐺 = (𝑢 ∈ ℝ, 𝑣 ∈ ℝ ↦ (𝑢 + (i · 𝑣)))    &   ⊢ 𝐵 = ran (𝑥 ∈ ran (,), 𝑦 ∈ ran (,) ↦ (𝑥 × 𝑦))    ⇒   ⊢ ((𝐴 ∈ (𝐽 ×t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∃𝑟 ∈ 𝐵 (𝑋 ∈ 𝑟 ∧ 𝑟 ⊆ 𝐴))
21.3.14.12  Order topology - misc. additions
Theorem	cnvordtrestixx 34070*	The restriction of the 'greater than' order to an interval gives the same topology as the subspace topology. (Contributed by Thierry Arnoux, 1-Apr-2017.)
⊢ 𝐴 ⊆ ℝ*    &   ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥[,]𝑦) ⊆ 𝐴)    ⇒   ⊢ ((ordTop‘ ≤ ) ↾t 𝐴) = (ordTop‘(◡ ≤ ∩ (𝐴 × 𝐴)))
Theorem	prsdm 34071	Domain of the relation of a proset. (Contributed by Thierry Arnoux, 11-Sep-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    ⇒   ⊢ (𝐾 ∈ Proset → dom ≤ = 𝐵)
Theorem	prsrn 34072	Range of the relation of a proset. (Contributed by Thierry Arnoux, 11-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    ⇒   ⊢ (𝐾 ∈ Proset → ran ≤ = 𝐵)
Theorem	prsss 34073	Relation of a subproset. (Contributed by Thierry Arnoux, 13-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    ⇒   ⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → ( ≤ ∩ (𝐴 × 𝐴)) = ((le‘𝐾) ∩ (𝐴 × 𝐴)))
Theorem	prsssdm 34074	Domain of a subproset relation. (Contributed by Thierry Arnoux, 12-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    ⇒   ⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → dom ( ≤ ∩ (𝐴 × 𝐴)) = 𝐴)
Theorem	ordtprsval 34075*	Value of the order topology for a proset. (Contributed by Thierry Arnoux, 11-Sep-2015.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    &   ⊢ 𝐸 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})    &   ⊢ 𝐹 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})    ⇒   ⊢ (𝐾 ∈ Proset → (ordTop‘ ≤ ) = (topGen‘(fi‘({𝐵} ∪ (𝐸 ∪ 𝐹)))))
Theorem	ordtprsuni 34076*	Value of the order topology. (Contributed by Thierry Arnoux, 13-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    &   ⊢ 𝐸 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥})    &   ⊢ 𝐹 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦})    ⇒   ⊢ (𝐾 ∈ Proset → 𝐵 = ∪ ({𝐵} ∪ (𝐸 ∪ 𝐹)))
Theorem	ordtcnvNEW 34077	The order dual generates the same topology as the original order. (Contributed by Mario Carneiro, 3-Sep-2015.) (Revised by Thierry Arnoux, 13-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    ⇒   ⊢ (𝐾 ∈ Proset → (ordTop‘◡ ≤ ) = (ordTop‘ ≤ ))
Theorem	ordtrestNEW 34078	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.) (Revised by Thierry Arnoux, 11-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    ⇒   ⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ⊆ ((ordTop‘ ≤ ) ↾t 𝐴))
Theorem	ordtrest2NEWlem 34079*	Lemma for ordtrest2NEW 34080. (Contributed by Mario Carneiro, 9-Sep-2015.) (Revised by Thierry Arnoux, 11-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    &   ⊢ (𝜑 → 𝐾 ∈ Toset)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝐵 ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)} ⊆ 𝐴)    ⇒   ⊢ (𝜑 → ∀𝑣 ∈ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴))))
Theorem	ordtrest2NEW 34080*	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.) (Revised by Thierry Arnoux, 11-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    &   ⊢ (𝜑 → 𝐾 ∈ Toset)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝐵 ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)} ⊆ 𝐴)    ⇒   ⊢ (𝜑 → (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) = ((ordTop‘ ≤ ) ↾t 𝐴))
Theorem	ordtconnlem1 34081*	Connectedness in the order topology of a toset. This is the "easy" direction of ordtconn 34082. See also reconnlem1 24771. (Contributed by Thierry Arnoux, 14-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    &   ⊢ 𝐽 = (ordTop‘ ≤ )    ⇒   ⊢ ((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) → ((𝐽 ↾t 𝐴) ∈ Conn → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴)))
Theorem	ordtconn 34082	Connectedness in the order topology of a complete uniform totally ordered space. (Contributed by Thierry Arnoux, 15-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    &   ⊢ 𝐽 = (ordTop‘ ≤ )    ⇒   ⊢ ⊤
21.3.14.13  Continuity in topological spaces - misc. additions
Theorem	mndpluscn 34083*	A mapping that is both a homeomorphism and a monoid homomorphism preserves the "continuousness" of the operation. (Contributed by Thierry Arnoux, 25-Mar-2017.)
⊢ 𝐹 ∈ (𝐽Homeo𝐾)    &   ⊢ + :(𝐵 × 𝐵)⟶𝐵    &   ⊢ ∗ :(𝐶 × 𝐶)⟶𝐶    &   ⊢ 𝐽 ∈ (TopOn‘𝐵)    &   ⊢ 𝐾 ∈ (TopOn‘𝐶)    &   ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ∗ (𝐹‘𝑦)))    &   ⊢ + ∈ ((𝐽 ×t 𝐽) Cn 𝐽)    ⇒   ⊢ ∗ ∈ ((𝐾 ×t 𝐾) Cn 𝐾)
Theorem	mhmhmeotmd 34084	Deduce a Topological Monoid using mapping that is both a homeomorphism and a monoid homomorphism. (Contributed by Thierry Arnoux, 21-Jun-2017.)
⊢ 𝐹 ∈ (𝑆 MndHom 𝑇)    &   ⊢ 𝐹 ∈ ((TopOpen‘𝑆)Homeo(TopOpen‘𝑇))    &   ⊢ 𝑆 ∈ TopMnd    &   ⊢ 𝑇 ∈ TopSp    ⇒   ⊢ 𝑇 ∈ TopMnd
Theorem	rmulccn 34085*	Multiplication by a real constant is a continuous function. (Contributed by Thierry Arnoux, 23-May-2017.) Avoid ax-mulf 11106. (Revised by GG, 16-Mar-2025.)
⊢ 𝐽 = (topGen‘ran (,))    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 · 𝐶)) ∈ (𝐽 Cn 𝐽))
Theorem	raddcn 34086*	Addition in the real numbers is a continuous function. (Contributed by Thierry Arnoux, 23-May-2017.)
⊢ 𝐽 = (topGen‘ran (,))    ⇒   ⊢ (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + 𝑦)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽)
Theorem	xrmulc1cn 34087*	The operation multiplying an extended real number by a nonnegative constant is continuous. (Contributed by Thierry Arnoux, 5-Jul-2017.)
⊢ 𝐽 = (ordTop‘ ≤ )    &   ⊢ 𝐹 = (𝑥 ∈ ℝ* ↦ (𝑥 ·e 𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ ℝ+)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐽))
Theorem	fmcncfil 34088	The image of a Cauchy filter by a continuous filter map is a Cauchy filter. (Contributed by Thierry Arnoux, 12-Nov-2017.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐾 = (MetOpen‘𝐸)    ⇒   ⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝐸 ∈ (∞Met‘𝑌) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝐵 ∈ (CauFil‘𝐷)) → ((𝑌 FilMap 𝐹)‘𝐵) ∈ (CauFil‘𝐸))
21.3.14.14  Topology of the extended nonnegative real numbers ordered monoid
Theorem	xrge0hmph 34089	The extended nonnegative reals are homeomorphic to the closed unit interval. (Contributed by Thierry Arnoux, 24-Mar-2017.)
⊢ II ≃ ((ordTop‘ ≤ ) ↾t (0[,]+∞))
Theorem	xrge0iifcnv 34090*	Define a bijection from [0, 1] onto [0, +∞]. (Contributed by Thierry Arnoux, 29-Mar-2017.)
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 0, +∞, -(log‘𝑥)))    ⇒   ⊢ (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) ∧ ◡𝐹 = (𝑦 ∈ (0[,]+∞) ↦ if(𝑦 = +∞, 0, (exp‘-𝑦))))
Theorem	xrge0iifcv 34091*	The defined function's value in the real. (Contributed by Thierry Arnoux, 1-Apr-2017.)
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 0, +∞, -(log‘𝑥)))    ⇒   ⊢ (𝑋 ∈ (0(,]1) → (𝐹‘𝑋) = -(log‘𝑋))
Theorem	xrge0iifiso 34092*	The defined bijection from the closed unit interval onto the extended nonnegative reals is an order isomorphism. (Contributed by Thierry Arnoux, 31-Mar-2017.)
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 0, +∞, -(log‘𝑥)))    ⇒   ⊢ 𝐹 Isom < , ◡ < ((0[,]1), (0[,]+∞))
Theorem	xrge0iifhmeo 34093*	Expose a homeomorphism from the closed unit interval to the extended nonnegative reals. (Contributed by Thierry Arnoux, 1-Apr-2017.)
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 0, +∞, -(log‘𝑥)))    &   ⊢ 𝐽 = ((ordTop‘ ≤ ) ↾t (0[,]+∞))    ⇒   ⊢ 𝐹 ∈ (IIHomeo𝐽)
Theorem	xrge0iifhom 34094*	The defined function from the closed unit interval to the extended nonnegative reals is a monoid homomorphism. (Contributed by Thierry Arnoux, 5-Apr-2017.)
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 0, +∞, -(log‘𝑥)))    &   ⊢ 𝐽 = ((ordTop‘ ≤ ) ↾t (0[,]+∞))    ⇒   ⊢ ((𝑋 ∈ (0[,]1) ∧ 𝑌 ∈ (0[,]1)) → (𝐹‘(𝑋 · 𝑌)) = ((𝐹‘𝑋) +𝑒 (𝐹‘𝑌)))
Theorem	xrge0iif1 34095*	Condition for the defined function, -(log‘𝑥) to be a monoid homomorphism. (Contributed by Thierry Arnoux, 20-Jun-2017.)
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 0, +∞, -(log‘𝑥)))    &   ⊢ 𝐽 = ((ordTop‘ ≤ ) ↾t (0[,]+∞))    ⇒   ⊢ (𝐹‘1) = 0
Theorem	xrge0iifmhm 34096*	The defined function from the closed unit interval to the extended nonnegative reals is a monoid homomorphism. (Contributed by Thierry Arnoux, 21-Jun-2017.)
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 0, +∞, -(log‘𝑥)))    &   ⊢ 𝐽 = ((ordTop‘ ≤ ) ↾t (0[,]+∞))    ⇒   ⊢ 𝐹 ∈ (((mulGrp‘ℂfld) ↾s (0[,]1)) MndHom (ℝ*𝑠 ↾s (0[,]+∞)))
Theorem	xrge0pluscn 34097*	The addition operation of the extended nonnegative real numbers monoid is continuous. (Contributed by Thierry Arnoux, 24-Mar-2017.)
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 0, +∞, -(log‘𝑥)))    &   ⊢ 𝐽 = ((ordTop‘ ≤ ) ↾t (0[,]+∞))    &   ⊢ + = ( +𝑒 ↾ ((0[,]+∞) × (0[,]+∞)))    ⇒   ⊢ + ∈ ((𝐽 ×t 𝐽) Cn 𝐽)
Theorem	xrge0mulc1cn 34098*	The operation multiplying a nonnegative real numbers by a nonnegative constant is continuous. (Contributed by Thierry Arnoux, 6-Jul-2017.)
⊢ 𝐽 = ((ordTop‘ ≤ ) ↾t (0[,]+∞))    &   ⊢ 𝐹 = (𝑥 ∈ (0[,]+∞) ↦ (𝑥 ·e 𝐶))    &   ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐽))
Theorem	xrge0tps 34099	The extended nonnegative real numbers monoid forms a topological space. (Contributed by Thierry Arnoux, 19-Jun-2017.)
⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ TopSp
Theorem	xrge0topn 34100	The topology of the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 20-Jun-2017.)
⊢ (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞))) = ((ordTop‘ ≤ ) ↾t (0[,]+∞))