![]() |
Metamath
Proof Explorer Theorem List (p. 237 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ptbasin2 23601* | The basis for a product topology is closed under intersections. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (fi‘𝐵) = 𝐵) | ||
Theorem | ptbas 23602* | The basis for a product topology is a basis. (Contributed by Mario Carneiro, 3-Feb-2015.) |
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐵 ∈ TopBases) | ||
Theorem | ptpjpre2 23603* | The basis for a product topology is a basis. (Contributed by Mario Carneiro, 3-Feb-2015.) |
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} & ⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ⇒ ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝐼 ∈ 𝐴 ∧ 𝑈 ∈ (𝐹‘𝐼))) → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝐼)) “ 𝑈) ∈ 𝐵) | ||
Theorem | ptbasfi 23604* | 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 23605 | The product topology is a topology. (Contributed by Mario Carneiro, 3-Feb-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (∏t‘𝐹) ∈ Top) | ||
Theorem | ptopn 23606* | A basic open set in the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶Top) & ⊢ (𝜑 → 𝑊 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑆 ∈ (𝐹‘𝑘)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝑊)) → 𝑆 = ∪ (𝐹‘𝑘)) ⇒ ⊢ (𝜑 → X𝑘 ∈ 𝐴 𝑆 ∈ (∏t‘𝐹)) | ||
Theorem | ptopn2 23607* | A sub-basic open set in the product topology. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶Top) & ⊢ (𝜑 → 𝑂 ∈ (𝐹‘𝑌)) ⇒ ⊢ (𝜑 → X𝑘 ∈ 𝐴 if(𝑘 = 𝑌, 𝑂, ∪ (𝐹‘𝑘)) ∈ (∏t‘𝐹)) | ||
Theorem | xkotf 23608* | Functionality of function 𝑇. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝐾 = {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp} & ⊢ 𝑇 = (𝑘 ∈ 𝐾, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ⇒ ⊢ 𝑇:(𝐾 × 𝑆)⟶𝒫 (𝑅 Cn 𝑆) | ||
Theorem | xkobval 23609* | 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 23610* | Value of the compact-open topology. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝐾 = {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp} & ⊢ 𝑇 = (𝑘 ∈ 𝐾, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ⇒ ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ↑ko 𝑅) = (topGen‘(fi‘ran 𝑇))) | ||
Theorem | xkotop 23611 | The compact-open topology is a topology. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ↑ko 𝑅) ∈ Top) | ||
Theorem | xkoopn 23612* | A basic open set of the compact-open topology. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ 𝑋 = ∪ 𝑅 & ⊢ (𝜑 → 𝑅 ∈ Top) & ⊢ (𝜑 → 𝑆 ∈ Top) & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) & ⊢ (𝜑 → (𝑅 ↾t 𝐴) ∈ Comp) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) ⇒ ⊢ (𝜑 → {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝐴) ⊆ 𝑈} ∈ (𝑆 ↑ko 𝑅)) | ||
Theorem | txtopi 23613 | The product of two topologies is a topology. (Contributed by Jeff Madsen, 15-Jun-2010.) |
⊢ 𝑅 ∈ Top & ⊢ 𝑆 ∈ Top ⇒ ⊢ (𝑅 ×t 𝑆) ∈ Top | ||
Theorem | txtopon 23614 | 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 23615 | The underlying set of the product of two topologies. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝑌 = ∪ 𝑆 ⇒ ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × 𝑌) = ∪ (𝑅 ×t 𝑆)) | ||
Theorem | txunii 23616 | The underlying set of the product of two topologies. (Contributed by Jeff Madsen, 15-Jun-2010.) |
⊢ 𝑅 ∈ Top & ⊢ 𝑆 ∈ Top & ⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝑌 = ∪ 𝑆 ⇒ ⊢ (𝑋 × 𝑌) = ∪ (𝑅 ×t 𝑆) | ||
Theorem | ptuni 23617* | The base set for the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.) |
⊢ 𝐽 = (∏t‘𝐹) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → X𝑥 ∈ 𝐴 ∪ (𝐹‘𝑥) = ∪ 𝐽) | ||
Theorem | ptunimpt 23618* | Base set of a product topology given by substitution. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ 𝐽 = (∏t‘(𝑥 ∈ 𝐴 ↦ 𝐾)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐾 ∈ Top) → X𝑥 ∈ 𝐴 ∪ 𝐾 = ∪ 𝐽) | ||
Theorem | pttopon 23619* | The base set for the product topology. (Contributed by Mario Carneiro, 22-Aug-2015.) |
⊢ 𝐽 = (∏t‘(𝑥 ∈ 𝐴 ↦ 𝐾)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐾 ∈ (TopOn‘𝐵)) → 𝐽 ∈ (TopOn‘X𝑥 ∈ 𝐴 𝐵)) | ||
Theorem | pttoponconst 23620 | The base set for a product topology when all factors are the same. (Contributed by Mario Carneiro, 22-Aug-2015.) |
⊢ 𝐽 = (∏t‘(𝐴 × {𝑅})) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ (TopOn‘𝑋)) → 𝐽 ∈ (TopOn‘(𝑋 ↑m 𝐴))) | ||
Theorem | ptuniconst 23621 | The base set for a product topology when all factors are the same. (Contributed by Mario Carneiro, 3-Feb-2015.) |
⊢ 𝐽 = (∏t‘(𝐴 × {𝑅})) & ⊢ 𝑋 = ∪ 𝑅 ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ Top) → (𝑋 ↑m 𝐴) = ∪ 𝐽) | ||
Theorem | xkouni 23622 | The base set of the compact-open topology. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ 𝐽 = (𝑆 ↑ko 𝑅) ⇒ ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) = ∪ 𝐽) | ||
Theorem | xkotopon 23623 | The base set of the compact-open topology. (Contributed by Mario Carneiro, 22-Aug-2015.) |
⊢ 𝐽 = (𝑆 ↑ko 𝑅) ⇒ ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝐽 ∈ (TopOn‘(𝑅 Cn 𝑆))) | ||
Theorem | ptval2 23624* | The value of the product topology function. (Contributed by Mario Carneiro, 7-Feb-2015.) |
⊢ 𝐽 = (∏t‘𝐹) & ⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐺 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐽 = (topGen‘(fi‘({𝑋} ∪ ran 𝐺)))) | ||
Theorem | txopn 23625 | The product of two open sets is open in the product topology. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) ∧ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆)) → (𝐴 × 𝐵) ∈ (𝑅 ×t 𝑆)) | ||
Theorem | txcld 23626 | The product of two closed sets is closed in the product topology. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 3-Sep-2015.) |
⊢ ((𝐴 ∈ (Clsd‘𝑅) ∧ 𝐵 ∈ (Clsd‘𝑆)) → (𝐴 × 𝐵) ∈ (Clsd‘(𝑅 ×t 𝑆))) | ||
Theorem | txcls 23627 | Closure of a rectangle in the product topology. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)) = (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵))) | ||
Theorem | txss12 23628 | Subset property of the topological product. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)) → (𝐴 ×t 𝐶) ⊆ (𝐵 ×t 𝐷)) | ||
Theorem | txbasval 23629 | It is sufficient to consider products of the bases for the topologies in the topological product. (Contributed by Mario Carneiro, 25-Aug-2014.) |
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → ((topGen‘𝑅) ×t (topGen‘𝑆)) = (𝑅 ×t 𝑆)) | ||
Theorem | neitx 23630 | The Cartesian product of two neighborhoods is a neighborhood in the product topology. (Contributed by Thierry Arnoux, 13-Jan-2018.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → (𝐴 × 𝐵) ∈ ((nei‘(𝐽 ×t 𝐾))‘(𝐶 × 𝐷))) | ||
Theorem | txcnpi 23631* | Continuity of a two-argument function at a point. (Contributed by Mario Carneiro, 20-Sep-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝐹 ∈ (((𝐽 ×t 𝐾) CnP 𝐿)‘〈𝐴, 𝐵〉)) & ⊢ (𝜑 → 𝑈 ∈ 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑌) & ⊢ (𝜑 → (𝐴𝐹𝐵) ∈ 𝑈) ⇒ ⊢ (𝜑 → ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐾 (𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐹 “ 𝑈))) | ||
Theorem | tx1cn 23632 | Continuity of the first projection map of a topological product. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Aug-2015.) |
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (1st ↾ (𝑋 × 𝑌)) ∈ ((𝑅 ×t 𝑆) Cn 𝑅)) | ||
Theorem | tx2cn 23633 | Continuity of the second projection map of a topological product. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Aug-2015.) |
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (2nd ↾ (𝑋 × 𝑌)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆)) | ||
Theorem | ptpjcn 23634* | Continuity of a projection map into a topological product. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 3-Feb-2015.) |
⊢ 𝑌 = ∪ 𝐽 & ⊢ 𝐽 = (∏t‘𝐹) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐼 ∈ 𝐴) → (𝑥 ∈ 𝑌 ↦ (𝑥‘𝐼)) ∈ (𝐽 Cn (𝐹‘𝐼))) | ||
Theorem | ptpjopn 23635* | The projection map is an open map. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ 𝑌 = ∪ 𝐽 & ⊢ 𝐽 = (∏t‘𝐹) ⇒ ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐼 ∈ 𝐴) ∧ 𝑈 ∈ 𝐽) → ((𝑥 ∈ 𝑌 ↦ (𝑥‘𝐼)) “ 𝑈) ∈ (𝐹‘𝐼)) | ||
Theorem | ptcld 23636* | A closed box in the product topology. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶Top) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (Clsd‘(𝐹‘𝑘))) ⇒ ⊢ (𝜑 → X𝑘 ∈ 𝐴 𝐶 ∈ (Clsd‘(∏t‘𝐹))) | ||
Theorem | ptcldmpt 23637* | A closed box in the product topology. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐽 ∈ Top) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (Clsd‘𝐽)) ⇒ ⊢ (𝜑 → X𝑘 ∈ 𝐴 𝐶 ∈ (Clsd‘(∏t‘(𝑘 ∈ 𝐴 ↦ 𝐽)))) | ||
Theorem | ptclsg 23638* | The closure of a box in the product topology is the box formed from the closures of the factors. The proof uses the axiom of choice; the last hypothesis is the choice assumption. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝐽 = (∏t‘(𝑘 ∈ 𝐴 ↦ 𝑅)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑅 ∈ (TopOn‘𝑋)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑆 ⊆ 𝑋) & ⊢ (𝜑 → ∪ 𝑘 ∈ 𝐴 𝑆 ∈ AC 𝐴) ⇒ ⊢ (𝜑 → ((cls‘𝐽)‘X𝑘 ∈ 𝐴 𝑆) = X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) | ||
Theorem | ptcls 23639* | The closure of a box in the product topology is the box formed from the closures of the factors. This theorem is an AC equivalent. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ 𝐽 = (∏t‘(𝑘 ∈ 𝐴 ↦ 𝑅)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑅 ∈ (TopOn‘𝑋)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑆 ⊆ 𝑋) ⇒ ⊢ (𝜑 → ((cls‘𝐽)‘X𝑘 ∈ 𝐴 𝑆) = X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) | ||
Theorem | dfac14lem 23640* | Lemma for dfac14 23641. By equipping 𝑆 ∪ {𝑃} for some 𝑃 ∉ 𝑆 with the particular point topology, we can show that 𝑃 is in the closure of 𝑆; hence the sequence 𝑃(𝑥) is in the product of the closures, and we can utilize this instance of ptcls 23639 to extract an element of the closure of X𝑘 ∈ 𝐼𝑆. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ≠ ∅) & ⊢ 𝑃 = 𝒫 ∪ 𝑆 & ⊢ 𝑅 = {𝑦 ∈ 𝒫 (𝑆 ∪ {𝑃}) ∣ (𝑃 ∈ 𝑦 → 𝑦 = (𝑆 ∪ {𝑃}))} & ⊢ 𝐽 = (∏t‘(𝑥 ∈ 𝐼 ↦ 𝑅)) & ⊢ (𝜑 → ((cls‘𝐽)‘X𝑥 ∈ 𝐼 𝑆) = X𝑥 ∈ 𝐼 ((cls‘𝑅)‘𝑆)) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐼 𝑆 ≠ ∅) | ||
Theorem | dfac14 23641* | Theorem ptcls 23639 is an equivalent of the axiom of choice. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ (CHOICE ↔ ∀𝑓(𝑓:dom 𝑓⟶Top → ∀𝑠 ∈ X 𝑘 ∈ dom 𝑓𝒫 ∪ (𝑓‘𝑘)((cls‘(∏t‘𝑓))‘X𝑘 ∈ dom 𝑓(𝑠‘𝑘)) = X𝑘 ∈ dom 𝑓((cls‘(𝑓‘𝑘))‘(𝑠‘𝑘)))) | ||
Theorem | xkoccn 23642* | The "constant function" function which maps 𝑥 ∈ 𝑌 to the constant function 𝑧 ∈ 𝑋 ↦ 𝑥 is a continuous function from 𝑋 into the space of continuous functions from 𝑌 to 𝑋. This can also be understood as the currying of the first projection function. (The currying of the second projection function is 𝑥 ∈ 𝑌 ↦ (𝑧 ∈ 𝑋 ↦ 𝑧), which we already know is continuous because it is a constant function.) (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑥 ∈ 𝑌 ↦ (𝑋 × {𝑥})) ∈ (𝑆 Cn (𝑆 ↑ko 𝑅))) | ||
Theorem | txcnp 23643* | If two functions are continuous at 𝐷, then the ordered pair of them is continuous at 𝐷 into the product topology. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍)) & ⊢ (𝜑 → 𝐷 ∈ 𝑋) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP 𝐾)‘𝐷)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ ((𝐽 CnP 𝐿)‘𝐷)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 〈𝐴, 𝐵〉) ∈ ((𝐽 CnP (𝐾 ×t 𝐿))‘𝐷)) | ||
Theorem | ptcnplem 23644* | Lemma for ptcnp 23645. (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ 𝐾 = (∏t‘𝐹) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼⟶Top) & ⊢ (𝜑 → 𝐷 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (𝐹‘𝑘))‘𝐷)) & ⊢ Ⅎ𝑘𝜓 & ⊢ ((𝜑 ∧ 𝜓) → 𝐺 Fn 𝐼) & ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ 𝐼) → (𝐺‘𝑘) ∈ (𝐹‘𝑘)) & ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ Fin) & ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ (𝐼 ∖ 𝑊)) → (𝐺‘𝑘) = ∪ (𝐹‘𝑘)) & ⊢ ((𝜑 ∧ 𝜓) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘))) | ||
Theorem | ptcnp 23645* | If every projection of a function is continuous at 𝐷, then the function itself is continuous at 𝐷 into the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ 𝐾 = (∏t‘𝐹) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼⟶Top) & ⊢ (𝜑 → 𝐷 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (𝐹‘𝑘))‘𝐷)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) ∈ ((𝐽 CnP 𝐾)‘𝐷)) | ||
Theorem | upxp 23646* | Universal property of the Cartesian product considered as a categorical product in the category of sets. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 27-Dec-2014.) |
⊢ 𝑃 = (1st ↾ (𝐵 × 𝐶)) & ⊢ 𝑄 = (2nd ↾ (𝐵 × 𝐶)) ⇒ ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) → ∃!ℎ(ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) | ||
Theorem | txcnmpt 23647* | A map into the product of two topological spaces is continuous if both of its projections are continuous. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ 𝑊 = ∪ 𝑈 & ⊢ 𝐻 = (𝑥 ∈ 𝑊 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) ⇒ ⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → 𝐻 ∈ (𝑈 Cn (𝑅 ×t 𝑆))) | ||
Theorem | uptx 23648* | Universal property of the binary topological product. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Aug-2015.) |
⊢ 𝑇 = (𝑅 ×t 𝑆) & ⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝑌 = ∪ 𝑆 & ⊢ 𝑍 = (𝑋 × 𝑌) & ⊢ 𝑃 = (1st ↾ 𝑍) & ⊢ 𝑄 = (2nd ↾ 𝑍) ⇒ ⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ∃!ℎ ∈ (𝑈 Cn 𝑇)(𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) | ||
Theorem | txcn 23649 | A map into the product of two topological spaces is continuous iff both of its projections are continuous. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Aug-2015.) |
⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝑌 = ∪ 𝑆 & ⊢ 𝑍 = (𝑋 × 𝑌) & ⊢ 𝑊 = ∪ 𝑈 & ⊢ 𝑃 = (1st ↾ 𝑍) & ⊢ 𝑄 = (2nd ↾ 𝑍) ⇒ ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) → (𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ↔ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆)))) | ||
Theorem | ptcn 23650* | If every projection of a function is continuous, then the function itself is continuous into the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.) |
⊢ 𝐾 = (∏t‘𝐹) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼⟶Top) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn (𝐹‘𝑘))) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) ∈ (𝐽 Cn 𝐾)) | ||
Theorem | prdstopn 23651 | Topology of a structure product. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 Fn 𝐼) & ⊢ 𝑂 = (TopOpen‘𝑌) ⇒ ⊢ (𝜑 → 𝑂 = (∏t‘(TopOpen ∘ 𝑅))) | ||
Theorem | prdstps 23652 | A structure product of topological spaces is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅:𝐼⟶TopSp) ⇒ ⊢ (𝜑 → 𝑌 ∈ TopSp) | ||
Theorem | pwstps 23653 | A structure power of a topological space is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) ⇒ ⊢ ((𝑅 ∈ TopSp ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ TopSp) | ||
Theorem | txrest 23654 | The subspace of a topological product space induced by a subset with a Cartesian product representation is a topological product of the subspaces induced by the subspaces of the terms of the products. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 2-Sep-2015.) |
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → ((𝑅 ×t 𝑆) ↾t (𝐴 × 𝐵)) = ((𝑅 ↾t 𝐴) ×t (𝑆 ↾t 𝐵))) | ||
Theorem | txdis 23655 | The topological product of discrete spaces is discrete. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝒫 𝐴 ×t 𝒫 𝐵) = 𝒫 (𝐴 × 𝐵)) | ||
Theorem | txindislem 23656 | Lemma for txindis 23657. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ (( I ‘𝐴) × ( I ‘𝐵)) = ( I ‘(𝐴 × 𝐵)) | ||
Theorem | txindis 23657 | The topological product of indiscrete spaces is indiscrete. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ ({∅, 𝐴} ×t {∅, 𝐵}) = {∅, (𝐴 × 𝐵)} | ||
Theorem | txdis1cn 23658* | A function is jointly continuous on a discrete left topology iff it is continuous as a function of its right argument, for each fixed left value. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝐾 ∈ Top) & ⊢ (𝜑 → 𝐹 Fn (𝑋 × 𝑌)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑦 ∈ 𝑌 ↦ (𝑥𝐹𝑦)) ∈ (𝐽 Cn 𝐾)) ⇒ ⊢ (𝜑 → 𝐹 ∈ ((𝒫 𝑋 ×t 𝐽) Cn 𝐾)) | ||
Theorem | txlly 23659* | If the property 𝐴 is preserved under topological products, then so is the property of being locally 𝐴. (Contributed by Mario Carneiro, 10-Mar-2015.) |
⊢ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐴) → (𝑗 ×t 𝑘) ∈ 𝐴) ⇒ ⊢ ((𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴) → (𝑅 ×t 𝑆) ∈ Locally 𝐴) | ||
Theorem | txnlly 23660* | If the property 𝐴 is preserved under topological products, then so is the property of being n-locally 𝐴. (Contributed by Mario Carneiro, 13-Apr-2015.) |
⊢ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐴) → (𝑗 ×t 𝑘) ∈ 𝐴) ⇒ ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → (𝑅 ×t 𝑆) ∈ 𝑛-Locally 𝐴) | ||
Theorem | pthaus 23661 | The product of a collection of Hausdorff spaces is Hausdorff. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) → (∏t‘𝐹) ∈ Haus) | ||
Theorem | ptrescn 23662* | Restriction is a continuous function on product topologies. (Contributed by Mario Carneiro, 7-Feb-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐽 = (∏t‘𝐹) & ⊢ 𝐾 = (∏t‘(𝐹 ↾ 𝐵)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → (𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) ∈ (𝐽 Cn 𝐾)) | ||
Theorem | txtube 23663* | 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 23664* | Lemma for txcmp 23666. (Contributed by Mario Carneiro, 14-Sep-2014.) |
⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝑌 = ∪ 𝑆 & ⊢ (𝜑 → 𝑅 ∈ Comp) & ⊢ (𝜑 → 𝑆 ∈ Comp) & ⊢ (𝜑 → 𝑊 ⊆ (𝑅 ×t 𝑆)) & ⊢ (𝜑 → (𝑋 × 𝑌) = ∪ 𝑊) & ⊢ (𝜑 → 𝐴 ∈ 𝑌) ⇒ ⊢ (𝜑 → ∃𝑢 ∈ 𝑆 (𝐴 ∈ 𝑢 ∧ ∃𝑣 ∈ (𝒫 𝑊 ∩ Fin)(𝑋 × 𝑢) ⊆ ∪ 𝑣)) | ||
Theorem | txcmplem2 23665* | Lemma for txcmp 23666. (Contributed by Mario Carneiro, 14-Sep-2014.) |
⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝑌 = ∪ 𝑆 & ⊢ (𝜑 → 𝑅 ∈ Comp) & ⊢ (𝜑 → 𝑆 ∈ Comp) & ⊢ (𝜑 → 𝑊 ⊆ (𝑅 ×t 𝑆)) & ⊢ (𝜑 → (𝑋 × 𝑌) = ∪ 𝑊) ⇒ ⊢ (𝜑 → ∃𝑣 ∈ (𝒫 𝑊 ∩ Fin)(𝑋 × 𝑌) = ∪ 𝑣) | ||
Theorem | txcmp 23666 | 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 23667 | 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 23668 | 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 23669 | 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 23670 | The topological product of two Hausdorff spaces is Hausdorff. (Contributed by Mario Carneiro, 23-Mar-2015.) |
⊢ ((𝑅 ∈ Haus ∧ 𝑆 ∈ Haus) → (𝑅 ×t 𝑆) ∈ Haus) | ||
Theorem | txlm 23671* | 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 23672* | 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 23673 | The topological product of two first-countable spaces is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → (𝑅 ×t 𝑆) ∈ 1stω) | ||
Theorem | tx2ndc 23674 | The topological product of two second-countable spaces is second-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ ((𝑅 ∈ 2ndω ∧ 𝑆 ∈ 2ndω) → (𝑅 ×t 𝑆) ∈ 2ndω) | ||
Theorem | txkgen 23675 | 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 23676 | 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 23677 | 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 23678 | 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 23679* | 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 23707.) (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ 𝑋 = ∪ 𝑅 ⇒ ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐴 ∈ 𝑋) → (𝑓 ∈ (𝑅 Cn 𝑆) ↦ (𝑓‘𝐴)) ∈ ((𝑆 ↑ko 𝑅) Cn 𝑆)) | ||
Theorem | xkoco1cn 23680* | If 𝐹 is a continuous function, then 𝑔 ↦ 𝑔 ∘ 𝐹 is a continuous function on function spaces. (The reason we prove this and xkoco2cn 23681 independently of the more general xkococn 23683 is because that requires some inconvenient extra assumptions on 𝑆.) (Contributed by Mario Carneiro, 20-Mar-2015.) |
⊢ (𝜑 → 𝑇 ∈ Top) & ⊢ (𝜑 → 𝐹 ∈ (𝑅 Cn 𝑆)) ⇒ ⊢ (𝜑 → (𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔 ∘ 𝐹)) ∈ ((𝑇 ↑ko 𝑆) Cn (𝑇 ↑ko 𝑅))) | ||
Theorem | xkoco2cn 23681* | 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 23682* | 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 23683* | 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 23684* | The identity function is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝑥) ∈ (𝐽 Cn 𝐽)) | ||
Theorem | cnmptc 23685* | A constant function is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝑃 ∈ 𝑌) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝑃) ∈ (𝐽 Cn 𝐾)) | ||
Theorem | cnmpt11 23686* | 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 23687* | 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 23688* | 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 23689* | 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 23690* | 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 23691* | 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 23692* | 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 23693* | 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 23694* | 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 23695* | 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 23696* | 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 23697* | 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 23698* | 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 23699* | The restriction of a continuous function to a subset is continuous. (Contributed by Mario Carneiro, 5-Jun-2014.) |
⊢ 𝐾 = (𝐽 ↾t 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ⊆ 𝑋) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐿)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿)) | ||
Theorem | cnmpt2res 23700* | 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 𝐿)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |