Home | Metamath
Proof Explorer Theorem List (p. 313 of 454) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28701) |
Hilbert Space Explorer
(28702-30224) |
Users' Mathboxes
(30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | crefdf 31201* | A formulation of crefi 31200 easier to use for definitions. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐵 = CovHasRef𝐴 & ⊢ (𝑧 ∈ 𝐴 → 𝜑) ⇒ ⊢ ((𝐽 ∈ 𝐵 ∧ 𝐶 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝐶) → ∃𝑧 ∈ 𝒫 𝐽(𝜑 ∧ 𝑧Ref𝐶)) | ||
Theorem | crefss 31202 | The "every open cover has an 𝐴 refinement" predicate respects inclusion. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
⊢ (𝐴 ⊆ 𝐵 → CovHasRef𝐴 ⊆ CovHasRef𝐵) | ||
Theorem | cmpcref 31203 | 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 31204* | Every open cover of a Compact space has a finite refinement. (Contributed by Thierry Arnoux, 1-Feb-2020.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Comp ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈) → ∃𝑣 ∈ 𝒫 𝐽(𝑣 ∈ Fin ∧ 𝑣Ref𝑈)) | ||
Syntax | cldlf 31205 | Extend class notation with the class of all Lindelöf spaces. |
class Ldlf | ||
Definition | df-ldlf 31206 | 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 31207* | Every open cover of a Lindelöf space has a countable refinement. (Contributed by Thierry Arnoux, 1-Feb-2020.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Ldlf ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈) → ∃𝑣 ∈ 𝒫 𝐽(𝑣 ≼ ω ∧ 𝑣Ref𝑈)) | ||
Syntax | cpcmp 31208 | Extend class notation with the class of all paracompact topologies. |
class Paracomp | ||
Definition | df-pcmp 31209 | 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 31210 | The predicate "is a paracompact topology". (Contributed by Thierry Arnoux, 7-Jan-2020.) |
⊢ (𝐽 ∈ Paracomp ↔ 𝐽 ∈ CovHasRef(LocFin‘𝐽)) | ||
Theorem | cmppcmp 31211 | Every compact space is paracompact. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
⊢ (𝐽 ∈ Comp → 𝐽 ∈ Paracomp) | ||
Theorem | dispcmp 31212 | Every discrete space is paracompact. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ Paracomp) | ||
Theorem | pcmplfin 31213* | 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 31214* | 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‘𝐽))) | ||
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 31221 for the definition of 𝑉). The closed sets of the topology are in the range of 𝑉 (see zartopon 31230). The correspondence with the open sets is made in zarcls 31227. As proved in zart0 31232, the Zariski topology is T0 , but generally not T1 . | ||
Syntax | crspec 31215 | Extend class notation with the spectrum of a ring. |
class Spec | ||
Definition | df-rspec 31216 | Define the spectrum of a ring. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
⊢ Spec = (𝑟 ∈ Ring ↦ ((IDLsrg‘𝑟) ↾s (PrmIdeal‘𝑟))) | ||
Theorem | rspecval 31217 | 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 31218 | 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 31219* | Topology component of the spectrum of a ring. (Contributed by Thierry Arnoux, 2-Jun-2024.) |
⊢ 𝑆 = (Spec‘𝑅) & ⊢ 𝐼 = (LIdeal‘𝑅) & ⊢ 𝐽 = ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗}) ⇒ ⊢ (𝑅 ∈ Ring → 𝐽 = (TopSet‘𝑆)) | ||
Theorem | rspectopn 31220* | The topology component of the spectrum of a ring. (Contributed by Thierry Arnoux, 4-Jun-2024.) |
⊢ 𝑆 = (Spec‘𝑅) & ⊢ 𝐼 = (LIdeal‘𝑅) & ⊢ 𝑃 = (PrmIdeal‘𝑅) & ⊢ 𝐽 = ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗}) ⇒ ⊢ (𝑅 ∈ Ring → 𝐽 = (TopOpen‘𝑆)) | ||
Theorem | zarcls0 31221* | 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 31222* | 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 31223* | 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 31224* | 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 31225* | 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 31226* | The closed points of Zariski topology are the maximal ideals. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}) & ⊢ 𝐵 = (LIdeal‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ({𝑀} = (𝑉‘𝑀) ↔ 𝑀 ∈ (MaxIdeal‘𝑅))) | ||
Theorem | zarcls 31227* | 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 31228* | 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 31229 | 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 31230 | The points of the Zariski topology are the prime ideals. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
⊢ 𝑆 = (Spec‘𝑅) & ⊢ 𝐽 = (TopOpen‘𝑆) & ⊢ 𝑃 = (PrmIdeal‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → 𝐽 ∈ (TopOn‘𝑃)) | ||
Theorem | zar0ring 31231 | The Zariski Topology of the trivial ring. (Contributed by Thierry Arnoux, 1-Jul-2024.) |
⊢ 𝑆 = (Spec‘𝑅) & ⊢ 𝐽 = (TopOpen‘𝑆) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (♯‘𝐵) = 1) → 𝐽 = {∅}) | ||
Theorem | zart0 31232 | 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 31233 | The Zariski topology restricted to maximal ideals is T1 . (Contributed by Thierry Arnoux, 16-Jun-2024.) |
⊢ 𝑆 = (Spec‘𝑅) & ⊢ 𝐽 = (TopOpen‘𝑆) & ⊢ 𝑀 = (MaxIdeal‘𝑅) & ⊢ 𝑇 = (𝐽 ↾t 𝑀) ⇒ ⊢ (𝑅 ∈ CRing → 𝑇 ∈ Fre) | ||
Theorem | zarcmplem 31234* | Lemma for zarcmp 31235. (Contributed by Thierry Arnoux, 2-Jul-2024.) |
⊢ 𝑆 = (Spec‘𝑅) & ⊢ 𝐽 = (TopOpen‘𝑆) & ⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}) ⇒ ⊢ (𝑅 ∈ CRing → 𝐽 ∈ Comp) | ||
Theorem | zarcmp 31235 | 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 31236 | The spectrum of a ring 𝑅 is a topological space. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
⊢ 𝑆 = (Spec‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → 𝑆 ∈ TopSp) | ||
Theorem | rhmpreimacnlem 31237* | Lemma for rhmpreimacn 31238. (Contributed by Thierry Arnoux, 7-Jul-2024.) |
⊢ 𝑇 = (Spec‘𝑅) & ⊢ 𝑈 = (Spec‘𝑆) & ⊢ 𝐴 = (PrmIdeal‘𝑅) & ⊢ 𝐵 = (PrmIdeal‘𝑆) & ⊢ 𝐽 = (TopOpen‘𝑇) & ⊢ 𝐾 = (TopOpen‘𝑈) & ⊢ 𝐺 = (𝑖 ∈ 𝐵 ↦ (◡𝐹 “ 𝑖)) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆)) & ⊢ (𝜑 → ran 𝐹 = (Base‘𝑆)) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) & ⊢ 𝑉 = (𝑗 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑗 ⊆ 𝑘}) & ⊢ 𝑊 = (𝑗 ∈ (LIdeal‘𝑆) ↦ {𝑘 ∈ 𝐵 ∣ 𝑗 ⊆ 𝑘}) ⇒ ⊢ (𝜑 → (𝑊‘(𝐹 “ 𝐼)) = (◡𝐺 “ (𝑉‘𝐼))) | ||
Theorem | rhmpreimacn 31238* | 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 𝐽)) | ||
Syntax | cmetid 31239 | Extend class notation with the class of metric identifications. |
class ~Met | ||
Syntax | cpstm 31240 | Extend class notation with the metric induced by a pseudometric. |
class pstoMet | ||
Definition | df-metid 31241* | 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 31242* | 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 31243* | Value of the metric identification relation. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
⊢ (𝐷 ∈ (PsMet‘𝑋) → (~Met‘𝐷) = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑥𝐷𝑦) = 0)}) | ||
Theorem | metidss 31244 | As a relation, the metric identification is a subset of a Cartesian product. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
⊢ (𝐷 ∈ (PsMet‘𝑋) → (~Met‘𝐷) ⊆ (𝑋 × 𝑋)) | ||
Theorem | metidv 31245 | 𝐴 and 𝐵 identify by the metric 𝐷 if their distance is zero. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴(~Met‘𝐷)𝐵 ↔ (𝐴𝐷𝐵) = 0)) | ||
Theorem | metideq 31246 | Basic property of the metric identification relation. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐴𝐷𝐸) = (𝐵𝐷𝐹)) | ||
Theorem | metider 31247 | The metric identification is an equivalence relation. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
⊢ (𝐷 ∈ (PsMet‘𝑋) → (~Met‘𝐷) Er 𝑋) | ||
Theorem | pstmval 31248* | Value of the metric induced by a pseudometric 𝐷. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
⊢ ∼ = (~Met‘𝐷) ⇒ ⊢ (𝐷 ∈ (PsMet‘𝑋) → (pstoMet‘𝐷) = (𝑎 ∈ (𝑋 / ∼ ), 𝑏 ∈ (𝑋 / ∼ ) ↦ ∪ {𝑧 ∣ ∃𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝑧 = (𝑥𝐷𝑦)})) | ||
Theorem | pstmfval 31249 | Function value of the metric induced by a pseudometric 𝐷 (Contributed by Thierry Arnoux, 11-Feb-2018.) |
⊢ ∼ = (~Met‘𝐷) ⇒ ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ([𝐴] ∼ (pstoMet‘𝐷)[𝐵] ∼ ) = (𝐴𝐷𝐵)) | ||
Theorem | pstmxmet 31250 | 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‘(𝑋 / ∼ ))) | ||
Theorem | hauseqcn 31251 | 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‘𝐽)‘𝐴) = 𝑋) ⇒ ⊢ (𝜑 → 𝐹 = 𝐺) | ||
Theorem | elunitge0 31252 | 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 31253 | 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 31254 | 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 31255 | The closed unit interval forms a topological monoid under multiplication. (Contributed by Thierry Arnoux, 25-Mar-2017.) |
⊢ 𝐼 = ((mulGrp‘ℂfld) ↾s (0[,]1)) ⇒ ⊢ 𝐼 ∈ TopMnd | ||
Theorem | unicls 31256 | The union of the closed set is the underlying set of the topology. (Contributed by Thierry Arnoux, 21-Sep-2017.) |
⊢ 𝐽 ∈ Top & ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ∪ (Clsd‘𝐽) = 𝑋 | ||
Theorem | tpr2tp 31257 | 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 31258 | 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 31259 | 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 31260 | 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 31261 | 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 31262 | 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 31263* | Lemma for cnre2csqima 31264. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
⊢ (𝐺 ↾ (ℝ × ℝ)) = (𝐻 ∘ 𝐹) & ⊢ 𝐹 Fn (ℝ × ℝ) & ⊢ 𝐺 Fn V & ⊢ (𝑥 ∈ (ℝ × ℝ) → (𝐺‘𝑥) ∈ ℝ) & ⊢ ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹) → (𝐻‘(𝑥 − 𝑦)) = ((𝐻‘𝑥) − (𝐻‘𝑦))) ⇒ ⊢ ((𝑋 ∈ (ℝ × ℝ) ∧ 𝑌 ∈ (ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (𝑌 ∈ (◡(𝐺 ↾ (ℝ × ℝ)) “ (((𝐺‘𝑋) − 𝐷)(,)((𝐺‘𝑋) + 𝐷))) → (abs‘(𝐻‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷)) | ||
Theorem | cnre2csqima 31264* | 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 31265* | 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 𝐽) ∧ 𝑋 ∈ 𝐴) → ∃𝑟 ∈ 𝐵 (𝑋 ∈ 𝑟 ∧ 𝑟 ⊆ 𝐴)) | ||
Theorem | cnvordtrestixx 31266* | 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 31267 | Domain of the relation of a proset. (Contributed by Thierry Arnoux, 11-Sep-2015.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ (𝐾 ∈ Proset → dom ≤ = 𝐵) | ||
Theorem | prsrn 31268 | Range of the relation of a proset. (Contributed by Thierry Arnoux, 11-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ (𝐾 ∈ Proset → ran ≤ = 𝐵) | ||
Theorem | prsss 31269 | Relation of a subproset. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → ( ≤ ∩ (𝐴 × 𝐴)) = ((le‘𝐾) ∩ (𝐴 × 𝐴))) | ||
Theorem | prsssdm 31270 | Domain of a subproset relation. (Contributed by Thierry Arnoux, 12-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → dom ( ≤ ∩ (𝐴 × 𝐴)) = 𝐴) | ||
Theorem | ordtprsval 31271* | 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 31272* | Value of the order topology. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) & ⊢ 𝐸 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) & ⊢ 𝐹 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) ⇒ ⊢ (𝐾 ∈ Proset → 𝐵 = ∪ ({𝐵} ∪ (𝐸 ∪ 𝐹))) | ||
Theorem | ordtcnvNEW 31273 | 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 31274 | 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 31275* | Lemma for ordtrest2NEW 31276. (Contributed by Mario Carneiro, 9-Sep-2015.) (Revised by Thierry Arnoux, 11-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) & ⊢ (𝜑 → 𝐾 ∈ Toset) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝐵 ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)} ⊆ 𝐴) ⇒ ⊢ (𝜑 → ∀𝑣 ∈ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))) | ||
Theorem | ordtrest2NEW 31276* | 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 31277* | Connectedness in the order topology of a toset. This is the "easy" direction of ordtconn 31278. See also reconnlem1 23431. (Contributed by Thierry Arnoux, 14-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) & ⊢ 𝐽 = (ordTop‘ ≤ ) ⇒ ⊢ ((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) → ((𝐽 ↾t 𝐴) ∈ Conn → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))) | ||
Theorem | ordtconn 31278 | Connectedness in the order topology of a complete uniform totally ordered space. (Contributed by Thierry Arnoux, 15-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) & ⊢ 𝐽 = (ordTop‘ ≤ ) ⇒ ⊢ ⊤ | ||
Theorem | mndpluscn 31279* | 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 31280 | 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 31281* | Multiplication by a real constant is a continuous function. (Contributed by Thierry Arnoux, 23-May-2017.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝑥 ∈ ℝ ↦ (𝑥 · 𝐶)) ∈ (𝐽 Cn 𝐽)) | ||
Theorem | raddcn 31282* | Addition in the real numbers is a continuous function. (Contributed by Thierry Arnoux, 23-May-2017.) |
⊢ 𝐽 = (topGen‘ran (,)) ⇒ ⊢ (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + 𝑦)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) | ||
Theorem | xrmulc1cn 31283* | 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 31284 | 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‘𝐸)) | ||
Theorem | xrge0hmph 31285 | The extended nonnegative reals are homeomorphic to the closed unit interval. (Contributed by Thierry Arnoux, 24-Mar-2017.) |
⊢ II ≃ ((ordTop‘ ≤ ) ↾t (0[,]+∞)) | ||
Theorem | xrge0iifcnv 31286* | 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 31287* | 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 31288* | 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 31289* | 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 31290* | 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 31291* | 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 31292* | 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 31293* | 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 31294* | 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 31295 | The extended nonnegative real numbers monoid forms a topological space. (Contributed by Thierry Arnoux, 19-Jun-2017.) |
⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ TopSp | ||
Theorem | xrge0topn 31296 | The topology of the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 20-Jun-2017.) |
⊢ (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞))) = ((ordTop‘ ≤ ) ↾t (0[,]+∞)) | ||
Theorem | xrge0haus 31297 | The topology of the extended nonnegative real numbers is Hausdorff. (Contributed by Thierry Arnoux, 26-Jul-2017.) |
⊢ (TopOpen‘(ℝ*𝑠 ↾s (0[,]+∞))) ∈ Haus | ||
Theorem | xrge0tmd 31298 | The extended nonnegative real numbers monoid is a topological monoid. (Contributed by Thierry Arnoux, 26-Mar-2017.) (Proof Shortened by Thierry Arnoux, 21-Jun-2017.) |
⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ TopMnd | ||
Theorem | xrge0tmdALT 31299 | Alternate proof of xrge0tmd 31298. (Contributed by Thierry Arnoux, 26-Mar-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ TopMnd | ||
Theorem | lmlim 31300 | Relate a limit in a given topology to a complex number limit, provided that topology agrees with the common topology on ℂ on the required subset. (Contributed by Thierry Arnoux, 11-Jul-2017.) |
⊢ 𝐽 ∈ (TopOn‘𝑌) & ⊢ (𝜑 → 𝐹:ℕ⟶𝑋) & ⊢ (𝜑 → 𝑃 ∈ 𝑋) & ⊢ (𝐽 ↾t 𝑋) = ((TopOpen‘ℂfld) ↾t 𝑋) & ⊢ 𝑋 ⊆ ℂ ⇒ ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ 𝐹 ⇝ 𝑃)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |