![]() |
Metamath
Proof Explorer Theorem List (p. 232 of 484) | < 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-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | restperf 23101 | Perfection of a subspace. Note that the term "perfect set" is reserved for closed sets which are perfect in the subspace topology. (Contributed by Mario Carneiro, 25-Dec-2016.) |
β’ π = βͺ π½ & β’ πΎ = (π½ βΎt π) β β’ ((π½ β Top β§ π β π) β (πΎ β Perf β π β ((limPtβπ½)βπ))) | ||
Theorem | perfopn 23102 | An open subset of a perfect space is perfect. (Contributed by Mario Carneiro, 25-Dec-2016.) |
β’ π = βͺ π½ & β’ πΎ = (π½ βΎt π) β β’ ((π½ β Perf β§ π β π½) β πΎ β Perf) | ||
Theorem | resstopn 23103 | The topology of a restricted structure. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ π» = (πΎ βΎs π΄) & β’ π½ = (TopOpenβπΎ) β β’ (π½ βΎt π΄) = (TopOpenβπ») | ||
Theorem | resstps 23104 | A restricted topological space is a topological space. Note that this theorem would not be true if TopSp was defined directly in terms of the TopSet slot instead of the TopOpen derived function. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ ((πΎ β TopSp β§ π΄ β π) β (πΎ βΎs π΄) β TopSp) | ||
Theorem | ordtbaslem 23105* | Lemma for ordtbas 23109. In a total order, unbounded-above intervals are closed under intersection. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π = dom π & β’ π΄ = ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π π₯}) β β’ (π β TosetRel β (fiβπ΄) = π΄) | ||
Theorem | ordtval 23106* | Value of the order topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π = dom π & β’ π΄ = ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π π₯}) & β’ π΅ = ran (π₯ β π β¦ {π¦ β π β£ Β¬ π₯π π¦}) β β’ (π β π β (ordTopβπ ) = (topGenβ(fiβ({π} βͺ (π΄ βͺ π΅))))) | ||
Theorem | ordtuni 23107* | Value of the order topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π = dom π & β’ π΄ = ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π π₯}) & β’ π΅ = ran (π₯ β π β¦ {π¦ β π β£ Β¬ π₯π π¦}) β β’ (π β π β π = βͺ ({π} βͺ (π΄ βͺ π΅))) | ||
Theorem | ordtbas2 23108* | Lemma for ordtbas 23109. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π = dom π & β’ π΄ = ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π π₯}) & β’ π΅ = ran (π₯ β π β¦ {π¦ β π β£ Β¬ π₯π π¦}) & β’ πΆ = ran (π β π, π β π β¦ {π¦ β π β£ (Β¬ π¦π π β§ Β¬ ππ π¦)}) β β’ (π β TosetRel β (fiβ(π΄ βͺ π΅)) = ((π΄ βͺ π΅) βͺ πΆ)) | ||
Theorem | ordtbas 23109* | In a total order, the finite intersections of the open rays generates the set of open intervals, but no more - these four collections form a subbasis for the order topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π = dom π & β’ π΄ = ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π π₯}) & β’ π΅ = ran (π₯ β π β¦ {π¦ β π β£ Β¬ π₯π π¦}) & β’ πΆ = ran (π β π, π β π β¦ {π¦ β π β£ (Β¬ π¦π π β§ Β¬ ππ π¦)}) β β’ (π β TosetRel β (fiβ({π} βͺ (π΄ βͺ π΅))) = (({π} βͺ (π΄ βͺ π΅)) βͺ πΆ)) | ||
Theorem | ordttopon 23110 | Value of the order topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π = dom π β β’ (π β π β (ordTopβπ ) β (TopOnβπ)) | ||
Theorem | ordtopn1 23111* | An upward ray (π, +β) is open. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π = dom π β β’ ((π β π β§ π β π) β {π₯ β π β£ Β¬ π₯π π} β (ordTopβπ )) | ||
Theorem | ordtopn2 23112* | A downward ray (-β, π) is open. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π = dom π β β’ ((π β π β§ π β π) β {π₯ β π β£ Β¬ ππ π₯} β (ordTopβπ )) | ||
Theorem | ordtopn3 23113* | An open interval (π΄, π΅) is open. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π = dom π β β’ ((π β π β§ π΄ β π β§ π΅ β π) β {π₯ β π β£ (Β¬ π₯π π΄ β§ Β¬ π΅π π₯)} β (ordTopβπ )) | ||
Theorem | ordtcld1 23114* | A downward ray (-β, π] is closed. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π = dom π β β’ ((π β π β§ π β π) β {π₯ β π β£ π₯π π} β (Clsdβ(ordTopβπ ))) | ||
Theorem | ordtcld2 23115* | An upward ray [π, +β) is closed. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π = dom π β β’ ((π β π β§ π β π) β {π₯ β π β£ ππ π₯} β (Clsdβ(ordTopβπ ))) | ||
Theorem | ordtcld3 23116* | A closed interval [π΄, π΅] is closed. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π = dom π β β’ ((π β π β§ π΄ β π β§ π΅ β π) β {π₯ β π β£ (π΄π π₯ β§ π₯π π΅)} β (Clsdβ(ordTopβπ ))) | ||
Theorem | ordttop 23117 | The order topology is a topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ (π β π β (ordTopβπ ) β Top) | ||
Theorem | ordtcnv 23118 | The order dual generates the same topology as the original order. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ (π β PosetRel β (ordTopββ‘π ) = (ordTopβπ )) | ||
Theorem | ordtrest 23119 | 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 23120* | Lemma for ordtrest2 23121. (Contributed by Mario Carneiro, 9-Sep-2015.) |
β’ π = dom π & β’ (π β π β TosetRel ) & β’ (π β π΄ β π) & β’ ((π β§ (π₯ β π΄ β§ π¦ β π΄)) β {π§ β π β£ (π₯π π§ β§ π§π π¦)} β π΄) β β’ (π β βπ£ β ran (π§ β π β¦ {π€ β π β£ Β¬ π€π π§})(π£ β© π΄) β (ordTopβ(π β© (π΄ Γ π΄)))) | ||
Theorem | ordtrest2 23121* | 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 23122 | The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ (ordTopβ β€ ) β (TopOnββ*) | ||
Theorem | letop 23123 | The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ (ordTopβ β€ ) β Top | ||
Theorem | letopuni 23124 | The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ β* = βͺ (ordTopβ β€ ) | ||
Theorem | xrstopn 23125 | The topology component of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ (ordTopβ β€ ) = (TopOpenββ*π ) | ||
Theorem | xrstps 23126 | The extended real number structure is a topological space. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ β*π β TopSp | ||
Theorem | leordtvallem1 23127* | Lemma for leordtval 23130. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π΄ = ran (π₯ β β* β¦ (π₯(,]+β)) β β’ π΄ = ran (π₯ β β* β¦ {π¦ β β* β£ Β¬ π¦ β€ π₯}) | ||
Theorem | leordtvallem2 23128* | Lemma for leordtval 23130. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π΄ = ran (π₯ β β* β¦ (π₯(,]+β)) & β’ π΅ = ran (π₯ β β* β¦ (-β[,)π₯)) β β’ π΅ = ran (π₯ β β* β¦ {π¦ β β* β£ Β¬ π₯ β€ π¦}) | ||
Theorem | leordtval2 23129 | The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π΄ = ran (π₯ β β* β¦ (π₯(,]+β)) & β’ π΅ = ran (π₯ β β* β¦ (-β[,)π₯)) β β’ (ordTopβ β€ ) = (topGenβ(fiβ(π΄ βͺ π΅))) | ||
Theorem | leordtval 23130 | The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π΄ = ran (π₯ β β* β¦ (π₯(,]+β)) & β’ π΅ = ran (π₯ β β* β¦ (-β[,)π₯)) & β’ πΆ = ran (,) β β’ (ordTopβ β€ ) = (topGenβ((π΄ βͺ π΅) βͺ πΆ)) | ||
Theorem | iccordt 23131 | A closed interval is closed in the order topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ (π΄[,]π΅) β (Clsdβ(ordTopβ β€ )) | ||
Theorem | iocpnfordt 23132 | 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 23133 | 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 23134 | An open interval is open in the order topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ (π΄(,)π΅) β (ordTopβ β€ ) | ||
Theorem | reordt 23135 | The real numbers are an open set in the topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ β β (ordTopβ β€ ) | ||
Theorem | lecldbas 23136 | 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 23137* | A neighborhood of +β contains an unbounded interval based at a real number. Together with xrtgioo 24735 (which describes neighborhoods of β) and mnfnei 23138, this gives all "negative" topological information ensuring that it is not too fine (and of course iooordt 23134 and similar ensure that it has all the sets we want). (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ ((π΄ β (ordTopβ β€ ) β§ +β β π΄) β βπ₯ β β (π₯(,]+β) β π΄) | ||
Theorem | mnfnei 23138* | A neighborhood of -β contains an unbounded interval based at a real number. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ ((π΄ β (ordTopβ β€ ) β§ -β β π΄) β βπ₯ β β (-β[,)π₯) β π΄) | ||
Theorem | ordtrestixx 23139* | 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 23140 | 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 23141 | Extend class notation with the class of continuous functions between topologies. |
class Cn | ||
Syntax | ccnp 23142 | Extend class notation with the class of functions between topologies continuous at a given point. |
class CnP | ||
Syntax | clm 23143 | 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 23144* | 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 23152 for the predicate form. (Contributed by NM, 17-Oct-2006.) |
β’ Cn = (π β Top, π β Top β¦ {π β (βͺ π βm βͺ π) β£ βπ¦ β π (β‘π β π¦) β π}) | ||
Definition | df-cnp 23145* | 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 23146* | 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 23147 | The topological space convergence relation is a relation. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 14-Nov-2013.) |
β’ Rel (βπ‘βπ½) | ||
Theorem | lmrcl 23148 | Reverse closure for the convergence relation. (Contributed by Mario Carneiro, 7-Sep-2015.) |
β’ (πΉ(βπ‘βπ½)π β π½ β Top) | ||
Theorem | lmfval 23149* | 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 23150* | 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 23151* | 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 23152* | 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 23153* | 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 23154* | 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 23155* | 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 23156* | 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 23157 | Reverse closure for a continuous function. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ (πΉ β (π½ Cn πΎ) β π½ β Top) | ||
Theorem | cntop2 23158 | Reverse closure for a continuous function. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ (πΉ β (π½ Cn πΎ) β πΎ β Top) | ||
Theorem | cnptop1 23159 | Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ (πΉ β ((π½ CnP πΎ)βπ) β π½ β Top) | ||
Theorem | cnptop2 23160 | Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ (πΉ β ((π½ CnP πΎ)βπ) β πΎ β Top) | ||
Theorem | iscnp3 23161* | 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 23162 | Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ π = βͺ π½ β β’ (πΉ β ((π½ CnP πΎ)βπ) β π β π) | ||
Theorem | cnf 23163 | A continuous function is a mapping. (Contributed by FL, 8-Dec-2006.) (Revised by Mario Carneiro, 21-Aug-2015.) |
β’ π = βͺ π½ & β’ π = βͺ πΎ β β’ (πΉ β (π½ Cn πΎ) β πΉ:πβΆπ) | ||
Theorem | cnpf 23164 | A continuous function at point π is a mapping. (Contributed by FL, 17-Nov-2006.) (Revised by Mario Carneiro, 21-Aug-2015.) |
β’ π = βͺ π½ & β’ π = βͺ πΎ β β’ (πΉ β ((π½ CnP πΎ)βπ) β πΉ:πβΆπ) | ||
Theorem | cnpcl 23165 | 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 23166 | A continuous function is a mapping. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ πΉ β (π½ Cn πΎ)) β πΉ:πβΆπ) | ||
Theorem | cnpf2 23167 | A continuous function at point π is a mapping. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ πΉ β ((π½ CnP πΎ)βπ)) β πΉ:πβΆπ) | ||
Theorem | cnprcl2 23168 | Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΉ β ((π½ CnP πΎ)βπ)) β π β π) | ||
Theorem | tgcn 23169* | 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 23170* | 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 23171* | 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 23172 | 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 23173* | Property of a function continuous at a point. (Contributed by FL, 31-Dec-2006.) |
β’ ((πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β πΎ β§ (πΉβπ) β π΄) β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π΄)) | ||
Theorem | idcn 23174 | 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 23175* | 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 23146. (Contributed by Mario Carneiro, 14-Nov-2013.) |
β’ (π β π½ β (TopOnβπ)) β β’ (π β (πΉ(βπ‘βπ½)π β (πΉ β (π βpm β) β§ π β π β§ βπ’ β π½ (π β π’ β βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆπ’)))) | ||
Theorem | lmbr2 23176* | 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 23177* | Express the binary relation "sequence πΉ converges to point π " in a metric space using an arbitrary upper set of integers. This version of lmbr2 23176 presupposes that πΉ is a function. (Contributed by Mario Carneiro, 14-Nov-2013.) |
β’ (π β π½ β (TopOnβπ)) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ:πβΆπ) & β’ ((π β§ π β π) β (πΉβπ) = π΄) β β’ (π β (πΉ(βπ‘βπ½)π β (π β π β§ βπ’ β π½ (π β π’ β βπ β π βπ β (β€β₯βπ)π΄ β π’)))) | ||
Theorem | lmconst 23178 | A constant sequence converges to its value. (Contributed by NM, 8-Nov-2007.) (Revised by Mario Carneiro, 14-Nov-2013.) |
β’ π = (β€β₯βπ) β β’ ((π½ β (TopOnβπ) β§ π β π β§ π β β€) β (π Γ {π})(βπ‘βπ½)π) | ||
Theorem | lmcvg 23179* | Convergence property of a converging sequence. (Contributed by Mario Carneiro, 14-Nov-2013.) |
β’ π = (β€β₯βπ) & β’ (π β π β π) & β’ (π β π β β€) & β’ (π β πΉ(βπ‘βπ½)π) & β’ (π β π β π½) β β’ (π β βπ β π βπ β (β€β₯βπ)(πΉβπ) β π) | ||
Theorem | iscnp4 23180* | 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 23181* | 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 23182 | An open subset of the codomain of a continuous function has an open preimage. (Contributed by FL, 15-Dec-2006.) |
β’ ((πΉ β (π½ Cn πΎ) β§ π΄ β πΎ) β (β‘πΉ β π΄) β π½) | ||
Theorem | cnco 23183 | 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 23184 | 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 23185 | 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 23186* | 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 23187 | Property of the preimage of a closure. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ π = βͺ πΎ β β’ ((πΉ β (π½ Cn πΎ) β§ π β π) β ((clsβπ½)β(β‘πΉ β π)) β (β‘πΉ β ((clsβπΎ)βπ))) | ||
Theorem | cnntri 23188 | Property of the preimage of an interior. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ π = βͺ πΎ β β’ ((πΉ β (π½ Cn πΎ) β§ π β π) β (β‘πΉ β ((intβπΎ)βπ)) β ((intβπ½)β(β‘πΉ β π))) | ||
Theorem | cnclsi 23189 | Property of the image of a closure. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ π = βͺ π½ β β’ ((πΉ β (π½ Cn πΎ) β§ π β π) β (πΉ β ((clsβπ½)βπ)) β ((clsβπΎ)β(πΉ β π))) | ||
Theorem | cncls2 23190* | Continuity in terms of closure. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆπ β§ βπ₯ β π« π((clsβπ½)β(β‘πΉ β π₯)) β (β‘πΉ β ((clsβπΎ)βπ₯))))) | ||
Theorem | cncls 23191* | 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 23192* | 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 23193 | 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 23194 | 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 23195 | 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 23196 | 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 23197* | 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 23198* | 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 23199* | Continuity in terms of neighborhoods. (Contributed by Thierry Arnoux, 3-Jan-2018.) |
β’ π = βͺ π½ & β’ π = βͺ πΎ β β’ ((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β (πΉ β (π½ Cn πΎ) β βπ β π βπ€ β ((neiβπΎ)β{(πΉβπ)})βπ£ β ((neiβπ½)β{π})(πΉ β π£) β π€)) | ||
Theorem | cnconst2 23200 | A constant function is continuous. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΅ β π) β (π Γ {π΅}) β (π½ Cn πΎ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |