![]() |
Metamath
Proof Explorer Theorem List (p. 224 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: | ![]() (1-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | qtopval2 22301* | Value of the quotient topology function when 𝐹 is a function on the base set. (Contributed by Mario Carneiro, 23-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐽 qTop 𝐹) = {𝑠 ∈ 𝒫 𝑌 ∣ (◡𝐹 “ 𝑠) ∈ 𝐽}) | ||
Theorem | elqtop 22302 | Value of the quotient topology function. (Contributed by Mario Carneiro, 23-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐴 ∈ (𝐽 qTop 𝐹) ↔ (𝐴 ⊆ 𝑌 ∧ (◡𝐹 “ 𝐴) ∈ 𝐽))) | ||
Theorem | qtopres 22303 | The quotient topology is unaffected by restriction to the base set. This property makes it slightly more convenient to use, since we don't have to require that 𝐹 be a function with domain 𝑋. (Contributed by Mario Carneiro, 23-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐹 ∈ 𝑉 → (𝐽 qTop 𝐹) = (𝐽 qTop (𝐹 ↾ 𝑋))) | ||
Theorem | qtoptop2 22304 | The quotient topology is a topology. (Contributed by Mario Carneiro, 23-Mar-2015.) |
⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) → (𝐽 qTop 𝐹) ∈ Top) | ||
Theorem | qtoptop 22305 | The quotient topology is a topology. (Contributed by Mario Carneiro, 23-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ Top) | ||
Theorem | elqtop2 22306 | Value of the quotient topology function. (Contributed by Mario Carneiro, 9-Apr-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑋–onto→𝑌) → (𝐴 ∈ (𝐽 qTop 𝐹) ↔ (𝐴 ⊆ 𝑌 ∧ (◡𝐹 “ 𝐴) ∈ 𝐽))) | ||
Theorem | qtopuni 22307 | The base set of the quotient topology. (Contributed by Mario Carneiro, 23-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐹:𝑋–onto→𝑌) → 𝑌 = ∪ (𝐽 qTop 𝐹)) | ||
Theorem | elqtop3 22308 | Value of the quotient topology function. (Contributed by Mario Carneiro, 9-Apr-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝐴 ∈ (𝐽 qTop 𝐹) ↔ (𝐴 ⊆ 𝑌 ∧ (◡𝐹 “ 𝐴) ∈ 𝐽))) | ||
Theorem | qtoptopon 22309 | The base set of the quotient topology. (Contributed by Mario Carneiro, 22-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌)) | ||
Theorem | qtopid 22310 | A quotient map is a continuous function into its quotient topology. (Contributed by Mario Carneiro, 23-Mar-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 Fn 𝑋) → 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹))) | ||
Theorem | idqtop 22311 | The quotient topology induced by the identity function is the original topology. (Contributed by Mario Carneiro, 30-Aug-2015.) |
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 qTop ( I ↾ 𝑋)) = 𝐽) | ||
Theorem | qtopcmplem 22312 | Lemma for qtopcmp 22313 and qtopconn 22314. (Contributed by Mario Carneiro, 24-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ (𝐽 ∈ 𝐴 → 𝐽 ∈ Top) & ⊢ ((𝐽 ∈ 𝐴 ∧ 𝐹:𝑋–onto→∪ (𝐽 qTop 𝐹) ∧ 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹))) → (𝐽 qTop 𝐹) ∈ 𝐴) ⇒ ⊢ ((𝐽 ∈ 𝐴 ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ 𝐴) | ||
Theorem | qtopcmp 22313 | A quotient of a compact space is compact. (Contributed by Mario Carneiro, 24-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Comp ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ Comp) | ||
Theorem | qtopconn 22314 | A quotient of a connected space is connected. (Contributed by Mario Carneiro, 24-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Conn ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ Conn) | ||
Theorem | qtopkgen 22315 | A quotient of a compactly generated space is compactly generated. (Contributed by Mario Carneiro, 9-Apr-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ ran 𝑘Gen ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ ran 𝑘Gen) | ||
Theorem | basqtop 22316 | An injection maps bases to bases. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → (𝐽 qTop 𝐹) ∈ TopBases) | ||
Theorem | tgqtop 22317 | An injection maps generated topologies to each other. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → ((topGen‘𝐽) qTop 𝐹) = (topGen‘(𝐽 qTop 𝐹))) | ||
Theorem | qtopcld 22318 | The property of being a closed set in the quotient topology. (Contributed by Mario Carneiro, 24-Mar-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝐴 ∈ (Clsd‘(𝐽 qTop 𝐹)) ↔ (𝐴 ⊆ 𝑌 ∧ (◡𝐹 “ 𝐴) ∈ (Clsd‘𝐽)))) | ||
Theorem | qtopcn 22319 | Universal property of a quotient map. (Contributed by Mario Carneiro, 23-Mar-2015.) |
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) → (𝐺 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ↔ (𝐺 ∘ 𝐹) ∈ (𝐽 Cn 𝐾))) | ||
Theorem | qtopss 22320 | A surjective continuous function from 𝐽 to 𝐾 induces a topology 𝐽 qTop 𝐹 on the base set of 𝐾. This topology is in general finer than 𝐾. Together with qtopid 22310, this implies that 𝐽 qTop 𝐹 is the finest topology making 𝐹 continuous, i.e. the final topology with respect to the family {𝐹}. (Contributed by Mario Carneiro, 24-Mar-2015.) |
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 = 𝑌) → 𝐾 ⊆ (𝐽 qTop 𝐹)) | ||
Theorem | qtopeu 22321* | Universal property of the quotient topology. If 𝐺 is a function from 𝐽 to 𝐾 which is equal on all equivalent elements under 𝐹, then there is a unique continuous map 𝑓:(𝐽 / 𝐹)⟶𝐾 such that 𝐺 = 𝑓 ∘ 𝐹, and we say that 𝐺 "passes to the quotient". (Contributed by Mario Carneiro, 24-Mar-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌) & ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → (𝐺‘𝑥) = (𝐺‘𝑦)) ⇒ ⊢ (𝜑 → ∃!𝑓 ∈ ((𝐽 qTop 𝐹) Cn 𝐾)𝐺 = (𝑓 ∘ 𝐹)) | ||
Theorem | qtoprest 22322 | If 𝐴 is a saturated open or closed set (where saturated means that 𝐴 = (◡𝐹 “ 𝑈) for some 𝑈), then the restriction of the quotient map 𝐹 to 𝐴 is a quotient map. (Contributed by Mario Carneiro, 24-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌) & ⊢ (𝜑 → 𝑈 ⊆ 𝑌) & ⊢ (𝜑 → 𝐴 = (◡𝐹 “ 𝑈)) & ⊢ (𝜑 → (𝐴 ∈ 𝐽 ∨ 𝐴 ∈ (Clsd‘𝐽))) ⇒ ⊢ (𝜑 → ((𝐽 qTop 𝐹) ↾t 𝑈) = ((𝐽 ↾t 𝐴) qTop (𝐹 ↾ 𝐴))) | ||
Theorem | qtopomap 22323* | If 𝐹 is a surjective continuous open map, then it is a quotient map. (An open map is a function that maps open sets to open sets.) (Contributed by Mario Carneiro, 24-Mar-2015.) |
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → ran 𝐹 = 𝑌) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (𝐹 “ 𝑥) ∈ 𝐾) ⇒ ⊢ (𝜑 → 𝐾 = (𝐽 qTop 𝐹)) | ||
Theorem | qtopcmap 22324* | If 𝐹 is a surjective continuous closed map, then it is a quotient map. (A closed map is a function that maps closed sets to closed sets.) (Contributed by Mario Carneiro, 24-Mar-2015.) |
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → ran 𝐹 = 𝑌) & ⊢ ((𝜑 ∧ 𝑥 ∈ (Clsd‘𝐽)) → (𝐹 “ 𝑥) ∈ (Clsd‘𝐾)) ⇒ ⊢ (𝜑 → 𝐾 = (𝐽 qTop 𝐹)) | ||
Theorem | imastopn 22325 | The topology of an image structure. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) & ⊢ 𝐽 = (TopOpen‘𝑅) & ⊢ 𝑂 = (TopOpen‘𝑈) ⇒ ⊢ (𝜑 → 𝑂 = (𝐽 qTop 𝐹)) | ||
Theorem | imastps 22326 | The image of a topological space under a function is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) & ⊢ (𝜑 → 𝑅 ∈ TopSp) ⇒ ⊢ (𝜑 → 𝑈 ∈ TopSp) | ||
Theorem | qustps 22327 | A quotient structure is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ (𝜑 → 𝑈 = (𝑅 /s 𝐸)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐸 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ TopSp) ⇒ ⊢ (𝜑 → 𝑈 ∈ TopSp) | ||
Theorem | kqfval 22328* | Value of the function appearing in df-kq 22299. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) ⇒ ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋) → (𝐹‘𝐴) = {𝑦 ∈ 𝐽 ∣ 𝐴 ∈ 𝑦}) | ||
Theorem | kqfeq 22329* | Two points in the Kolmogorov quotient are equal iff the original points are topologically indistinguishable. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) ⇒ ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐹‘𝐴) = (𝐹‘𝐵) ↔ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 ↔ 𝐵 ∈ 𝑦))) | ||
Theorem | kqffn 22330* | The topological indistinguishability map is a function on the base. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) ⇒ ⊢ (𝐽 ∈ 𝑉 → 𝐹 Fn 𝑋) | ||
Theorem | kqval 22331* | Value of the quotient topology function. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) ⇒ ⊢ (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) = (𝐽 qTop 𝐹)) | ||
Theorem | kqtopon 22332* | The Kolmogorov quotient is a topology on the quotient set. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) ⇒ ⊢ (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹)) | ||
Theorem | kqid 22333* | The topological indistinguishability map is a continuous function into the Kolmogorov quotient. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) ⇒ ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐹 ∈ (𝐽 Cn (KQ‘𝐽))) | ||
Theorem | ist0-4 22334* | The topological indistinguishability map is injective iff the space is T0. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) ⇒ ⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Kol2 ↔ 𝐹:𝑋–1-1→V)) | ||
Theorem | kqfvima 22335* | When the image set is open, the quotient map satisfies a partial converse to fnfvima 6973, which is normally only true for injective functions. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋) → (𝐴 ∈ 𝑈 ↔ (𝐹‘𝐴) ∈ (𝐹 “ 𝑈))) | ||
Theorem | kqsat 22336* | Any open set is saturated with respect to the topological indistinguishability map (in the terminology of qtoprest 22322). (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽) → (◡𝐹 “ (𝐹 “ 𝑈)) = 𝑈) | ||
Theorem | kqdisj 22337* | A version of imain 6409 for the topological indistinguishability map. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽) → ((𝐹 “ 𝑈) ∩ (𝐹 “ (𝐴 ∖ 𝑈))) = ∅) | ||
Theorem | kqcldsat 22338* | Any closed set is saturated with respect to the topological indistinguishability map (in the terminology of qtoprest 22322). (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → (◡𝐹 “ (𝐹 “ 𝑈)) = 𝑈) | ||
Theorem | kqopn 22339* | The topological indistinguishability map is an open map. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽) → (𝐹 “ 𝑈) ∈ (KQ‘𝐽)) | ||
Theorem | kqcld 22340* | The topological indistinguishability map is a closed map. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → (𝐹 “ 𝑈) ∈ (Clsd‘(KQ‘𝐽))) | ||
Theorem | kqt0lem 22341* | Lemma for kqt0 22351. (Contributed by Mario Carneiro, 23-Mar-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) ⇒ ⊢ (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) ∈ Kol2) | ||
Theorem | isr0 22342* | The property "𝐽 is an R0 space". A space is R0 if any two topologically distinguishable points are separated (there is an open set containing each one and disjoint from the other). Or in contraposition, if every open set which contains 𝑥 also contains 𝑦, so there is no separation, then 𝑥 and 𝑦 are members of the same open sets. We have chosen not to give this definition a name, because it turns out that a space is R0 if and only if its Kolmogorov quotient is T1, so that is what we prove here. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) ⇒ ⊢ (𝐽 ∈ (TopOn‘𝑋) → ((KQ‘𝐽) ∈ Fre ↔ ∀𝑧 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜) → ∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜)))) | ||
Theorem | r0cld 22343* | The analogue of the T1 axiom (singletons are closed) for an R0 space. In an R0 space the set of all points topologically indistinguishable from 𝐴 is closed. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre ∧ 𝐴 ∈ 𝑋) → {𝑧 ∈ 𝑋 ∣ ∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 ↔ 𝐴 ∈ 𝑜)} ∈ (Clsd‘𝐽)) | ||
Theorem | regr1lem 22344* | Lemma for regr1 22355. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐽 ∈ Reg) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝑈 ∈ 𝐽) & ⊢ (𝜑 → ¬ ∃𝑚 ∈ (KQ‘𝐽)∃𝑛 ∈ (KQ‘𝐽)((𝐹‘𝐴) ∈ 𝑚 ∧ (𝐹‘𝐵) ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅)) ⇒ ⊢ (𝜑 → (𝐴 ∈ 𝑈 → 𝐵 ∈ 𝑈)) | ||
Theorem | regr1lem2 22345* | A Kolmogorov quotient of a regular space is Hausdorff. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → (KQ‘𝐽) ∈ Haus) | ||
Theorem | kqreglem1 22346* | A Kolmogorov quotient of a regular space is regular. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Reg) → (KQ‘𝐽) ∈ Reg) | ||
Theorem | kqreglem2 22347* | If the Kolmogorov quotient of a space is regular then so is the original space. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Reg) → 𝐽 ∈ Reg) | ||
Theorem | kqnrmlem1 22348* | A Kolmogorov quotient of a normal space is normal. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ∈ Nrm) → (KQ‘𝐽) ∈ Nrm) | ||
Theorem | kqnrmlem2 22349* | If the Kolmogorov quotient of a space is normal then so is the original space. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Nrm) → 𝐽 ∈ Nrm) | ||
Theorem | kqtop 22350 | The Kolmogorov quotient is a topology on the quotient set. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ (𝐽 ∈ Top ↔ (KQ‘𝐽) ∈ Top) | ||
Theorem | kqt0 22351 | The Kolmogorov quotient is T0 even if the original topology is not. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ (𝐽 ∈ Top ↔ (KQ‘𝐽) ∈ Kol2) | ||
Theorem | kqf 22352 | The Kolmogorov quotient is a topology on the quotient set. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ KQ:Top⟶Kol2 | ||
Theorem | r0sep 22353* | The separation property of an R0 space. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ (KQ‘𝐽) ∈ Fre) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → 𝐵 ∈ 𝑜) → ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ↔ 𝐵 ∈ 𝑜))) | ||
Theorem | nrmr0reg 22354 | A normal R0 space is also regular. These spaces are usually referred to as normal regular spaces. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ ((𝐽 ∈ Nrm ∧ (KQ‘𝐽) ∈ Fre) → 𝐽 ∈ Reg) | ||
Theorem | regr1 22355 | A regular space is R1, which means that any two topologically distinct points can be separated by neighborhoods. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ (𝐽 ∈ Reg → (KQ‘𝐽) ∈ Haus) | ||
Theorem | kqreg 22356 | The Kolmogorov quotient of a regular space is regular. By regr1 22355 it is also Hausdorff, so we can also say that a space is regular iff the Kolmogorov quotient is regular Hausdorff (T3). (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ (𝐽 ∈ Reg ↔ (KQ‘𝐽) ∈ Reg) | ||
Theorem | kqnrm 22357 | The Kolmogorov quotient of a normal space is normal. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ (𝐽 ∈ Nrm ↔ (KQ‘𝐽) ∈ Nrm) | ||
Syntax | chmeo 22358 | Extend class notation with the class of all homeomorphisms. |
class Homeo | ||
Syntax | chmph 22359 | Extend class notation with the relation "is homeomorphic to.". |
class ≃ | ||
Definition | df-hmeo 22360* | Function returning all the homeomorphisms from topology 𝑗 to topology 𝑘. (Contributed by FL, 14-Feb-2007.) |
⊢ Homeo = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑓 ∈ (𝑗 Cn 𝑘) ∣ ◡𝑓 ∈ (𝑘 Cn 𝑗)}) | ||
Definition | df-hmph 22361 | Definition of the relation 𝑥 is homeomorphic to 𝑦. (Contributed by FL, 14-Feb-2007.) |
⊢ ≃ = (◡Homeo “ (V ∖ 1o)) | ||
Theorem | hmeofn 22362 | The set of homeomorphisms is a function on topologies. (Contributed by Mario Carneiro, 23-Aug-2015.) |
⊢ Homeo Fn (Top × Top) | ||
Theorem | hmeofval 22363* | The set of all the homeomorphisms between two topologies. (Contributed by FL, 14-Feb-2007.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝐽Homeo𝐾) = {𝑓 ∈ (𝐽 Cn 𝐾) ∣ ◡𝑓 ∈ (𝐾 Cn 𝐽)} | ||
Theorem | ishmeo 22364 | The predicate F is a homeomorphism between topology 𝐽 and topology 𝐾. Criterion of [BourbakiTop1] p. I.2. (Contributed by FL, 14-Feb-2007.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝐹 ∈ (𝐽Homeo𝐾) ↔ (𝐹 ∈ (𝐽 Cn 𝐾) ∧ ◡𝐹 ∈ (𝐾 Cn 𝐽))) | ||
Theorem | hmeocn 22365 | A homeomorphism is continuous. (Contributed by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐹 ∈ (𝐽 Cn 𝐾)) | ||
Theorem | hmeocnvcn 22366 | The converse of a homeomorphism is continuous. (Contributed by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → ◡𝐹 ∈ (𝐾 Cn 𝐽)) | ||
Theorem | hmeocnv 22367 | The converse of a homeomorphism is a homeomorphism. (Contributed by FL, 5-Mar-2007.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → ◡𝐹 ∈ (𝐾Homeo𝐽)) | ||
Theorem | hmeof1o2 22368 | A homeomorphism is a 1-1-onto mapping. (Contributed by Mario Carneiro, 22-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ (𝐽Homeo𝐾)) → 𝐹:𝑋–1-1-onto→𝑌) | ||
Theorem | hmeof1o 22369 | A homeomorphism is a 1-1-onto mapping. (Contributed by FL, 5-Mar-2007.) (Revised by Mario Carneiro, 30-May-2014.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐹:𝑋–1-1-onto→𝑌) | ||
Theorem | hmeoima 22370 | The image of an open set by a homeomorphism is an open set. (Contributed by FL, 5-Mar-2007.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ∈ 𝐽) → (𝐹 “ 𝐴) ∈ 𝐾) | ||
Theorem | hmeoopn 22371 | Homeomorphisms preserve openness. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → (𝐴 ∈ 𝐽 ↔ (𝐹 “ 𝐴) ∈ 𝐾)) | ||
Theorem | hmeocld 22372 | Homeomorphisms preserve closedness. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → (𝐴 ∈ (Clsd‘𝐽) ↔ (𝐹 “ 𝐴) ∈ (Clsd‘𝐾))) | ||
Theorem | hmeocls 22373 | Homeomorphisms preserve closures. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → ((cls‘𝐾)‘(𝐹 “ 𝐴)) = (𝐹 “ ((cls‘𝐽)‘𝐴))) | ||
Theorem | hmeontr 22374 | Homeomorphisms preserve interiors. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐴 ⊆ 𝑋) → ((int‘𝐾)‘(𝐹 “ 𝐴)) = (𝐹 “ ((int‘𝐽)‘𝐴))) | ||
Theorem | hmeoimaf1o 22375* | The function mapping open sets to their images under a homeomorphism is a bijection of topologies. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ 𝐺 = (𝑥 ∈ 𝐽 ↦ (𝐹 “ 𝑥)) ⇒ ⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐺:𝐽–1-1-onto→𝐾) | ||
Theorem | hmeores 22376 | The restriction of a homeomorphism is a homeomorphism. (Contributed by Mario Carneiro, 14-Sep-2014.) (Proof shortened by Mario Carneiro, 22-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝑌 ⊆ 𝑋) → (𝐹 ↾ 𝑌) ∈ ((𝐽 ↾t 𝑌)Homeo(𝐾 ↾t (𝐹 “ 𝑌)))) | ||
Theorem | hmeoco 22377 | The composite of two homeomorphisms is a homeomorphism. (Contributed by FL, 9-Mar-2007.) (Proof shortened by Mario Carneiro, 23-Aug-2015.) |
⊢ ((𝐹 ∈ (𝐽Homeo𝐾) ∧ 𝐺 ∈ (𝐾Homeo𝐿)) → (𝐺 ∘ 𝐹) ∈ (𝐽Homeo𝐿)) | ||
Theorem | idhmeo 22378 | The identity function is a homeomorphism. (Contributed by FL, 14-Feb-2007.) (Proof shortened by Mario Carneiro, 23-Aug-2015.) |
⊢ (𝐽 ∈ (TopOn‘𝑋) → ( I ↾ 𝑋) ∈ (𝐽Homeo𝐽)) | ||
Theorem | hmeocnvb 22379 | The converse of a homeomorphism is a homeomorphism. (Contributed by FL, 5-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.) |
⊢ (Rel 𝐹 → (◡𝐹 ∈ (𝐽Homeo𝐾) ↔ 𝐹 ∈ (𝐾Homeo𝐽))) | ||
Theorem | hmeoqtop 22380 | A homeomorphism is a quotient map. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐾 = (𝐽 qTop 𝐹)) | ||
Theorem | hmph 22381 | Express the predicate 𝐽 is homeomorphic to 𝐾. (Contributed by FL, 14-Feb-2007.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝐽 ≃ 𝐾 ↔ (𝐽Homeo𝐾) ≠ ∅) | ||
Theorem | hmphi 22382 | If there is a homeomorphism between spaces, then the spaces are homeomorphic. (Contributed by Mario Carneiro, 23-Aug-2015.) |
⊢ (𝐹 ∈ (𝐽Homeo𝐾) → 𝐽 ≃ 𝐾) | ||
Theorem | hmphtop 22383 | Reverse closure for the homeomorphic predicate. (Contributed by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Top ∧ 𝐾 ∈ Top)) | ||
Theorem | hmphtop1 22384 | The relation "being homeomorphic to" implies the operands are topologies. (Contributed by FL, 23-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.) |
⊢ (𝐽 ≃ 𝐾 → 𝐽 ∈ Top) | ||
Theorem | hmphtop2 22385 | The relation "being homeomorphic to" implies the operands are topologies. (Contributed by FL, 23-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.) |
⊢ (𝐽 ≃ 𝐾 → 𝐾 ∈ Top) | ||
Theorem | hmphref 22386 | "Is homeomorphic to" is reflexive. (Contributed by FL, 25-Feb-2007.) (Proof shortened by Mario Carneiro, 23-Aug-2015.) |
⊢ (𝐽 ∈ Top → 𝐽 ≃ 𝐽) | ||
Theorem | hmphsym 22387 | "Is homeomorphic to" is symmetric. (Contributed by FL, 8-Mar-2007.) (Proof shortened by Mario Carneiro, 30-May-2014.) |
⊢ (𝐽 ≃ 𝐾 → 𝐾 ≃ 𝐽) | ||
Theorem | hmphtr 22388 | "Is homeomorphic to" is transitive. (Contributed by FL, 9-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.) |
⊢ ((𝐽 ≃ 𝐾 ∧ 𝐾 ≃ 𝐿) → 𝐽 ≃ 𝐿) | ||
Theorem | hmpher 22389 | "Is homeomorphic to" is an equivalence relation. (Contributed by FL, 22-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.) |
⊢ ≃ Er Top | ||
Theorem | hmphen 22390 | Homeomorphisms preserve the cardinality of the topologies. (Contributed by FL, 1-Jun-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐽 ≃ 𝐾 → 𝐽 ≈ 𝐾) | ||
Theorem | hmphsymb 22391 | "Is homeomorphic to" is symmetric. (Contributed by FL, 22-Feb-2007.) |
⊢ (𝐽 ≃ 𝐾 ↔ 𝐾 ≃ 𝐽) | ||
Theorem | haushmphlem 22392* | Lemma for haushmph 22397 and similar theorems. If the topological property 𝐴 is preserved under injective preimages, then property 𝐴 is preserved under homeomorphisms. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ (𝐽 ∈ 𝐴 → 𝐽 ∈ Top) & ⊢ ((𝐽 ∈ 𝐴 ∧ 𝑓:∪ 𝐾–1-1→∪ 𝐽 ∧ 𝑓 ∈ (𝐾 Cn 𝐽)) → 𝐾 ∈ 𝐴) ⇒ ⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ 𝐴 → 𝐾 ∈ 𝐴)) | ||
Theorem | cmphmph 22393 | Compactness is a topological property-that is, for any two homeomorphic topologies, either both are compact or neither is. (Contributed by Jeff Hankins, 30-Jun-2009.) (Revised by Mario Carneiro, 23-Aug-2015.) |
⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Comp → 𝐾 ∈ Comp)) | ||
Theorem | connhmph 22394 | Connectedness is a topological property. (Contributed by Jeff Hankins, 3-Jul-2009.) |
⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Conn → 𝐾 ∈ Conn)) | ||
Theorem | t0hmph 22395 | T0 is a topological property. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Kol2 → 𝐾 ∈ Kol2)) | ||
Theorem | t1hmph 22396 | T1 is a topological property. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Fre → 𝐾 ∈ Fre)) | ||
Theorem | haushmph 22397 | Hausdorff-ness is a topological property. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Haus → 𝐾 ∈ Haus)) | ||
Theorem | reghmph 22398 | Regularity is a topological property. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Reg → 𝐾 ∈ Reg)) | ||
Theorem | nrmhmph 22399 | Normality is a topological property. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Nrm → 𝐾 ∈ Nrm)) | ||
Theorem | hmph0 22400 | A topology homeomorphic to the empty set is empty. (Contributed by FL, 18-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐽 ≃ {∅} ↔ 𝐽 = {∅}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |