HomeHome Intuitionistic Logic Explorer
Theorem List (p. 142 of 153)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 14101-14200   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremiscn 14101* The predicate "the class 𝐹 is a continuous function from topology 𝐽 to topology 𝐾". Definition of continuous function in [Munkres] p. 102. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) β†’ (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘¦ ∈ 𝐾 (◑𝐹 β€œ 𝑦) ∈ 𝐽)))
 
Theoremcnpval 14102* The set of all functions from topology 𝐽 to topology 𝐾 that are continuous at a point 𝑃. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ 𝑃 ∈ 𝑋) β†’ ((𝐽 CnP 𝐾)β€˜π‘ƒ) = {𝑓 ∈ (π‘Œ β†‘π‘š 𝑋) ∣ βˆ€π‘¦ ∈ 𝐾 ((π‘“β€˜π‘ƒ) ∈ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝑓 β€œ π‘₯) βŠ† 𝑦))})
 
Theoremiscnp 14103* The predicate "the class 𝐹 is a continuous function from topology 𝐽 to topology 𝐾 at point 𝑃". Based on Theorem 7.2(g) of [Munkres] p. 107. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ 𝑃 ∈ 𝑋) β†’ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ↔ (𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘¦ ∈ 𝐾 ((πΉβ€˜π‘ƒ) ∈ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦)))))
 
Theoremiscn2 14104* The predicate "the class 𝐹 is a continuous function from topology 𝐽 to topology 𝐾". Definition of continuous function in [Munkres] p. 102. (Contributed by Mario Carneiro, 21-Aug-2015.)
𝑋 = βˆͺ 𝐽    &   π‘Œ = βˆͺ 𝐾    β‡’   (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘¦ ∈ 𝐾 (◑𝐹 β€œ 𝑦) ∈ 𝐽)))
 
Theoremcntop1 14105 Reverse closure for a continuous function. (Contributed by Mario Carneiro, 21-Aug-2015.)
(𝐹 ∈ (𝐽 Cn 𝐾) β†’ 𝐽 ∈ Top)
 
Theoremcntop2 14106 Reverse closure for a continuous function. (Contributed by Mario Carneiro, 21-Aug-2015.)
(𝐹 ∈ (𝐽 Cn 𝐾) β†’ 𝐾 ∈ Top)
 
Theoremiscnp3 14107* The predicate "the class 𝐹 is a continuous function from topology 𝐽 to topology 𝐾 at point 𝑃". (Contributed by NM, 15-May-2007.)
((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ 𝑃 ∈ 𝑋) β†’ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ↔ (𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘¦ ∈ 𝐾 ((πΉβ€˜π‘ƒ) ∈ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ π‘₯ βŠ† (◑𝐹 β€œ 𝑦))))))
 
Theoremcnf 14108 A continuous function is a mapping. (Contributed by FL, 8-Dec-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
𝑋 = βˆͺ 𝐽    &   π‘Œ = βˆͺ 𝐾    β‡’   (𝐹 ∈ (𝐽 Cn 𝐾) β†’ 𝐹:π‘‹βŸΆπ‘Œ)
 
Theoremcnf2 14109 A continuous function is a mapping. (Contributed by Mario Carneiro, 21-Aug-2015.)
((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) β†’ 𝐹:π‘‹βŸΆπ‘Œ)
 
Theoremcnprcl2k 14110 Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.) (Revised by Jim Kingdon, 28-Mar-2023.)
((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ Top ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ)) β†’ 𝑃 ∈ 𝑋)
 
Theoremcnpf2 14111 A continuous function at point 𝑃 is a mapping. (Contributed by Mario Carneiro, 21-Aug-2015.) (Revised by Jim Kingdon, 28-Mar-2023.)
((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ)) β†’ 𝐹:π‘‹βŸΆπ‘Œ)
 
Theoremtgcn 14112* The continuity predicate when the range is given by a basis for a topology. (Contributed by Mario Carneiro, 7-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
(πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))    &   (πœ‘ β†’ 𝐾 = (topGenβ€˜π΅))    &   (πœ‘ β†’ 𝐾 ∈ (TopOnβ€˜π‘Œ))    β‡’   (πœ‘ β†’ (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘¦ ∈ 𝐡 (◑𝐹 β€œ 𝑦) ∈ 𝐽)))
 
Theoremtgcnp 14113* The "continuous at a point" predicate when the range is given by a basis for a topology. (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
(πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))    &   (πœ‘ β†’ 𝐾 = (topGenβ€˜π΅))    &   (πœ‘ β†’ 𝐾 ∈ (TopOnβ€˜π‘Œ))    &   (πœ‘ β†’ 𝑃 ∈ 𝑋)    β‡’   (πœ‘ β†’ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ↔ (𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘¦ ∈ 𝐡 ((πΉβ€˜π‘ƒ) ∈ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦)))))
 
Theoremssidcn 14114 The identity function is a continuous function from one topology to another topology on the same set iff the domain is finer than the codomain. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 21-Aug-2015.)
((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘‹)) β†’ (( I β†Ύ 𝑋) ∈ (𝐽 Cn 𝐾) ↔ 𝐾 βŠ† 𝐽))
 
Theoremicnpimaex 14115* Property of a function continuous at a point. (Contributed by FL, 31-Dec-2006.) (Revised by Jim Kingdon, 28-Mar-2023.)
(((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ 𝑃 ∈ 𝑋) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐴 ∈ 𝐾 ∧ (πΉβ€˜π‘ƒ) ∈ 𝐴)) β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝐴))
 
Theoremidcn 14116 A restricted identity function is a continuous function. (Contributed by FL, 27-Dec-2006.) (Proof shortened by Mario Carneiro, 21-Mar-2015.)
(𝐽 ∈ (TopOnβ€˜π‘‹) β†’ ( I β†Ύ 𝑋) ∈ (𝐽 Cn 𝐽))
 
Theoremlmbr 14117* Express the binary relation "sequence 𝐹 converges to point 𝑃 " in a topological space. Definition 1.4-1 of [Kreyszig] p. 25. The condition 𝐹 βŠ† (β„‚ Γ— 𝑋) allows us to use objects more general than sequences when convenient; see the comment in df-lm 14094. (Contributed by Mario Carneiro, 14-Nov-2013.)
(πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))    β‡’   (πœ‘ β†’ (𝐹(β‡π‘‘β€˜π½)𝑃 ↔ (𝐹 ∈ (𝑋 ↑pm β„‚) ∧ 𝑃 ∈ 𝑋 ∧ βˆ€π‘’ ∈ 𝐽 (𝑃 ∈ 𝑒 β†’ βˆƒπ‘¦ ∈ ran β„€β‰₯(𝐹 β†Ύ 𝑦):π‘¦βŸΆπ‘’))))
 
Theoremlmbr2 14118* Express the binary relation "sequence 𝐹 converges to point 𝑃 " in a metric space using an arbitrary upper set of integers. (Contributed by Mario Carneiro, 14-Nov-2013.)
(πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))    &   π‘ = (β„€β‰₯β€˜π‘€)    &   (πœ‘ β†’ 𝑀 ∈ β„€)    β‡’   (πœ‘ β†’ (𝐹(β‡π‘‘β€˜π½)𝑃 ↔ (𝐹 ∈ (𝑋 ↑pm β„‚) ∧ 𝑃 ∈ 𝑋 ∧ βˆ€π‘’ ∈ 𝐽 (𝑃 ∈ 𝑒 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(π‘˜ ∈ dom 𝐹 ∧ (πΉβ€˜π‘˜) ∈ 𝑒)))))
 
Theoremlmbrf 14119* Express the binary relation "sequence 𝐹 converges to point 𝑃 " in a metric space using an arbitrary upper set of integers. This version of lmbr2 14118 presupposes that 𝐹 is a function. (Contributed by Mario Carneiro, 14-Nov-2013.)
(πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))    &   π‘ = (β„€β‰₯β€˜π‘€)    &   (πœ‘ β†’ 𝑀 ∈ β„€)    &   (πœ‘ β†’ 𝐹:π‘βŸΆπ‘‹)    &   ((πœ‘ ∧ π‘˜ ∈ 𝑍) β†’ (πΉβ€˜π‘˜) = 𝐴)    β‡’   (πœ‘ β†’ (𝐹(β‡π‘‘β€˜π½)𝑃 ↔ (𝑃 ∈ 𝑋 ∧ βˆ€π‘’ ∈ 𝐽 (𝑃 ∈ 𝑒 β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)𝐴 ∈ 𝑒))))
 
Theoremlmconst 14120 A constant sequence converges to its value. (Contributed by NM, 8-Nov-2007.) (Revised by Mario Carneiro, 14-Nov-2013.)
𝑍 = (β„€β‰₯β€˜π‘€)    β‡’   ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝑃 ∈ 𝑋 ∧ 𝑀 ∈ β„€) β†’ (𝑍 Γ— {𝑃})(β‡π‘‘β€˜π½)𝑃)
 
Theoremlmcvg 14121* Convergence property of a converging sequence. (Contributed by Mario Carneiro, 14-Nov-2013.)
𝑍 = (β„€β‰₯β€˜π‘€)    &   (πœ‘ β†’ 𝑃 ∈ π‘ˆ)    &   (πœ‘ β†’ 𝑀 ∈ β„€)    &   (πœ‘ β†’ 𝐹(β‡π‘‘β€˜π½)𝑃)    &   (πœ‘ β†’ π‘ˆ ∈ 𝐽)    β‡’   (πœ‘ β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘˜ ∈ (β„€β‰₯β€˜π‘—)(πΉβ€˜π‘˜) ∈ π‘ˆ)
 
Theoremiscnp4 14122* The predicate "the class 𝐹 is a continuous function from topology 𝐽 to topology 𝐾 at point 𝑃 " in terms of neighborhoods. (Contributed by FL, 18-Jul-2011.) (Revised by Mario Carneiro, 10-Sep-2015.)
((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ 𝑃 ∈ 𝑋) β†’ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ↔ (𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘¦ ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π‘ƒ)})βˆƒπ‘₯ ∈ ((neiβ€˜π½)β€˜{𝑃})(𝐹 β€œ π‘₯) βŠ† 𝑦)))
 
Theoremcnpnei 14123* A condition for continuity at a point in terms of neighborhoods. (Contributed by Jeff Hankins, 7-Sep-2009.)
𝑋 = βˆͺ 𝐽    &   π‘Œ = βˆͺ 𝐾    β‡’   (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) ∧ 𝐴 ∈ 𝑋) β†’ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄) ↔ βˆ€π‘¦ ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π΄)})(◑𝐹 β€œ 𝑦) ∈ ((neiβ€˜π½)β€˜{𝐴})))
 
Theoremcnima 14124 An open subset of the codomain of a continuous function has an open preimage. (Contributed by FL, 15-Dec-2006.)
((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ 𝐾) β†’ (◑𝐹 β€œ 𝐴) ∈ 𝐽)
 
Theoremcnco 14125 The composition of two continuous functions is a continuous function. (Contributed by FL, 8-Dec-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐺 ∈ (𝐾 Cn 𝐿)) β†’ (𝐺 ∘ 𝐹) ∈ (𝐽 Cn 𝐿))
 
Theoremcnptopco 14126 The composition of a function 𝐹 continuous at 𝑃 with a function continuous at (πΉβ€˜π‘ƒ) is continuous at 𝑃. Proposition 2 of [BourbakiTop1] p. I.9. (Contributed by FL, 16-Nov-2006.) (Proof shortened by Mario Carneiro, 27-Dec-2014.)
(((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐿 ∈ Top) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ∧ 𝐺 ∈ ((𝐾 CnP 𝐿)β€˜(πΉβ€˜π‘ƒ)))) β†’ (𝐺 ∘ 𝐹) ∈ ((𝐽 CnP 𝐿)β€˜π‘ƒ))
 
Theoremcnclima 14127 A closed subset of the codomain of a continuous function has a closed preimage. (Contributed by NM, 15-Mar-2007.) (Revised by Mario Carneiro, 21-Aug-2015.)
((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ (Clsdβ€˜πΎ)) β†’ (◑𝐹 β€œ 𝐴) ∈ (Clsdβ€˜π½))
 
Theoremcnntri 14128 Property of the preimage of an interior. (Contributed by Mario Carneiro, 25-Aug-2015.)
π‘Œ = βˆͺ 𝐾    β‡’   ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑆 βŠ† π‘Œ) β†’ (◑𝐹 β€œ ((intβ€˜πΎ)β€˜π‘†)) βŠ† ((intβ€˜π½)β€˜(◑𝐹 β€œ 𝑆)))
 
Theoremcnntr 14129* Continuity in terms of interior. (Contributed by Jeff Hankins, 2-Oct-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.)
((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) β†’ (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝒫 π‘Œ(◑𝐹 β€œ ((intβ€˜πΎ)β€˜π‘₯)) βŠ† ((intβ€˜π½)β€˜(◑𝐹 β€œ π‘₯)))))
 
Theoremcnss1 14130 If the topology 𝐾 is finer than 𝐽, then there are more continuous functions from 𝐾 than from 𝐽. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 21-Aug-2015.)
𝑋 = βˆͺ 𝐽    β‡’   ((𝐾 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 βŠ† 𝐾) β†’ (𝐽 Cn 𝐿) βŠ† (𝐾 Cn 𝐿))
 
Theoremcnss2 14131 If the topology 𝐾 is finer than 𝐽, then there are fewer continuous functions into 𝐾 than into 𝐽 from some other space. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 21-Aug-2015.)
π‘Œ = βˆͺ 𝐾    β‡’   ((𝐿 ∈ (TopOnβ€˜π‘Œ) ∧ 𝐿 βŠ† 𝐾) β†’ (𝐽 Cn 𝐾) βŠ† (𝐽 Cn 𝐿))
 
Theoremcncnpi 14132 A continuous function is continuous at all points. One direction of Theorem 7.2(g) of [Munkres] p. 107. (Contributed by Raph Levien, 20-Nov-2006.) (Proof shortened by Mario Carneiro, 21-Aug-2015.)
𝑋 = βˆͺ 𝐽    β‡’   ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 ∈ 𝑋) β†’ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π΄))
 
Theoremcnsscnp 14133 The set of continuous functions is a subset of the set of continuous functions at a point. (Contributed by Raph Levien, 21-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
𝑋 = βˆͺ 𝐽    β‡’   (𝑃 ∈ 𝑋 β†’ (𝐽 Cn 𝐾) βŠ† ((𝐽 CnP 𝐾)β€˜π‘ƒ))
 
Theoremcncnp 14134* A continuous function is continuous at all points. Theorem 7.2(g) of [Munkres] p. 107. (Contributed by NM, 15-May-2007.) (Proof shortened by Mario Carneiro, 21-Aug-2015.)
((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) β†’ (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘₯ ∈ 𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘₯))))
 
Theoremcncnp2m 14135* A continuous function is continuous at all points. Theorem 7.2(g) of [Munkres] p. 107. (Contributed by Raph Levien, 20-Nov-2006.) (Revised by Jim Kingdon, 30-Mar-2023.)
𝑋 = βˆͺ 𝐽    &   π‘Œ = βˆͺ 𝐾    β‡’   ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ βˆƒπ‘¦ 𝑦 ∈ 𝑋) β†’ (𝐹 ∈ (𝐽 Cn 𝐾) ↔ βˆ€π‘₯ ∈ 𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘₯)))
 
Theoremcnnei 14136* Continuity in terms of neighborhoods. (Contributed by Thierry Arnoux, 3-Jan-2018.)
𝑋 = βˆͺ 𝐽    &   π‘Œ = βˆͺ 𝐾    β‡’   ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐹:π‘‹βŸΆπ‘Œ) β†’ (𝐹 ∈ (𝐽 Cn 𝐾) ↔ βˆ€π‘ ∈ 𝑋 βˆ€π‘€ ∈ ((neiβ€˜πΎ)β€˜{(πΉβ€˜π‘)})βˆƒπ‘£ ∈ ((neiβ€˜π½)β€˜{𝑝})(𝐹 β€œ 𝑣) βŠ† 𝑀))
 
Theoremcnconst2 14137 A constant function is continuous. (Contributed by Mario Carneiro, 19-Mar-2015.)
((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ 𝐡 ∈ π‘Œ) β†’ (𝑋 Γ— {𝐡}) ∈ (𝐽 Cn 𝐾))
 
Theoremcnconst 14138 A constant function is continuous. (Contributed by FL, 15-Jan-2007.) (Proof shortened by Mario Carneiro, 19-Mar-2015.)
(((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) ∧ (𝐡 ∈ π‘Œ ∧ 𝐹:π‘‹βŸΆ{𝐡})) β†’ 𝐹 ∈ (𝐽 Cn 𝐾))
 
Theoremcnrest 14139 Continuity of a restriction from a subspace. (Contributed by Jeff Hankins, 11-Jul-2009.) (Revised by Mario Carneiro, 21-Aug-2015.)
𝑋 = βˆͺ 𝐽    β‡’   ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐴 βŠ† 𝑋) β†’ (𝐹 β†Ύ 𝐴) ∈ ((𝐽 β†Ύt 𝐴) Cn 𝐾))
 
Theoremcnrest2 14140 Equivalence of continuity in the parent topology and continuity in a subspace. (Contributed by Jeff Hankins, 10-Jul-2009.) (Proof shortened by Mario Carneiro, 21-Aug-2015.)
((𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ ran 𝐹 βŠ† 𝐡 ∧ 𝐡 βŠ† π‘Œ) β†’ (𝐹 ∈ (𝐽 Cn 𝐾) ↔ 𝐹 ∈ (𝐽 Cn (𝐾 β†Ύt 𝐡))))
 
Theoremcnrest2r 14141 Equivalence of continuity in the parent topology and continuity in a subspace. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 7-Jun-2014.)
(𝐾 ∈ Top β†’ (𝐽 Cn (𝐾 β†Ύt 𝐡)) βŠ† (𝐽 Cn 𝐾))
 
Theoremcnptopresti 14142 One direction of cnptoprest 14143 under the weaker condition that the point is in the subset rather than the interior of the subset. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Jim Kingdon, 31-Mar-2023.)
(((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ Top) ∧ (𝐴 βŠ† 𝑋 ∧ 𝑃 ∈ 𝐴 ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ))) β†’ (𝐹 β†Ύ 𝐴) ∈ (((𝐽 β†Ύt 𝐴) CnP 𝐾)β€˜π‘ƒ))
 
Theoremcnptoprest 14143 Equivalence of continuity at a point and continuity of the restricted function at a point. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 5-Apr-2023.)
𝑋 = βˆͺ 𝐽    &   π‘Œ = βˆͺ 𝐾    β‡’   (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝐴 βŠ† 𝑋) ∧ (𝑃 ∈ ((intβ€˜π½)β€˜π΄) ∧ 𝐹:π‘‹βŸΆπ‘Œ)) β†’ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ↔ (𝐹 β†Ύ 𝐴) ∈ (((𝐽 β†Ύt 𝐴) CnP 𝐾)β€˜π‘ƒ)))
 
Theoremcnptoprest2 14144 Equivalence of point-continuity in the parent topology and point-continuity in a subspace. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 6-Apr-2023.)
𝑋 = βˆͺ 𝐽    &   π‘Œ = βˆͺ 𝐾    β‡’   (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:π‘‹βŸΆπ΅ ∧ 𝐡 βŠ† π‘Œ)) β†’ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ↔ 𝐹 ∈ ((𝐽 CnP (𝐾 β†Ύt 𝐡))β€˜π‘ƒ)))
 
Theoremcndis 14145 Every function is continuous when the domain is discrete. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 21-Aug-2015.)
((𝐴 ∈ 𝑉 ∧ 𝐽 ∈ (TopOnβ€˜π‘‹)) β†’ (𝒫 𝐴 Cn 𝐽) = (𝑋 β†‘π‘š 𝐴))
 
Theoremcnpdis 14146 If 𝐴 is an isolated point in 𝑋 (or equivalently, the singleton {𝐴} is open in 𝑋), then every function is continuous at 𝐴. (Contributed by Mario Carneiro, 9-Sep-2015.)
(((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ 𝐴 ∈ 𝑋) ∧ {𝐴} ∈ 𝐽) β†’ ((𝐽 CnP 𝐾)β€˜π΄) = (π‘Œ β†‘π‘š 𝑋))
 
Theoremlmfpm 14147 If 𝐹 converges, then 𝐹 is a partial function. (Contributed by Mario Carneiro, 23-Dec-2013.)
((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐹(β‡π‘‘β€˜π½)𝑃) β†’ 𝐹 ∈ (𝑋 ↑pm β„‚))
 
Theoremlmfss 14148 Inclusion of a function having a limit (used to ensure the limit relation is a set, under our definition). (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 23-Dec-2013.)
((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐹(β‡π‘‘β€˜π½)𝑃) β†’ 𝐹 βŠ† (β„‚ Γ— 𝑋))
 
Theoremlmcl 14149 Closure of a limit. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 23-Dec-2013.)
((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐹(β‡π‘‘β€˜π½)𝑃) β†’ 𝑃 ∈ 𝑋)
 
Theoremlmss 14150 Limit on a subspace. (Contributed by NM, 30-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.)
𝐾 = (𝐽 β†Ύt π‘Œ)    &   π‘ = (β„€β‰₯β€˜π‘€)    &   (πœ‘ β†’ π‘Œ ∈ 𝑉)    &   (πœ‘ β†’ 𝐽 ∈ Top)    &   (πœ‘ β†’ 𝑃 ∈ π‘Œ)    &   (πœ‘ β†’ 𝑀 ∈ β„€)    &   (πœ‘ β†’ 𝐹:π‘βŸΆπ‘Œ)    β‡’   (πœ‘ β†’ (𝐹(β‡π‘‘β€˜π½)𝑃 ↔ 𝐹(β‡π‘‘β€˜πΎ)𝑃))
 
Theoremsslm 14151 A finer topology has fewer convergent sequences (but the sequences that do converge, converge to the same value). (Contributed by Mario Carneiro, 15-Sep-2015.)
((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘‹) ∧ 𝐽 βŠ† 𝐾) β†’ (β‡π‘‘β€˜πΎ) βŠ† (β‡π‘‘β€˜π½))
 
Theoremlmres 14152 A function converges iff its restriction to an upper integers set converges. (Contributed by Mario Carneiro, 31-Dec-2013.)
(πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))    &   (πœ‘ β†’ 𝐹 ∈ (𝑋 ↑pm β„‚))    &   (πœ‘ β†’ 𝑀 ∈ β„€)    β‡’   (πœ‘ β†’ (𝐹(β‡π‘‘β€˜π½)𝑃 ↔ (𝐹 β†Ύ (β„€β‰₯β€˜π‘€))(β‡π‘‘β€˜π½)𝑃))
 
Theoremlmff 14153* If 𝐹 converges, there is some upper integer set on which 𝐹 is a total function. (Contributed by Mario Carneiro, 31-Dec-2013.)
𝑍 = (β„€β‰₯β€˜π‘€)    &   (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))    &   (πœ‘ β†’ 𝑀 ∈ β„€)    &   (πœ‘ β†’ 𝐹 ∈ dom (β‡π‘‘β€˜π½))    β‡’   (πœ‘ β†’ βˆƒπ‘— ∈ 𝑍 (𝐹 β†Ύ (β„€β‰₯β€˜π‘—)):(β„€β‰₯β€˜π‘—)βŸΆπ‘‹)
 
Theoremlmtopcnp 14154 The image of a convergent sequence under a continuous map is convergent to the image of the original point. (Contributed by Mario Carneiro, 3-May-2014.) (Revised by Jim Kingdon, 6-Apr-2023.)
(πœ‘ β†’ 𝐹(β‡π‘‘β€˜π½)𝑃)    &   (πœ‘ β†’ 𝐾 ∈ Top)    &   (πœ‘ β†’ 𝐺 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ))    β‡’   (πœ‘ β†’ (𝐺 ∘ 𝐹)(β‡π‘‘β€˜πΎ)(πΊβ€˜π‘ƒ))
 
Theoremlmcn 14155 The image of a convergent sequence under a continuous map is convergent to the image of the original point. (Contributed by Mario Carneiro, 3-May-2014.)
(πœ‘ β†’ 𝐹(β‡π‘‘β€˜π½)𝑃)    &   (πœ‘ β†’ 𝐺 ∈ (𝐽 Cn 𝐾))    β‡’   (πœ‘ β†’ (𝐺 ∘ 𝐹)(β‡π‘‘β€˜πΎ)(πΊβ€˜π‘ƒ))
 
8.1.8  Product topologies
 
Syntaxctx 14156 Extend class notation with the binary topological product operation.
class Γ—t
 
Definitiondf-tx 14157* 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 (π‘₯ ∈ π‘Ÿ, 𝑦 ∈ 𝑠 ↦ (π‘₯ Γ— 𝑦))))
 
Theoremtxvalex 14158 Existence of the binary topological product. If 𝑅 and 𝑆 are known to be topologies, see txtop 14164. (Contributed by Jim Kingdon, 3-Aug-2023.)
((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ π‘Š) β†’ (𝑅 Γ—t 𝑆) ∈ V)
 
Theoremtxval 14159* Value of the binary topological product operation. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 30-Aug-2015.)
𝐡 = ran (π‘₯ ∈ 𝑅, 𝑦 ∈ 𝑆 ↦ (π‘₯ Γ— 𝑦))    β‡’   ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ π‘Š) β†’ (𝑅 Γ—t 𝑆) = (topGenβ€˜π΅))
 
Theoremtxuni2 14160* The underlying set of the product of two topologies. (Contributed by Mario Carneiro, 31-Aug-2015.)
𝐡 = ran (π‘₯ ∈ 𝑅, 𝑦 ∈ 𝑆 ↦ (π‘₯ Γ— 𝑦))    &   π‘‹ = βˆͺ 𝑅    &   π‘Œ = βˆͺ 𝑆    β‡’   (𝑋 Γ— π‘Œ) = βˆͺ 𝐡
 
Theoremtxbasex 14161* The basis for the product topology is a set. (Contributed by Mario Carneiro, 2-Sep-2015.)
𝐡 = ran (π‘₯ ∈ 𝑅, 𝑦 ∈ 𝑆 ↦ (π‘₯ Γ— 𝑦))    β‡’   ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ π‘Š) β†’ 𝐡 ∈ V)
 
Theoremtxbas 14162* 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)
 
Theoremeltx 14163* 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 𝐾) ↔ βˆ€π‘ ∈ 𝑆 βˆƒπ‘₯ ∈ 𝐽 βˆƒπ‘¦ ∈ 𝐾 (𝑝 ∈ (π‘₯ Γ— 𝑦) ∧ (π‘₯ Γ— 𝑦) βŠ† 𝑆)))
 
Theoremtxtop 14164 The product of two topologies is a topology. (Contributed by Jeff Madsen, 2-Sep-2009.)
((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝑅 Γ—t 𝑆) ∈ Top)
 
Theoremtxtopi 14165 The product of two topologies is a topology. (Contributed by Jeff Madsen, 15-Jun-2010.)
𝑅 ∈ Top    &   π‘† ∈ Top    β‡’   (𝑅 Γ—t 𝑆) ∈ Top
 
Theoremtxtopon 14166 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β€˜(𝑋 Γ— π‘Œ)))
 
Theoremtxuni 14167 The underlying set of the product of two topologies. (Contributed by Jeff Madsen, 2-Sep-2009.)
𝑋 = βˆͺ 𝑅    &   π‘Œ = βˆͺ 𝑆    β‡’   ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝑋 Γ— π‘Œ) = βˆͺ (𝑅 Γ—t 𝑆))
 
Theoremtxunii 14168 The underlying set of the product of two topologies. (Contributed by Jeff Madsen, 15-Jun-2010.)
𝑅 ∈ Top    &   π‘† ∈ Top    &   π‘‹ = βˆͺ 𝑅    &   π‘Œ = βˆͺ 𝑆    β‡’   (𝑋 Γ— π‘Œ) = βˆͺ (𝑅 Γ—t 𝑆)
 
Theoremtxopn 14169 The product of two open sets is open in the product topology. (Contributed by Jeff Madsen, 2-Sep-2009.)
(((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ π‘Š) ∧ (𝐴 ∈ 𝑅 ∧ 𝐡 ∈ 𝑆)) β†’ (𝐴 Γ— 𝐡) ∈ (𝑅 Γ—t 𝑆))
 
Theoremtxss12 14170 Subset property of the topological product. (Contributed by Mario Carneiro, 2-Sep-2015.)
(((𝐡 ∈ 𝑉 ∧ 𝐷 ∈ π‘Š) ∧ (𝐴 βŠ† 𝐡 ∧ 𝐢 βŠ† 𝐷)) β†’ (𝐴 Γ—t 𝐢) βŠ† (𝐡 Γ—t 𝐷))
 
Theoremtxbasval 14171 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 𝑆))
 
Theoremneitx 14172 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 𝐾))β€˜(𝐢 Γ— 𝐷)))
 
Theoremtx1cn 14173 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 𝑅))
 
Theoremtx2cn 14174 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 𝑆))
 
Theoremtxcnp 14175* 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 𝐿))β€˜π·))
 
Theoremupxp 14176* 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 β†Ύ (𝐡 Γ— 𝐢))    β‡’   ((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟢𝐡 ∧ 𝐺:𝐴⟢𝐢) β†’ βˆƒ!β„Ž(β„Ž:𝐴⟢(𝐡 Γ— 𝐢) ∧ 𝐹 = (𝑃 ∘ β„Ž) ∧ 𝐺 = (𝑄 ∘ β„Ž)))
 
Theoremtxcnmpt 14177* 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 𝑆)))
 
Theoremuptx 14178* 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 𝑇)(𝐹 = (𝑃 ∘ β„Ž) ∧ 𝐺 = (𝑄 ∘ β„Ž)))
 
Theoremtxcn 14179 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 𝑆))))
 
Theoremtxrest 14180 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 𝐡)))
 
Theoremtxdis 14181 The topological product of discrete spaces is discrete. (Contributed by Mario Carneiro, 14-Aug-2015.)
((𝐴 ∈ 𝑉 ∧ 𝐡 ∈ π‘Š) β†’ (𝒫 𝐴 Γ—t 𝒫 𝐡) = 𝒫 (𝐴 Γ— 𝐡))
 
Theoremtxdis1cn 14182* 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 𝐾))
 
Theoremtxlm 14183* 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 𝐾))βŸ¨π‘…, π‘†βŸ©))
 
Theoremlmcn2 14184* 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 𝑁))    &   π» = (𝑛 ∈ 𝑍 ↦ ((πΉβ€˜π‘›)𝑂(πΊβ€˜π‘›)))    β‡’   (πœ‘ β†’ 𝐻(β‡π‘‘β€˜π‘)(𝑅𝑂𝑆))
 
8.1.9  Continuous function-builders
 
Theoremcnmptid 14185* The identity function is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
(πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))    β‡’   (πœ‘ β†’ (π‘₯ ∈ 𝑋 ↦ π‘₯) ∈ (𝐽 Cn 𝐽))
 
Theoremcnmptc 14186* A constant function is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
(πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))    &   (πœ‘ β†’ 𝐾 ∈ (TopOnβ€˜π‘Œ))    &   (πœ‘ β†’ 𝑃 ∈ π‘Œ)    β‡’   (πœ‘ β†’ (π‘₯ ∈ 𝑋 ↦ 𝑃) ∈ (𝐽 Cn 𝐾))
 
Theoremcnmpt11 14187* 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 𝐿))
 
Theoremcnmpt11f 14188* 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 𝐿))
 
Theoremcnmpt1t 14189* 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 𝐿)))
 
Theoremcnmpt12f 14190* 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 𝑀))
 
Theoremcnmpt12 14191* 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 𝑀))
 
Theoremcnmpt1st 14192* 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 𝐽))
 
Theoremcnmpt2nd 14193* 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 𝐾))
 
Theoremcnmpt2c 14194* A constant function is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
(πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))    &   (πœ‘ β†’ 𝐾 ∈ (TopOnβ€˜π‘Œ))    &   (πœ‘ β†’ 𝐿 ∈ (TopOnβ€˜π‘))    &   (πœ‘ β†’ 𝑃 ∈ 𝑍)    β‡’   (πœ‘ β†’ (π‘₯ ∈ 𝑋, 𝑦 ∈ π‘Œ ↦ 𝑃) ∈ ((𝐽 Γ—t 𝐾) Cn 𝐿))
 
Theoremcnmpt21 14195* 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 𝑀))
 
Theoremcnmpt21f 14196* 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 𝑀))
 
Theoremcnmpt2t 14197* 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 𝑀)))
 
Theoremcnmpt22 14198* 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 𝑁))
 
Theoremcnmpt22f 14199* 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 𝑁))
 
Theoremcnmpt1res 14200* The restriction of a continuous function to a subset is continuous. (Contributed by Mario Carneiro, 5-Jun-2014.)
𝐾 = (𝐽 β†Ύt π‘Œ)    &   (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))    &   (πœ‘ β†’ π‘Œ βŠ† 𝑋)    &   (πœ‘ β†’ (π‘₯ ∈ 𝑋 ↦ 𝐴) ∈ (𝐽 Cn 𝐿))    β‡’   (πœ‘ β†’ (π‘₯ ∈ π‘Œ ↦ 𝐴) ∈ (𝐾 Cn 𝐿))
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15237
  Copyright terms: Public domain < Previous  Next >