![]() |
Metamath
Proof Explorer Theorem List (p. 232 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | leordtvallem1 23101* | Lemma for leordtval 23104. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π΄ = ran (π₯ β β* β¦ (π₯(,]+β)) β β’ π΄ = ran (π₯ β β* β¦ {π¦ β β* β£ Β¬ π¦ β€ π₯}) | ||
Theorem | leordtvallem2 23102* | Lemma for leordtval 23104. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π΄ = ran (π₯ β β* β¦ (π₯(,]+β)) & β’ π΅ = ran (π₯ β β* β¦ (-β[,)π₯)) β β’ π΅ = ran (π₯ β β* β¦ {π¦ β β* β£ Β¬ π₯ β€ π¦}) | ||
Theorem | leordtval2 23103 | The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π΄ = ran (π₯ β β* β¦ (π₯(,]+β)) & β’ π΅ = ran (π₯ β β* β¦ (-β[,)π₯)) β β’ (ordTopβ β€ ) = (topGenβ(fiβ(π΄ βͺ π΅))) | ||
Theorem | leordtval 23104 | The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π΄ = ran (π₯ β β* β¦ (π₯(,]+β)) & β’ π΅ = ran (π₯ β β* β¦ (-β[,)π₯)) & β’ πΆ = ran (,) β β’ (ordTopβ β€ ) = (topGenβ((π΄ βͺ π΅) βͺ πΆ)) | ||
Theorem | iccordt 23105 | A closed interval is closed in the order topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ (π΄[,]π΅) β (Clsdβ(ordTopβ β€ )) | ||
Theorem | iocpnfordt 23106 | An unbounded above open interval is open in the order topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ (π΄(,]+β) β (ordTopβ β€ ) | ||
Theorem | icomnfordt 23107 | An unbounded above open interval is open in the order topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ (-β[,)π΄) β (ordTopβ β€ ) | ||
Theorem | iooordt 23108 | An open interval is open in the order topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ (π΄(,)π΅) β (ordTopβ β€ ) | ||
Theorem | reordt 23109 | The real numbers are an open set in the topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ β β (ordTopβ β€ ) | ||
Theorem | lecldbas 23110 | The set of closed intervals forms a closed subbasis for the topology on the extended reals. Since our definition of a basis is in terms of open sets, we express this by showing that the complements of closed intervals form an open subbasis for the topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ πΉ = (π₯ β ran [,] β¦ (β* β π₯)) β β’ (ordTopβ β€ ) = (topGenβ(fiβran πΉ)) | ||
Theorem | pnfnei 23111* | A neighborhood of +β contains an unbounded interval based at a real number. Together with xrtgioo 24709 (which describes neighborhoods of β) and mnfnei 23112, this gives all "negative" topological information ensuring that it is not too fine (and of course iooordt 23108 and similar ensure that it has all the sets we want). (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ ((π΄ β (ordTopβ β€ ) β§ +β β π΄) β βπ₯ β β (π₯(,]+β) β π΄) | ||
Theorem | mnfnei 23112* | A neighborhood of -β contains an unbounded interval based at a real number. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ ((π΄ β (ordTopβ β€ ) β§ -β β π΄) β βπ₯ β β (-β[,)π₯) β π΄) | ||
Theorem | ordtrestixx 23113* | The restriction of the less than order to an interval gives the same topology as the subspace topology. (Contributed by Mario Carneiro, 9-Sep-2015.) |
β’ π΄ β β* & β’ ((π₯ β π΄ β§ π¦ β π΄) β (π₯[,]π¦) β π΄) β β’ ((ordTopβ β€ ) βΎt π΄) = (ordTopβ( β€ β© (π΄ Γ π΄))) | ||
Theorem | ordtresticc 23114 | The restriction of the less than order to a closed interval gives the same topology as the subspace topology. (Contributed by Mario Carneiro, 9-Sep-2015.) |
β’ ((ordTopβ β€ ) βΎt (π΄[,]π΅)) = (ordTopβ( β€ β© ((π΄[,]π΅) Γ (π΄[,]π΅)))) | ||
Syntax | ccn 23115 | Extend class notation with the class of continuous functions between topologies. |
class Cn | ||
Syntax | ccnp 23116 | Extend class notation with the class of functions between topologies continuous at a given point. |
class CnP | ||
Syntax | clm 23117 | Extend class notation with a function on topological spaces whose value is the convergence relation for limit sequences in the space. |
class βπ‘ | ||
Definition | df-cn 23118* | Define a function on two topologies whose value is the set of continuous mappings from the first topology to the second. Based on definition of continuous function in [Munkres] p. 102. See iscn 23126 for the predicate form. (Contributed by NM, 17-Oct-2006.) |
β’ Cn = (π β Top, π β Top β¦ {π β (βͺ π βm βͺ π) β£ βπ¦ β π (β‘π β π¦) β π}) | ||
Definition | df-cnp 23119* | Define a function on two topologies whose value is the set of continuous mappings at a specified point in the first topology. Based on Theorem 7.2(g) of [Munkres] p. 107. (Contributed by NM, 17-Oct-2006.) |
β’ CnP = (π β Top, π β Top β¦ (π₯ β βͺ π β¦ {π β (βͺ π βm βͺ π) β£ βπ¦ β π ((πβπ₯) β π¦ β βπ β π (π₯ β π β§ (π β π) β π¦))})) | ||
Definition | df-lm 23120* | Define a function on topologies whose value is the convergence relation for sequences into the given topological space. Although π is typically a sequence (a function from an upperset of integers) with values in the topological space, it need not be. Note, however, that the limit property concerns only values at integers, so that the real-valued function (π₯ β β β¦ (sinβ(Ο Β· π₯))) converges to zero (in the standard topology on the reals) with this definition. (Contributed by NM, 7-Sep-2006.) |
β’ βπ‘ = (π β Top β¦ {β¨π, π₯β© β£ (π β (βͺ π βpm β) β§ π₯ β βͺ π β§ βπ’ β π (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))}) | ||
Theorem | lmrel 23121 | The topological space convergence relation is a relation. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 14-Nov-2013.) |
β’ Rel (βπ‘βπ½) | ||
Theorem | lmrcl 23122 | Reverse closure for the convergence relation. (Contributed by Mario Carneiro, 7-Sep-2015.) |
β’ (πΉ(βπ‘βπ½)π β π½ β Top) | ||
Theorem | lmfval 23123* | The relation "sequence π converges to point π¦ " in a metric space. (Contributed by NM, 7-Sep-2006.) (Revised by Mario Carneiro, 21-Aug-2015.) |
β’ (π½ β (TopOnβπ) β (βπ‘βπ½) = {β¨π, π₯β© β£ (π β (π βpm β) β§ π₯ β π β§ βπ’ β π½ (π₯ β π’ β βπ¦ β ran β€β₯(π βΎ π¦):π¦βΆπ’))}) | ||
Theorem | cnfval 23124* | The set of all continuous functions from topology π½ to topology πΎ. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (π½ Cn πΎ) = {π β (π βm π) β£ βπ¦ β πΎ (β‘π β π¦) β π½}) | ||
Theorem | cnpfval 23125* | The function mapping the points in a topology π½ to the set of all functions from π½ to topology πΎ continuous at that point. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (π½ CnP πΎ) = (π₯ β π β¦ {π β (π βm π) β£ βπ€ β πΎ ((πβπ₯) β π€ β βπ£ β π½ (π₯ β π£ β§ (π β π£) β π€))})) | ||
Theorem | iscn 23126* | 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 23127* | 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 πΎ)βπ) = {π β (π βm π) β£ βπ¦ β πΎ ((πβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (π β π₯) β π¦))}) | ||
Theorem | iscnp 23128* | 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 23129* | 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 | iscnp2 23130* | 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 Mario Carneiro, 21-Aug-2015.) |
β’ π = βͺ π½ & β’ π = βͺ πΎ β β’ (πΉ β ((π½ CnP πΎ)βπ) β ((π½ β Top β§ πΎ β Top β§ π β π) β§ (πΉ:πβΆπ β§ βπ¦ β πΎ ((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦))))) | ||
Theorem | cntop1 23131 | Reverse closure for a continuous function. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ (πΉ β (π½ Cn πΎ) β π½ β Top) | ||
Theorem | cntop2 23132 | Reverse closure for a continuous function. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ (πΉ β (π½ Cn πΎ) β πΎ β Top) | ||
Theorem | cnptop1 23133 | Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ (πΉ β ((π½ CnP πΎ)βπ) β π½ β Top) | ||
Theorem | cnptop2 23134 | Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ (πΉ β ((π½ CnP πΎ)βπ) β πΎ β Top) | ||
Theorem | iscnp3 23135* | The predicate "the class πΉ is a continuous function from topology π½ to topology πΎ at point π". (Contributed by NM, 15-May-2007.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ¦ β πΎ ((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ π₯ β (β‘πΉ β π¦)))))) | ||
Theorem | cnprcl 23136 | Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ π = βͺ π½ β β’ (πΉ β ((π½ CnP πΎ)βπ) β π β π) | ||
Theorem | cnf 23137 | A continuous function is a mapping. (Contributed by FL, 8-Dec-2006.) (Revised by Mario Carneiro, 21-Aug-2015.) |
β’ π = βͺ π½ & β’ π = βͺ πΎ β β’ (πΉ β (π½ Cn πΎ) β πΉ:πβΆπ) | ||
Theorem | cnpf 23138 | A continuous function at point π is a mapping. (Contributed by FL, 17-Nov-2006.) (Revised by Mario Carneiro, 21-Aug-2015.) |
β’ π = βͺ π½ & β’ π = βͺ πΎ β β’ (πΉ β ((π½ CnP πΎ)βπ) β πΉ:πβΆπ) | ||
Theorem | cnpcl 23139 | The value of a continuous function from π½ to πΎ at point π belongs to the underlying set of topology πΎ. (Contributed by FL, 27-Dec-2006.) (Revised by Mario Carneiro, 21-Aug-2015.) |
β’ π = βͺ π½ & β’ π = βͺ πΎ β β’ ((πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β π) β (πΉβπ΄) β π) | ||
Theorem | cnf2 23140 | A continuous function is a mapping. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ πΉ β (π½ Cn πΎ)) β πΉ:πβΆπ) | ||
Theorem | cnpf2 23141 | A continuous function at point π is a mapping. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ πΉ β ((π½ CnP πΎ)βπ)) β πΉ:πβΆπ) | ||
Theorem | cnprcl2 23142 | Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΉ β ((π½ CnP πΎ)βπ)) β π β π) | ||
Theorem | tgcn 23143* | 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 23144* | 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 | subbascn 23145* | The continuity predicate when the range is given by a subbasis for a topology. (Contributed by Mario Carneiro, 7-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β π΅ β π) & β’ (π β πΎ = (topGenβ(fiβπ΅))) & β’ (π β πΎ β (TopOnβπ)) β β’ (π β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆπ β§ βπ¦ β π΅ (β‘πΉ β π¦) β π½))) | ||
Theorem | ssidcn 23146 | 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 | cnpimaex 23147* | Property of a function continuous at a point. (Contributed by FL, 31-Dec-2006.) |
β’ ((πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β πΎ β§ (πΉβπ) β π΄) β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π΄)) | ||
Theorem | idcn 23148 | 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 23149* | Express the binary relation "sequence πΉ converges to point π " in a topological space. Definition 1.4-1 of [Kreyszig] p. 25. The condition πΉ β (β Γ π) allows to use objects more general than sequences when convenient; see the comment in df-lm 23120. (Contributed by Mario Carneiro, 14-Nov-2013.) |
β’ (π β π½ β (TopOnβπ)) β β’ (π β (πΉ(βπ‘βπ½)π β (πΉ β (π βpm β) β§ π β π β§ βπ’ β π½ (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’)))) | ||
Theorem | lmbr2 23150* | 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 23151* | Express the binary relation "sequence πΉ converges to point π " in a metric space using an arbitrary upper set of integers. This version of lmbr2 23150 presupposes that πΉ is a function. (Contributed by Mario Carneiro, 14-Nov-2013.) |
β’ (π β π½ β (TopOnβπ)) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆπ) & β’ ((π β§ π β π) β (πΉβπ) = π΄) β β’ (π β (πΉ(βπ‘βπ½)π β (π β π β§ βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)π΄ β π’)))) | ||
Theorem | lmconst 23152 | A constant sequence converges to its value. (Contributed by NM, 8-Nov-2007.) (Revised by Mario Carneiro, 14-Nov-2013.) |
β’ π = (β€β₯βπ) β β’ ((π½ β (TopOnβπ) β§ π β π β§ π β β€) β (π Γ {π})(βπ‘βπ½)π) | ||
Theorem | lmcvg 23153* | Convergence property of a converging sequence. (Contributed by Mario Carneiro, 14-Nov-2013.) |
β’ π = (β€β₯βπ) & β’ (π β π β π) & β’ (π β π β β€) & β’ (π β πΉ(βπ‘βπ½)π) & β’ (π β π β π½) β β’ (π β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π) | ||
Theorem | iscnp4 23154* | 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 23155* | 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 23156 | An open subset of the codomain of a continuous function has an open preimage. (Contributed by FL, 15-Dec-2006.) |
β’ ((πΉ β (π½ Cn πΎ) β§ π΄ β πΎ) β (β‘πΉ β π΄) β π½) | ||
Theorem | cnco 23157 | 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 | cnpco 23158 | 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.) |
β’ ((πΉ β ((π½ CnP πΎ)βπ) β§ πΊ β ((πΎ CnP πΏ)β(πΉβπ))) β (πΊ β πΉ) β ((π½ CnP πΏ)βπ)) | ||
Theorem | cnclima 23159 | 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 | iscncl 23160* | A characterization of a continuity function using closed sets. Theorem 1(d) of [BourbakiTop1] p. I.9. (Contributed by FL, 19-Nov-2006.) (Proof shortened by Mario Carneiro, 21-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½)))) | ||
Theorem | cncls2i 23161 | Property of the preimage of a closure. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ π = βͺ πΎ β β’ ((πΉ β (π½ Cn πΎ) β§ π β π) β ((clsβπ½)β(β‘πΉ β π)) β (β‘πΉ β ((clsβπΎ)βπ))) | ||
Theorem | cnntri 23162 | Property of the preimage of an interior. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ π = βͺ πΎ β β’ ((πΉ β (π½ Cn πΎ) β§ π β π) β (β‘πΉ β ((intβπΎ)βπ)) β ((intβπ½)β(β‘πΉ β π))) | ||
Theorem | cnclsi 23163 | Property of the image of a closure. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ π = βͺ π½ β β’ ((πΉ β (π½ Cn πΎ) β§ π β π) β (πΉ β ((clsβπ½)βπ)) β ((clsβπΎ)β(πΉ β π))) | ||
Theorem | cncls2 23164* | Continuity in terms of closure. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆπ β§ βπ₯ β π« π((clsβπ½)β(β‘πΉ β π₯)) β (β‘πΉ β ((clsβπΎ)βπ₯))))) | ||
Theorem | cncls 23165* | Continuity in terms of closure. (Contributed by Jeff Hankins, 1-Oct-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆπ β§ βπ₯ β π« π(πΉ β ((clsβπ½)βπ₯)) β ((clsβπΎ)β(πΉ β π₯))))) | ||
Theorem | cnntr 23166* | 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 23167 | 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 23168 | 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 23169 | 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 23170 | 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 23171* | 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 | cncnp2 23172* | A continuous function is continuous at all points. 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 | cnnei 23173* | Continuity in terms of neighborhoods. (Contributed by Thierry Arnoux, 3-Jan-2018.) |
β’ π = βͺ π½ & β’ π = βͺ πΎ β β’ ((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β (πΉ β (π½ Cn πΎ) β βπ β π βπ€ β ((neiβπΎ)β{(πΉβπ)})βπ£ β ((neiβπ½)β{π})(πΉ β π£) β π€)) | ||
Theorem | cnconst2 23174 | A constant function is continuous. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΅ β π) β (π Γ {π΅}) β (π½ Cn πΎ)) | ||
Theorem | cnconst 23175 | A constant function is continuous. (Contributed by FL, 15-Jan-2007.) (Proof shortened by Mario Carneiro, 19-Mar-2015.) |
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π΅ β π β§ πΉ:πβΆ{π΅})) β πΉ β (π½ Cn πΎ)) | ||
Theorem | cnrest 23176 | 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 23177 | 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 23178 | 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 | cnpresti 23179 | One direction of cnprest 23180 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 Mario Carneiro, 1-May-2015.) |
β’ π = βͺ π½ β β’ ((π΄ β π β§ π β π΄ β§ πΉ β ((π½ CnP πΎ)βπ)) β (πΉ βΎ π΄) β (((π½ βΎt π΄) CnP πΎ)βπ)) | ||
Theorem | cnprest 23180 | Equivalence of continuity at a point and continuity of the restricted function at a point. (Contributed by Mario Carneiro, 8-Aug-2014.) |
β’ π = βͺ π½ & β’ π = βͺ πΎ β β’ (((π½ β Top β§ π΄ β π) β§ (π β ((intβπ½)βπ΄) β§ πΉ:πβΆπ)) β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ βΎ π΄) β (((π½ βΎt π΄) CnP πΎ)βπ))) | ||
Theorem | cnprest2 23181 | Equivalence of point-continuity in the parent topology and point-continuity in a subspace. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 21-Aug-2015.) |
β’ π = βͺ π½ & β’ π = βͺ πΎ β β’ ((πΎ β Top β§ πΉ:πβΆπ΅ β§ π΅ β π) β (πΉ β ((π½ CnP πΎ)βπ) β πΉ β ((π½ CnP (πΎ βΎt π΅))βπ))) | ||
Theorem | cndis 23182 | 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 π½) = (π βm π΄)) | ||
Theorem | cnindis 23183 | Every function is continuous when the codomain is indiscrete (trivial). (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Mario Carneiro, 21-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β (π½ Cn {β , π΄}) = (π΄ βm π)) | ||
Theorem | cnpdis 23184 | 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 πΎ)βπ΄) = (π βm π)) | ||
Theorem | paste 23185 | Pasting lemma. If π΄ and π΅ are closed sets in π with π΄ βͺ π΅ = π, then any function whose restrictions to π΄ and π΅ are continuous is continuous on all of π. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 21-Aug-2015.) |
β’ π = βͺ π½ & β’ π = βͺ πΎ & β’ (π β π΄ β (Clsdβπ½)) & β’ (π β π΅ β (Clsdβπ½)) & β’ (π β (π΄ βͺ π΅) = π) & β’ (π β πΉ:πβΆπ) & β’ (π β (πΉ βΎ π΄) β ((π½ βΎt π΄) Cn πΎ)) & β’ (π β (πΉ βΎ π΅) β ((π½ βΎt π΅) Cn πΎ)) β β’ (π β πΉ β (π½ Cn πΎ)) | ||
Theorem | lmfpm 23186 | If πΉ converges, then πΉ is a partial function. (Contributed by Mario Carneiro, 23-Dec-2013.) |
β’ ((π½ β (TopOnβπ) β§ πΉ(βπ‘βπ½)π) β πΉ β (π βpm β)) | ||
Theorem | lmfss 23187 | 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 23188 | Closure of a limit. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 23-Dec-2013.) |
β’ ((π½ β (TopOnβπ) β§ πΉ(βπ‘βπ½)π) β π β π) | ||
Theorem | lmss 23189 | Limit on a subspace. (Contributed by NM, 30-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.) |
β’ πΎ = (π½ βΎt π) & β’ π = (β€β₯βπ) & β’ (π β π β π) & β’ (π β π½ β Top) & β’ (π β π β π) & β’ (π β π β β€) & β’ (π β πΉ:πβΆπ) β β’ (π β (πΉ(βπ‘βπ½)π β πΉ(βπ‘βπΎ)π)) | ||
Theorem | sslm 23190 | 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 23191 | A function converges iff its restriction to an upper integers set converges. (Contributed by Mario Carneiro, 31-Dec-2013.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ β (π βpm β)) & β’ (π β π β β€) β β’ (π β (πΉ(βπ‘βπ½)π β (πΉ βΎ (β€β₯βπ))(βπ‘βπ½)π)) | ||
Theorem | lmff 23192* | If πΉ converges, there is some upper integer set on which πΉ is a total function. (Contributed by Mario Carneiro, 31-Dec-2013.) |
β’ π = (β€β₯βπ) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β β€) & β’ (π β πΉ β dom (βπ‘βπ½)) β β’ (π β βπ β π (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆπ) | ||
Theorem | lmcls 23193* | Any convergent sequence of points in a subset of a topological space converges to a point in the closure of the subset. (Contributed by Mario Carneiro, 30-Dec-2013.) (Revised by Mario Carneiro, 1-May-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β β€) & β’ (π β πΉ(βπ‘βπ½)π) & β’ ((π β§ π β π) β (πΉβπ) β π) & β’ (π β π β π) β β’ (π β π β ((clsβπ½)βπ)) | ||
Theorem | lmcld 23194* | Any convergent sequence of points in a closed subset of a topological space converges to a point in the set. (Contributed by Mario Carneiro, 30-Dec-2013.) |
β’ π = (β€β₯βπ) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β β€) & β’ (π β πΉ(βπ‘βπ½)π) & β’ ((π β§ π β π) β (πΉβπ) β π) & β’ (π β π β (Clsdβπ½)) β β’ (π β π β π) | ||
Theorem | lmcnp 23195 | 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.) |
β’ (π β πΉ(βπ‘βπ½)π) & β’ (π β πΊ β ((π½ CnP πΎ)βπ)) β β’ (π β (πΊ β πΉ)(βπ‘βπΎ)(πΊβπ)) | ||
Theorem | lmcn 23196 | 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 πΎ)) β β’ (π β (πΊ β πΉ)(βπ‘βπΎ)(πΊβπ)) | ||
Syntax | ct0 23197 | Extend class notation with the class of all T0 spaces. |
class Kol2 | ||
Syntax | ct1 23198 | Extend class notation to include T1 spaces (also called FrΓ©chet spaces). |
class Fre | ||
Syntax | cha 23199 | Extend class notation with the class of all Hausdorff spaces. |
class Haus | ||
Syntax | creg 23200 | Extend class notation with the class of all regular topologies. |
class Reg |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |