Home | Metamath
Proof Explorer Theorem List (p. 225 of 461) | < 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-28865) |
Hilbert Space Explorer
(28866-30388) |
Users' Mathboxes
(30389-46009) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pthaus 22401 | The product of a collection of Hausdorff spaces is Hausdorff. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) → (∏t‘𝐹) ∈ Haus) | ||
Theorem | ptrescn 22402* | Restriction is a continuous function on product topologies. (Contributed by Mario Carneiro, 7-Feb-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐽 = (∏t‘𝐹) & ⊢ 𝐾 = (∏t‘(𝐹 ↾ 𝐵)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → (𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) ∈ (𝐽 Cn 𝐾)) | ||
Theorem | txtube 22403* | The "tube lemma". If 𝑋 is compact and there is an open set 𝑈 containing the line 𝑋 × {𝐴}, then there is a "tube" 𝑋 × 𝑢 for some neighborhood 𝑢 of 𝐴 which is entirely contained within 𝑈. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝑌 = ∪ 𝑆 & ⊢ (𝜑 → 𝑅 ∈ Comp) & ⊢ (𝜑 → 𝑆 ∈ Top) & ⊢ (𝜑 → 𝑈 ∈ (𝑅 ×t 𝑆)) & ⊢ (𝜑 → (𝑋 × {𝐴}) ⊆ 𝑈) & ⊢ (𝜑 → 𝐴 ∈ 𝑌) ⇒ ⊢ (𝜑 → ∃𝑢 ∈ 𝑆 (𝐴 ∈ 𝑢 ∧ (𝑋 × 𝑢) ⊆ 𝑈)) | ||
Theorem | txcmplem1 22404* | Lemma for txcmp 22406. (Contributed by Mario Carneiro, 14-Sep-2014.) |
⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝑌 = ∪ 𝑆 & ⊢ (𝜑 → 𝑅 ∈ Comp) & ⊢ (𝜑 → 𝑆 ∈ Comp) & ⊢ (𝜑 → 𝑊 ⊆ (𝑅 ×t 𝑆)) & ⊢ (𝜑 → (𝑋 × 𝑌) = ∪ 𝑊) & ⊢ (𝜑 → 𝐴 ∈ 𝑌) ⇒ ⊢ (𝜑 → ∃𝑢 ∈ 𝑆 (𝐴 ∈ 𝑢 ∧ ∃𝑣 ∈ (𝒫 𝑊 ∩ Fin)(𝑋 × 𝑢) ⊆ ∪ 𝑣)) | ||
Theorem | txcmplem2 22405* | Lemma for txcmp 22406. (Contributed by Mario Carneiro, 14-Sep-2014.) |
⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝑌 = ∪ 𝑆 & ⊢ (𝜑 → 𝑅 ∈ Comp) & ⊢ (𝜑 → 𝑆 ∈ Comp) & ⊢ (𝜑 → 𝑊 ⊆ (𝑅 ×t 𝑆)) & ⊢ (𝜑 → (𝑋 × 𝑌) = ∪ 𝑊) ⇒ ⊢ (𝜑 → ∃𝑣 ∈ (𝒫 𝑊 ∩ Fin)(𝑋 × 𝑌) = ∪ 𝑣) | ||
Theorem | txcmp 22406 | The topological product of two compact spaces is compact. (Contributed by Mario Carneiro, 14-Sep-2014.) (Proof shortened 21-Mar-2015.) |
⊢ ((𝑅 ∈ Comp ∧ 𝑆 ∈ Comp) → (𝑅 ×t 𝑆) ∈ Comp) | ||
Theorem | txcmpb 22407 | The topological product of two nonempty topologies is compact iff the component topologies are both compact. (Contributed by Mario Carneiro, 14-Sep-2014.) |
⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝑌 = ∪ 𝑆 ⇒ ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅)) → ((𝑅 ×t 𝑆) ∈ Comp ↔ (𝑅 ∈ Comp ∧ 𝑆 ∈ Comp))) | ||
Theorem | hausdiag 22408 | A topology is Hausdorff iff the diagonal set is closed in the topology's product with itself. EDITORIAL: very clumsy proof, can probably be shortened substantially. (Contributed by Stefan O'Rear, 25-Jan-2015.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ( I ↾ 𝑋) ∈ (Clsd‘(𝐽 ×t 𝐽)))) | ||
Theorem | hauseqlcld 22409 | In a Hausdorff topology, the equalizer of two continuous functions is closed (thus, two continuous functions which agree on a dense set agree everywhere). (Contributed by Stefan O'Rear, 25-Jan-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝜑 → 𝐾 ∈ Haus) & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾)) ⇒ ⊢ (𝜑 → dom (𝐹 ∩ 𝐺) ∈ (Clsd‘𝐽)) | ||
Theorem | txhaus 22410 | The topological product of two Hausdorff spaces is Hausdorff. (Contributed by Mario Carneiro, 23-Mar-2015.) |
⊢ ((𝑅 ∈ Haus ∧ 𝑆 ∈ Haus) → (𝑅 ×t 𝑆) ∈ Haus) | ||
Theorem | txlm 22411* | Two sequences converge iff the sequence of their ordered pairs converges. Proposition 14-2.6 of [Gleason] p. 230. (Contributed by NM, 16-Jul-2007.) (Revised by Mario Carneiro, 5-May-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝐹:𝑍⟶𝑋) & ⊢ (𝜑 → 𝐺:𝑍⟶𝑌) & ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉) ⇒ ⊢ (𝜑 → ((𝐹(⇝𝑡‘𝐽)𝑅 ∧ 𝐺(⇝𝑡‘𝐾)𝑆) ↔ 𝐻(⇝𝑡‘(𝐽 ×t 𝐾))〈𝑅, 𝑆〉)) | ||
Theorem | lmcn2 22412* | The image of a convergent sequence under a continuous map is convergent to the image of the original point. Binary operation version. (Contributed by Mario Carneiro, 15-May-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝐹:𝑍⟶𝑋) & ⊢ (𝜑 → 𝐺:𝑍⟶𝑌) & ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑅) & ⊢ (𝜑 → 𝐺(⇝𝑡‘𝐾)𝑆) & ⊢ (𝜑 → 𝑂 ∈ ((𝐽 ×t 𝐾) Cn 𝑁)) & ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)𝑂(𝐺‘𝑛))) ⇒ ⊢ (𝜑 → 𝐻(⇝𝑡‘𝑁)(𝑅𝑂𝑆)) | ||
Theorem | tx1stc 22413 | The topological product of two first-countable spaces is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → (𝑅 ×t 𝑆) ∈ 1stω) | ||
Theorem | tx2ndc 22414 | The topological product of two second-countable spaces is second-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ ((𝑅 ∈ 2ndω ∧ 𝑆 ∈ 2ndω) → (𝑅 ×t 𝑆) ∈ 2ndω) | ||
Theorem | txkgen 22415 | The topological product of a locally compact space and a compactly generated Hausdorff space is compactly generated. (The condition on 𝑆 can also be replaced with either "compactly generated weak Hausdorff (CGWH)" or "compact Hausdorff-ly generated (CHG)", where WH means that all images of compact Hausdorff spaces are closed and CHG means that a set is open iff it is open in all compact Hausdorff spaces.) (Contributed by Mario Carneiro, 23-Mar-2015.) |
⊢ ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ (ran 𝑘Gen ∩ Haus)) → (𝑅 ×t 𝑆) ∈ ran 𝑘Gen) | ||
Theorem | xkohaus 22416 | If the codomain space is Hausdorff, then the compact-open topology of continuous functions is also Hausdorff. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Haus) → (𝑆 ↑ko 𝑅) ∈ Haus) | ||
Theorem | xkoptsub 22417 | The compact-open topology is finer than the product topology restricted to continuous functions. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝐽 = (∏t‘(𝑋 × {𝑆})) ⇒ ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝐽 ↾t (𝑅 Cn 𝑆)) ⊆ (𝑆 ↑ko 𝑅)) | ||
Theorem | xkopt 22418 | The compact-open topology on a discrete set coincides with the product topology where all the factors are the same. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 12-Sep-2015.) |
⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝑅 ↑ko 𝒫 𝐴) = (∏t‘(𝐴 × {𝑅}))) | ||
Theorem | xkopjcn 22419* | Continuity of a projection map from the space of continuous functions. (This theorem can be strengthened, to joint continuity in both 𝑓 and 𝐴 as a function on (𝑆 ↑ko 𝑅) ×t 𝑅, but not without stronger assumptions on 𝑅; see xkofvcn 22447.) (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ 𝑋 = ∪ 𝑅 ⇒ ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐴 ∈ 𝑋) → (𝑓 ∈ (𝑅 Cn 𝑆) ↦ (𝑓‘𝐴)) ∈ ((𝑆 ↑ko 𝑅) Cn 𝑆)) | ||
Theorem | xkoco1cn 22420* | If 𝐹 is a continuous function, then 𝑔 ↦ 𝑔 ∘ 𝐹 is a continuous function on function spaces. (The reason we prove this and xkoco2cn 22421 independently of the more general xkococn 22423 is because that requires some inconvenient extra assumptions on 𝑆.) (Contributed by Mario Carneiro, 20-Mar-2015.) |
⊢ (𝜑 → 𝑇 ∈ Top) & ⊢ (𝜑 → 𝐹 ∈ (𝑅 Cn 𝑆)) ⇒ ⊢ (𝜑 → (𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔 ∘ 𝐹)) ∈ ((𝑇 ↑ko 𝑆) Cn (𝑇 ↑ko 𝑅))) | ||
Theorem | xkoco2cn 22421* | If 𝐹 is a continuous function, then 𝑔 ↦ 𝐹 ∘ 𝑔 is a continuous function on function spaces. (Contributed by Mario Carneiro, 23-Mar-2015.) |
⊢ (𝜑 → 𝑅 ∈ Top) & ⊢ (𝜑 → 𝐹 ∈ (𝑆 Cn 𝑇)) ⇒ ⊢ (𝜑 → (𝑔 ∈ (𝑅 Cn 𝑆) ↦ (𝐹 ∘ 𝑔)) ∈ ((𝑆 ↑ko 𝑅) Cn (𝑇 ↑ko 𝑅))) | ||
Theorem | xkococnlem 22422* | Continuity of the composition operation as a function on continuous function spaces. (Contributed by Mario Carneiro, 20-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ 𝐹 = (𝑓 ∈ (𝑆 Cn 𝑇), 𝑔 ∈ (𝑅 Cn 𝑆) ↦ (𝑓 ∘ 𝑔)) & ⊢ (𝜑 → 𝑆 ∈ 𝑛-Locally Comp) & ⊢ (𝜑 → 𝐾 ⊆ ∪ 𝑅) & ⊢ (𝜑 → (𝑅 ↾t 𝐾) ∈ Comp) & ⊢ (𝜑 → 𝑉 ∈ 𝑇) & ⊢ (𝜑 → 𝐴 ∈ (𝑆 Cn 𝑇)) & ⊢ (𝜑 → 𝐵 ∈ (𝑅 Cn 𝑆)) & ⊢ (𝜑 → ((𝐴 ∘ 𝐵) “ 𝐾) ⊆ 𝑉) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ ((𝑇 ↑ko 𝑆) ×t (𝑆 ↑ko 𝑅))(〈𝐴, 𝐵〉 ∈ 𝑧 ∧ 𝑧 ⊆ (◡𝐹 “ {ℎ ∈ (𝑅 Cn 𝑇) ∣ (ℎ “ 𝐾) ⊆ 𝑉}))) | ||
Theorem | xkococn 22423* | Continuity of the composition operation as a function on continuous function spaces. (Contributed by Mario Carneiro, 20-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ 𝐹 = (𝑓 ∈ (𝑆 Cn 𝑇), 𝑔 ∈ (𝑅 Cn 𝑆) ↦ (𝑓 ∘ 𝑔)) ⇒ ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ 𝑛-Locally Comp ∧ 𝑇 ∈ Top) → 𝐹 ∈ (((𝑇 ↑ko 𝑆) ×t (𝑆 ↑ko 𝑅)) Cn (𝑇 ↑ko 𝑅))) | ||
Theorem | cnmptid 22424* | The identity function is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝑥) ∈ (𝐽 Cn 𝐽)) | ||
Theorem | cnmptc 22425* | A constant function is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝑃 ∈ 𝑌) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝑃) ∈ (𝐽 Cn 𝐾)) | ||
Theorem | cnmpt11 22426* | The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → (𝑦 ∈ 𝑌 ↦ 𝐵) ∈ (𝐾 Cn 𝐿)) & ⊢ (𝑦 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐶) ∈ (𝐽 Cn 𝐿)) | ||
Theorem | cnmpt11f 22427* | The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝐹 ∈ (𝐾 Cn 𝐿)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐹‘𝐴)) ∈ (𝐽 Cn 𝐿)) | ||
Theorem | cnmpt1t 22428* | The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐿)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) ∈ (𝐽 Cn (𝐾 ×t 𝐿))) | ||
Theorem | cnmpt12f 22429* | The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐿)) & ⊢ (𝜑 → 𝐹 ∈ ((𝐾 ×t 𝐿) Cn 𝑀)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴𝐹𝐵)) ∈ (𝐽 Cn 𝑀)) | ||
Theorem | cnmpt12 22430* | The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 12-Jun-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐿)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍)) & ⊢ (𝜑 → (𝑦 ∈ 𝑌, 𝑧 ∈ 𝑍 ↦ 𝐶) ∈ ((𝐾 ×t 𝐿) Cn 𝑀)) & ⊢ ((𝑦 = 𝐴 ∧ 𝑧 = 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐷) ∈ (𝐽 Cn 𝑀)) | ||
Theorem | cnmpt1st 22431* | The projection onto the first coordinate is continuous. (Contributed by Mario Carneiro, 6-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝑥) ∈ ((𝐽 ×t 𝐾) Cn 𝐽)) | ||
Theorem | cnmpt2nd 22432* | The projection onto the second coordinate is continuous. (Contributed by Mario Carneiro, 6-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝑦) ∈ ((𝐽 ×t 𝐾) Cn 𝐾)) | ||
Theorem | cnmpt2c 22433* | A constant function is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍)) & ⊢ (𝜑 → 𝑃 ∈ 𝑍) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝑃) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) | ||
Theorem | cnmpt21 22434* | The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) & ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍)) & ⊢ (𝜑 → (𝑧 ∈ 𝑍 ↦ 𝐵) ∈ (𝐿 Cn 𝑀)) & ⊢ (𝑧 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶) ∈ ((𝐽 ×t 𝐾) Cn 𝑀)) | ||
Theorem | cnmpt21f 22435* | The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) & ⊢ (𝜑 → 𝐹 ∈ (𝐿 Cn 𝑀)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝐹‘𝐴)) ∈ ((𝐽 ×t 𝐾) Cn 𝑀)) | ||
Theorem | cnmpt2t 22436* | The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐽 ×t 𝐾) Cn 𝑀)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈𝐴, 𝐵〉) ∈ ((𝐽 ×t 𝐾) Cn (𝐿 ×t 𝑀))) | ||
Theorem | cnmpt22 22437* | The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐽 ×t 𝐾) Cn 𝑀)) & ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍)) & ⊢ (𝜑 → 𝑀 ∈ (TopOn‘𝑊)) & ⊢ (𝜑 → (𝑧 ∈ 𝑍, 𝑤 ∈ 𝑊 ↦ 𝐶) ∈ ((𝐿 ×t 𝑀) Cn 𝑁)) & ⊢ ((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐷) ∈ ((𝐽 ×t 𝐾) Cn 𝑁)) | ||
Theorem | cnmpt22f 22438* | The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐽 ×t 𝐾) Cn 𝑀)) & ⊢ (𝜑 → 𝐹 ∈ ((𝐿 ×t 𝑀) Cn 𝑁)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝐴𝐹𝐵)) ∈ ((𝐽 ×t 𝐾) Cn 𝑁)) | ||
Theorem | cnmpt1res 22439* | The restriction of a continuous function to a subset is continuous. (Contributed by Mario Carneiro, 5-Jun-2014.) |
⊢ 𝐾 = (𝐽 ↾t 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ⊆ 𝑋) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐿)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿)) | ||
Theorem | cnmpt2res 22440* | The restriction of a continuous function to a subset is continuous. (Contributed by Mario Carneiro, 6-Jun-2014.) |
⊢ 𝐾 = (𝐽 ↾t 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ⊆ 𝑋) & ⊢ 𝑁 = (𝑀 ↾t 𝑊) & ⊢ (𝜑 → 𝑀 ∈ (TopOn‘𝑍)) & ⊢ (𝜑 → 𝑊 ⊆ 𝑍) & ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑍 ↦ 𝐴) ∈ ((𝐽 ×t 𝑀) Cn 𝐿)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑌, 𝑦 ∈ 𝑊 ↦ 𝐴) ∈ ((𝐾 ×t 𝑁) Cn 𝐿)) | ||
Theorem | cnmptcom 22441* | The argument converse of a continuous function is continuous. (Contributed by Mario Carneiro, 6-Jun-2014.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) ⇒ ⊢ (𝜑 → (𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐾 ×t 𝐽) Cn 𝐿)) | ||
Theorem | cnmptkc 22442* | The curried first projection function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝑥)) ∈ (𝐽 Cn (𝐽 ↑ko 𝐾))) | ||
Theorem | cnmptkp 22443* | The evaluation of the inner function in a curried function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) & ⊢ (𝜑 → 𝐵 ∈ 𝑌) & ⊢ (𝑦 = 𝐵 → 𝐴 = 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐶) ∈ (𝐽 Cn 𝐿)) | ||
Theorem | cnmptk1 22444* | The composition of a curried function with a one-arg function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) & ⊢ (𝜑 → (𝑧 ∈ 𝑍 ↦ 𝐵) ∈ (𝐿 Cn 𝑀)) & ⊢ (𝑧 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐶)) ∈ (𝐽 Cn (𝑀 ↑ko 𝐾))) | ||
Theorem | cnmpt1k 22445* | The composition of a one-arg function with a curried function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍)) & ⊢ (𝜑 → 𝑀 ∈ (TopOn‘𝑊)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐿)) & ⊢ (𝜑 → (𝑦 ∈ 𝑌 ↦ (𝑧 ∈ 𝑍 ↦ 𝐵)) ∈ (𝐾 Cn (𝑀 ↑ko 𝐿))) & ⊢ (𝑧 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (𝑦 ∈ 𝑌 ↦ (𝑥 ∈ 𝑋 ↦ 𝐶)) ∈ (𝐾 Cn (𝑀 ↑ko 𝐽))) | ||
Theorem | cnmptkk 22446* | The composition of two curried functions is jointly continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍)) & ⊢ (𝜑 → 𝑀 ∈ (TopOn‘𝑊)) & ⊢ (𝜑 → 𝐿 ∈ 𝑛-Locally Comp) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑧 ∈ 𝑍 ↦ 𝐵)) ∈ (𝐽 Cn (𝑀 ↑ko 𝐿))) & ⊢ (𝑧 = 𝐴 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐶)) ∈ (𝐽 Cn (𝑀 ↑ko 𝐾))) | ||
Theorem | xkofvcn 22447* | Joint continuity of the function value operation as a function on continuous function spaces. (Compare xkopjcn 22419.) (Contributed by Mario Carneiro, 20-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝐹 = (𝑓 ∈ (𝑅 Cn 𝑆), 𝑥 ∈ 𝑋 ↦ (𝑓‘𝑥)) ⇒ ⊢ ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ Top) → 𝐹 ∈ (((𝑆 ↑ko 𝑅) ×t 𝑅) Cn 𝑆)) | ||
Theorem | cnmptk1p 22448* | The evaluation of a curried function by a one-arg function is jointly continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍)) & ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally Comp) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐾)) & ⊢ (𝑦 = 𝐵 → 𝐴 = 𝐶) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐶) ∈ (𝐽 Cn 𝐿)) | ||
Theorem | cnmptk2 22449* | The uncurrying of a curried function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍)) & ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally Comp) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) | ||
Theorem | xkoinjcn 22450* | Continuity of "injection", i.e. currying, as a function on continuous function spaces. (Contributed by Mario Carneiro, 23-Mar-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 〈𝑦, 𝑥〉)) ⇒ ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → 𝐹 ∈ (𝑅 Cn ((𝑆 ×t 𝑅) ↑ko 𝑆))) | ||
Theorem | cnmpt2k 22451* | The currying of a two-argument function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ (𝐽 Cn (𝐿 ↑ko 𝐾))) | ||
Theorem | txconn 22452 | The topological product of two connected spaces is connected. (Contributed by Mario Carneiro, 29-Mar-2015.) |
⊢ ((𝑅 ∈ Conn ∧ 𝑆 ∈ Conn) → (𝑅 ×t 𝑆) ∈ Conn) | ||
Theorem | imasnopn 22453 | If a relation graph is open, then an image set of a singleton is also open. Corollary of Proposition 4 of [BourbakiTop1] p. I.26. (Contributed by Thierry Arnoux, 14-Jan-2018.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (𝐽 ×t 𝐾) ∧ 𝐴 ∈ 𝑋)) → (𝑅 “ {𝐴}) ∈ 𝐾) | ||
Theorem | imasncld 22454 | If a relation graph is closed, then an image set of a singleton is also closed. Corollary of Proposition 4 of [BourbakiTop1] p. I.26. (Contributed by Thierry Arnoux, 14-Jan-2018.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ∈ (Clsd‘(𝐽 ×t 𝐾)) ∧ 𝐴 ∈ 𝑋)) → (𝑅 “ {𝐴}) ∈ (Clsd‘𝐾)) | ||
Theorem | imasncls 22455 | If a relation graph is closed, then an image set of a singleton is also closed. Corollary of Proposition 4 of [BourbakiTop1] p. I.26. (Contributed by Thierry Arnoux, 14-Jan-2018.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑅 ⊆ (𝑋 × 𝑌) ∧ 𝐴 ∈ 𝑋)) → ((cls‘𝐾)‘(𝑅 “ {𝐴})) ⊆ (((cls‘(𝐽 ×t 𝐾))‘𝑅) “ {𝐴})) | ||
Syntax | ckq 22456 | Extend class notation with the Kolmogorov quotient function. |
class KQ | ||
Definition | df-kq 22457* | Define the Kolmogorov quotient. This is a function on topologies which maps a topology to its quotient under the topological distinguishability map, which takes a point to the set of open sets that contain it. Two points are mapped to the same image under this function iff they are topologically indistinguishable. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ KQ = (𝑗 ∈ Top ↦ (𝑗 qTop (𝑥 ∈ ∪ 𝑗 ↦ {𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦}))) | ||
Theorem | qtopval 22458* | Value of the quotient topology function. (Contributed by Mario Carneiro, 23-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊) → (𝐽 qTop 𝐹) = {𝑠 ∈ 𝒫 (𝐹 “ 𝑋) ∣ ((◡𝐹 “ 𝑠) ∩ 𝑋) ∈ 𝐽}) | ||
Theorem | qtopval2 22459* | 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 22460 | Value of the quotient topology function. (Contributed by Mario Carneiro, 23-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑍–onto→𝑌 ∧ 𝑍 ⊆ 𝑋) → (𝐴 ∈ (𝐽 qTop 𝐹) ↔ (𝐴 ⊆ 𝑌 ∧ (◡𝐹 “ 𝐴) ∈ 𝐽))) | ||
Theorem | qtopres 22461 | 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 22462 | The quotient topology is a topology. (Contributed by Mario Carneiro, 23-Mar-2015.) |
⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹) → (𝐽 qTop 𝐹) ∈ Top) | ||
Theorem | qtoptop 22463 | The quotient topology is a topology. (Contributed by Mario Carneiro, 23-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ Top) | ||
Theorem | elqtop2 22464 | Value of the quotient topology function. (Contributed by Mario Carneiro, 9-Apr-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐹:𝑋–onto→𝑌) → (𝐴 ∈ (𝐽 qTop 𝐹) ↔ (𝐴 ⊆ 𝑌 ∧ (◡𝐹 “ 𝐴) ∈ 𝐽))) | ||
Theorem | qtopuni 22465 | The base set of the quotient topology. (Contributed by Mario Carneiro, 23-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐹:𝑋–onto→𝑌) → 𝑌 = ∪ (𝐽 qTop 𝐹)) | ||
Theorem | elqtop3 22466 | Value of the quotient topology function. (Contributed by Mario Carneiro, 9-Apr-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝐴 ∈ (𝐽 qTop 𝐹) ↔ (𝐴 ⊆ 𝑌 ∧ (◡𝐹 “ 𝐴) ∈ 𝐽))) | ||
Theorem | qtoptopon 22467 | The base set of the quotient topology. (Contributed by Mario Carneiro, 22-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌)) | ||
Theorem | qtopid 22468 | A quotient map is a continuous function into its quotient topology. (Contributed by Mario Carneiro, 23-Mar-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 Fn 𝑋) → 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹))) | ||
Theorem | idqtop 22469 | The quotient topology induced by the identity function is the original topology. (Contributed by Mario Carneiro, 30-Aug-2015.) |
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 qTop ( I ↾ 𝑋)) = 𝐽) | ||
Theorem | qtopcmplem 22470 | Lemma for qtopcmp 22471 and qtopconn 22472. (Contributed by Mario Carneiro, 24-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ (𝐽 ∈ 𝐴 → 𝐽 ∈ Top) & ⊢ ((𝐽 ∈ 𝐴 ∧ 𝐹:𝑋–onto→∪ (𝐽 qTop 𝐹) ∧ 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹))) → (𝐽 qTop 𝐹) ∈ 𝐴) ⇒ ⊢ ((𝐽 ∈ 𝐴 ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ 𝐴) | ||
Theorem | qtopcmp 22471 | A quotient of a compact space is compact. (Contributed by Mario Carneiro, 24-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Comp ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ Comp) | ||
Theorem | qtopconn 22472 | A quotient of a connected space is connected. (Contributed by Mario Carneiro, 24-Mar-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Conn ∧ 𝐹 Fn 𝑋) → (𝐽 qTop 𝐹) ∈ Conn) | ||
Theorem | qtopkgen 22473 | 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 22474 | An injection maps bases to bases. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ TopBases ∧ 𝐹:𝑋–1-1-onto→𝑌) → (𝐽 qTop 𝐹) ∈ TopBases) | ||
Theorem | tgqtop 22475 | 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 22476 | 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 22477 | Universal property of a quotient map. (Contributed by Mario Carneiro, 23-Mar-2015.) |
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑍)) ∧ (𝐹:𝑋–onto→𝑌 ∧ 𝐺:𝑌⟶𝑍)) → (𝐺 ∈ ((𝐽 qTop 𝐹) Cn 𝐾) ↔ (𝐺 ∘ 𝐹) ∈ (𝐽 Cn 𝐾))) | ||
Theorem | qtopss 22478 | 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 22468, 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 22479* | 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 22480 | 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 22481* | 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 22482* | 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 22483 | The topology of an image structure. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) & ⊢ (𝜑 → 𝑅 ∈ 𝑊) & ⊢ 𝐽 = (TopOpen‘𝑅) & ⊢ 𝑂 = (TopOpen‘𝑈) ⇒ ⊢ (𝜑 → 𝑂 = (𝐽 qTop 𝐹)) | ||
Theorem | imastps 22484 | 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 22485 | A quotient structure is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ (𝜑 → 𝑈 = (𝑅 /s 𝐸)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐸 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ TopSp) ⇒ ⊢ (𝜑 → 𝑈 ∈ TopSp) | ||
Theorem | kqfval 22486* | Value of the function appearing in df-kq 22457. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) ⇒ ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋) → (𝐹‘𝐴) = {𝑦 ∈ 𝐽 ∣ 𝐴 ∈ 𝑦}) | ||
Theorem | kqfeq 22487* | Two points in the Kolmogorov quotient are equal iff the original points are topologically indistinguishable. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) ⇒ ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐹‘𝐴) = (𝐹‘𝐵) ↔ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 ↔ 𝐵 ∈ 𝑦))) | ||
Theorem | kqffn 22488* | The topological indistinguishability map is a function on the base. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) ⇒ ⊢ (𝐽 ∈ 𝑉 → 𝐹 Fn 𝑋) | ||
Theorem | kqval 22489* | Value of the quotient topology function. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) ⇒ ⊢ (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) = (𝐽 qTop 𝐹)) | ||
Theorem | kqtopon 22490* | The Kolmogorov quotient is a topology on the quotient set. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) ⇒ ⊢ (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) ∈ (TopOn‘ran 𝐹)) | ||
Theorem | kqid 22491* | 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 22492* | 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 22493* | When the image set is open, the quotient map satisfies a partial converse to fnfvima 7018, which is normally only true for injective functions. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑋) → (𝐴 ∈ 𝑈 ↔ (𝐹‘𝐴) ∈ (𝐹 “ 𝑈))) | ||
Theorem | kqsat 22494* | Any open set is saturated with respect to the topological indistinguishability map (in the terminology of qtoprest 22480). (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽) → (◡𝐹 “ (𝐹 “ 𝑈)) = 𝑈) | ||
Theorem | kqdisj 22495* | A version of imain 6434 for the topological indistinguishability map. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽) → ((𝐹 “ 𝑈) ∩ (𝐹 “ (𝐴 ∖ 𝑈))) = ∅) | ||
Theorem | kqcldsat 22496* | Any closed set is saturated with respect to the topological indistinguishability map (in the terminology of qtoprest 22480). (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → (◡𝐹 “ (𝐹 “ 𝑈)) = 𝑈) | ||
Theorem | kqopn 22497* | The topological indistinguishability map is an open map. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽) → (𝐹 “ 𝑈) ∈ (KQ‘𝐽)) | ||
Theorem | kqcld 22498* | The topological indistinguishability map is a closed map. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ (Clsd‘𝐽)) → (𝐹 “ 𝑈) ∈ (Clsd‘(KQ‘𝐽))) | ||
Theorem | kqt0lem 22499* | Lemma for kqt0 22509. (Contributed by Mario Carneiro, 23-Mar-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) ⇒ ⊢ (𝐽 ∈ (TopOn‘𝑋) → (KQ‘𝐽) ∈ Kol2) | ||
Theorem | isr0 22500* | 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 ↔ ∀𝑧 ∈ 𝑋 ∀𝑤 ∈ 𝑋 (∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 → 𝑤 ∈ 𝑜) → ∀𝑜 ∈ 𝐽 (𝑧 ∈ 𝑜 ↔ 𝑤 ∈ 𝑜)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |