mmtheorems78 - Metamath Proof Explorer

Jump to page: Contents + 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10722

Statement List for Metamath Proof Explorer - 7701-7800 - Page 78 of 108

Type	Label	Description
Statement
Theorem	cls0 7701	The closure of the empty set.
|- (J e. Top -> ((cls` J)` (/)) = (/))
Theorem	ntr0 7702	The interior of the empty set.
|- (J e. Top -> ((int` J)` (/)) = (/))
Theorem	elcls3 7703	Membership in a closure in terms of the members of a basis. Theorem 6.5(b) of [Munkres] p. 95.
|- J = (topGen` B)   &   |- X = U.J   =>   |- ((B e. Bases /\ S (_ X /\ P e. X) -> (P e. ((cls` J)` S) <-> A.x e. B (P e. x -> (x i^i S) =/= (/))))
Neighborhoods
Syntax	cnei 7704	Extend class notation with neighborhood relation for topologies.
class nei
Definition	df-nei 7705	Define a function on topologies whose value is a map from a subset to its neighborhoods.
|- nei = {<.j, y>. | (j e. Top /\ y = {<.z, v>. | (z (_ U.j /\ v = {w | (w (_ U.j /\ E.g e. j (z (_ g /\ g (_ w))})})}
Theorem	neifval 7706	The neighborhood function on the subsets of a topology's base set.
|- X = U.J   =>   |- (J e. Top -> (nei` J) = {<.z, w>. | (z (_ X /\ w = {v | (v (_ X /\ E.g e. J (z (_ g /\ g (_ v))})})
Theorem	neif 7707	The neighborhood function is a function of the subsets of a topology's base set.
|- X = U.J   =>   |- (J e. Top -> (nei` J) Fn P~X)
Theorem	neiss2 7708	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.)
|- X = U.J   =>   |- ((J e. Top /\ N e. ((nei` J)` S)) -> S (_ X)
Theorem	neival 7709	The set of neighborhoods of a subset of the base set of a topology.
|- X = U.J   =>   |- ((J e. Top /\ S (_ X) -> ((nei` J)` S) = {v | (v (_ X /\ E.g e. J (S (_ g /\ g (_ v))})
Theorem	isnei 7710	The predicate "N is a neighborhood of S." (Contributed by FL, 25-Sep-2006.)
|- X = U.J   =>   |- ((J e. Top /\ S (_ X) -> (N e. ((nei` J)` S) <-> (N (_ X /\ E.g e. J (S (_ g /\ g (_ N))))
Theorem	neiint 7711	An intuitive definition of a neighborhood in terms of interior. (Contributed by Szymon Jaroszewicz, 18-Dec-2007.)
|- X = U.J   =>   |- ((J e. Top /\ S (_ X /\ N (_ X) -> (N e. ((nei` J)` S) <-> S (_ ((int` J)` N)))
Theorem	isneip 7712	The predicate "N is a neighborhood of point P."
|- X = U.J   =>   |- ((J e. Top /\ P e. X) -> (N e. ((nei` J)` {P}) <-> (N (_ X /\ E.g e. J (P e. g /\ g (_ N))))
Theorem	neii1 7713	A neighborhood is included in the topology's base set.
|- X = U.J   =>   |- ((J e. Top /\ N e. ((nei` J)` S)) -> N (_ X)
Theorem	neii2 7714	Property of a neighborhood.
|- ((J e. Top /\ N e. ((nei` J)` S)) -> E.g e. J (S (_ g /\ g (_ N))
Theorem	neiss 7715	Any neighborhood of a set S is also a neighborhood of any subset R (_ S. Bourbaki TG I.2. (Contributed by FL, 25-Sep-2006.)
|- ((J e. Top /\ N e. ((nei` J)` S) /\ R (_ S) -> N e. ((nei` J)` R))
Theorem	ssnei 7716	A set is included in its neighborhoods. Based on Bourbaki TG I.3 Viii. (Contributed by FL, 16-Nov-2006.)
|- ((J e. Top /\ N e. ((nei` J)` S)) -> S (_ N)
Theorem	elnei 7717	A point belongs to any of its neighborhoods. Based on Bourbaki TG I.3 Viii. (Contributed by FL, 28-Sep-2006.)
|- ((J e. Top /\ P e. A /\ N e. ((nei` J)` {P})) -> P e. N)
Theorem	0nnei 7718	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 7719	A neighborhood of a set is a neighborhood of every point in the set. Bourbaki TG I.2. (Contributed by FL, 16-Nov-2006.)
|- X = U.J   =>   |- ((J e. Top /\ S (_ X /\ S =/= (/)) -> (N e. ((nei` J)` S) <-> A.p e. S N e. ((nei` J)` {p})))
Theorem	opnneissb 7720	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 (_ X) -> (S (_ N <-> N e. ((nei` J)` S)))
Theorem	opnssneib 7721	Any superset of an open set is a neighborhood of it.
|- X = U.J   =>   |- ((J e. Top /\ S e. J /\ N (_ X) -> (S (_ N <-> N e. ((nei` J)` S)))
Theorem	ssnei2 7722	Any subset of X containing a neigborhood of a set is a neighborhood of this set. Based on Bourbaki TG I.3 Vi. (Contributed by FL, 2-Oct-2006.)
|- X = U.J   =>   |- (((J e. Top /\ N e. ((nei` J)` S)) /\ (N (_ M /\ M (_ X)) -> M e. ((nei` J)` S))
Theorem	neindisj 7723	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.
|- X = U.J   =>   |- (((J e. Top /\ S (_ X) /\ (P e. ((cls` J)` S) /\ N e. ((nei` J)` {P}))) -> (N i^i S) =/= (/))
Theorem	opnneiss 7724	An open set is a neighborhood of any of its subsets.
|- ((J e. Top /\ N e. J /\ S (_ N) -> N e. ((nei` J)` S))
Theorem	opnneip 7725	An open set is a neighborhood of any of its members.
|- ((J e. Top /\ N e. J /\ P e. N) -> N e. ((nei` J)` {P}))
Theorem	tpnei 7726	The underlying set of a topology is a neighborhood of any of its subsets. Special case of opnneiss 7724. (Contributed by FL, 2-Oct-2006.)
|- X = U.J   =>   |- (J e. Top -> (S (_ X <-> X e. ((nei` J)` S)))
Theorem	unnei 7727	The union of the neighborhoods of a set equals the topology's underlying set. (Contributed by FL, 18-Sep-2007.)
|- X = U.J   =>   |- ((J e. Top /\ S (_ X) -> U.((nei` J)` S) = X)
Theorem	innei 7728	The intersection of two neighborhoods of a set is also a neighborhood of the set. Based on Bourbaki TG I.3 Vii. (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 7729	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 7730	For any neighborhood N of S, there is a neighborhood x of S such that N is a neighborhood of all subsets of x. Based on Bourbaki TG I.3 Viv. (Contributed by FL, 2-Oct-2006.)
|- ((J e. Top /\ N e. ((nei` J)` S)) -> E.x e. ((nei` J)` S)A.y(y (_ x -> N e. ((nei` J)` y)))
Theorem	0nei 7731	The empty set is a neighborhood of itself. (Contributed by FL, 10-Dec-2006.)
|- (J e. Top -> (/) e. ((nei` J)` (/)))
Limit points
Syntax	clp 7732	Extend class notation with the limit point function for topologies.
class limPt
Definition	df-lp 7733	Define a function on topologies whose value is the set of limit points of the subsets of the base set. See lpval 7735.
|- limPt = {<.z, w>. | (z e. Top /\ w = {<.x, y>. | (x (_ U.z /\ y = {v | v e. ((cls` J)` (x \ {v}))})})}
Theorem	lpfval 7734	The limit point function on the subsets of a topology's base set.
|- X = U.J   =>   |- (J e. Top -> (limPt` J) = {<.x, y>. | (x (_ X /\ y = {v | v e. ((cls` J)` (x \ {v}))})})
Theorem	lpval 7735	The set of limit points of a subset of the base set of a topology. Alternate definition of limit point in [Munkres] p. 97.
|- X = U.J   =>   |- ((J e. Top /\ S (_ X) -> ((limPt` J)` S) = {x | x e. ((cls` J)` (S \ {x}))})
Theorem	islp 7736	The predicate "P is a limit point of S."
|- X = U.J   =>   |- ((J e. Top /\ S (_ X) -> (P e. ((limPt` J)` S) <-> P e. ((cls` J)` (S \ {P}))))
Theorem	lpsscls 7737	The limits points of a subset are included in the subset's closure.
|- X = U.J   =>   |- ((J e. Top /\ S (_ X) -> ((limPt` J)` S) (_ ((cls` J)` S))
Theorem	lpss 7738	The limits points of a subset are included in the base set.
|- X = U.J   =>   |- ((J e. Top /\ S (_ X) -> ((limPt` J)` S) (_ X)
Theorem	islp2 7739	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.
|- X = U.J   =>   |- ((J e. Top /\ S (_ X /\ P e. X) -> (P e. ((limPt` J)` S) <-> A.n e. ((nei` J)` {P})(n i^i (S \ {P})) =/= (/)))
Theorem	clslp 7740	The closure of a subset of a topological space is the subset together with its limit points. Theorem 6.6 of [Munkres] p. 97.
|- X = U.J   =>   |- ((J e. Top /\ S (_ X) -> ((cls` J)` S) = (S u. ((limPt` J)` S)))
Theorem	islpi 7741	A point belonging to a set's closure but not the set itself is a limit point.
|- X = U.J   =>   |- (((J e. Top /\ S (_ X) /\ (P e. ((cls` J)` S) /\ -. P e. S)) -> P e. ((limPt` J)` S))
Theorem	cldlp 7742	A subset of a topological space is closed iff it contains all its limit points. Corollary 6.7 of [Munkres] p. 97.
|- X = U.J   =>   |- ((J e. Top /\ S (_ X) -> (S e. (Clsd` J) <-> ((limPt` J)` S) (_ S))
Theorem	qdensere 7743	QQ is dense in the standard topology on RR.
|- ((cls` (topGen` ran (,)))` QQ) = RR
Continuity
Syntax	ccn 7744	Extend class notation with the set of continuous functions between topologies.
class Cn
Syntax	ccnp 7745	Extend class notation with the set of functions between topologies continuous at a point.
class CnP
Definition	df-cn 7746	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 7750 for the predicate form.
|- Cn = {<.<.j, k>., z>. | ((j e. Top /\ k e. Top) /\ z = {f e. (U.