![]() |
Metamath
Proof Explorer Theorem List (p. 228 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ordtcld1 22701* | A downward ray (-β, π] is closed. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π = dom π β β’ ((π β π β§ π β π) β {π₯ β π β£ π₯π π} β (Clsdβ(ordTopβπ ))) | ||
Theorem | ordtcld2 22702* | An upward ray [π, +β) is closed. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π = dom π β β’ ((π β π β§ π β π) β {π₯ β π β£ ππ π₯} β (Clsdβ(ordTopβπ ))) | ||
Theorem | ordtcld3 22703* | A closed interval [π΄, π΅] is closed. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π = dom π β β’ ((π β π β§ π΄ β π β§ π΅ β π) β {π₯ β π β£ (π΄π π₯ β§ π₯π π΅)} β (Clsdβ(ordTopβπ ))) | ||
Theorem | ordttop 22704 | The order topology is a topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ (π β π β (ordTopβπ ) β Top) | ||
Theorem | ordtcnv 22705 | The order dual generates the same topology as the original order. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ (π β PosetRel β (ordTopββ‘π ) = (ordTopβπ )) | ||
Theorem | ordtrest 22706 | The subspace topology of an order topology is in general finer than the topology generated by the restricted order, but we do have inclusion in one direction. (Contributed by Mario Carneiro, 9-Sep-2015.) |
β’ ((π β PosetRel β§ π΄ β π) β (ordTopβ(π β© (π΄ Γ π΄))) β ((ordTopβπ ) βΎt π΄)) | ||
Theorem | ordtrest2lem 22707* | Lemma for ordtrest2 22708. (Contributed by Mario Carneiro, 9-Sep-2015.) |
β’ π = dom π & β’ (π β π β TosetRel ) & β’ (π β π΄ β π) & β’ ((π β§ (π₯ β π΄ β§ π¦ β π΄)) β {π§ β π β£ (π₯π π§ β§ π§π π¦)} β π΄) β β’ (π β βπ£ β ran (π§ β π β¦ {π€ β π β£ Β¬ π€π π§})(π£ β© π΄) β (ordTopβ(π β© (π΄ Γ π΄)))) | ||
Theorem | ordtrest2 22708* | An interval-closed set π΄ in a total order has the same subspace topology as the restricted order topology. (An interval-closed set is the same thing as an open or half-open or closed interval in β, but in other sets like β there are interval-closed sets like (Ο, +β) β© β that are not intervals.) (Contributed by Mario Carneiro, 9-Sep-2015.) |
β’ π = dom π & β’ (π β π β TosetRel ) & β’ (π β π΄ β π) & β’ ((π β§ (π₯ β π΄ β§ π¦ β π΄)) β {π§ β π β£ (π₯π π§ β§ π§π π¦)} β π΄) β β’ (π β (ordTopβ(π β© (π΄ Γ π΄))) = ((ordTopβπ ) βΎt π΄)) | ||
Theorem | letopon 22709 | The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ (ordTopβ β€ ) β (TopOnββ*) | ||
Theorem | letop 22710 | The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ (ordTopβ β€ ) β Top | ||
Theorem | letopuni 22711 | The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ β* = βͺ (ordTopβ β€ ) | ||
Theorem | xrstopn 22712 | The topology component of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ (ordTopβ β€ ) = (TopOpenββ*π ) | ||
Theorem | xrstps 22713 | The extended real number structure is a topological space. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ β*π β TopSp | ||
Theorem | leordtvallem1 22714* | Lemma for leordtval 22717. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π΄ = ran (π₯ β β* β¦ (π₯(,]+β)) β β’ π΄ = ran (π₯ β β* β¦ {π¦ β β* β£ Β¬ π¦ β€ π₯}) | ||
Theorem | leordtvallem2 22715* | Lemma for leordtval 22717. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π΄ = ran (π₯ β β* β¦ (π₯(,]+β)) & β’ π΅ = ran (π₯ β β* β¦ (-β[,)π₯)) β β’ π΅ = ran (π₯ β β* β¦ {π¦ β β* β£ Β¬ π₯ β€ π¦}) | ||
Theorem | leordtval2 22716 | The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π΄ = ran (π₯ β β* β¦ (π₯(,]+β)) & β’ π΅ = ran (π₯ β β* β¦ (-β[,)π₯)) β β’ (ordTopβ β€ ) = (topGenβ(fiβ(π΄ βͺ π΅))) | ||
Theorem | leordtval 22717 | The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π΄ = ran (π₯ β β* β¦ (π₯(,]+β)) & β’ π΅ = ran (π₯ β β* β¦ (-β[,)π₯)) & β’ πΆ = ran (,) β β’ (ordTopβ β€ ) = (topGenβ((π΄ βͺ π΅) βͺ πΆ)) | ||
Theorem | iccordt 22718 | A closed interval is closed in the order topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ (π΄[,]π΅) β (Clsdβ(ordTopβ β€ )) | ||
Theorem | iocpnfordt 22719 | 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 22720 | 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 22721 | An open interval is open in the order topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ (π΄(,)π΅) β (ordTopβ β€ ) | ||
Theorem | reordt 22722 | The real numbers are an open set in the topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ β β (ordTopβ β€ ) | ||
Theorem | lecldbas 22723 | 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 22724* | A neighborhood of +β contains an unbounded interval based at a real number. Together with xrtgioo 24322 (which describes neighborhoods of β) and mnfnei 22725, this gives all "negative" topological information ensuring that it is not too fine (and of course iooordt 22721 and similar ensure that it has all the sets we want). (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ ((π΄ β (ordTopβ β€ ) β§ +β β π΄) β βπ₯ β β (π₯(,]+β) β π΄) | ||
Theorem | mnfnei 22725* | A neighborhood of -β contains an unbounded interval based at a real number. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ ((π΄ β (ordTopβ β€ ) β§ -β β π΄) β βπ₯ β β (-β[,)π₯) β π΄) | ||
Theorem | ordtrestixx 22726* | 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 22727 | 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 22728 | Extend class notation with the class of continuous functions between topologies. |
class Cn | ||
Syntax | ccnp 22729 | Extend class notation with the class of functions between topologies continuous at a given point. |
class CnP | ||
Syntax | clm 22730 | 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 22731* | 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 22739 for the predicate form. (Contributed by NM, 17-Oct-2006.) |
β’ Cn = (π β Top, π β Top β¦ {π β (βͺ π βm βͺ π) β£ βπ¦ β π (β‘π β π¦) β π}) | ||
Definition | df-cnp 22732* | 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 22733* | 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 22734 | The topological space convergence relation is a relation. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 14-Nov-2013.) |
β’ Rel (βπ‘βπ½) | ||
Theorem | lmrcl 22735 | Reverse closure for the convergence relation. (Contributed by Mario Carneiro, 7-Sep-2015.) |
β’ (πΉ(βπ‘βπ½)π β π½ β Top) | ||
Theorem | lmfval 22736* | 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 22737* | 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 22738* | 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 22739* | 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 22740* | 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 22741* | 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 22742* | 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 22743* | 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 22744 | Reverse closure for a continuous function. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ (πΉ β (π½ Cn πΎ) β π½ β Top) | ||
Theorem | cntop2 22745 | Reverse closure for a continuous function. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ (πΉ β (π½ Cn πΎ) β πΎ β Top) | ||
Theorem | cnptop1 22746 | Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ (πΉ β ((π½ CnP πΎ)βπ) β π½ β Top) | ||
Theorem | cnptop2 22747 | Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ (πΉ β ((π½ CnP πΎ)βπ) β πΎ β Top) | ||
Theorem | iscnp3 22748* | 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 22749 | Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ π = βͺ π½ β β’ (πΉ β ((π½ CnP πΎ)βπ) β π β π) | ||
Theorem | cnf 22750 | A continuous function is a mapping. (Contributed by FL, 8-Dec-2006.) (Revised by Mario Carneiro, 21-Aug-2015.) |
β’ π = βͺ π½ & β’ π = βͺ πΎ β β’ (πΉ β (π½ Cn πΎ) β πΉ:πβΆπ) | ||
Theorem | cnpf 22751 | A continuous function at point π is a mapping. (Contributed by FL, 17-Nov-2006.) (Revised by Mario Carneiro, 21-Aug-2015.) |
β’ π = βͺ π½ & β’ π = βͺ πΎ β β’ (πΉ β ((π½ CnP πΎ)βπ) β πΉ:πβΆπ) | ||
Theorem | cnpcl 22752 | 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 22753 | A continuous function is a mapping. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ πΉ β (π½ Cn πΎ)) β πΉ:πβΆπ) | ||
Theorem | cnpf2 22754 | A continuous function at point π is a mapping. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ πΉ β ((π½ CnP πΎ)βπ)) β πΉ:πβΆπ) | ||
Theorem | cnprcl2 22755 | Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΉ β ((π½ CnP πΎ)βπ)) β π β π) | ||
Theorem | tgcn 22756* | 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 22757* | 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 22758* | 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 22759 | 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 22760* | Property of a function continuous at a point. (Contributed by FL, 31-Dec-2006.) |
β’ ((πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β πΎ β§ (πΉβπ) β π΄) β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π΄)) | ||
Theorem | idcn 22761 | 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 22762* | 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 22733. (Contributed by Mario Carneiro, 14-Nov-2013.) |
β’ (π β π½ β (TopOnβπ)) β β’ (π β (πΉ(βπ‘βπ½)π β (πΉ β (π βpm β) β§ π β π β§ βπ’ β π½ (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’)))) | ||
Theorem | lmbr2 22763* | 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 22764* | Express the binary relation "sequence πΉ converges to point π " in a metric space using an arbitrary upper set of integers. This version of lmbr2 22763 presupposes that πΉ is a function. (Contributed by Mario Carneiro, 14-Nov-2013.) |
β’ (π β π½ β (TopOnβπ)) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆπ) & β’ ((π β§ π β π) β (πΉβπ) = π΄) β β’ (π β (πΉ(βπ‘βπ½)π β (π β π β§ βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)π΄ β π’)))) | ||
Theorem | lmconst 22765 | A constant sequence converges to its value. (Contributed by NM, 8-Nov-2007.) (Revised by Mario Carneiro, 14-Nov-2013.) |
β’ π = (β€β₯βπ) β β’ ((π½ β (TopOnβπ) β§ π β π β§ π β β€) β (π Γ {π})(βπ‘βπ½)π) | ||
Theorem | lmcvg 22766* | Convergence property of a converging sequence. (Contributed by Mario Carneiro, 14-Nov-2013.) |
β’ π = (β€β₯βπ) & β’ (π β π β π) & β’ (π β π β β€) & β’ (π β πΉ(βπ‘βπ½)π) & β’ (π β π β π½) β β’ (π β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π) | ||
Theorem | iscnp4 22767* | 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 22768* | 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 22769 | An open subset of the codomain of a continuous function has an open preimage. (Contributed by FL, 15-Dec-2006.) |
β’ ((πΉ β (π½ Cn πΎ) β§ π΄ β πΎ) β (β‘πΉ β π΄) β π½) | ||
Theorem | cnco 22770 | 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 22771 | 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 22772 | 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 22773* | 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 22774 | Property of the preimage of a closure. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ π = βͺ πΎ β β’ ((πΉ β (π½ Cn πΎ) β§ π β π) β ((clsβπ½)β(β‘πΉ β π)) β (β‘πΉ β ((clsβπΎ)βπ))) | ||
Theorem | cnntri 22775 | Property of the preimage of an interior. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ π = βͺ πΎ β β’ ((πΉ β (π½ Cn πΎ) β§ π β π) β (β‘πΉ β ((intβπΎ)βπ)) β ((intβπ½)β(β‘πΉ β π))) | ||
Theorem | cnclsi 22776 | Property of the image of a closure. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ π = βͺ π½ β β’ ((πΉ β (π½ Cn πΎ) β§ π β π) β (πΉ β ((clsβπ½)βπ)) β ((clsβπΎ)β(πΉ β π))) | ||
Theorem | cncls2 22777* | Continuity in terms of closure. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆπ β§ βπ₯ β π« π((clsβπ½)β(β‘πΉ β π₯)) β (β‘πΉ β ((clsβπΎ)βπ₯))))) | ||
Theorem | cncls 22778* | 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 22779* | 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 22780 | 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 22781 | 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 22782 | 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 22783 | 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 22784* | 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 22785* | 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 22786* | Continuity in terms of neighborhoods. (Contributed by Thierry Arnoux, 3-Jan-2018.) |
β’ π = βͺ π½ & β’ π = βͺ πΎ β β’ ((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β (πΉ β (π½ Cn πΎ) β βπ β π βπ€ β ((neiβπΎ)β{(πΉβπ)})βπ£ β ((neiβπ½)β{π})(πΉ β π£) β π€)) | ||
Theorem | cnconst2 22787 | A constant function is continuous. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΅ β π) β (π Γ {π΅}) β (π½ Cn πΎ)) | ||
Theorem | cnconst 22788 | A constant function is continuous. (Contributed by FL, 15-Jan-2007.) (Proof shortened by Mario Carneiro, 19-Mar-2015.) |
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π΅ β π β§ πΉ:πβΆ{π΅})) β πΉ β (π½ Cn πΎ)) | ||
Theorem | cnrest 22789 | 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 22790 | 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 22791 | 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 22792 | One direction of cnprest 22793 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 22793 | 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 22794 | 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 22795 | 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 22796 | 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 22797 | 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 22798 | 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 22799 | If πΉ converges, then πΉ is a partial function. (Contributed by Mario Carneiro, 23-Dec-2013.) |
β’ ((π½ β (TopOnβπ) β§ πΉ(βπ‘βπ½)π) β πΉ β (π βpm β)) | ||
Theorem | lmfss 22800 | 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βπ) β§ πΉ(βπ‘βπ½)π) β πΉ β (β Γ π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |