![]() |
Metamath
Proof Explorer Theorem List (p. 219 of 437) | < 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-28347) |
![]() (28348-29872) |
![]() (29873-43657) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | xkoopn 21801* | A basic open set of the compact-open topology. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ 𝑋 = ∪ 𝑅 & ⊢ (𝜑 → 𝑅 ∈ Top) & ⊢ (𝜑 → 𝑆 ∈ Top) & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) & ⊢ (𝜑 → (𝑅 ↾t 𝐴) ∈ Comp) & ⊢ (𝜑 → 𝑈 ∈ 𝑆) ⇒ ⊢ (𝜑 → {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ 𝐴) ⊆ 𝑈} ∈ (𝑆 ^ko 𝑅)) | ||
Theorem | txtopi 21802 | The product of two topologies is a topology. (Contributed by Jeff Madsen, 15-Jun-2010.) |
⊢ 𝑅 ∈ Top & ⊢ 𝑆 ∈ Top ⇒ ⊢ (𝑅 ×t 𝑆) ∈ Top | ||
Theorem | txtopon 21803 | 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 21804 | The underlying set of the product of two topologies. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝑌 = ∪ 𝑆 ⇒ ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × 𝑌) = ∪ (𝑅 ×t 𝑆)) | ||
Theorem | txunii 21805 | The underlying set of the product of two topologies. (Contributed by Jeff Madsen, 15-Jun-2010.) |
⊢ 𝑅 ∈ Top & ⊢ 𝑆 ∈ Top & ⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝑌 = ∪ 𝑆 ⇒ ⊢ (𝑋 × 𝑌) = ∪ (𝑅 ×t 𝑆) | ||
Theorem | ptuni 21806* | The base set for the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.) |
⊢ 𝐽 = (∏t‘𝐹) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → X𝑥 ∈ 𝐴 ∪ (𝐹‘𝑥) = ∪ 𝐽) | ||
Theorem | ptunimpt 21807* | Base set of a product topology given by substitution. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ 𝐽 = (∏t‘(𝑥 ∈ 𝐴 ↦ 𝐾)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐾 ∈ Top) → X𝑥 ∈ 𝐴 ∪ 𝐾 = ∪ 𝐽) | ||
Theorem | pttopon 21808* | The base set for the product topology. (Contributed by Mario Carneiro, 22-Aug-2015.) |
⊢ 𝐽 = (∏t‘(𝑥 ∈ 𝐴 ↦ 𝐾)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐾 ∈ (TopOn‘𝐵)) → 𝐽 ∈ (TopOn‘X𝑥 ∈ 𝐴 𝐵)) | ||
Theorem | pttoponconst 21809 | The base set for a product topology when all factors are the same. (Contributed by Mario Carneiro, 22-Aug-2015.) |
⊢ 𝐽 = (∏t‘(𝐴 × {𝑅})) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ (TopOn‘𝑋)) → 𝐽 ∈ (TopOn‘(𝑋 ↑𝑚 𝐴))) | ||
Theorem | ptuniconst 21810 | The base set for a product topology when all factors are the same. (Contributed by Mario Carneiro, 3-Feb-2015.) |
⊢ 𝐽 = (∏t‘(𝐴 × {𝑅})) & ⊢ 𝑋 = ∪ 𝑅 ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ Top) → (𝑋 ↑𝑚 𝐴) = ∪ 𝐽) | ||
Theorem | xkouni 21811 | The base set of the compact-open topology. (Contributed by Mario Carneiro, 19-Mar-2015.) |
⊢ 𝐽 = (𝑆 ^ko 𝑅) ⇒ ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) = ∪ 𝐽) | ||
Theorem | xkotopon 21812 | The base set of the compact-open topology. (Contributed by Mario Carneiro, 22-Aug-2015.) |
⊢ 𝐽 = (𝑆 ^ko 𝑅) ⇒ ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝐽 ∈ (TopOn‘(𝑅 Cn 𝑆))) | ||
Theorem | ptval2 21813* | The value of the product topology function. (Contributed by Mario Carneiro, 7-Feb-2015.) |
⊢ 𝐽 = (∏t‘𝐹) & ⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐺 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐽 = (topGen‘(fi‘({𝑋} ∪ ran 𝐺)))) | ||
Theorem | txopn 21814 | The product of two open sets is open in the product topology. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) ∧ (𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆)) → (𝐴 × 𝐵) ∈ (𝑅 ×t 𝑆)) | ||
Theorem | txcld 21815 | 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 21816 | Closure of a rectangle in the product topology. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)) = (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵))) | ||
Theorem | txss12 21817 | Subset property of the topological product. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊) ∧ (𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷)) → (𝐴 ×t 𝐶) ⊆ (𝐵 ×t 𝐷)) | ||
Theorem | txbasval 21818 | 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 21819 | 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 21820* | Continuity of a two-argument function at a point. (Contributed by Mario Carneiro, 20-Sep-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝐹 ∈ (((𝐽 ×t 𝐾) CnP 𝐿)‘〈𝐴, 𝐵〉)) & ⊢ (𝜑 → 𝑈 ∈ 𝐿) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑌) & ⊢ (𝜑 → (𝐴𝐹𝐵) ∈ 𝑈) ⇒ ⊢ (𝜑 → ∃𝑢 ∈ 𝐽 ∃𝑣 ∈ 𝐾 (𝐴 ∈ 𝑢 ∧ 𝐵 ∈ 𝑣 ∧ (𝑢 × 𝑣) ⊆ (◡𝐹 “ 𝑈))) | ||
Theorem | tx1cn 21821 | 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 21822 | 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 21823* | 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 21824* | The projection map is an open map. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ 𝑌 = ∪ 𝐽 & ⊢ 𝐽 = (∏t‘𝐹) ⇒ ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐼 ∈ 𝐴) ∧ 𝑈 ∈ 𝐽) → ((𝑥 ∈ 𝑌 ↦ (𝑥‘𝐼)) “ 𝑈) ∈ (𝐹‘𝐼)) | ||
Theorem | ptcld 21825* | A closed box in the product topology. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶Top) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (Clsd‘(𝐹‘𝑘))) ⇒ ⊢ (𝜑 → X𝑘 ∈ 𝐴 𝐶 ∈ (Clsd‘(∏t‘𝐹))) | ||
Theorem | ptcldmpt 21826* | A closed box in the product topology. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐽 ∈ Top) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ (Clsd‘𝐽)) ⇒ ⊢ (𝜑 → X𝑘 ∈ 𝐴 𝐶 ∈ (Clsd‘(∏t‘(𝑘 ∈ 𝐴 ↦ 𝐽)))) | ||
Theorem | ptclsg 21827* | 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 21828* | 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 21829* | Lemma for dfac14 21830. 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 21828 to extract an element of the closure of X𝑘 ∈ 𝐼𝑆. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ∈ 𝑊) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ≠ ∅) & ⊢ 𝑃 = 𝒫 ∪ 𝑆 & ⊢ 𝑅 = {𝑦 ∈ 𝒫 (𝑆 ∪ {𝑃}) ∣ (𝑃 ∈ 𝑦 → 𝑦 = (𝑆 ∪ {𝑃}))} & ⊢ 𝐽 = (∏t‘(𝑥 ∈ 𝐼 ↦ 𝑅)) & ⊢ (𝜑 → ((cls‘𝐽)‘X𝑥 ∈ 𝐼 𝑆) = X𝑥 ∈ 𝐼 ((cls‘𝑅)‘𝑆)) ⇒ ⊢ (𝜑 → X𝑥 ∈ 𝐼 𝑆 ≠ ∅) | ||
Theorem | dfac14 21830* | Theorem ptcls 21828 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 21831* | 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 21832* | 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 21833* | Lemma for ptcnp 21834. (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ 𝐾 = (∏t‘𝐹) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼⟶Top) & ⊢ (𝜑 → 𝐷 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (𝐹‘𝑘))‘𝐷)) & ⊢ Ⅎ𝑘𝜓 & ⊢ ((𝜑 ∧ 𝜓) → 𝐺 Fn 𝐼) & ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ 𝐼) → (𝐺‘𝑘) ∈ (𝐹‘𝑘)) & ⊢ ((𝜑 ∧ 𝜓) → 𝑊 ∈ Fin) & ⊢ (((𝜑 ∧ 𝜓) ∧ 𝑘 ∈ (𝐼 ∖ 𝑊)) → (𝐺‘𝑘) = ∪ (𝐹‘𝑘)) & ⊢ ((𝜑 ∧ 𝜓) → ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴))‘𝐷) ∈ X𝑘 ∈ 𝐼 (𝐺‘𝑘)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → ∃𝑧 ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((𝑥 ∈ 𝑋 ↦ (𝑘 ∈ 𝐼 ↦ 𝐴)) “ 𝑧) ⊆ X𝑘 ∈ 𝐼 (𝐺‘𝑘))) | ||
Theorem | ptcnp 21834* | 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 21835* | 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 21836* | 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 21837* | 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 21838 | 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 21839* | 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 21840 | Topology of a structure product. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 Fn 𝐼) & ⊢ 𝑂 = (TopOpen‘𝑌) ⇒ ⊢ (𝜑 → 𝑂 = (∏t‘(TopOpen ∘ 𝑅))) | ||
Theorem | prdstps 21841 | A structure product of topologies is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅:𝐼⟶TopSp) ⇒ ⊢ (𝜑 → 𝑌 ∈ TopSp) | ||
Theorem | pwstps 21842 | A structure product of topologies is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) ⇒ ⊢ ((𝑅 ∈ TopSp ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ TopSp) | ||
Theorem | txrest 21843 | 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 21844 | The topological product of discrete spaces is discrete. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝒫 𝐴 ×t 𝒫 𝐵) = 𝒫 (𝐴 × 𝐵)) | ||
Theorem | txindislem 21845 | Lemma for txindis 21846. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ (( I ‘𝐴) × ( I ‘𝐵)) = ( I ‘(𝐴 × 𝐵)) | ||
Theorem | txindis 21846 | The topological product of indiscrete spaces is indiscrete. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ ({∅, 𝐴} ×t {∅, 𝐵}) = {∅, (𝐴 × 𝐵)} | ||
Theorem | txdis1cn 21847* | 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 21848* | 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 21849* | 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 21850 | The product of a collection of Hausdorff spaces is Hausdorff. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Haus) → (∏t‘𝐹) ∈ Haus) | ||
Theorem | ptrescn 21851* | Restriction is a continuous function on product topologies. (Contributed by Mario Carneiro, 7-Feb-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐽 = (∏t‘𝐹) & ⊢ 𝐾 = (∏t‘(𝐹 ↾ 𝐵)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → (𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) ∈ (𝐽 Cn 𝐾)) | ||
Theorem | txtube 21852* | 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 21853* | Lemma for txcmp 21855. (Contributed by Mario Carneiro, 14-Sep-2014.) |
⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝑌 = ∪ 𝑆 & ⊢ (𝜑 → 𝑅 ∈ Comp) & ⊢ (𝜑 → 𝑆 ∈ Comp) & ⊢ (𝜑 → 𝑊 ⊆ (𝑅 ×t 𝑆)) & ⊢ (𝜑 → (𝑋 × 𝑌) = ∪ 𝑊) & ⊢ (𝜑 → 𝐴 ∈ 𝑌) ⇒ ⊢ (𝜑 → ∃𝑢 ∈ 𝑆 (𝐴 ∈ 𝑢 ∧ ∃𝑣 ∈ (𝒫 𝑊 ∩ Fin)(𝑋 × 𝑢) ⊆ ∪ 𝑣)) | ||
Theorem | txcmplem2 21854* | Lemma for txcmp 21855. (Contributed by Mario Carneiro, 14-Sep-2014.) |
⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝑌 = ∪ 𝑆 & ⊢ (𝜑 → 𝑅 ∈ Comp) & ⊢ (𝜑 → 𝑆 ∈ Comp) & ⊢ (𝜑 → 𝑊 ⊆ (𝑅 ×t 𝑆)) & ⊢ (𝜑 → (𝑋 × 𝑌) = ∪ 𝑊) ⇒ ⊢ (𝜑 → ∃𝑣 ∈ (𝒫 𝑊 ∩ Fin)(𝑋 × 𝑌) = ∪ 𝑣) | ||
Theorem | txcmp 21855 | 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 21856 | 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 21857 | 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 21858 | 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 21859 | The topological product of two Hausdorff spaces is Hausdorff. (Contributed by Mario Carneiro, 23-Mar-2015.) |
⊢ ((𝑅 ∈ Haus ∧ 𝑆 ∈ Haus) → (𝑅 ×t 𝑆) ∈ Haus) | ||
Theorem | txlm 21860* | 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 21861* | 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 21862 | The topological product of two first-countable spaces is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ ((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) → (𝑅 ×t 𝑆) ∈ 1st𝜔) | ||
Theorem | tx2ndc 21863 | The topological product of two second-countable spaces is second-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ ((𝑅 ∈ 2nd𝜔 ∧ 𝑆 ∈ 2nd𝜔) → (𝑅 ×t 𝑆) ∈ 2nd𝜔) | ||
Theorem | txkgen 21864 | 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 21865 | 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 21866 | 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 21867 | 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 21868* | 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 21896.) (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ 𝑋 = ∪ 𝑅 ⇒ ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐴 ∈ 𝑋) → (𝑓 ∈ (𝑅 Cn 𝑆) ↦ (𝑓‘𝐴)) ∈ ((𝑆 ^ko 𝑅) Cn 𝑆)) | ||
Theorem | xkoco1cn 21869* | If 𝐹 is a continuous function, then 𝑔 ↦ 𝑔 ∘ 𝐹 is a continuous function on function spaces. (The reason we prove this and xkoco2cn 21870 independently of the more general xkococn 21872 is because that requires some inconvenient extra assumptions on 𝑆.) (Contributed by Mario Carneiro, 20-Mar-2015.) |
⊢ (𝜑 → 𝑇 ∈ Top) & ⊢ (𝜑 → 𝐹 ∈ (𝑅 Cn 𝑆)) ⇒ ⊢ (𝜑 → (𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔 ∘ 𝐹)) ∈ ((𝑇 ^ko 𝑆) Cn (𝑇 ^ko 𝑅))) | ||
Theorem | xkoco2cn 21870* | 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 21871* | 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 21872* | 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 21873* | The identity function is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝑥) ∈ (𝐽 Cn 𝐽)) | ||
Theorem | cnmptc 21874* | A constant function is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝑃 ∈ 𝑌) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝑃) ∈ (𝐽 Cn 𝐾)) | ||
Theorem | cnmpt11 21875* | 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 21876* | 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 21877* | 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 21878* | 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 21879* | 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 21880* | 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 21881* | 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 21882* | 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 21883* | 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 21884* | 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 21885* | 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 21886* | 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 21887* | 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 21888* | The restriction of a continuous function to a subset is continuous. (Contributed by Mario Carneiro, 5-Jun-2014.) |
⊢ 𝐾 = (𝐽 ↾t 𝑌) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑌 ⊆ 𝑋) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐿)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑌 ↦ 𝐴) ∈ (𝐾 Cn 𝐿)) | ||
Theorem | cnmpt2res 21889* | 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 21890* | The argument converse of a continuous function is continuous. (Contributed by Mario Carneiro, 6-Jun-2014.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) ⇒ ⊢ (𝜑 → (𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 𝐴) ∈ ((𝐾 ×t 𝐽) Cn 𝐿)) | ||
Theorem | cnmptkc 21891* | 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 21892* | 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 21893* | 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 21894* | 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 21895* | 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 21896* | Joint continuity of the function value operation as a function on continuous function spaces. (Compare xkopjcn 21868.) (Contributed by Mario Carneiro, 20-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
⊢ 𝑋 = ∪ 𝑅 & ⊢ 𝐹 = (𝑓 ∈ (𝑅 Cn 𝑆), 𝑥 ∈ 𝑋 ↦ (𝑓‘𝑥)) ⇒ ⊢ ((𝑅 ∈ 𝑛-Locally Comp ∧ 𝑆 ∈ Top) → 𝐹 ∈ (((𝑆 ^ko 𝑅) ×t 𝑅) Cn 𝑆)) | ||
Theorem | cnmptk1p 21897* | 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 21898* | 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 21899* | 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 21900* | The currying of a two-argument function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐽 ×t 𝐾) Cn 𝐿)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐴)) ∈ (𝐽 Cn (𝐿 ^ko 𝐾))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |