P. 202 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 20101-20200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	isclo 20101*	A set A is clopen iff for every point x in the space there is a neighborhood y such that all the points in y are in A iff x is. (Contributed by Mario Carneiro, 10-Mar-2015.)
|- X = U. J   =>    |- ( ( J e. Top /\ A C_ X ) -> ( A e. ( J i^i ( Clsd ` J ) ) <-> A. x e. X E. y e. J ( x e. y /\ A. z e. y ( x e. A <-> z e. A ) ) ) )
Theorem	isclo2 20102*	A set A is clopen iff for every point x in the space there is a neighborhood y of x which is either disjoint from A or contained in A. (Contributed by Mario Carneiro, 7-Jul-2015.)
|- X = U. J   =>    |- ( ( J e. Top /\ A C_ X ) -> ( A e. ( J i^i ( Clsd ` J ) ) <-> A. x e. X E. y e. J ( x e. y /\ A. z e. y ( z e. A -> y C_ A ) ) ) )
Theorem	discld 20103	The open sets of a discrete topology are closed and its closed sets are open. (Contributed by FL, 7-Jun-2007.) (Revised by Mario Carneiro, 7-Apr-2015.)
|- ( A e. V -> ( Clsd ` ~P A ) = ~P A )
Theorem	sn0cld 20104	The closed sets of the topology { (/) }. (Contributed by FL, 5-Jan-2009.)
|- ( Clsd ` { (/) } ) = { (/) }
Theorem	indiscld 20105	The closed sets of an indiscrete topology. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- ( Clsd ` { (/) , A } ) = { (/) , A }
Theorem	mretopd 20106*	A Moore collection which is closed under finite unions called topological; such a collection is the closed sets of a canonically associated topology. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- ( ph -> M e. (Moore ` B ) )   &    |- ( ph -> (/) e. M )   &    |- ( ( ph /\ x e. M /\ y e. M ) -> ( x u. y ) e. M )   &    |- J = { z e. ~P B | ( B \ z ) e. M }   =>    |- ( ph -> ( J e. (TopOn ` B ) /\ M = ( Clsd ` J ) ) )
Theorem	toponmre 20107	The topologies over a given base set form a Moore collection: the intersection of any family of them is a topology, including the empty (relative) intersection which gives the discrete topology distop 20009. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by Mario Carneiro, 5-May-2015.)
|- ( B e. V -> (TopOn ` B ) e. (Moore ` ~P B ) )
Theorem	cldmreon 20108	The closed sets of a topology over a set are a Moore collection over the same set. (Contributed by Stefan O'Rear, 31-Jan-2015.)
|- ( J e. (TopOn ` B ) -> ( Clsd ` J ) e. (Moore ` B ) )
Theorem	iscldtop 20109*	A family is the closed sets of a topology iff it is a Moore collection and closed under finite union. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- ( K e. ( Clsd " (TopOn ` B ) ) <-> ( K e. (Moore ` B ) /\ (/) e. K /\ A. x e. K A. y e. K ( x u. y ) e. K ) )
Theorem	mreclatdemoBAD 20110	The closed subspaces of a topology-bearing module form a complete lattice. Demonstration for mreclatBAD 16432. (Contributed by Stefan O'Rear, 31-Jan-2015.) TODO (df-riota 6267 update): This proof uses the old df-clat 16353 and references the required instance of mreclatBAD 16432 as a hypothesis. When mreclatBAD 16432 is corrected to become mreclat, delete this theorem and uncomment the mreclatdemo below.
|- ( ( ( LSubSp ` W ) i^i ( Clsd ` ( TopOpen ` W ) ) ) e. (Moore ` U. ( TopOpen ` W ) ) -> (toInc ` ( ( LSubSp ` W ) i^i ( Clsd ` ( TopOpen ` W ) ) ) ) e. CLat )   =>    |- ( W e. ( TopSp i^i LMod ) -> (toInc ` ( ( LSubSp ` W ) i^i ( Clsd ` ( TopOpen ` W ) ) ) ) e. CLat )
12.1.5  Neighborhoods
Syntax	cnei 20111	Extend class notation with neighborhood relation for topologies.
class nei
Definition	df-nei 20112*	Define a function on topologies whose value is a map from a subset to its neighborhoods. (Contributed by NM, 11-Feb-2007.)
|- nei = ( j e. Top |-> ( x e. ~P U. j |-> { y e. ~P U. j | E. g e. j ( x C_ g /\ g C_ y ) } ) )
Theorem	neifval 20113*	The neighborhood function on the subsets of a topology's base set. (Contributed by NM, 11-Feb-2007.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- X = U. J   =>    |- ( J e. Top -> ( nei ` J ) = ( x e. ~P X |-> { v e. ~P X | E. g e. J ( x C_ g /\ g C_ v ) } ) )
Theorem	neif 20114	The neighborhood function is a function of the subsets of a topology's base set. (Contributed by NM, 12-Feb-2007.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- X = U. J   =>    |- ( J e. Top -> ( nei ` J ) Fn ~P X )
Theorem	neiss2 20115	A set with a neighborhood is a subset of the topology's base set. (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.)
|- X = U. J   =>    |- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> S C_ X )
Theorem	neival 20116*	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.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( ( nei ` J ) ` S ) = { v e. ~P X | E. g e. J ( S C_ g /\ g C_ v ) } )
Theorem	isnei 20117*	The predicate " N is a neighborhood of S." (Contributed by FL, 25-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( N e. ( ( nei ` J ) ` S ) <-> ( N C_ X /\ E. g e. J ( S C_ g /\ g C_ N ) ) ) )
Theorem	neiint 20118	An intuitive definition of a neighborhood in terms of interior. (Contributed by Szymon Jaroszewicz, 18-Dec-2007.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X /\ N C_ X ) -> ( N e. ( ( nei ` J ) ` S ) <-> S C_ ( ( int ` J ) ` N ) ) )
Theorem	isneip 20119*	The predicate " N is a neighborhood of point P." (Contributed by NM, 26-Feb-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ P e. X ) -> ( N e. ( ( nei ` J ) ` { P } ) <-> ( N C_ X /\ E. g e. J ( P e. g /\ g C_ N ) ) ) )
Theorem	neii1 20120	A neighborhood is included in the topology's base set. (Contributed by NM, 12-Feb-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> N C_ X )
Theorem	neisspw 20121	The neighborhoods of any set are subsets of the base set. (Contributed by Stefan O'Rear, 6-Aug-2015.)
|- X = U. J   =>    |- ( J e. Top -> ( ( nei ` J ) ` S ) C_ ~P X )
Theorem	neii2 20122*	Property of a neighborhood. (Contributed by NM, 12-Feb-2007.)
|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> E. g e. J ( S C_ g /\ g C_ N ) )
Theorem	neiss 20123	Any neighborhood of a set S is also a neighborhood of any subset R C_ S. Theorem of [BourbakiTop1] p. I.2. (Contributed by FL, 25-Sep-2006.)
|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ R C_ S ) -> N e. ( ( nei ` J ) ` R ) )
Theorem	ssnei 20124	A set is included in its neighborhoods. Proposition Viii of [BourbakiTop1] p. I.3 . (Contributed by FL, 16-Nov-2006.)
|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> S C_ N )
Theorem	elnei 20125	A point belongs to any of its neighborhoods. Proposition Viii of [BourbakiTop1] p. I.3. (Contributed by FL, 28-Sep-2006.)
|- ( ( J e. Top /\ P e. A /\ N e. ( ( nei ` J ) ` { P } ) ) -> P e. N )
Theorem	0nnei 20126	The empty set is not a neighborhood of a nonempty set. (Contributed by FL, 18-Sep-2007.)
|- ( ( J e. Top /\ S =/= (/) ) -> -. (/) e. ( ( nei ` J ) ` S ) )
Theorem	neips 20127*	A neighborhood of a set is a neighborhood of every point in the set. Proposition of [BourbakiTop1] p. I.2. (Contributed by FL, 16-Nov-2006.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> ( N e. ( ( nei ` J ) ` S ) <-> A. p e. S N e. ( ( nei ` J ) ` { p } ) ) )
Theorem	opnneissb 20128	An open set is a neighborhood of any of its subsets. (Contributed by FL, 2-Oct-2006.)
|- X = U. J   =>    |- ( ( J e. Top /\ N e. J /\ S C_ X ) -> ( S C_ N <-> N e. ( ( nei ` J ) ` S ) ) )
Theorem	opnssneib 20129	Any superset of an open set is a neighborhood of it. (Contributed by NM, 14-Feb-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ S e. J /\ N C_ X ) -> ( S C_ N <-> N e. ( ( nei ` J ) ` S ) ) )
Theorem	ssnei2 20130	Any subset of X containing a neighborhood of a set is a neighborhood of this set. Proposition Vi of [BourbakiTop1] p. I.3. (Contributed by FL, 2-Oct-2006.)
|- X = U. J   =>    |- ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ ( N C_ M /\ M C_ X ) ) -> M e. ( ( nei ` J ) ` S ) )
Theorem	neindisj 20131	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.)
|- X = U. J   =>    |- ( ( ( J e. Top /\ S C_ X ) /\ ( P e. ( ( cls ` J ) ` S ) /\ N e. ( ( nei ` J ) ` { P } ) ) ) -> ( N i^i S ) =/= (/) )
Theorem	opnneiss 20132	An open set is a neighborhood of any of its subsets. (Contributed by NM, 13-Feb-2007.)
|- ( ( J e. Top /\ N e. J /\ S C_ N ) -> N e. ( ( nei ` J ) ` S ) )
Theorem	opnneip 20133	An open set is a neighborhood of any of its members. (Contributed by NM, 8-Mar-2007.)
|- ( ( J e. Top /\ N e. J /\ P e. N ) -> N e. ( ( nei ` J ) ` { P } ) )
Theorem	opnnei 20134*	A set is open iff it is a neighborhood of all its points. ( Contributed by Jeff Hankins, 15-Sep-2009.) (Contributed by NM, 16-Sep-2009.)
|- ( J e. Top -> ( S e. J <-> A. x e. S S e. ( ( nei ` J ) ` { x } ) ) )
Theorem	tpnei 20135	The underlying set of a topology is a neighborhood of any of its subsets. Special case of opnneiss 20132. (Contributed by FL, 2-Oct-2006.)
|- X = U. J   =>    |- ( J e. Top -> ( S C_ X <-> X e. ( ( nei ` J ) ` S ) ) )
Theorem	neiuni 20136	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.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> X = U. ( ( nei ` J ) ` S ) )
Theorem	neindisj2 20137*	A point P belongs to the closure of a set S iff every neighborhood of P meets S. (Contributed by FL, 15-Sep-2013.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X /\ P e. X ) -> ( P e. ( ( cls ` J ) ` S ) <-> A. n e. ( ( nei ` J ) ` { P } ) ( n i^i S ) =/= (/) ) )
Theorem	topssnei 20138	A finer topology has more neighborhoods. (Contributed by Mario Carneiro, 9-Apr-2015.)
|- X = U. J   &    |- Y = U. K   =>    |- ( ( ( J e. Top /\ K e. Top /\ X = Y ) /\ J C_ K ) -> ( ( nei ` J ) ` S ) C_ ( ( nei ` K ) ` S ) )
Theorem	innei 20139	The intersection of two neighborhoods of a set is also a neighborhood of the set. Proposition Vii of [BourbakiTop1] p. I.3 . (Contributed by FL, 28-Sep-2006.)
|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ M e. ( ( nei ` J ) ` S ) ) -> ( N i^i M ) e. ( ( nei ` J ) ` S ) )
Theorem	opnneiid 20140	Only an open set is a neighborhood of itself. (Contributed by FL, 2-Oct-2006.)
|- ( J e. Top -> ( N e. ( ( nei ` J ) ` N ) <-> N e. J ) )
Theorem	neissex 20141*	For any neighborhood N of S, there is a neighborhood x of S such that N is a neighborhood of all subsets of x. Proposition Viv of [BourbakiTop1] p. I.3 . (Contributed by FL, 2-Oct-2006.)
|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> E. x e. ( ( nei ` J ) ` S ) A. y ( y C_ x -> N e. ( ( nei ` J ) ` y ) ) )
Theorem	0nei 20142	The empty set is a neighborhood of itself. (Contributed by FL, 10-Dec-2006.)
|- ( J e. Top -> (/) e. ( ( nei ` J ) ` (/) ) )
Theorem	neipeltop 20143*	Lemma for neiptopreu 20147 (Contributed by Thierry Arnoux, 6-Jan-2018.)
|- J = { a e. ~P X | A. p e. a a e. ( N ` p ) }   =>    |- ( C e. J <-> ( C C_ X /\ A. p e. C C e. ( N ` p ) ) )
Theorem	neiptopuni 20144*	Lemma for neiptopreu 20147 (Contributed by Thierry Arnoux, 6-Jan-2018.)
|- J = { a e. ~P X | A. p e. a a e. ( N ` p ) }   &    |- ( ph -> N : X --> ~P ~P X )   &    |- ( ( ( ( ph /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) -> b e. ( N ` p ) )   &    |- ( ( ph /\ p e. X ) -> ( fi ` ( N ` p ) ) C_ ( N ` p ) )   &    |- ( ( ( ph /\ p e. X ) /\ a e. ( N ` p ) ) -> p e. a )   &    |- ( ( ( ph /\ p e. X ) /\ a e. ( N ` p ) ) -> E. b e. ( N ` p ) A. q e. b a e. ( N ` q ) )   &    |- ( ( ph /\ p e. X ) -> X e. ( N ` p ) )   =>    |- ( ph -> X = U. J )
Theorem	neiptoptop 20145*	Lemma for neiptopreu 20147 (Contributed by Thierry Arnoux, 7-Jan-2018.)
|- J = { a e. ~P X | A. p e. a a e. ( N ` p ) }   &    |- ( ph -> N : X --> ~P ~P X )   &    |- ( ( ( ( ph /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) -> b e. ( N ` p ) )   &    |- ( ( ph /\ p e. X ) -> ( fi ` ( N ` p ) ) C_ ( N ` p ) )   &    |- ( ( ( ph /\ p e. X ) /\ a e. ( N ` p ) ) -> p e. a )   &    |- ( ( ( ph /\ p e. X ) /\ a e. ( N ` p ) ) -> E. b e. ( N ` p ) A. q e. b a e. ( N ` q ) )   &    |- ( ( ph /\ p e. X ) -> X e. ( N ` p ) )   =>    |- ( ph -> J e. Top )
Theorem	neiptopnei 20146*	Lemma for neiptopreu 20147 (Contributed by Thierry Arnoux, 7-Jan-2018.)
|- J = { a e. ~P X | A. p e. a a e. ( N ` p ) }   &    |- ( ph -> N : X --> ~P ~P X )   &    |- ( ( ( ( ph /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) -> b e. ( N ` p ) )   &    |- ( ( ph /\ p e. X ) -> ( fi ` ( N ` p ) ) C_ ( N ` p ) )   &    |- ( ( ( ph /\ p e. X ) /\ a e. ( N ` p ) ) -> p e. a )   &    |- ( ( ( ph /\ p e. X ) /\ a e. ( N ` p ) ) -> E. b e. ( N ` p ) A. q e. b a e. ( N ` q ) )   &    |- ( ( ph /\ p e. X ) -> X e. ( N ` p ) )   =>    |- ( ph -> N = ( p e. X |-> ( ( nei ` J ) ` { p } ) ) )
Theorem	neiptopreu 20147*	If, to each element P of a set X, we associate a set ( N ` P ) fulfilling the properties Vi, Vii, Viii and property Viv of [BourbakiTop1] p. I.2. , corresponding to ssnei 20124, innei 20139, elnei 20125 and neissex 20141, then there is a unique topology j such that for any point p, ( N ` p ) is the set of neighborhoods of p. Proposition 2 of [BourbakiTop1] p. I.3. This can be used to build a topology from a set of neighborhoods. Note that the additional condition that X is a neighborhood of all points was added. (Contributed by Thierry Arnoux, 6-Jan-2018.)
|- J = { a e. ~P X | A. p e. a a e. ( N ` p ) }   &    |- ( ph -> N : X --> ~P ~P X )   &    |- ( ( ( ( ph /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) -> b e. ( N ` p ) )   &    |- ( ( ph /\ p e. X ) -> ( fi ` ( N ` p ) ) C_ ( N ` p ) )   &    |- ( ( ( ph /\ p e. X ) /\ a e. ( N ` p ) ) -> p e. a )   &    |- ( ( ( ph /\ p e. X ) /\ a e. ( N ` p ) ) -> E. b e. ( N ` p ) A. q e. b a e. ( N ` q ) )   &    |- ( ( ph /\ p e. X ) -> X e. ( N ` p ) )   =>    |- ( ph -> E! j e. (TopOn ` X ) N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) )
12.1.6  Limit points and perfect sets
Syntax	clp 20148	Extend class notation with the limit point function for topologies.
class limPt
Syntax	cperf 20149	Extend class notation with the class of all perfect spaces.
class Perf
Definition	df-lp 20150*	Define a function on topologies whose value is the set of limit points of the subsets of the base set. See lpval 20153. (Contributed by NM, 10-Feb-2007.)
|- limPt = ( j e. Top |-> ( x e. ~P U. j |-> { y | y e. ( ( cls ` j ) ` ( x \ { y } ) ) } ) )
Definition	df-perf 20151	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 = { j e. Top | ( ( limPt ` j ) ` U. j ) = U. j }
Theorem	lpfval 20152*	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.)
|- X = U. J   =>    |- ( J e. Top -> ( limPt ` J ) = ( x e. ~P X |-> { y | y e. ( ( cls ` J ) ` ( x \ { y } ) ) } ) )
Theorem	lpval 20153*	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.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( ( limPt ` J ) ` S ) = { x | x e. ( ( cls ` J ) ` ( S \ { x } ) ) } )
Theorem	islp 20154	The predicate " P is a limit point of S." (Contributed by NM, 10-Feb-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( P e. ( ( limPt ` J ) ` S ) <-> P e. ( ( cls ` J ) ` ( S \ { P } ) ) ) )
Theorem	lpsscls 20155	The limit points of a subset are included in the subset's closure. (Contributed by NM, 26-Feb-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( ( limPt ` J ) ` S ) C_ ( ( cls ` J ) ` S ) )
Theorem	lpss 20156	The limit points of a subset are included in the base set. (Contributed by NM, 9-Nov-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( ( limPt ` J ) ` S ) C_ X )
Theorem	lpdifsn 20157	P is a limit point of S iff it is a limit point of S \ { P }. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( P e. ( ( limPt ` J ) ` S ) <-> P e. ( ( limPt ` J ) ` ( S \ { P } ) ) ) )
Theorem	lpss3 20158	Subset relationship for limit points. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X /\ T C_ S ) -> ( ( limPt ` J ) ` T ) C_ ( ( limPt ` J ) ` S ) )
Theorem	islp2 20159*	The predicate " P is a limit point of S," 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.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X /\ P e. X ) -> ( P e. ( ( limPt ` J ) ` S ) <-> A. n e. ( ( nei ` J ) ` { P } ) ( n i^i ( S \ { P } ) ) =/= (/) ) )
Theorem	islp3 20160*	The predicate " P is a limit point of S " in terms of open sets. see islp2 20159, elcls 20087, islp 20154. (Contributed by FL, 31-Jul-2009.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X /\ P e. X ) -> ( P e. ( ( limPt ` J ) ` S ) <-> A. x e. J ( P e. x -> ( x i^i ( S \ { P } ) ) =/= (/) ) ) )
Theorem	maxlp 20161	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.)
|- X = U. J   =>    |- ( J e. Top -> ( P e. ( ( limPt ` J ) ` X ) <-> ( P e. X /\ -. { P } e. J ) ) )
Theorem	clslp 20162	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.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) = ( S u. ( ( limPt ` J ) ` S ) ) )
Theorem	islpi 20163	A point belonging to a set's closure but not the set itself is a limit point. (Contributed by NM, 8-Nov-2007.)
|- X = U. J   =>    |- ( ( ( J e. Top /\ S C_ X ) /\ ( P e. ( ( cls ` J ) ` S ) /\ -. P e. S ) ) -> P e. ( ( limPt ` J ) ` S ) )
Theorem	cldlp 20164	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.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( S e. ( Clsd ` J ) <-> ( ( limPt ` J ) ` S ) C_ S ) )
Theorem	isperf 20165	Definition of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016.)
|- X = U. J   =>    |- ( J e. Perf <-> ( J e. Top /\ ( ( limPt ` J ) ` X ) = X ) )
Theorem	isperf2 20166	Definition of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016.)
|- X = U. J   =>    |- ( J e. Perf <-> ( J e. Top /\ X C_ ( ( limPt ` J ) ` X ) ) )
Theorem	isperf3 20167*	A perfect space is a topology which has no open singletons. (Contributed by Mario Carneiro, 24-Dec-2016.)
|- X = U. J   =>    |- ( J e. Perf <-> ( J e. Top /\ A. x e. X -. { x } e. J ) )
Theorem	perflp 20168	The limit points of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016.)
|- X = U. J   =>    |- ( J e. Perf -> ( ( limPt ` J ) ` X ) = X )
Theorem	perfi 20169	Property of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016.)
|- X = U. J   =>    |- ( ( J e. Perf /\ P e. X ) -> -. { P } e. J )
Theorem	perftop 20170	A perfect space is a topology. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- ( J e. Perf -> J e. Top )
12.1.7  Subspace topologies
Theorem	restrcl 20171	Reverse closure for the subspace topology. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 1-May-2015.)
|- ( ( J ↾t A ) e. Top -> ( J e. _V /\ A e. _V ) )
Theorem	restbas 20172	A subspace topology basis is a basis. Y is normally a subset of the base set of J. (Contributed by Mario Carneiro, 19-Mar-2015.)
|- ( B e. TopBases -> ( B ↾t A ) e. TopBases )
Theorem	tgrest 20173	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.)
|- ( ( B e. V /\ A e. W ) -> ( topGen ` ( B ↾t A ) ) = ( ( topGen ` B ) ↾t A ) )
Theorem	resttop 20174	A subspace topology is a topology. Definition of subspace topology in [Munkres] p. 89. A is normally a subset of the base set of J. (Contributed by FL, 15-Apr-2007.) (Revised by Mario Carneiro, 1-May-2015.)
|- ( ( J e. Top /\ A e. V ) -> ( J ↾t A ) e. Top )
Theorem	resttopon 20175	A subspace topology is a topology on the base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ A C_ X ) -> ( J ↾t A ) e. (TopOn ` A ) )
Theorem	restuni 20176	The underlying set of a subspace topology. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 13-Aug-2015.)
|- X = U. J   =>    |- ( ( J e. Top /\ A C_ X ) -> A = U. ( J ↾t A ) )
Theorem	stoig 20177	The topological space built with a subspace topology. (Contributed by FL, 5-Jan-2009.) (Proof shortened by Mario Carneiro, 1-May-2015.)
|- X = U. J   =>    |- ( ( J e. Top /\ A C_ X ) -> { <. ( Base ` ndx ) , A >. , <. (TopSet ` ndx ) , ( J ↾t A ) >. } e. TopSp )
Theorem	restco 20178	Composition of subspaces. (Contributed by Mario Carneiro, 15-Dec-2013.) (Revised by Mario Carneiro, 1-May-2015.)
|- ( ( J e. V /\ A e. W /\ B e. X ) -> ( ( J ↾t A ) ↾t B ) = ( J ↾t ( A i^i B ) ) )
Theorem	restabs 20179	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.)
|- ( ( J e. V /\ S C_ T /\ T e. W ) -> ( ( J ↾t T ) ↾t S ) = ( J ↾t S ) )
Theorem	restin 20180	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.)
|- X = U. J   =>    |- ( ( J e. V /\ A e. W ) -> ( J ↾t A ) = ( J ↾t ( A i^i X ) ) )
Theorem	restuni2 20181	The underlying set of a subspace topology. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- X = U. J   =>    |- ( ( J e. Top /\ A e. V ) -> ( A i^i X ) = U. ( J ↾t A ) )
Theorem	resttopon2 20182	The underlying set of a subspace topology. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ A e. V ) -> ( J ↾t A ) e. (TopOn ` ( A i^i X ) ) )
Theorem	rest0 20183	The subspace topology induced by the topology J on the empty set. (Contributed by FL, 22-Dec-2008.) (Revised by Mario Carneiro, 1-May-2015.)
|- ( J e. Top -> ( J ↾t (/) ) = { (/) } )
Theorem	restsn 20184	The only subspace topology induced by the topology { (/) }. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 15-Dec-2013.)
|- ( A e. V -> ( { (/) } ↾t A ) = { (/) } )
Theorem	restsn2 20185	The subspace topology induced by a singleton. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 16-Sep-2015.)
|- ( ( J e. (TopOn ` X ) /\ A e. X ) -> ( J ↾t { A } ) = ~P { A } )
Theorem	restcld 20186*	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.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( A e. ( Clsd ` ( J ↾t S ) ) <-> E. x e. ( Clsd ` J ) A = ( x i^i S ) ) )
Theorem	restcldi 20187	A closed set is closed in the subspace topology. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- X = U. J   =>    |- ( ( A C_ X /\ B e. ( Clsd ` J ) /\ B C_ A ) -> B e. ( Clsd ` ( J ↾t A ) ) )
Theorem	restcldr 20188	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.)
|- ( ( A e. ( Clsd ` J ) /\ B e. ( Clsd ` ( J ↾t A ) ) ) -> B e. ( Clsd ` J ) )
Theorem	restopnb 20189	If B is an open subset of the subspace base set A, then any subset of B is open iff it is open in A. (Contributed by Mario Carneiro, 2-Mar-2015.)
|- ( ( ( J e. Top /\ A e. V ) /\ ( B e. J /\ B C_ A /\ C C_ B ) ) -> ( C e. J <-> C e. ( J ↾t A ) ) )
Theorem	ssrest 20190	If K is a finer topology than J, then the subspace topologies induced by A maintain this relationship. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 1-May-2015.)
|- ( ( K e. V /\ J C_ K ) -> ( J ↾t A ) C_ ( K ↾t A ) )
Theorem	restopn2 20191	The if A is open, then B is open in A iff it is an open subset of A. (Contributed by Mario Carneiro, 2-Mar-2015.)
|- ( ( J e. Top /\ A e. J ) -> ( B e. ( J ↾t A ) <-> ( B e. J /\ B C_ A ) ) )
Theorem	restdis 20192	A subspace of a discrete topology is discrete. (Contributed by Mario Carneiro, 19-Mar-2015.)
|- ( ( A e. V /\ B C_ A ) -> ( ~P A ↾t B ) = ~P B )
Theorem	restfpw 20193	The restriction of the set of finite subsets of A is the set of finite subsets of B. (Contributed by Mario Carneiro, 18-Sep-2015.)
|- ( ( A e. V /\ B C_ A ) -> ( ( ~P A i^i Fin ) ↾t B ) = ( ~P B i^i Fin ) )
Theorem	neitr 20194	The neighborhood of a trace is the trace of the neighborhood. (Contributed by Thierry Arnoux, 17-Jan-2018.)
|- X = U. J   =>    |- ( ( J e. Top /\ A C_ X /\ B C_ A ) -> ( ( nei ` ( J ↾t A ) ) ` B ) = ( ( ( nei ` J ) ` B ) ↾t A ) )
Theorem	restcls 20195	A closure in a subspace topology. (Contributed by Jeff Hankins, 22-Jan-2010.) (Revised by Mario Carneiro, 15-Dec-2013.)
|- X = U. J   &    |- K = ( J ↾t Y )   =>    |- ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( cls ` K ) ` S ) = ( ( ( cls ` J ) ` S ) i^i Y ) )
Theorem	restntr 20196	An interior in a subspace topology. Willard in General Topology says that there is no analog of restcls 20195 for interiors. In some sense, that is true. (Contributed by Jeff Hankins, 23-Jan-2010.) (Revised by Mario Carneiro, 15-Dec-2013.)
|- X = U. J   &    |- K = ( J ↾t Y )   =>    |- ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( int ` K ) ` S ) = ( ( ( int ` J ) ` ( S u. ( X \ Y ) ) ) i^i Y ) )
Theorem	restlp 20197	The limit points of a subset restrict naturally in a subspace. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- X = U. J   &    |- K = ( J ↾t Y )   =>    |- ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( limPt ` K ) ` S ) = ( ( ( limPt ` J ) ` S ) i^i Y ) )
Theorem	restperf 20198	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.)
|- X = U. J   &    |- K = ( J ↾t Y )   =>    |- ( ( J e. Top /\ Y C_ X ) -> ( K e. Perf <-> Y C_ ( ( limPt ` J ) ` Y ) ) )
Theorem	perfopn 20199	An open subset of a perfect space is perfect. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- X = U. J   &    |- K = ( J ↾t Y )   =>    |- ( ( J e. Perf /\ Y e. J ) -> K e. Perf )
Theorem	resstopn 20200	The topology of a restricted structure. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- H = ( K ↾s A )   &    |- J = ( TopOpen ` K )   =>    |- ( J ↾t A ) = ( TopOpen ` H )