| Metamath
Proof Explorer Theorem List (p. 236 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | hausnlly 23501 | A Hausdorff space is n-locally Hausdorff iff it is locally Hausdorff (both notions are thus referred to as "locally Hausdorff"). (Contributed by Mario Carneiro, 2-Mar-2015.) |
| ⊢ (𝐽 ∈ 𝑛-Locally Haus ↔ 𝐽 ∈ Locally Haus) | ||
| Theorem | hausllycmp 23502 | A compact Hausdorff space is locally compact. (Contributed by Mario Carneiro, 2-Mar-2015.) |
| ⊢ ((𝐽 ∈ Haus ∧ 𝐽 ∈ Comp) → 𝐽 ∈ 𝑛-Locally Comp) | ||
| Theorem | cldllycmp 23503 | A closed subspace of a locally compact space is also locally compact. (The analogous result for open subspaces follows from the more general nllyrest 23494.) (Contributed by Mario Carneiro, 2-Mar-2015.) |
| ⊢ ((𝐽 ∈ 𝑛-Locally Comp ∧ 𝐴 ∈ (Clsd‘𝐽)) → (𝐽 ↾t 𝐴) ∈ 𝑛-Locally Comp) | ||
| Theorem | lly1stc 23504 | First-countability is a local property (unlike second-countability). (Contributed by Mario Carneiro, 21-Mar-2015.) |
| ⊢ Locally 1stω = 1stω | ||
| Theorem | dislly 23505* | The discrete space 𝒫 𝑋 is locally 𝐴 if and only if every singleton space has property 𝐴. (Contributed by Mario Carneiro, 20-Mar-2015.) |
| ⊢ (𝑋 ∈ 𝑉 → (𝒫 𝑋 ∈ Locally 𝐴 ↔ ∀𝑥 ∈ 𝑋 𝒫 {𝑥} ∈ 𝐴)) | ||
| Theorem | disllycmp 23506 | A discrete space is locally compact. (Contributed by Mario Carneiro, 20-Mar-2015.) |
| ⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ Locally Comp) | ||
| Theorem | dis1stc 23507 | A discrete space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
| ⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ 1stω) | ||
| Theorem | hausmapdom 23508 | If 𝑋 is a first-countable Hausdorff space, then the cardinality of the closure of a set 𝐴 is bounded by ℕ to the power 𝐴. In particular, a first-countable Hausdorff space with a dense subset 𝐴 has cardinality at most 𝐴↑ℕ, and a separable first-countable Hausdorff space has cardinality at most 𝒫 ℕ. (Compare hauspwpwdom 23996 to see a weaker result if the assumption of first-countability is omitted.) (Contributed by Mario Carneiro, 9-Apr-2015.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋) → ((cls‘𝐽)‘𝐴) ≼ (𝐴 ↑m ℕ)) | ||
| Theorem | hauspwdom 23509 | Simplify the cardinal 𝐴↑ℕ of hausmapdom 23508 to 𝒫 𝐵 = 2↑𝐵 when 𝐵 is an infinite cardinal greater than 𝐴. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Mario Carneiro, 30-Apr-2015.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (((𝐽 ∈ Haus ∧ 𝐽 ∈ 1stω ∧ 𝐴 ⊆ 𝑋) ∧ (𝐴 ≼ 𝒫 𝐵 ∧ ℕ ≼ 𝐵)) → ((cls‘𝐽)‘𝐴) ≼ 𝒫 𝐵) | ||
| Syntax | cref 23510 | Extend class definition to include the refinement relation. |
| class Ref | ||
| Syntax | cptfin 23511 | Extend class definition to include the class of point-finite covers. |
| class PtFin | ||
| Syntax | clocfin 23512 | Extend class definition to include the class of locally finite covers. |
| class LocFin | ||
| Definition | df-ref 23513* | Define the refinement relation. (Contributed by Jeff Hankins, 18-Jan-2010.) |
| ⊢ Ref = {〈𝑥, 𝑦〉 ∣ (∪ 𝑦 = ∪ 𝑥 ∧ ∀𝑧 ∈ 𝑥 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)} | ||
| Definition | df-ptfin 23514* | Define "point-finite." (Contributed by Jeff Hankins, 21-Jan-2010.) |
| ⊢ PtFin = {𝑥 ∣ ∀𝑦 ∈ ∪ 𝑥{𝑧 ∈ 𝑥 ∣ 𝑦 ∈ 𝑧} ∈ Fin} | ||
| Definition | df-locfin 23515* | Define "locally finite." (Contributed by Jeff Hankins, 21-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
| ⊢ LocFin = (𝑥 ∈ Top ↦ {𝑦 ∣ (∪ 𝑥 = ∪ 𝑦 ∧ ∀𝑝 ∈ ∪ 𝑥∃𝑛 ∈ 𝑥 (𝑝 ∈ 𝑛 ∧ {𝑠 ∈ 𝑦 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin))}) | ||
| Theorem | refrel 23516 | Refinement is a relation. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
| ⊢ Rel Ref | ||
| Theorem | isref 23517* | The property of being a refinement of a cover. Dr. Nyikos once commented in class that the term "refinement" is actually misleading and that people are inclined to confuse it with the notion defined in isfne 36340. On the other hand, the two concepts do seem to have a dual relationship. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
| ⊢ 𝑋 = ∪ 𝐴 & ⊢ 𝑌 = ∪ 𝐵 ⇒ ⊢ (𝐴 ∈ 𝐶 → (𝐴Ref𝐵 ↔ (𝑌 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦))) | ||
| Theorem | refbas 23518 | A refinement covers the same set. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
| ⊢ 𝑋 = ∪ 𝐴 & ⊢ 𝑌 = ∪ 𝐵 ⇒ ⊢ (𝐴Ref𝐵 → 𝑌 = 𝑋) | ||
| Theorem | refssex 23519* | Every set in a refinement has a superset in the original cover. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
| ⊢ ((𝐴Ref𝐵 ∧ 𝑆 ∈ 𝐴) → ∃𝑥 ∈ 𝐵 𝑆 ⊆ 𝑥) | ||
| Theorem | ssref 23520 | A subcover is a refinement of the original cover. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
| ⊢ 𝑋 = ∪ 𝐴 & ⊢ 𝑌 = ∪ 𝐵 ⇒ ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐴 ⊆ 𝐵 ∧ 𝑋 = 𝑌) → 𝐴Ref𝐵) | ||
| Theorem | refref 23521 | Reflexivity of refinement. (Contributed by Jeff Hankins, 18-Jan-2010.) |
| ⊢ (𝐴 ∈ 𝑉 → 𝐴Ref𝐴) | ||
| Theorem | reftr 23522 | Refinement is transitive. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
| ⊢ ((𝐴Ref𝐵 ∧ 𝐵Ref𝐶) → 𝐴Ref𝐶) | ||
| Theorem | refun0 23523 | Adding the empty set preserves refinements. (Contributed by Thierry Arnoux, 31-Jan-2020.) |
| ⊢ ((𝐴Ref𝐵 ∧ 𝐵 ≠ ∅) → (𝐴 ∪ {∅})Ref𝐵) | ||
| Theorem | isptfin 23524* | The statement "is a point-finite cover." (Contributed by Jeff Hankins, 21-Jan-2010.) |
| ⊢ 𝑋 = ∪ 𝐴 ⇒ ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ PtFin ↔ ∀𝑥 ∈ 𝑋 {𝑦 ∈ 𝐴 ∣ 𝑥 ∈ 𝑦} ∈ Fin)) | ||
| Theorem | islocfin 23525* | The statement "is a locally finite cover." (Contributed by Jeff Hankins, 21-Jan-2010.) |
| ⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐴 ⇒ ⊢ (𝐴 ∈ (LocFin‘𝐽) ↔ (𝐽 ∈ Top ∧ 𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin))) | ||
| Theorem | finptfin 23526 | A finite cover is a point-finite cover. (Contributed by Jeff Hankins, 21-Jan-2010.) |
| ⊢ (𝐴 ∈ Fin → 𝐴 ∈ PtFin) | ||
| Theorem | ptfinfin 23527* | A point covered by a point-finite cover is only covered by finitely many elements. (Contributed by Jeff Hankins, 21-Jan-2010.) |
| ⊢ 𝑋 = ∪ 𝐴 ⇒ ⊢ ((𝐴 ∈ PtFin ∧ 𝑃 ∈ 𝑋) → {𝑥 ∈ 𝐴 ∣ 𝑃 ∈ 𝑥} ∈ Fin) | ||
| Theorem | finlocfin 23528 | A finite cover of a topological space is a locally finite cover. (Contributed by Jeff Hankins, 21-Jan-2010.) |
| ⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐴 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝑋 = 𝑌) → 𝐴 ∈ (LocFin‘𝐽)) | ||
| Theorem | locfintop 23529 | A locally finite cover covers a topological space. (Contributed by Jeff Hankins, 21-Jan-2010.) |
| ⊢ (𝐴 ∈ (LocFin‘𝐽) → 𝐽 ∈ Top) | ||
| Theorem | locfinbas 23530 | A locally finite cover must cover the base set of its corresponding topological space. (Contributed by Jeff Hankins, 21-Jan-2010.) |
| ⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐴 ⇒ ⊢ (𝐴 ∈ (LocFin‘𝐽) → 𝑋 = 𝑌) | ||
| Theorem | locfinnei 23531* | A point covered by a locally finite cover has a neighborhood which intersects only finitely many elements of the cover. (Contributed by Jeff Hankins, 21-Jan-2010.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐴 ∈ (LocFin‘𝐽) ∧ 𝑃 ∈ 𝑋) → ∃𝑛 ∈ 𝐽 (𝑃 ∈ 𝑛 ∧ {𝑠 ∈ 𝐴 ∣ (𝑠 ∩ 𝑛) ≠ ∅} ∈ Fin)) | ||
| Theorem | lfinpfin 23532 | A locally finite cover is point-finite. (Contributed by Jeff Hankins, 21-Jan-2010.) (Proof shortened by Mario Carneiro, 11-Sep-2015.) |
| ⊢ (𝐴 ∈ (LocFin‘𝐽) → 𝐴 ∈ PtFin) | ||
| Theorem | lfinun 23533 | Adding a finite set preserves locally finite covers. (Contributed by Thierry Arnoux, 31-Jan-2020.) |
| ⊢ ((𝐴 ∈ (LocFin‘𝐽) ∧ 𝐵 ∈ Fin ∧ ∪ 𝐵 ⊆ ∪ 𝐽) → (𝐴 ∪ 𝐵) ∈ (LocFin‘𝐽)) | ||
| Theorem | locfincmp 23534 | For a compact space, the locally finite covers are precisely the finite covers. Sadly, this property does not properly characterize all compact spaces. (Contributed by Jeff Hankins, 22-Jan-2010.) (Proof shortened by Mario Carneiro, 11-Sep-2015.) |
| ⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐶 ⇒ ⊢ (𝐽 ∈ Comp → (𝐶 ∈ (LocFin‘𝐽) ↔ (𝐶 ∈ Fin ∧ 𝑋 = 𝑌))) | ||
| Theorem | unisngl 23535* | Taking the union of the set of singletons recovers the initial set. (Contributed by Thierry Arnoux, 9-Jan-2020.) |
| ⊢ 𝐶 = {𝑢 ∣ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}} ⇒ ⊢ 𝑋 = ∪ 𝐶 | ||
| Theorem | dissnref 23536* | The set of singletons is a refinement of any open covering of the discrete topology. (Contributed by Thierry Arnoux, 9-Jan-2020.) |
| ⊢ 𝐶 = {𝑢 ∣ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}} ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ ∪ 𝑌 = 𝑋) → 𝐶Ref𝑌) | ||
| Theorem | dissnlocfin 23537* | The set of singletons is locally finite in the discrete topology. (Contributed by Thierry Arnoux, 9-Jan-2020.) |
| ⊢ 𝐶 = {𝑢 ∣ ∃𝑥 ∈ 𝑋 𝑢 = {𝑥}} ⇒ ⊢ (𝑋 ∈ 𝑉 → 𝐶 ∈ (LocFin‘𝒫 𝑋)) | ||
| Theorem | locfindis 23538 | The locally finite covers of a discrete space are precisely the point-finite covers. (Contributed by Jeff Hankins, 22-Jan-2010.) (Proof shortened by Mario Carneiro, 11-Sep-2015.) |
| ⊢ 𝑌 = ∪ 𝐶 ⇒ ⊢ (𝐶 ∈ (LocFin‘𝒫 𝑋) ↔ (𝐶 ∈ PtFin ∧ 𝑋 = 𝑌)) | ||
| Theorem | locfincf 23539 | A locally finite cover in a coarser topology is locally finite in a finer topology. (Contributed by Jeff Hankins, 22-Jan-2010.) (Proof shortened by Mario Carneiro, 11-Sep-2015.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) → (LocFin‘𝐽) ⊆ (LocFin‘𝐾)) | ||
| Theorem | comppfsc 23540* | A space where every open cover has a point-finite subcover is compact. This is significant in part because it shows half of the proposition that if only half the generalization in the definition of metacompactness (and consequently paracompactness) is performed, one does not obtain any more spaces. (Contributed by Jeff Hankins, 21-Jan-2010.) (Proof shortened by Mario Carneiro, 11-Sep-2015.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (𝐽 ∈ Comp ↔ ∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ PtFin (𝑑 ⊆ 𝑐 ∧ 𝑋 = ∪ 𝑑)))) | ||
| Syntax | ckgen 23541 | Extend class notation with the compact generator operation. |
| class 𝑘Gen | ||
| Definition | df-kgen 23542* | Define the "compact generator", the functor from topological spaces to compactly generated spaces. Also known as the k-ification operation. A set is k-open, i.e. 𝑥 ∈ (𝑘Gen‘𝑗), iff the preimage of 𝑥 is open in all compact Hausdorff spaces. (Contributed by Mario Carneiro, 20-Mar-2015.) |
| ⊢ 𝑘Gen = (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 ∪ 𝑗 ∣ ∀𝑘 ∈ 𝒫 ∪ 𝑗((𝑗 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝑗 ↾t 𝑘))}) | ||
| Theorem | kgenval 23543* | Value of the compact generator. (The "k" in 𝑘Gen comes from the name "k-space" for these spaces, after the German word kompakt.) (Contributed by Mario Carneiro, 20-Mar-2015.) |
| ⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝑘Gen‘𝐽) = {𝑥 ∈ 𝒫 𝑋 ∣ ∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘))}) | ||
| Theorem | elkgen 23544* | Value of the compact generator. (Contributed by Mario Carneiro, 20-Mar-2015.) |
| ⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐴 ∈ (𝑘Gen‘𝐽) ↔ (𝐴 ⊆ 𝑋 ∧ ∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (𝐴 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘))))) | ||
| Theorem | kgeni 23545 | Property of the open sets in the compact generator. (Contributed by Mario Carneiro, 20-Mar-2015.) |
| ⊢ ((𝐴 ∈ (𝑘Gen‘𝐽) ∧ (𝐽 ↾t 𝐾) ∈ Comp) → (𝐴 ∩ 𝐾) ∈ (𝐽 ↾t 𝐾)) | ||
| Theorem | kgentopon 23546 | The compact generator generates a topology. (Contributed by Mario Carneiro, 22-Aug-2015.) |
| ⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝑘Gen‘𝐽) ∈ (TopOn‘𝑋)) | ||
| Theorem | kgenuni 23547 | The base set of the compact generator is the same as the original topology. (Contributed by Mario Carneiro, 20-Mar-2015.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → 𝑋 = ∪ (𝑘Gen‘𝐽)) | ||
| Theorem | kgenftop 23548 | The compact generator generates a topology. (Contributed by Mario Carneiro, 20-Mar-2015.) |
| ⊢ (𝐽 ∈ Top → (𝑘Gen‘𝐽) ∈ Top) | ||
| Theorem | kgenf 23549 | The compact generator is a function on topologies. (Contributed by Mario Carneiro, 20-Mar-2015.) |
| ⊢ 𝑘Gen:Top⟶Top | ||
| Theorem | kgentop 23550 | A compactly generated space is a topology. (Note: henceforth we will use the idiom "𝐽 ∈ ran 𝑘Gen " to denote "𝐽 is compactly generated", since as we will show a space is compactly generated iff it is in the range of the compact generator.) (Contributed by Mario Carneiro, 20-Mar-2015.) |
| ⊢ (𝐽 ∈ ran 𝑘Gen → 𝐽 ∈ Top) | ||
| Theorem | kgenss 23551 | The compact generator generates a finer topology than the original. (Contributed by Mario Carneiro, 20-Mar-2015.) |
| ⊢ (𝐽 ∈ Top → 𝐽 ⊆ (𝑘Gen‘𝐽)) | ||
| Theorem | kgenhaus 23552 | The compact generator generates another Hausdorff topology given a Hausdorff topology to start from. (Contributed by Mario Carneiro, 21-Mar-2015.) |
| ⊢ (𝐽 ∈ Haus → (𝑘Gen‘𝐽) ∈ Haus) | ||
| Theorem | kgencmp 23553 | The compact generator topology is the same as the original topology on compact subspaces. (Contributed by Mario Carneiro, 20-Mar-2015.) |
| ⊢ ((𝐽 ∈ Top ∧ (𝐽 ↾t 𝐾) ∈ Comp) → (𝐽 ↾t 𝐾) = ((𝑘Gen‘𝐽) ↾t 𝐾)) | ||
| Theorem | kgencmp2 23554 | The compact generator topology has the same compact sets as the original topology. (Contributed by Mario Carneiro, 20-Mar-2015.) |
| ⊢ (𝐽 ∈ Top → ((𝐽 ↾t 𝐾) ∈ Comp ↔ ((𝑘Gen‘𝐽) ↾t 𝐾) ∈ Comp)) | ||
| Theorem | kgenidm 23555 | The compact generator is idempotent on compactly generated spaces. (Contributed by Mario Carneiro, 20-Mar-2015.) |
| ⊢ (𝐽 ∈ ran 𝑘Gen → (𝑘Gen‘𝐽) = 𝐽) | ||
| Theorem | iskgen2 23556 | A space is compactly generated iff it contains its image under the compact generator. (Contributed by Mario Carneiro, 20-Mar-2015.) |
| ⊢ (𝐽 ∈ ran 𝑘Gen ↔ (𝐽 ∈ Top ∧ (𝑘Gen‘𝐽) ⊆ 𝐽)) | ||
| Theorem | iskgen3 23557* | Derive the usual definition of "compactly generated". A topology is compactly generated if every subset of 𝑋 that is open in every compact subset is open. (Contributed by Mario Carneiro, 20-Mar-2015.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ ran 𝑘Gen ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝒫 𝑋(∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (𝑥 ∩ 𝑘) ∈ (𝐽 ↾t 𝑘)) → 𝑥 ∈ 𝐽))) | ||
| Theorem | llycmpkgen2 23558* | A locally compact space is compactly generated. (This variant of llycmpkgen 23560 uses the weaker definition of locally compact, "every point has a compact neighborhood", instead of "every point has a local base of compact neighborhoods".) (Contributed by Mario Carneiro, 21-Mar-2015.) |
| ⊢ 𝑋 = ∪ 𝐽 & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ∃𝑘 ∈ ((nei‘𝐽)‘{𝑥})(𝐽 ↾t 𝑘) ∈ Comp) ⇒ ⊢ (𝜑 → 𝐽 ∈ ran 𝑘Gen) | ||
| Theorem | cmpkgen 23559 | A compact space is compactly generated. (Contributed by Mario Carneiro, 21-Mar-2015.) |
| ⊢ (𝐽 ∈ Comp → 𝐽 ∈ ran 𝑘Gen) | ||
| Theorem | llycmpkgen 23560 | A locally compact space is compactly generated. (Contributed by Mario Carneiro, 21-Mar-2015.) |
| ⊢ (𝐽 ∈ 𝑛-Locally Comp → 𝐽 ∈ ran 𝑘Gen) | ||
| Theorem | 1stckgenlem 23561 | The one-point compactification of ℕ is compact. (Contributed by Mario Carneiro, 21-Mar-2015.) |
| ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐹:ℕ⟶𝑋) & ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝐴) ⇒ ⊢ (𝜑 → (𝐽 ↾t (ran 𝐹 ∪ {𝐴})) ∈ Comp) | ||
| Theorem | 1stckgen 23562 | A first-countable space is compactly generated. (Contributed by Mario Carneiro, 21-Mar-2015.) |
| ⊢ (𝐽 ∈ 1stω → 𝐽 ∈ ran 𝑘Gen) | ||
| Theorem | kgen2ss 23563 | The compact generator preserves the subset (fineness) relationship on topologies. (Contributed by Mario Carneiro, 21-Mar-2015.) |
| ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) → (𝑘Gen‘𝐽) ⊆ (𝑘Gen‘𝐾)) | ||
| Theorem | kgencn 23564* | A function from a compactly generated space is continuous iff it is continuous "on compacta". (Contributed by Mario Carneiro, 21-Mar-2015.) |
| ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ ((𝑘Gen‘𝐽) Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑘 ∈ 𝒫 𝑋((𝐽 ↾t 𝑘) ∈ Comp → (𝐹 ↾ 𝑘) ∈ ((𝐽 ↾t 𝑘) Cn 𝐾))))) | ||
| Theorem | kgencn2 23565* | A function 𝐹:𝐽⟶𝐾 from a compactly generated space is continuous iff for all compact spaces 𝑧 and continuous 𝑔:𝑧⟶𝐽, the composite 𝐹 ∘ 𝑔:𝑧⟶𝐾 is continuous. (Contributed by Mario Carneiro, 21-Mar-2015.) |
| ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ ((𝑘Gen‘𝐽) Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑧 ∈ Comp ∀𝑔 ∈ (𝑧 Cn 𝐽)(𝐹 ∘ 𝑔) ∈ (𝑧 Cn 𝐾)))) | ||
| Theorem | kgencn3 23566 | The set of continuous functions from 𝐽 to 𝐾 is unaffected by k-ification of 𝐾, if 𝐽 is already compactly generated. (Contributed by Mario Carneiro, 21-Mar-2015.) |
| ⊢ ((𝐽 ∈ ran 𝑘Gen ∧ 𝐾 ∈ Top) → (𝐽 Cn 𝐾) = (𝐽 Cn (𝑘Gen‘𝐾))) | ||
| Theorem | kgen2cn 23567 | A continuous function is also continuous with the domain and codomain replaced by their compact generator topologies. (Contributed by Mario Carneiro, 21-Mar-2015.) |
| ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹 ∈ ((𝑘Gen‘𝐽) Cn (𝑘Gen‘𝐾))) | ||
| Syntax | ctx 23568 | Extend class notation with the binary topological product operation. |
| class ×t | ||
| Syntax | cxko 23569 | Extend class notation with a function whose value is the compact-open topology. |
| class ↑ko | ||
| Definition | df-tx 23570* | Define the binary topological product, which is homeomorphic to the general topological product over a two element set, but is more convenient to use. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ ×t = (𝑟 ∈ V, 𝑠 ∈ V ↦ (topGen‘ran (𝑥 ∈ 𝑟, 𝑦 ∈ 𝑠 ↦ (𝑥 × 𝑦)))) | ||
| Definition | df-xko 23571* | Define the compact-open topology, which is the natural topology on the set of continuous functions between two topological spaces. (Contributed by Mario Carneiro, 19-Mar-2015.) |
| ⊢ ↑ko = (𝑠 ∈ Top, 𝑟 ∈ Top ↦ (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 ∪ 𝑟 ∣ (𝑟 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑠 ↦ {𝑓 ∈ (𝑟 Cn 𝑠) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})))) | ||
| Theorem | txval 23572* | Value of the binary topological product operation. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 30-Aug-2015.) |
| ⊢ 𝐵 = ran (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑆 ↦ (𝑥 × 𝑦)) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (𝑅 ×t 𝑆) = (topGen‘𝐵)) | ||
| Theorem | txuni2 23573* | The underlying set of the product of two topologies. (Contributed by Mario Carneiro, 31-Aug-2015.) |
| ⊢ 𝐵 = ran (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑆 ↦ (𝑥 × 𝑦)) & ⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝑌 = ∪ 𝑆 ⇒ ⊢ (𝑋 × 𝑌) = ∪ 𝐵 | ||
| Theorem | txbasex 23574* | The basis for the product topology is a set. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| ⊢ 𝐵 = ran (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑆 ↦ (𝑥 × 𝑦)) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → 𝐵 ∈ V) | ||
| Theorem | txbas 23575* | The set of Cartesian products of elements from two topological bases is a basis. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 31-Aug-2015.) |
| ⊢ 𝐵 = ran (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑆 ↦ (𝑥 × 𝑦)) ⇒ ⊢ ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → 𝐵 ∈ TopBases) | ||
| Theorem | eltx 23576* | A set in a product is open iff each point is surrounded by an open rectangle. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
| ⊢ ((𝐽 ∈ 𝑉 ∧ 𝐾 ∈ 𝑊) → (𝑆 ∈ (𝐽 ×t 𝐾) ↔ ∀𝑝 ∈ 𝑆 ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ 𝐾 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ 𝑆))) | ||
| Theorem | txtop 23577 | The product of two topologies is a topology. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top) | ||
| Theorem | ptval 23578* | The value of the product topology function. (Contributed by Mario Carneiro, 3-Feb-2015.) |
| ⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴) → (∏t‘𝐹) = (topGen‘𝐵)) | ||
| Theorem | ptpjpre1 23579* | The preimage of a projection function can be expressed as an indexed cartesian product. (Contributed by Mario Carneiro, 6-Feb-2015.) |
| ⊢ 𝑋 = X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) ⇒ ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝐼 ∈ 𝐴 ∧ 𝑈 ∈ (𝐹‘𝐼))) → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝐼)) “ 𝑈) = X𝑘 ∈ 𝐴 if(𝑘 = 𝐼, 𝑈, ∪ (𝐹‘𝑘))) | ||
| Theorem | elpt 23580* | Elementhood in the bases of a product topology. (Contributed by Mario Carneiro, 3-Feb-2015.) |
| ⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ⇒ ⊢ (𝑆 ∈ 𝐵 ↔ ∃ℎ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑤 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑤)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑆 = X𝑦 ∈ 𝐴 (ℎ‘𝑦))) | ||
| Theorem | elptr 23581* | A basic open set in the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.) |
| ⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ (𝐺 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝐺‘𝑦) ∈ (𝐹‘𝑦)) ∧ (𝑊 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑊)(𝐺‘𝑦) = ∪ (𝐹‘𝑦))) → X𝑦 ∈ 𝐴 (𝐺‘𝑦) ∈ 𝐵) | ||
| Theorem | elptr2 23582* | A basic open set in the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.) |
| ⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑊 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑆 ∈ (𝐹‘𝑘)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝑊)) → 𝑆 = ∪ (𝐹‘𝑘)) ⇒ ⊢ (𝜑 → X𝑘 ∈ 𝐴 𝑆 ∈ 𝐵) | ||
| Theorem | ptbasid 23583* | The base set of the product topology is a basic open set. (Contributed by Mario Carneiro, 3-Feb-2015.) |
| ⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) ∈ 𝐵) | ||
| Theorem | ptuni2 23584* | The base set for the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.) |
| ⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) = ∪ 𝐵) | ||
| Theorem | ptbasin 23585* | The basis for a product topology is closed under intersections. (Contributed by Mario Carneiro, 3-Feb-2015.) |
| ⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ⇒ ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ∩ 𝑌) ∈ 𝐵) | ||
| Theorem | ptbasin2 23586* | The basis for a product topology is closed under intersections. (Contributed by Mario Carneiro, 19-Mar-2015.) |
| ⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (fi‘𝐵) = 𝐵) | ||
| Theorem | ptbas 23587* | The basis for a product topology is a basis. (Contributed by Mario Carneiro, 3-Feb-2015.) |
| ⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐵 ∈ TopBases) | ||
| Theorem | ptpjpre2 23588* | The basis for a product topology is a basis. (Contributed by Mario Carneiro, 3-Feb-2015.) |
| ⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} & ⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ⇒ ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝐼 ∈ 𝐴 ∧ 𝑈 ∈ (𝐹‘𝐼))) → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝐼)) “ 𝑈) ∈ 𝐵) | ||
| Theorem | ptbasfi 23589* | The basis for the product topology can also be written as the set of finite intersections of "cylinder sets", the preimages of projections into one factor from open sets in the factor. (We have to add 𝑋 itself to the list because if 𝐴 is empty we get (fi‘∅) = ∅ while 𝐵 = {∅}.) (Contributed by Mario Carneiro, 3-Feb-2015.) |
| ⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} & ⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐵 = (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))) | ||
| Theorem | pttop 23590 | The product topology is a topology. (Contributed by Mario Carneiro, 3-Feb-2015.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (∏t‘𝐹) ∈ Top) | ||
| Theorem | ptopn 23591* | A basic open set in the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶Top) & ⊢ (𝜑 → 𝑊 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑆 ∈ (𝐹‘𝑘)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝑊)) → 𝑆 = ∪ (𝐹‘𝑘)) ⇒ ⊢ (𝜑 → X𝑘 ∈ 𝐴 𝑆 ∈ (∏t‘𝐹)) | ||
| Theorem | ptopn2 23592* | A sub-basic open set in the product topology. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶Top) & ⊢ (𝜑 → 𝑂 ∈ (𝐹‘𝑌)) ⇒ ⊢ (𝜑 → X𝑘 ∈ 𝐴 if(𝑘 = 𝑌, 𝑂, ∪ (𝐹‘𝑘)) ∈ (∏t‘𝐹)) | ||
| Theorem | xkotf 23593* | Functionality of function 𝑇. (Contributed by Mario Carneiro, 19-Mar-2015.) |
| ⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝐾 = {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp} & ⊢ 𝑇 = (𝑘 ∈ 𝐾, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ⇒ ⊢ 𝑇:(𝐾 × 𝑆)⟶𝒫 (𝑅 Cn 𝑆) | ||
| Theorem | xkobval 23594* | Alternative expression for the subbase of the compact-open topology. (Contributed by Mario Carneiro, 23-Mar-2015.) |
| ⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝐾 = {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp} & ⊢ 𝑇 = (𝑘 ∈ 𝐾, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ⇒ ⊢ ran 𝑇 = {𝑠 ∣ ∃𝑘 ∈ 𝒫 𝑋∃𝑣 ∈ 𝑆 ((𝑅 ↾t 𝑘) ∈ Comp ∧ 𝑠 = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})} | ||
| Theorem | xkoval 23595* | Value of the compact-open topology. (Contributed by Mario Carneiro, 19-Mar-2015.) |
| ⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝐾 = {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp} & ⊢ 𝑇 = (𝑘 ∈ 𝐾, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ⇒ ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ↑ko 𝑅) = (topGen‘(fi‘ran 𝑇))) | ||
| Theorem | xkotop 23596 | The compact-open topology is a topology. (Contributed by Mario Carneiro, 19-Mar-2015.) |
| ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ↑ko 𝑅) ∈ Top) | ||
| Theorem | xkoopn 23597* | A basic open set of the compact-open topology. (Contributed by Mario Carneiro, 19-Mar-2015.) |
| ⊢ 𝑋 = ∪ 𝑅 & ⊢ (𝜑 → 𝑅 ∈ Top) & ⊢ (𝜑 → 𝑆 ∈ Top) & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) & ⊢ (𝜑 → (𝑅 ↾t 𝐴) ∈ Comp) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) ⇒ ⊢ (𝜑 → {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝐴) ⊆ 𝑈} ∈ (𝑆 ↑ko 𝑅)) | ||
| Theorem | txtopi 23598 | The product of two topologies is a topology. (Contributed by Jeff Madsen, 15-Jun-2010.) |
| ⊢ 𝑅 ∈ Top & ⊢ 𝑆 ∈ Top ⇒ ⊢ (𝑅 ×t 𝑆) ∈ Top | ||
| Theorem | txtopon 23599 | The underlying set of the product of two topologies. (Contributed by Mario Carneiro, 22-Aug-2015.) (Revised by Mario Carneiro, 2-Sep-2015.) |
| ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑅 ×t 𝑆) ∈ (TopOn‘(𝑋 × 𝑌))) | ||
| Theorem | txuni 23600 | The underlying set of the product of two topologies. (Contributed by Jeff Madsen, 2-Sep-2009.) |
| ⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝑌 = ∪ 𝑆 ⇒ ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × 𝑌) = ∪ (𝑅 ×t 𝑆)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |