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-10781

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

Type	Label	Description
Statement
Theorem	ntrtop 7701	The interior of a topology's underlying set is entire set.
|- X = U.J   =>   |- (J e. Top -> ((int` J)` X) = X)
Theorem	0ntr 7702	A subset with an empty interior cannot cover a whole (nonempty) topology.
|- X = U.J   =>   |- (((J e. Top /\ X =/= (/)) /\ (S (_ X /\ ((int` J)` S) = (/))) -> (X \ S) =/= (/))
Theorem	clsss2 7703	If a subset is included in a closed set, so is the subset's closure.
|- X = U.J   =>   |- ((J e. Top /\ C e. (Clsd` J) /\ S (_ C) -> ((cls` J)` S) (_ C)
Theorem	elcls 7704	Membership in a closure. Theorem 6.5(a) of [Munkres] p. 95.
|- X = U.J   =>   |- ((J e. Top /\ S (_ X /\ P e. X) -> (P e. ((cls` J)` S) <-> A.x e. J (P e. x -> (x i^i S) =/= (/))))
Theorem	elcls2 7705	Membership in a closure.
|- X = U.J   =>   |- ((J e. Top /\ S (_ X) -> (P e. ((cls` J)` S) <-> (P e. X /\ A.x e. J (P e. x -> (x i^i S) =/= (/)))))
Theorem	clsndisj 7706	Any open set containing a point that belongs to the closure of a subset intersects the subset. One direction of Theorem 6.5(a) of [Munkres] p. 95.
|- X = U.J   =>   |- (((J e. Top /\ S (_ X /\ P e. ((cls` J)` S)) /\ (U e. J /\ P e. U)) -> (U i^i S) =/= (/))
Theorem	ntrcls0 7707	A subset whose closure has an empty interior also has an empty interior.
|- X = U.J   =>   |- ((J e. Top /\ S (_ X /\ ((int` J)` ((cls` J)` S)) = (/)) -> ((int` J)` S) = (/))
Theorem	ntreq0 7708	Two ways to say that a subset has an empty interior.
|- X = U.J   =>   |- ((J e. Top /\ S (_ X) -> (((int` J)` S) = (/) <-> A.x e. J (x (_ S -> x = (/))))
Theorem	cls0 7709	The closure of the empty set.
|- (J e. Top -> ((cls` J)` (/)) = (/))
Theorem	ntr0 7710	The interior of the empty set.
|- (J e. Top -> ((int` J)` (/)) = (/))
Theorem	elcls3 7711	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 7712	Extend class notation with neighborhood relation for topologies.
class nei
Definition	df-nei 7713	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 7714	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 7715	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 7716	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 7717	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 7718	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 7719	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 7720	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 7721	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 7722	Property of a neighborhood.
|- ((J e. Top /\ N e. ((nei` J)` S)) -> E.g e. J (S (_ g /\ g (_ N))
Theorem	neiss 7723	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 7724	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 7725	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 7726	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 7727	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 7728	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 7729	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 7730	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 7731	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 7732	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 7733	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 7734	The underlying set of a topology is a neighborhood of any of its subsets. Special case of opnneiss 7732. (Contributed by FL, 2-Oct-2006.)
|- X = U.J   =>   |- (J e. Top -> (S (_ X <-> X e. ((nei` J)` S)))
Theorem	unnei 7735	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 7736	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 7737	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 7738	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 7739	The empty set is a neighborhood of itself. (Contributed by FL, 10-Dec-2006.)
|- (J e. Top -> (/) e. ((nei` J)` (/)))
Limit points
Syntax	clp 7740	Extend class notation with the limit point function for topologies.
class limPt
Definition	df-lp 7741	Define a function on topologies whose value is the set of limit points of the subsets of the base set. See lpval 7743.
|- limPt = {<.z, w>. | (z e. Top /\ w = {<.x, y>. | (x (_ U.z /\ y = {v | v e. ((cls` J)` (x \ {v}))})})}
Theorem	lpfval 7742	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 7743	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 7744	The predicate "P is a limit point of S."
|- X = U.J   =>   |- ((J e. Top /\ S (_ X) -> (