Type | Label | Description |
Statement |
|
Theorem | iscn 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 πΎ) β (πΉ:πβΆπ β§ βπ¦ β πΎ (β‘πΉ β π¦) β π½))) |
|
Theorem | cnpval 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 πΎ)βπ) = {π β (π βπ π) β£ βπ¦ β πΎ ((πβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (π β π₯) β π¦))}) |
|
Theorem | iscnp 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 πΎ)βπ) β (πΉ:πβΆπ β§ βπ¦ β πΎ ((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦))))) |
|
Theorem | iscn2 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) β§ (πΉ:πβΆπ β§ βπ¦ β πΎ (β‘πΉ β π¦) β π½))) |
|
Theorem | cntop1 14105 |
Reverse closure for a continuous function. (Contributed by Mario
Carneiro, 21-Aug-2015.)
|
β’ (πΉ β (π½ Cn πΎ) β π½ β Top) |
|
Theorem | cntop2 14106 |
Reverse closure for a continuous function. (Contributed by Mario
Carneiro, 21-Aug-2015.)
|
β’ (πΉ β (π½ Cn πΎ) β πΎ β Top) |
|
Theorem | iscnp3 14107* |
The predicate "the class πΉ is a continuous function from
topology
π½ to topology πΎ at point π".
(Contributed by NM,
15-May-2007.)
|
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ¦ β πΎ ((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ π₯ β (β‘πΉ β π¦)))))) |
|
Theorem | cnf 14108 |
A continuous function is a mapping. (Contributed by FL, 8-Dec-2006.)
(Revised by Mario Carneiro, 21-Aug-2015.)
|
β’ π = βͺ π½ & β’ π = βͺ
πΎ
β β’ (πΉ β (π½ Cn πΎ) β πΉ:πβΆπ) |
|
Theorem | cnf2 14109 |
A continuous function is a mapping. (Contributed by Mario Carneiro,
21-Aug-2015.)
|
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ πΉ β (π½ Cn πΎ)) β πΉ:πβΆπ) |
|
Theorem | cnprcl2k 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 πΎ)βπ)) β π β π) |
|
Theorem | cnpf2 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 πΎ)βπ)) β πΉ:πβΆπ) |
|
Theorem | tgcn 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 πΎ) β (πΉ:πβΆπ β§ βπ¦ β π΅ (β‘πΉ β π¦) β π½))) |
|
Theorem | tgcnp 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 πΎ)βπ) β (πΉ:πβΆπ β§ βπ¦ β π΅ ((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦))))) |
|
Theorem | ssidcn 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 πΎ) β πΎ β π½)) |
|
Theorem | icnpimaex 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 πΎ)βπ) β§ π΄ β πΎ β§ (πΉβπ) β π΄)) β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π΄)) |
|
Theorem | idcn 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 π½)) |
|
Theorem | lmbr 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 β€β₯(πΉ βΎ π¦):π¦βΆπ’)))) |
|
Theorem | lmbr2 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 πΉ β§ (πΉβπ) β π’))))) |
|
Theorem | lmbrf 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βπ)) & β’ π =
(β€β₯βπ)
& β’ (π β π β β€) & β’ (π β πΉ:πβΆπ)
& β’ ((π β§ π β π) β (πΉβπ) = π΄) β β’ (π β (πΉ(βπ‘βπ½)π β (π β π β§ βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)π΄ β π’)))) |
|
Theorem | lmconst 14120 |
A constant sequence converges to its value. (Contributed by NM,
8-Nov-2007.) (Revised by Mario Carneiro, 14-Nov-2013.)
|
β’ π = (β€β₯βπ)
β β’ ((π½ β (TopOnβπ) β§ π β π β§ π β β€) β (π Γ {π})(βπ‘βπ½)π) |
|
Theorem | lmcvg 14121* |
Convergence property of a converging sequence. (Contributed by Mario
Carneiro, 14-Nov-2013.)
|
β’ π = (β€β₯βπ) & β’ (π β π β π)
& β’ (π β π β β€) & β’ (π β πΉ(βπ‘βπ½)π)
& β’ (π β π β π½) β β’ (π β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π) |
|
Theorem | iscnp4 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βπ½)β{π})(πΉ β π₯) β π¦))) |
|
Theorem | cnpnei 14123* |
A condition for continuity at a point in terms of neighborhoods.
(Contributed by Jeff Hankins, 7-Sep-2009.)
|
β’ π = βͺ π½ & β’ π = βͺ
πΎ
β β’ (((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β (πΉ β ((π½ CnP πΎ)βπ΄) β βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄}))) |
|
Theorem | cnima 14124 |
An open subset of the codomain of a continuous function has an open
preimage. (Contributed by FL, 15-Dec-2006.)
|
β’ ((πΉ β (π½ Cn πΎ) β§ π΄ β πΎ) β (β‘πΉ β π΄) β π½) |
|
Theorem | cnco 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 πΏ)) |
|
Theorem | cnptopco 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 πΏ)βπ)) |
|
Theorem | cnclima 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βπ½)) |
|
Theorem | cnntri 14128 |
Property of the preimage of an interior. (Contributed by Mario
Carneiro, 25-Aug-2015.)
|
β’ π = βͺ πΎ β β’ ((πΉ β (π½ Cn πΎ) β§ π β π) β (β‘πΉ β ((intβπΎ)βπ)) β ((intβπ½)β(β‘πΉ β π))) |
|
Theorem | cnntr 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βπ½)β(β‘πΉ β π₯))))) |
|
Theorem | cnss1 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 πΏ)) |
|
Theorem | cnss2 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 πΏ)) |
|
Theorem | cncnpi 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 πΎ)βπ΄)) |
|
Theorem | cnsscnp 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 πΎ)βπ)) |
|
Theorem | cncnp 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 πΎ)βπ₯)))) |
|
Theorem | cncnp2m 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 πΎ)βπ₯))) |
|
Theorem | cnnei 14136* |
Continuity in terms of neighborhoods. (Contributed by Thierry Arnoux,
3-Jan-2018.)
|
β’ π = βͺ π½ & β’ π = βͺ
πΎ
β β’ ((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β (πΉ β (π½ Cn πΎ) β βπ β π βπ€ β ((neiβπΎ)β{(πΉβπ)})βπ£ β ((neiβπ½)β{π})(πΉ β π£) β π€)) |
|
Theorem | cnconst2 14137 |
A constant function is continuous. (Contributed by Mario Carneiro,
19-Mar-2015.)
|
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΅ β π) β (π Γ {π΅}) β (π½ Cn πΎ)) |
|
Theorem | cnconst 14138 |
A constant function is continuous. (Contributed by FL, 15-Jan-2007.)
(Proof shortened by Mario Carneiro, 19-Mar-2015.)
|
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π΅ β π β§ πΉ:πβΆ{π΅})) β πΉ β (π½ Cn πΎ)) |
|
Theorem | cnrest 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 πΎ)) |
|
Theorem | cnrest2 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 π΅)))) |
|
Theorem | cnrest2r 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 πΎ)) |
|
Theorem | cnptopresti 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 πΎ)βπ)) |
|
Theorem | cnptoprest 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 πΎ)βπ))) |
|
Theorem | cnptoprest2 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 π΅))βπ))) |
|
Theorem | cndis 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 π½) = (π βπ π΄)) |
|
Theorem | cnpdis 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 πΎ)βπ΄) = (π βπ π)) |
|
Theorem | lmfpm 14147 |
If πΉ converges, then πΉ is a
partial function. (Contributed by
Mario Carneiro, 23-Dec-2013.)
|
β’ ((π½ β (TopOnβπ) β§ πΉ(βπ‘βπ½)π) β πΉ β (π βpm
β)) |
|
Theorem | lmfss 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βπ) β§ πΉ(βπ‘βπ½)π) β πΉ β (β Γ π)) |
|
Theorem | lmcl 14149 |
Closure of a limit. (Contributed by NM, 19-Dec-2006.) (Revised by
Mario Carneiro, 23-Dec-2013.)
|
β’ ((π½ β (TopOnβπ) β§ πΉ(βπ‘βπ½)π) β π β π) |
|
Theorem | lmss 14150 |
Limit on a subspace. (Contributed by NM, 30-Jan-2008.) (Revised by
Mario Carneiro, 30-Dec-2013.)
|
β’ πΎ = (π½ βΎt π)
& β’ π = (β€β₯βπ) & β’ (π β π β π)
& β’ (π β π½ β Top) & β’ (π β π β π)
& β’ (π β π β β€) & β’ (π β πΉ:πβΆπ) β β’ (π β (πΉ(βπ‘βπ½)π β πΉ(βπ‘βπΎ)π)) |
|
Theorem | sslm 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βπ) β§ π½ β πΎ) β
(βπ‘βπΎ) β
(βπ‘βπ½)) |
|
Theorem | lmres 14152 |
A function converges iff its restriction to an upper integers set
converges. (Contributed by Mario Carneiro, 31-Dec-2013.)
|
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ β (π βpm
β))
& β’ (π β π β β€)
β β’ (π β (πΉ(βπ‘βπ½)π β (πΉ βΎ
(β€β₯βπ))(βπ‘βπ½)π)) |
|
Theorem | lmff 14153* |
If πΉ converges, there is some upper
integer set on which πΉ is
a total function. (Contributed by Mario Carneiro, 31-Dec-2013.)
|
β’ π = (β€β₯βπ) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β β€) & β’ (π β πΉ β dom
(βπ‘βπ½)) β β’ (π β βπ β π (πΉ βΎ
(β€β₯βπ)):(β€β₯βπ)βΆπ) |
|
Theorem | lmtopcnp 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 πΎ)βπ)) β β’ (π β (πΊ β πΉ)(βπ‘βπΎ)(πΊβπ)) |
|
Theorem | lmcn 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
|
|
Syntax | ctx 14156 |
Extend class notation with the binary topological product operation.
|
class Γt |
|
Definition | df-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 (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)))) |
|
Theorem | txvalex 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) |
|
Theorem | txval 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βπ΅)) |
|
Theorem | txuni2 14160* |
The underlying set of the product of two topologies. (Contributed by
Mario Carneiro, 31-Aug-2015.)
|
β’ π΅ = ran (π₯ β π
, π¦ β π β¦ (π₯ Γ π¦))
& β’ π = βͺ π
& β’ π = βͺ
π
β β’ (π Γ π) = βͺ π΅ |
|
Theorem | txbasex 14161* |
The basis for the product topology is a set. (Contributed by Mario
Carneiro, 2-Sep-2015.)
|
β’ π΅ = ran (π₯ β π
, π¦ β π β¦ (π₯ Γ π¦)) β β’ ((π
β π β§ π β π) β π΅ β V) |
|
Theorem | txbas 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) |
|
Theorem | eltx 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 πΎ) β βπ β π βπ₯ β π½ βπ¦ β πΎ (π β (π₯ Γ π¦) β§ (π₯ Γ π¦) β π))) |
|
Theorem | txtop 14164 |
The product of two topologies is a topology. (Contributed by Jeff
Madsen, 2-Sep-2009.)
|
β’ ((π
β Top β§ π β Top) β (π
Γt π) β Top) |
|
Theorem | txtopi 14165 |
The product of two topologies is a topology. (Contributed by Jeff
Madsen, 15-Jun-2010.)
|
β’ π
β Top & β’ π β
Top β β’ (π
Γt π) β Top |
|
Theorem | txtopon 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β(π Γ π))) |
|
Theorem | txuni 14167 |
The underlying set of the product of two topologies. (Contributed by
Jeff Madsen, 2-Sep-2009.)
|
β’ π = βͺ π
& β’ π = βͺ
π
β β’ ((π
β Top β§ π β Top) β (π Γ π) = βͺ (π
Γt π)) |
|
Theorem | txunii 14168 |
The underlying set of the product of two topologies. (Contributed by
Jeff Madsen, 15-Jun-2010.)
|
β’ π
β Top & β’ π β Top & β’ π = βͺ
π
& β’ π = βͺ
π
β β’ (π Γ π) = βͺ (π
Γt π) |
|
Theorem | txopn 14169 |
The product of two open sets is open in the product topology.
(Contributed by Jeff Madsen, 2-Sep-2009.)
|
β’ (((π
β π β§ π β π) β§ (π΄ β π
β§ π΅ β π)) β (π΄ Γ π΅) β (π
Γt π)) |
|
Theorem | txss12 14170 |
Subset property of the topological product. (Contributed by Mario
Carneiro, 2-Sep-2015.)
|
β’ (((π΅ β π β§ π· β π) β§ (π΄ β π΅ β§ πΆ β π·)) β (π΄ Γt πΆ) β (π΅ Γt π·)) |
|
Theorem | txbasval 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 π)) |
|
Theorem | neitx 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 πΎ))β(πΆ Γ π·))) |
|
Theorem | tx1cn 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 π
)) |
|
Theorem | tx2cn 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 π)) |
|
Theorem | txcnp 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 πΏ))βπ·)) |
|
Theorem | upxp 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 βΎ
(π΅ Γ πΆ))
β β’ ((π΄ β π· β§ πΉ:π΄βΆπ΅ β§ πΊ:π΄βΆπΆ) β β!β(β:π΄βΆ(π΅ Γ πΆ) β§ πΉ = (π β β) β§ πΊ = (π β β))) |
|
Theorem | txcnmpt 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 π))) |
|
Theorem | uptx 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 π)(πΉ = (π β β) β§ πΊ = (π β β))) |
|
Theorem | txcn 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 π)))) |
|
Theorem | txrest 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 π΅))) |
|
Theorem | txdis 14181 |
The topological product of discrete spaces is discrete. (Contributed by
Mario Carneiro, 14-Aug-2015.)
|
β’ ((π΄ β π β§ π΅ β π) β (π« π΄ Γt π« π΅) = π« (π΄ Γ π΅)) |
|
Theorem | txdis1cn 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 πΎ)) |
|
Theorem | txlm 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 πΎ))β¨π
, πβ©)) |
|
Theorem | lmcn2 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
|
|
Theorem | cnmptid 14185* |
The identity function is continuous. (Contributed by Mario Carneiro,
5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
β’ (π β π½ β (TopOnβπ)) β β’ (π β (π₯ β π β¦ π₯) β (π½ Cn π½)) |
|
Theorem | cnmptc 14186* |
A constant function is continuous. (Contributed by Mario Carneiro,
5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β π β π) β β’ (π β (π₯ β π β¦ π) β (π½ Cn πΎ)) |
|
Theorem | cnmpt11 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 πΏ)) |
|
Theorem | cnmpt11f 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 πΏ)) |
|
Theorem | cnmpt1t 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 πΏ))) |
|
Theorem | cnmpt12f 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 π)) |
|
Theorem | cnmpt12 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 π)) |
|
Theorem | cnmpt1st 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 π½)) |
|
Theorem | cnmpt2nd 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 πΎ)) |
|
Theorem | cnmpt2c 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 πΏ)) |
|
Theorem | cnmpt21 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 π)) |
|
Theorem | cnmpt21f 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 π)) |
|
Theorem | cnmpt2t 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 π))) |
|
Theorem | cnmpt22 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 π)) |
|
Theorem | cnmpt22f 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 π)) |
|
Theorem | cnmpt1res 14200* |
The restriction of a continuous function to a subset is continuous.
(Contributed by Mario Carneiro, 5-Jun-2014.)
|
β’ πΎ = (π½ βΎt π)
& β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π)
& β’ (π β (π₯ β π β¦ π΄) β (π½ Cn πΏ)) β β’ (π β (π₯ β π β¦ π΄) β (πΎ Cn πΏ)) |