![]() |
Metamath
Proof Explorer Theorem List (p. 227 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 | ||
Syntax | cnei 22601 | Extend class notation with neighborhood relation for topologies. |
class nei | ||
Definition | df-nei 22602* | Define a function on topologies whose value is a map from a subset to its neighborhoods. (Contributed by NM, 11-Feb-2007.) |
β’ nei = (π β Top β¦ (π₯ β π« βͺ π β¦ {π¦ β π« βͺ π β£ βπ β π (π₯ β π β§ π β π¦)})) | ||
Theorem | neifval 22603* | Value of the neighborhood function on the subsets of the base set of a topology. (Contributed by NM, 11-Feb-2007.) (Revised by Mario Carneiro, 11-Nov-2013.) |
β’ π = βͺ π½ β β’ (π½ β Top β (neiβπ½) = (π₯ β π« π β¦ {π£ β π« π β£ βπ β π½ (π₯ β π β§ π β π£)})) | ||
Theorem | neif 22604 | The neighborhood function is a function from the set of the subsets of the base set of a topology. (Contributed by NM, 12-Feb-2007.) (Revised by Mario Carneiro, 11-Nov-2013.) |
β’ π = βͺ π½ β β’ (π½ β Top β (neiβπ½) Fn π« π) | ||
Theorem | neiss2 22605 | A set with a neighborhood is a subset of the base set of a topology. (This theorem depends on a function's value being empty outside of its domain, but it will make later theorems simpler to state.) (Contributed by NM, 12-Feb-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β ((neiβπ½)βπ)) β π β π) | ||
Theorem | neival 22606* | Value of the set of neighborhoods of a subset of the base set of a topology. (Contributed by NM, 11-Feb-2007.) (Revised by Mario Carneiro, 11-Nov-2013.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β ((neiβπ½)βπ) = {π£ β π« π β£ βπ β π½ (π β π β§ π β π£)}) | ||
Theorem | isnei 22607* | The predicate "the class π is a neighborhood of π". (Contributed by FL, 25-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β (π β ((neiβπ½)βπ) β (π β π β§ βπ β π½ (π β π β§ π β π)))) | ||
Theorem | neiint 22608 | An intuitive definition of a neighborhood in terms of interior. (Contributed by Szymon Jaroszewicz, 18-Dec-2007.) (Revised by Mario Carneiro, 11-Nov-2013.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π β§ π β π) β (π β ((neiβπ½)βπ) β π β ((intβπ½)βπ))) | ||
Theorem | isneip 22609* | The predicate "the class π is a neighborhood of point π". (Contributed by NM, 26-Feb-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β (π β ((neiβπ½)β{π}) β (π β π β§ βπ β π½ (π β π β§ π β π)))) | ||
Theorem | neii1 22610 | A neighborhood is included in the topology's base set. (Contributed by NM, 12-Feb-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β ((neiβπ½)βπ)) β π β π) | ||
Theorem | neisspw 22611 | The neighborhoods of any set are subsets of the base set. (Contributed by Stefan O'Rear, 6-Aug-2015.) |
β’ π = βͺ π½ β β’ (π½ β Top β ((neiβπ½)βπ) β π« π) | ||
Theorem | neii2 22612* | Property of a neighborhood. (Contributed by NM, 12-Feb-2007.) |
β’ ((π½ β Top β§ π β ((neiβπ½)βπ)) β βπ β π½ (π β π β§ π β π)) | ||
Theorem | neiss 22613 | Any neighborhood of a set π is also a neighborhood of any subset π β π. Similar to Proposition 1 of [BourbakiTop1] p. I.2. (Contributed by FL, 25-Sep-2006.) |
β’ ((π½ β Top β§ π β ((neiβπ½)βπ) β§ π β π) β π β ((neiβπ½)βπ )) | ||
Theorem | ssnei 22614 | A set is included in any of its neighborhoods. Generalization to subsets of elnei 22615. (Contributed by FL, 16-Nov-2006.) |
β’ ((π½ β Top β§ π β ((neiβπ½)βπ)) β π β π) | ||
Theorem | elnei 22615 | A point belongs to any of its neighborhoods. Property Viii of [BourbakiTop1] p. I.3. (Contributed by FL, 28-Sep-2006.) |
β’ ((π½ β Top β§ π β π΄ β§ π β ((neiβπ½)β{π})) β π β π) | ||
Theorem | 0nnei 22616 | The empty set is not a neighborhood of a nonempty set. (Contributed by FL, 18-Sep-2007.) |
β’ ((π½ β Top β§ π β β ) β Β¬ β β ((neiβπ½)βπ)) | ||
Theorem | neips 22617* | A neighborhood of a set is a neighborhood of every point in the set. Proposition 1 of [BourbakiTop1] p. I.2. (Contributed by FL, 16-Nov-2006.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π β§ π β β ) β (π β ((neiβπ½)βπ) β βπ β π π β ((neiβπ½)β{π}))) | ||
Theorem | opnneissb 22618 | An open set is a neighborhood of any of its subsets. (Contributed by FL, 2-Oct-2006.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π½ β§ π β π) β (π β π β π β ((neiβπ½)βπ))) | ||
Theorem | opnssneib 22619 | Any superset of an open set is a neighborhood of it. (Contributed by NM, 14-Feb-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π½ β§ π β π) β (π β π β π β ((neiβπ½)βπ))) | ||
Theorem | ssnei2 22620 | Any subset π of π containing a neighborhood π of a set π is a neighborhood of this set. Generalization to subsets of Property Vi of [BourbakiTop1] p. I.3. (Contributed by FL, 2-Oct-2006.) |
β’ π = βͺ π½ β β’ (((π½ β Top β§ π β ((neiβπ½)βπ)) β§ (π β π β§ π β π)) β π β ((neiβπ½)βπ)) | ||
Theorem | neindisj 22621 | Any neighborhood of an element in the closure of a subset intersects the subset. Part of proof of Theorem 6.6 of [Munkres] p. 97. (Contributed by NM, 26-Feb-2007.) |
β’ π = βͺ π½ β β’ (((π½ β Top β§ π β π) β§ (π β ((clsβπ½)βπ) β§ π β ((neiβπ½)β{π}))) β (π β© π) β β ) | ||
Theorem | opnneiss 22622 | An open set is a neighborhood of any of its subsets. (Contributed by NM, 13-Feb-2007.) |
β’ ((π½ β Top β§ π β π½ β§ π β π) β π β ((neiβπ½)βπ)) | ||
Theorem | opnneip 22623 | An open set is a neighborhood of any of its members. (Contributed by NM, 8-Mar-2007.) |
β’ ((π½ β Top β§ π β π½ β§ π β π) β π β ((neiβπ½)β{π})) | ||
Theorem | opnnei 22624* | A set is open iff it is a neighborhood of all of its points. (Contributed by Jeff Hankins, 15-Sep-2009.) |
β’ (π½ β Top β (π β π½ β βπ₯ β π π β ((neiβπ½)β{π₯}))) | ||
Theorem | tpnei 22625 | The underlying set of a topology is a neighborhood of any of its subsets. Special case of opnneiss 22622. (Contributed by FL, 2-Oct-2006.) |
β’ π = βͺ π½ β β’ (π½ β Top β (π β π β π β ((neiβπ½)βπ))) | ||
Theorem | neiuni 22626 | The union of the neighborhoods of a set equals the topology's underlying set. (Contributed by FL, 18-Sep-2007.) (Revised by Mario Carneiro, 9-Apr-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β π = βͺ ((neiβπ½)βπ)) | ||
Theorem | neindisj2 22627* | A point π belongs to the closure of a set π iff every neighborhood of π meets π. (Contributed by FL, 15-Sep-2013.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π β§ π β π) β (π β ((clsβπ½)βπ) β βπ β ((neiβπ½)β{π})(π β© π) β β )) | ||
Theorem | topssnei 22628 | A finer topology has more neighborhoods. (Contributed by Mario Carneiro, 9-Apr-2015.) |
β’ π = βͺ π½ & β’ π = βͺ πΎ β β’ (((π½ β Top β§ πΎ β Top β§ π = π) β§ π½ β πΎ) β ((neiβπ½)βπ) β ((neiβπΎ)βπ)) | ||
Theorem | innei 22629 | The intersection of two neighborhoods of a set is also a neighborhood of the set. Generalization to subsets of Property Vii of [BourbakiTop1] p. I.3 for binary intersections. (Contributed by FL, 28-Sep-2006.) |
β’ ((π½ β Top β§ π β ((neiβπ½)βπ) β§ π β ((neiβπ½)βπ)) β (π β© π) β ((neiβπ½)βπ)) | ||
Theorem | opnneiid 22630 | Only an open set is a neighborhood of itself. (Contributed by FL, 2-Oct-2006.) |
β’ (π½ β Top β (π β ((neiβπ½)βπ) β π β π½)) | ||
Theorem | neissex 22631* | For any neighborhood π of π, there is a neighborhood π₯ of π such that π is a neighborhood of all subsets of π₯. Generalization to subsets of Property Viv of [BourbakiTop1] p. I.3. (Contributed by FL, 2-Oct-2006.) |
β’ ((π½ β Top β§ π β ((neiβπ½)βπ)) β βπ₯ β ((neiβπ½)βπ)βπ¦(π¦ β π₯ β π β ((neiβπ½)βπ¦))) | ||
Theorem | 0nei 22632 | The empty set is a neighborhood of itself. (Contributed by FL, 10-Dec-2006.) |
β’ (π½ β Top β β β ((neiβπ½)ββ )) | ||
Theorem | neipeltop 22633* | Lemma for neiptopreu 22637. (Contributed by Thierry Arnoux, 6-Jan-2018.) |
β’ π½ = {π β π« π β£ βπ β π π β (πβπ)} β β’ (πΆ β π½ β (πΆ β π β§ βπ β πΆ πΆ β (πβπ))) | ||
Theorem | neiptopuni 22634* | Lemma for neiptopreu 22637. (Contributed by Thierry Arnoux, 6-Jan-2018.) |
β’ π½ = {π β π« π β£ βπ β π π β (πβπ)} & β’ (π β π:πβΆπ« π« π) & β’ ((((π β§ π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β π β (πβπ)) & β’ ((π β§ π β π) β (fiβ(πβπ)) β (πβπ)) & β’ (((π β§ π β π) β§ π β (πβπ)) β π β π) & β’ (((π β§ π β π) β§ π β (πβπ)) β βπ β (πβπ)βπ β π π β (πβπ)) & β’ ((π β§ π β π) β π β (πβπ)) β β’ (π β π = βͺ π½) | ||
Theorem | neiptoptop 22635* | Lemma for neiptopreu 22637. (Contributed by Thierry Arnoux, 7-Jan-2018.) |
β’ π½ = {π β π« π β£ βπ β π π β (πβπ)} & β’ (π β π:πβΆπ« π« π) & β’ ((((π β§ π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β π β (πβπ)) & β’ ((π β§ π β π) β (fiβ(πβπ)) β (πβπ)) & β’ (((π β§ π β π) β§ π β (πβπ)) β π β π) & β’ (((π β§ π β π) β§ π β (πβπ)) β βπ β (πβπ)βπ β π π β (πβπ)) & β’ ((π β§ π β π) β π β (πβπ)) β β’ (π β π½ β Top) | ||
Theorem | neiptopnei 22636* | Lemma for neiptopreu 22637. (Contributed by Thierry Arnoux, 7-Jan-2018.) |
β’ π½ = {π β π« π β£ βπ β π π β (πβπ)} & β’ (π β π:πβΆπ« π« π) & β’ ((((π β§ π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β π β (πβπ)) & β’ ((π β§ π β π) β (fiβ(πβπ)) β (πβπ)) & β’ (((π β§ π β π) β§ π β (πβπ)) β π β π) & β’ (((π β§ π β π) β§ π β (πβπ)) β βπ β (πβπ)βπ β π π β (πβπ)) & β’ ((π β§ π β π) β π β (πβπ)) β β’ (π β π = (π β π β¦ ((neiβπ½)β{π}))) | ||
Theorem | neiptopreu 22637* | If, to each element π of a set π, we associate a set (πβπ) fulfilling Properties Vi, Vii, Viii and Property Viv of [BourbakiTop1] p. I.2. , corresponding to ssnei 22614, innei 22629, elnei 22615 and neissex 22631, then there is a unique topology π such that for any point π, (πβπ) is the set of neighborhoods of π. Proposition 2 of [BourbakiTop1] p. I.3. This can be used to build a topology from a set of neighborhoods. Note that innei 22629 uses binary intersections whereas Property Vii mentions finite intersections (which includes the empty intersection of subsets of π, which is equal to π), so we add the hypothesis that π is a neighborhood of all points. TODO: when df-fi 9406 includes the empty intersection, remove that extra hypothesis. (Contributed by Thierry Arnoux, 6-Jan-2018.) |
β’ π½ = {π β π« π β£ βπ β π π β (πβπ)} & β’ (π β π:πβΆπ« π« π) & β’ ((((π β§ π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β π β (πβπ)) & β’ ((π β§ π β π) β (fiβ(πβπ)) β (πβπ)) & β’ (((π β§ π β π) β§ π β (πβπ)) β π β π) & β’ (((π β§ π β π) β§ π β (πβπ)) β βπ β (πβπ)βπ β π π β (πβπ)) & β’ ((π β§ π β π) β π β (πβπ)) β β’ (π β β!π β (TopOnβπ)π = (π β π β¦ ((neiβπ)β{π}))) | ||
Syntax | clp 22638 | Extend class notation with the limit point function for topologies. |
class limPt | ||
Syntax | cperf 22639 | Extend class notation with the class of all perfect spaces. |
class Perf | ||
Definition | df-lp 22640* | Define a function on topologies whose value is the set of limit points of the subsets of the base set. See lpval 22643. (Contributed by NM, 10-Feb-2007.) |
β’ limPt = (π β Top β¦ (π₯ β π« βͺ π β¦ {π¦ β£ π¦ β ((clsβπ)β(π₯ β {π¦}))})) | ||
Definition | df-perf 22641 | Define the class of all perfect spaces. A perfect space is one for which every point in the set is a limit point of the whole space. (Contributed by Mario Carneiro, 24-Dec-2016.) |
β’ Perf = {π β Top β£ ((limPtβπ)ββͺ π) = βͺ π} | ||
Theorem | lpfval 22642* | The limit point function on the subsets of a topology's base set. (Contributed by NM, 10-Feb-2007.) (Revised by Mario Carneiro, 11-Nov-2013.) |
β’ π = βͺ π½ β β’ (π½ β Top β (limPtβπ½) = (π₯ β π« π β¦ {π¦ β£ π¦ β ((clsβπ½)β(π₯ β {π¦}))})) | ||
Theorem | lpval 22643* | The set of limit points of a subset of the base set of a topology. Alternate definition of limit point in [Munkres] p. 97. (Contributed by NM, 10-Feb-2007.) (Revised by Mario Carneiro, 11-Nov-2013.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β ((limPtβπ½)βπ) = {π₯ β£ π₯ β ((clsβπ½)β(π β {π₯}))}) | ||
Theorem | islp 22644 | The predicate "the class π is a limit point of π". (Contributed by NM, 10-Feb-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β (π β ((limPtβπ½)βπ) β π β ((clsβπ½)β(π β {π})))) | ||
Theorem | lpsscls 22645 | The limit points of a subset are included in the subset's closure. (Contributed by NM, 26-Feb-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β ((limPtβπ½)βπ) β ((clsβπ½)βπ)) | ||
Theorem | lpss 22646 | The limit points of a subset are included in the base set. (Contributed by NM, 9-Nov-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β ((limPtβπ½)βπ) β π) | ||
Theorem | lpdifsn 22647 | π is a limit point of π iff it is a limit point of π β {π}. (Contributed by Mario Carneiro, 25-Dec-2016.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β (π β ((limPtβπ½)βπ) β π β ((limPtβπ½)β(π β {π})))) | ||
Theorem | lpss3 22648 | Subset relationship for limit points. (Contributed by Mario Carneiro, 25-Dec-2016.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π β§ π β π) β ((limPtβπ½)βπ) β ((limPtβπ½)βπ)) | ||
Theorem | islp2 22649* | The predicate "π is a limit point of π " in terms of neighborhoods. Definition of limit point in [Munkres] p. 97. Although Munkres uses open neighborhoods, it also works for our more general neighborhoods. (Contributed by NM, 26-Feb-2007.) (Proof shortened by Mario Carneiro, 25-Dec-2016.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π β§ π β π) β (π β ((limPtβπ½)βπ) β βπ β ((neiβπ½)β{π})(π β© (π β {π})) β β )) | ||
Theorem | islp3 22650* | The predicate "π is a limit point of π " in terms of open sets. see islp2 22649, elcls 22577, islp 22644. (Contributed by FL, 31-Jul-2009.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π β§ π β π) β (π β ((limPtβπ½)βπ) β βπ₯ β π½ (π β π₯ β (π₯ β© (π β {π})) β β ))) | ||
Theorem | maxlp 22651 | A point is a limit point of the whole space iff the singleton of the point is not open. (Contributed by Mario Carneiro, 24-Dec-2016.) |
β’ π = βͺ π½ β β’ (π½ β Top β (π β ((limPtβπ½)βπ) β (π β π β§ Β¬ {π} β π½))) | ||
Theorem | clslp 22652 | The closure of a subset of a topological space is the subset together with its limit points. Theorem 6.6 of [Munkres] p. 97. (Contributed by NM, 26-Feb-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β ((clsβπ½)βπ) = (π βͺ ((limPtβπ½)βπ))) | ||
Theorem | islpi 22653 | A point belonging to a set's closure but not the set itself is a limit point. (Contributed by NM, 8-Nov-2007.) |
β’ π = βͺ π½ β β’ (((π½ β Top β§ π β π) β§ (π β ((clsβπ½)βπ) β§ Β¬ π β π)) β π β ((limPtβπ½)βπ)) | ||
Theorem | cldlp 22654 | A subset of a topological space is closed iff it contains all its limit points. Corollary 6.7 of [Munkres] p. 97. (Contributed by NM, 26-Feb-2007.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β (π β (Clsdβπ½) β ((limPtβπ½)βπ) β π)) | ||
Theorem | isperf 22655 | Definition of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016.) |
β’ π = βͺ π½ β β’ (π½ β Perf β (π½ β Top β§ ((limPtβπ½)βπ) = π)) | ||
Theorem | isperf2 22656 | Definition of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016.) |
β’ π = βͺ π½ β β’ (π½ β Perf β (π½ β Top β§ π β ((limPtβπ½)βπ))) | ||
Theorem | isperf3 22657* | A perfect space is a topology which has no open singletons. (Contributed by Mario Carneiro, 24-Dec-2016.) |
β’ π = βͺ π½ β β’ (π½ β Perf β (π½ β Top β§ βπ₯ β π Β¬ {π₯} β π½)) | ||
Theorem | perflp 22658 | The limit points of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016.) |
β’ π = βͺ π½ β β’ (π½ β Perf β ((limPtβπ½)βπ) = π) | ||
Theorem | perfi 22659 | Property of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016.) |
β’ π = βͺ π½ β β’ ((π½ β Perf β§ π β π) β Β¬ {π} β π½) | ||
Theorem | perftop 22660 | A perfect space is a topology. (Contributed by Mario Carneiro, 25-Dec-2016.) |
β’ (π½ β Perf β π½ β Top) | ||
Theorem | restrcl 22661 | Reverse closure for the subspace topology. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 1-May-2015.) |
β’ ((π½ βΎt π΄) β Top β (π½ β V β§ π΄ β V)) | ||
Theorem | restbas 22662 | A subspace topology basis is a basis. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ (π΅ β TopBases β (π΅ βΎt π΄) β TopBases) | ||
Theorem | tgrest 22663 | A subspace can be generated by restricted sets from a basis for the original topology. (Contributed by Mario Carneiro, 19-Mar-2015.) (Proof shortened by Mario Carneiro, 30-Aug-2015.) |
β’ ((π΅ β π β§ π΄ β π) β (topGenβ(π΅ βΎt π΄)) = ((topGenβπ΅) βΎt π΄)) | ||
Theorem | resttop 22664 | A subspace topology is a topology. Definition of subspace topology in [Munkres] p. 89. π΄ is normally a subset of the base set of π½. (Contributed by FL, 15-Apr-2007.) (Revised by Mario Carneiro, 1-May-2015.) |
β’ ((π½ β Top β§ π΄ β π) β (π½ βΎt π΄) β Top) | ||
Theorem | resttopon 22665 | A subspace topology is a topology on the base set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β (π½ βΎt π΄) β (TopOnβπ΄)) | ||
Theorem | restuni 22666 | The underlying set of a subspace topology. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 13-Aug-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π) β π΄ = βͺ (π½ βΎt π΄)) | ||
Theorem | stoig 22667 | The topological space built with a subspace topology. (Contributed by FL, 5-Jan-2009.) (Proof shortened by Mario Carneiro, 1-May-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π) β {β¨(Baseβndx), π΄β©, β¨(TopSetβndx), (π½ βΎt π΄)β©} β TopSp) | ||
Theorem | restco 22668 | Composition of subspaces. (Contributed by Mario Carneiro, 15-Dec-2013.) (Revised by Mario Carneiro, 1-May-2015.) |
β’ ((π½ β π β§ π΄ β π β§ π΅ β π) β ((π½ βΎt π΄) βΎt π΅) = (π½ βΎt (π΄ β© π΅))) | ||
Theorem | restabs 22669 | Equivalence of being a subspace of a subspace and being a subspace of the original. (Contributed by Jeff Hankins, 11-Jul-2009.) (Proof shortened by Mario Carneiro, 1-May-2015.) |
β’ ((π½ β π β§ π β π β§ π β π) β ((π½ βΎt π) βΎt π) = (π½ βΎt π)) | ||
Theorem | restin 22670 | When the subspace region is not a subset of the base of the topology, the resulting set is the same as the subspace restricted to the base. (Contributed by Mario Carneiro, 15-Dec-2013.) |
β’ π = βͺ π½ β β’ ((π½ β π β§ π΄ β π) β (π½ βΎt π΄) = (π½ βΎt (π΄ β© π))) | ||
Theorem | restuni2 22671 | The underlying set of a subspace topology. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π) β (π΄ β© π) = βͺ (π½ βΎt π΄)) | ||
Theorem | resttopon2 22672 | The underlying set of a subspace topology. (Contributed by Mario Carneiro, 13-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β (π½ βΎt π΄) β (TopOnβ(π΄ β© π))) | ||
Theorem | rest0 22673 | The subspace topology induced by the topology π½ on the empty set. (Contributed by FL, 22-Dec-2008.) (Revised by Mario Carneiro, 1-May-2015.) |
β’ (π½ β Top β (π½ βΎt β ) = {β }) | ||
Theorem | restsn 22674 | The only subspace topology induced by the topology {β }. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) |
β’ (π΄ β π β ({β } βΎt π΄) = {β }) | ||
Theorem | restsn2 22675 | The subspace topology induced by a singleton. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 16-Sep-2015.) |
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β (π½ βΎt {π΄}) = π« {π΄}) | ||
Theorem | restcld 22676* | A closed set of a subspace topology is a closed set of the original topology intersected with the subset. (Contributed by FL, 11-Jul-2009.) (Proof shortened by Mario Carneiro, 15-Dec-2013.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π β π) β (π΄ β (Clsdβ(π½ βΎt π)) β βπ₯ β (Clsdβπ½)π΄ = (π₯ β© π))) | ||
Theorem | restcldi 22677 | A closed set is closed in the subspace topology. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ π = βͺ π½ β β’ ((π΄ β π β§ π΅ β (Clsdβπ½) β§ π΅ β π΄) β π΅ β (Clsdβ(π½ βΎt π΄))) | ||
Theorem | restcldr 22678 | A set which is closed in the subspace topology induced by a closed set is closed in the original topology. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ ((π΄ β (Clsdβπ½) β§ π΅ β (Clsdβ(π½ βΎt π΄))) β π΅ β (Clsdβπ½)) | ||
Theorem | restopnb 22679 | If π΅ is an open subset of the subspace base set π΄, then any subset of π΅ is open iff it is open in π΄. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ (((π½ β Top β§ π΄ β π) β§ (π΅ β π½ β§ π΅ β π΄ β§ πΆ β π΅)) β (πΆ β π½ β πΆ β (π½ βΎt π΄))) | ||
Theorem | ssrest 22680 | If πΎ is a finer topology than π½, then the subspace topologies induced by π΄ maintain this relationship. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 1-May-2015.) |
β’ ((πΎ β π β§ π½ β πΎ) β (π½ βΎt π΄) β (πΎ βΎt π΄)) | ||
Theorem | restopn2 22681 | If π΄ is open, then π΅ is open in π΄ iff it is an open subset of π΄. (Contributed by Mario Carneiro, 2-Mar-2015.) |
β’ ((π½ β Top β§ π΄ β π½) β (π΅ β (π½ βΎt π΄) β (π΅ β π½ β§ π΅ β π΄))) | ||
Theorem | restdis 22682 | A subspace of a discrete topology is discrete. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ ((π΄ β π β§ π΅ β π΄) β (π« π΄ βΎt π΅) = π« π΅) | ||
Theorem | restfpw 22683 | The restriction of the set of finite subsets of π΄ is the set of finite subsets of π΅. (Contributed by Mario Carneiro, 18-Sep-2015.) |
β’ ((π΄ β π β§ π΅ β π΄) β ((π« π΄ β© Fin) βΎt π΅) = (π« π΅ β© Fin)) | ||
Theorem | neitr 22684 | The neighborhood of a trace is the trace of the neighborhood. (Contributed by Thierry Arnoux, 17-Jan-2018.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ π΄ β π β§ π΅ β π΄) β ((neiβ(π½ βΎt π΄))βπ΅) = (((neiβπ½)βπ΅) βΎt π΄)) | ||
Theorem | restcls 22685 | A closure in a subspace topology. (Contributed by Jeff Hankins, 22-Jan-2010.) (Revised by Mario Carneiro, 15-Dec-2013.) |
β’ π = βͺ π½ & β’ πΎ = (π½ βΎt π) β β’ ((π½ β Top β§ π β π β§ π β π) β ((clsβπΎ)βπ) = (((clsβπ½)βπ) β© π)) | ||
Theorem | restntr 22686 | An interior in a subspace topology. Willard in General Topology says that there is no analogue of restcls 22685 for interiors. In some sense, that is true. (Contributed by Jeff Hankins, 23-Jan-2010.) (Revised by Mario Carneiro, 15-Dec-2013.) |
β’ π = βͺ π½ & β’ πΎ = (π½ βΎt π) β β’ ((π½ β Top β§ π β π β§ π β π) β ((intβπΎ)βπ) = (((intβπ½)β(π βͺ (π β π))) β© π)) | ||
Theorem | restlp 22687 | The limit points of a subset restrict naturally in a subspace. (Contributed by Mario Carneiro, 25-Dec-2016.) |
β’ π = βͺ π½ & β’ πΎ = (π½ βΎt π) β β’ ((π½ β Top β§ π β π β§ π β π) β ((limPtβπΎ)βπ) = (((limPtβπ½)βπ) β© π)) | ||
Theorem | restperf 22688 | 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 22689 | An open subset of a perfect space is perfect. (Contributed by Mario Carneiro, 25-Dec-2016.) |
β’ π = βͺ π½ & β’ πΎ = (π½ βΎt π) β β’ ((π½ β Perf β§ π β π½) β πΎ β Perf) | ||
Theorem | resstopn 22690 | The topology of a restricted structure. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ π» = (πΎ βΎs π΄) & β’ π½ = (TopOpenβπΎ) β β’ (π½ βΎt π΄) = (TopOpenβπ») | ||
Theorem | resstps 22691 | 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 22692* | Lemma for ordtbas 22696. In a total order, unbounded-above intervals are closed under intersection. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π = dom π & β’ π΄ = ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π π₯}) β β’ (π β TosetRel β (fiβπ΄) = π΄) | ||
Theorem | ordtval 22693* | Value of the order topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π = dom π & β’ π΄ = ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π π₯}) & β’ π΅ = ran (π₯ β π β¦ {π¦ β π β£ Β¬ π₯π π¦}) β β’ (π β π β (ordTopβπ ) = (topGenβ(fiβ({π} βͺ (π΄ βͺ π΅))))) | ||
Theorem | ordtuni 22694* | Value of the order topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π = dom π & β’ π΄ = ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π π₯}) & β’ π΅ = ran (π₯ β π β¦ {π¦ β π β£ Β¬ π₯π π¦}) β β’ (π β π β π = βͺ ({π} βͺ (π΄ βͺ π΅))) | ||
Theorem | ordtbas2 22695* | Lemma for ordtbas 22696. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π = dom π & β’ π΄ = ran (π₯ β π β¦ {π¦ β π β£ Β¬ π¦π π₯}) & β’ π΅ = ran (π₯ β π β¦ {π¦ β π β£ Β¬ π₯π π¦}) & β’ πΆ = ran (π β π, π β π β¦ {π¦ β π β£ (Β¬ π¦π π β§ Β¬ ππ π¦)}) β β’ (π β TosetRel β (fiβ(π΄ βͺ π΅)) = ((π΄ βͺ π΅) βͺ πΆ)) | ||
Theorem | ordtbas 22696* | 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 22697 | Value of the order topology. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π = dom π β β’ (π β π β (ordTopβπ ) β (TopOnβπ)) | ||
Theorem | ordtopn1 22698* | An upward ray (π, +β) is open. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π = dom π β β’ ((π β π β§ π β π) β {π₯ β π β£ Β¬ π₯π π} β (ordTopβπ )) | ||
Theorem | ordtopn2 22699* | A downward ray (-β, π) is open. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π = dom π β β’ ((π β π β§ π β π) β {π₯ β π β£ Β¬ ππ π₯} β (ordTopβπ )) | ||
Theorem | ordtopn3 22700* | An open interval (π΄, π΅) is open. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π = dom π β β’ ((π β π β§ π΄ β π β§ π΅ β π) β {π₯ β π β£ (Β¬ π₯π π΄ β§ Β¬ π΅π π₯)} β (ordTopβπ )) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |