Home | Metamath
Proof Explorer Theorem List (p. 222 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-xko 22101* | 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 22102* | 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 22103* | The underlying set of the product of two topologies. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ 𝐵 = ran (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑆 ↦ (𝑥 × 𝑦)) & ⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝑌 = ∪ 𝑆 ⇒ ⊢ (𝑋 × 𝑌) = ∪ 𝐵 | ||
Theorem | txbasex 22104* | The basis for the product topology is a set. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ 𝐵 = ran (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑆 ↦ (𝑥 × 𝑦)) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → 𝐵 ∈ V) | ||
Theorem | txbas 22105* | 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 22106* | 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 22107 | The product of two topologies is a topology. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top) | ||
Theorem | ptval 22108* | The value of the product topology function. (Contributed by Mario Carneiro, 3-Feb-2015.) |
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴) → (∏t‘𝐹) = (topGen‘𝐵)) | ||
Theorem | ptpjpre1 22109* | 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 22110* | Elementhood in the bases of a product topology. (Contributed by Mario Carneiro, 3-Feb-2015.) |
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ⇒ ⊢ (𝑆 ∈ 𝐵 ↔ ∃ℎ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑤 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑤)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑆 = X𝑦 ∈ 𝐴 (ℎ‘𝑦))) | ||
Theorem | elptr 22111* | A basic open set in the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.) |
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ (𝐺 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝐺‘𝑦) ∈ (𝐹‘𝑦)) ∧ (𝑊 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑊)(𝐺‘𝑦) = ∪ (𝐹‘𝑦))) → X𝑦 ∈ 𝐴 (𝐺‘𝑦) ∈ 𝐵) | ||
Theorem | elptr2 22112* | A basic open set in the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.) |
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑊 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑆 ∈ (𝐹‘𝑘)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝑊)) → 𝑆 = ∪ (𝐹‘𝑘)) ⇒ ⊢ (𝜑 → X𝑘 ∈ 𝐴 𝑆 ∈ 𝐵) | ||
Theorem | ptbasid 22113* | 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 22114* | The base set for the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.) |
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) = ∪ 𝐵) | ||
Theorem | ptbasin 22115* | The basis for a product topology is closed under intersections. (Contributed by Mario Carneiro, 3-Feb-2015.) |
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ⇒ ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ∩ 𝑌) ∈ 𝐵) | ||
Theorem | ptbasin2 22116* | The basis for a product topology is closed under intersections. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (fi‘𝐵) = 𝐵) | ||
Theorem | ptbas 22117* | The basis for a product topology is a basis. (Contributed by Mario Carneiro, 3-Feb-2015.) |
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐵 ∈ TopBases) | ||
Theorem | ptpjpre2 22118* | The basis for a product topology is a basis. (Contributed by Mario Carneiro, 3-Feb-2015.) |
⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} & ⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ⇒ ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝐼 ∈ 𝐴 ∧ 𝑈 ∈ (𝐹‘𝐼))) → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝐼)) “ 𝑈) ∈ 𝐵) | ||
Theorem | ptbasfi 22119* | 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 22120 | The product topology is a topology. (Contributed by Mario Carneiro, 3-Feb-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (∏t‘𝐹) ∈ Top) | ||
Theorem | ptopn 22121* | A basic open set in the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶Top) & ⊢ (𝜑 → 𝑊 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑆 ∈ (𝐹‘𝑘)) & ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝑊)) → 𝑆 = ∪ (𝐹‘𝑘)) ⇒ ⊢ (𝜑 → X𝑘 ∈ 𝐴 𝑆 ∈ (∏t‘𝐹)) | ||
Theorem | ptopn2 22122* | A sub-basic open set in the product topology. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶Top) & ⊢ (𝜑 → 𝑂 ∈ (𝐹‘𝑌)) ⇒ ⊢ (𝜑 → X𝑘 ∈ 𝐴 if(𝑘 = 𝑌, 𝑂, ∪ (𝐹‘𝑘)) ∈ (∏t‘𝐹)) | ||
Theorem | xkotf 22123* | Functionality of function 𝑇. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝐾 = {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp} & ⊢ 𝑇 = (𝑘 ∈ 𝐾, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ⇒ ⊢ 𝑇:(𝐾 × 𝑆)⟶𝒫 (𝑅 Cn 𝑆) | ||
Theorem | xkobval 22124* | 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 22125* | Value of the compact-open topology. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝐾 = {𝑥 ∈ 𝒫 𝑋 ∣ (𝑅 ↾t 𝑥) ∈ Comp} & ⊢ 𝑇 = (𝑘 ∈ 𝐾, 𝑣 ∈ 𝑆 ↦ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ⇒ ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ↑ko 𝑅) = (topGen‘(fi‘ran 𝑇))) | ||
Theorem | xkotop 22126 | The compact-open topology is a topology. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ↑ko 𝑅) ∈ Top) | ||
Theorem | xkoopn 22127* | A basic open set of the compact-open topology. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ 𝑋 = ∪ 𝑅 & ⊢ (𝜑 → 𝑅 ∈ Top) & ⊢ (𝜑 → 𝑆 ∈ Top) & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) & ⊢ (𝜑 → (𝑅 ↾t 𝐴) ∈ Comp) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) ⇒ ⊢ (𝜑 → {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝐴) ⊆ 𝑈} ∈ (𝑆 ↑ko 𝑅)) | ||
Theorem | txtopi 22128 | The product of two topologies is a topology. (Contributed by Jeff Madsen, 15-Jun-2010.) |
⊢ 𝑅 ∈ Top & ⊢ 𝑆 ∈ Top ⇒ ⊢ (𝑅 ×t 𝑆) ∈ Top | ||
Theorem | txtopon 22129 | 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 22130 | The underlying set of the product of two topologies. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝑌 = ∪ 𝑆 ⇒ ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × 𝑌) = ∪ (𝑅 ×t 𝑆)) | ||
Theorem | txunii 22131 | The underlying set of the product of two topologies. (Contributed by Jeff Madsen, 15-Jun-2010.) |
⊢ 𝑅 ∈ Top & ⊢ 𝑆 ∈ Top & ⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝑌 = ∪ 𝑆 ⇒ ⊢ (𝑋 × 𝑌) = ∪ (𝑅 ×t 𝑆) | ||
Theorem | ptuni 22132* | The base set for the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.) |
⊢ 𝐽 = (∏t‘𝐹) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → X𝑥 ∈ 𝐴 ∪ (𝐹‘𝑥) = ∪ 𝐽) | ||
Theorem | ptunimpt 22133* | Base set of a product topology given by substitution. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ 𝐽 = (∏t‘(𝑥 ∈ 𝐴 ↦ 𝐾)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐾 ∈ Top) → X𝑥 ∈ 𝐴 ∪ 𝐾 = ∪ 𝐽) | ||
Theorem | pttopon 22134* | The base set for the product topology. (Contributed by Mario Carneiro, 22-Aug-2015.) |
⊢ 𝐽 = (∏t‘(𝑥 ∈ 𝐴 ↦ 𝐾)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐾 ∈ (TopOn‘𝐵)) → 𝐽 ∈ (TopOn‘X𝑥 ∈ 𝐴 𝐵)) | ||
Theorem | pttoponconst 22135 | 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 22136 | 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 22137 | The base set of the compact-open topology. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ 𝐽 = (𝑆 ↑ko 𝑅) ⇒ ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) = ∪ 𝐽) | ||
Theorem | xkotopon 22138 | The base set of the compact-open topology. (Contributed by Mario Carneiro, 22-Aug-2015.) |
⊢ 𝐽 = (𝑆 ↑ko 𝑅) ⇒ ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝐽 ∈ (TopOn‘(𝑅 Cn 𝑆))) | ||
Theorem | ptval2 22139* | The value of the product topology function. (Contributed by Mario Carneiro, 7-Feb-2015.) |
⊢ 𝐽 = (∏t‘𝐹) & ⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐺 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐽 = (topGen‘(fi‘({𝑋} ∪ ran 𝐺)))) | ||
Theorem | txopn 22140 | The product of two open sets is open in the product topology. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) ∧ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆)) → (𝐴 × 𝐵) ∈ (𝑅 ×t 𝑆)) | ||
Theorem | txcld 22141 | 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 22142 | Closure of a rectangle in the product topology. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)) = (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵))) | ||
Theorem | txss12 22143 | Subset property of the topological product. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)) → (𝐴 ×t 𝐶) ⊆ (𝐵 ×t 𝐷)) | ||
Theorem | txbasval 22144 | 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 22145 | 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 22146* | Continuity of a two-argument function at a point. (Contributed by Mario Carneiro, 20-Sep-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝐹 ∈ (((𝐽 ×t 𝐾) CnP 𝐿)‘〈𝐴, 𝐵〉)) & ⊢ (𝜑 → 𝑈 ∈ 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑌) & ⊢ (𝜑 → (𝐴𝐹𝐵) ∈ 𝑈) ⇒ ⊢ (𝜑 → ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐾 (𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐹 “ 𝑈))) | ||
Theorem | tx1cn 22147 | 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 22148 | 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 22149* | 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 22150* | The projection map is an open map. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ 𝑌 = ∪ 𝐽 & ⊢ 𝐽 = (∏t‘𝐹) ⇒ ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐼 ∈ 𝐴) ∧ 𝑈 ∈ 𝐽) → ((𝑥 ∈ 𝑌 ↦ (𝑥‘𝐼)) “ 𝑈) ∈ (𝐹‘𝐼)) | ||
Theorem | ptcld 22151* | A closed box in the product topology. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶Top) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (Clsd‘(𝐹‘𝑘))) ⇒ ⊢ (𝜑 → X𝑘 ∈ 𝐴 𝐶 ∈ (Clsd‘(∏t‘𝐹))) | ||
Theorem | ptcldmpt 22152* | A closed box in the product topology. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐽 ∈ Top) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (Clsd‘𝐽)) ⇒ ⊢ (𝜑 → X𝑘 ∈ 𝐴 𝐶 ∈ (Clsd‘(∏t‘(𝑘 ∈ 𝐴 ↦ 𝐽)))) | ||
Theorem | ptclsg 22153* | 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 22154* | 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 22155* | Lemma for dfac14 22156. 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 22154 to extract an element of the closure of X𝑘 ∈ 𝐼𝑆. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ≠ ∅) & ⊢ 𝑃 = 𝒫 ∪ 𝑆 & ⊢ 𝑅 = {𝑦 ∈ 𝒫 (𝑆 ∪ {𝑃}) ∣ (𝑃 ∈ 𝑦 → 𝑦 = (𝑆 ∪ {𝑃}))} & ⊢ 𝐽 = (∏t‘(𝑥 ∈ 𝐼 ↦ 𝑅)) & ⊢ (𝜑 → ((cls‘𝐽)‘X𝑥 ∈ 𝐼 𝑆) = X𝑥 ∈ 𝐼 ((cls‘𝑅)‘𝑆)) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐼 𝑆 ≠ ∅) | ||
Theorem | dfac14 22156* | Theorem ptcls 22154 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 22157* | 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 22158* | 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 22159* | Lemma for ptcnp 22160. (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ 𝐾 = (∏t‘𝐹) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼⟶Top) & ⊢ (𝜑 → 𝐷 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (𝐹‘𝑘))‘𝐷)) & ⊢ Ⅎ𝑘𝜓 & ⊢ ((𝜑 ∧ 𝜓) → 𝐺 Fn 𝐼) & ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ 𝐼) → (𝐺‘𝑘) ∈ (𝐹‘𝑘)) & ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ Fin) & ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ (𝐼 ∖ 𝑊)) → (𝐺‘𝑘) = ∪ (𝐹‘𝑘)) & ⊢ ((𝜑 ∧ 𝜓) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘))) | ||
Theorem | ptcnp 22160* | 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 22161* | 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 22162* | 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 22163* | 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 22164 | 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 22165* | 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 22166 | Topology of a structure product. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 Fn 𝐼) & ⊢ 𝑂 = (TopOpen‘𝑌) ⇒ ⊢ (𝜑 → 𝑂 = (∏t‘(TopOpen ∘ 𝑅))) | ||
Theorem | prdstps 22167 | A structure product of topologies is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅:𝐼⟶TopSp) ⇒ ⊢ (𝜑 → 𝑌 ∈ TopSp) | ||
Theorem | pwstps 22168 | A structure product of topologies is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) ⇒ ⊢ ((𝑅 ∈ TopSp ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ TopSp) | ||
Theorem | txrest 22169 | 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 22170 | The topological product of discrete spaces is discrete. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝒫 𝐴 ×t 𝒫 𝐵) = 𝒫 (𝐴 × 𝐵)) | ||
Theorem | txindislem 22171 | Lemma for txindis 22172. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ (( I ‘𝐴) × ( I ‘𝐵)) = ( I ‘(𝐴 × 𝐵)) | ||
Theorem | txindis 22172 | The topological product of indiscrete spaces is indiscrete. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ ({∅, 𝐴} ×t {∅, 𝐵}) = {∅, (𝐴 × 𝐵)} | ||
Theorem | txdis1cn 22173* | 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 22174* | 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 22175* | 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 22176 | The product of a collection of Hausdorff spaces is Hausdorff. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) → (∏t‘𝐹) ∈ Haus) | ||
Theorem | ptrescn 22177* | Restriction is a continuous function on product topologies. (Contributed by Mario Carneiro, 7-Feb-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐽 = (∏t‘𝐹) & ⊢ 𝐾 = (∏t‘(𝐹 ↾ 𝐵)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → (𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) ∈ (𝐽 Cn 𝐾)) | ||
Theorem | txtube 22178* | 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 22179* | Lemma for txcmp 22181. (Contributed by Mario Carneiro, 14-Sep-2014.) |
⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝑌 = ∪ 𝑆 & ⊢ (𝜑 → 𝑅 ∈ Comp) & ⊢ (𝜑 → 𝑆 ∈ Comp) & ⊢ (𝜑 → 𝑊 ⊆ (𝑅 ×t 𝑆)) & ⊢ (𝜑 → (𝑋 × 𝑌) = ∪ 𝑊) & ⊢ (𝜑 → 𝐴 ∈ 𝑌) ⇒ ⊢ (𝜑 → ∃𝑢 ∈ 𝑆 (𝐴 ∈ 𝑢 ∧ ∃𝑣 ∈ (𝒫 𝑊 ∩ Fin)(𝑋 × 𝑢) ⊆ ∪ 𝑣)) | ||
Theorem | txcmplem2 22180* | Lemma for txcmp 22181. (Contributed by Mario Carneiro, 14-Sep-2014.) |
⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝑌 = ∪ 𝑆 & ⊢ (𝜑 → 𝑅 ∈ Comp) & ⊢ (𝜑 → 𝑆 ∈ Comp) & ⊢ (𝜑 → 𝑊 ⊆ (𝑅 ×t 𝑆)) & ⊢ (𝜑 → (𝑋 × 𝑌) = ∪ 𝑊) ⇒ ⊢ (𝜑 → ∃𝑣 ∈ (𝒫 𝑊 ∩ Fin)(𝑋 × 𝑌) = ∪ 𝑣) | ||
Theorem | txcmp 22181 | 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 22182 | 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 22183 | 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 22184 | 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 22185 | The topological product of two Hausdorff spaces is Hausdorff. (Contributed by Mario Carneiro, 23-Mar-2015.) |
⊢ ((𝑅 ∈ Haus ∧ 𝑆 ∈ Haus) → (𝑅 ×t 𝑆) ∈ Haus) | ||
Theorem | txlm 22186* | 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 22187* | 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 22188 | The topological product of two first-countable spaces is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → (𝑅 ×t 𝑆) ∈ 1stω) | ||
Theorem | tx2ndc 22189 | The topological product of two second-countable spaces is second-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ ((𝑅 ∈ 2ndω ∧ 𝑆 ∈ 2ndω) → (𝑅 ×t 𝑆) ∈ 2ndω) | ||
Theorem | txkgen 22190 | 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 22191 | 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 22192 | 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 22193 | 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 22194* | 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 22222.) (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ 𝑋 = ∪ 𝑅 ⇒ ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐴 ∈ 𝑋) → (𝑓 ∈ (𝑅 Cn 𝑆) ↦ (𝑓‘𝐴)) ∈ ((𝑆 ↑ko 𝑅) Cn 𝑆)) | ||
Theorem | xkoco1cn 22195* | If 𝐹 is a continuous function, then 𝑔 ↦ 𝑔 ∘ 𝐹 is a continuous function on function spaces. (The reason we prove this and xkoco2cn 22196 independently of the more general xkococn 22198 is because that requires some inconvenient extra assumptions on 𝑆.) (Contributed by Mario Carneiro, 20-Mar-2015.) |
⊢ (𝜑 → 𝑇 ∈ Top) & ⊢ (𝜑 → 𝐹 ∈ (𝑅 Cn 𝑆)) ⇒ ⊢ (𝜑 → (𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔 ∘ 𝐹)) ∈ ((𝑇 ↑ko 𝑆) Cn (𝑇 ↑ko 𝑅))) | ||
Theorem | xkoco2cn 22196* | 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 22197* | 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 22198* | 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 22199* | The identity function is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝑥) ∈ (𝐽 Cn 𝐽)) | ||
Theorem | cnmptc 22200* | A constant function is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝑃 ∈ 𝑌) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝑃) ∈ (𝐽 Cn 𝐾)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |