mmtheorems77 - 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-10682

Statement List for Metamath Proof Explorer - 7601-7700 - Page 77 of 107

Type	Label	Description
Statement
Theorem	2basgent 7601	Conditions that determine the equality of two generated topologies.
|- (((B e. Bases /\ C e. Bases) /\ (B (_ C /\ C (_ (topGen` B))) -> (topGen` B) = (topGen` C))
Theorem	bastop 7602	A subset of a topology is a basis for the topology iff every member of the topology is a union of members of the basis. We use the idiom "B e. Bases /\ (topGen` B) = J" to express "B is a basis for topology J," since we do not have a separate notation for this. Definition 15.35 of [Schechter] p. 428.
|- ((J e. Top /\ B (_ J) -> ((B e. Bases /\ (topGen` B) = J) <-> A.x e. J E.y(y (_ B /\ x = U.y)))
Theorem	bastop2 7603	A version of bastop 7602 that doesn't have B (_ J in the antecedent.
|- (J e. Top -> ((B e. Bases /\ (topGen` B) = J) <-> (B (_ J /\ A.x e. J E.y(y (_ B /\ x = U.y))))
Subbases for topologies
Theorem	subbas 7604	The collection of finite intersections of the elements of any set A is a basis for a topology (on U.A by subbas2 7605). The set A is called a subbasis for that topology. Theorem for subbases in [Munkres] p. 82. See abfii1 4551 through abfii5 4555 for other ways to express the collection of finite intersections.
|- A e. V   &   |- B = {x | E.y(y (_ A /\ E.z e. om y ~~ z /\ x = |^|y)}   =>   |- B e. Bases
Theorem	subbas2 7605	The collection of finite intersections of any set (subbasis) A is a basis for a topology on U.A. Justifies the definition of subbasis in [Munkres] p. 82 (after using unitgt 7583).
|- B = {x | E.y(y (_ A /\ E.z e. om y ~~ z /\ x = |^|y)}   =>   |- U.B = U.A
Examples of topologies
Theorem	subtop 7606	A subspace topology is a topology. Definition of subspace topology in [Munkres] p. 89. Y is normally a subset of the base set of J. (Contributed by FL, 15-Apr-2007.)
|- (J e. Top -> {x | E.y e. J x = (y i^i Y)} e. Top)
Theorem	sn0top 7607	The singleton of the empty set is a topology. (Contributed by Stefan Allan, 3-Mar-2006.)
|- {(/)} e. Top
Theorem	indistop 7608	The indiscrete topology on a set A. Part of Example 2 in [Munkres] p. 77. (Contributed by FL, 16-Jul-2006.)
|- A e. V   =>   |- {(/), A} e. Top
Theorem	distop 7609	The discrete topology on a set A. Part of Example 2 in [Munkres] p. 77. (Contributed by FL, 18-Jul-2006.)
|- A e. V   =>   |- P~A e. Top
Theorem	fctop 7610	The finite complement topology on a set A. Example 3 in [Munkres] p. 77. (Contributed by FL, 15-Aug-2006.)
|- A e. V   =>   |- {x | (x (_ A /\ (E.n e. om (A \ x) ~~ n \/ x = (/)))} e. Top
Theorem	fctop2 7611	The finite complement topology on a set A. Example 3 in [Munkres] p. 77. (This version of fctop 7610 requires the Axiom of Infinity.) (Contributed by FL, 20-Aug-2006.)
|- A e. V   =>   |- {x | (x (_ A /\ ((A \ x) ~< om \/ x = (/)))} e. Top
Theorem	cctop 7612	The countable complement topology on a set A. Example 4 in [Munkres] p. 77. (Contributed by FL, 29-Aug-2006.)
|- A e. V   =>   |- {x | (x (_ A /\ ((A \ x) ~<_ om \/ x = (/)))} e. Top
Theorem	indistps 7613	The indiscrete topology on a set A expressed as a topological space. (Contributed by FL, 19-Jul-2006.)
|- A e. V   =>   |- <.A, {(/), A}>. e. TopSp
Theorem	distps 7614	The discrete topology on a set A expressed as a topological space. (Contributed by FL, 20-Aug-2006.)
|- A e. V   =>   |- <.A, P~A>. e. TopSp
Theorem	retopbas 7615	A basis for the standard topology on the reals.
|- ran (,) e. Bases
Theorem	retop 7616	The standard topology on the reals. (Contributed by FL, 4-Jun-2007.)
|- (topGen` ran (,)) e. Top
Theorem	uniretop 7617	The underlying set of the standard topology on the reals is the reals. (Contributed by FL, 4-Jun-2007.)
|- U.(topGen` ran (,)) = RR
Theorem	retps 7618	The standard topological space on the reals.
|- <.RR, (topGen` ran (,))>. e. TopSp
Theorem	iooretop 7619	Open intervals are open sets of the standard topology on the reals . (Contributed by FL, 18-Jun-2007.)
|- (A(,)B) e. (topGen` ran (,))
Closure and interior
Syntax	ccld 7620	Extend class notation with the set of closed sets of a topology.
class Clsd
Syntax	cnt 7621	Extend class notation with interior of a subset of a topology base set.
class int
Syntax	ccl 7622	Extend class notation with closure of a subset of a topology base set.
class cls
Definition	df-cld 7623	Define a function on topologies whose value is the set of closed sets of the topology.
|- Clsd = {<.z, w>. | (z e. Top /\ w = {x | (x (_ U.z /\ (U.z \ x) e. z)})}
Definition	df-ntr 7624	Define a function on topologies whose value is the interior function on the subsets of the base set. See ntrval 7636.
|- int = {<.z, w>. | (z e. Top /\ w = {<.x, y>. | (x (_ U.z /\ y = U.{v e. z | v (_ x})})}
Definition	df-cls 7625	Define a function on topologies whose value is the closure function on the subsets of the base set. See clsval 7637.
|- cls = {<.z, w>. | (z e. Top /\ w = {<.x, y>. | (x (_ U.z /\ y = |^|{v e. (Clsd` z) | x (_ v})})}
Theorem	cldval 7626	The set of closed sets of a topology. (Note that the set of open sets is just the topology itself, so we don't have a separate definition.)
|- X = U.J   =>   |- (J e. Top -> (Clsd` J) = {x | (x (_ X /\ (X \ x) e. J)})
Theorem	ntrfval 7627	The interior function on the subsets of a topology's base set.
|- X = U.J   =>   |- (J e. Top -> (int` J) = {<.x, y>. | (x (_ X /\ y = U.{v e. J | v (_ x})})
Theorem	clsfval 7628	The closure function on the subsets of a topology's base set.
|- X = U.J   =>   |- (J e. Top -> (cls` J) = {<.x, y>. | (x (_ X /\ y = |^|{v e. (Clsd` J) | x (_ v})})
Theorem	iscld 7629	The predicate "S is a closed set."
|- X = U.J   =>   |- (J e. Top -> (S e. (Clsd` J) <-> (S (_ X /\ (X \ S) e. J)))
Theorem	iscld2 7630	A subset of the underlying set of a topology is closed iff its complement is open.
|- X = U.J   =>   |- ((J e. Top /\ S (_ X) -> (S e. (Clsd` J) <-> (X \ S) e. J))
Theorem	cldss 7631	A closed set is a subset of the underlying set of a topology.
|- X = U.J   =>   |- ((J e. Top /\ S e. (Clsd` J)) -> S (_ X)
Theorem	cldopn 7632	The complement of a closed set is open.
|- X = U.J   =>   |- ((J e. Top /\ S e. (Clsd` J)) -> (X \ S) e. J)
Theorem	isopn2 7633	A subset of the underlying set of a topology is open iff its complement is closed.
|- X = U.J   =>   |- ((J e. Top /\ S (_ X) -> (S e. J <-> (X \ S) e. (Clsd` J)))
Theorem	opncld 7634	The complement of an open set is closed.
|- X = U.J   =>   |- ((J e. Top /\ S e. J) -> (X \ S) e. (Clsd` J))
Theorem	topcld 7635	The underlying set of a topology is closed. Part of Theorem 6.1(1) of [Munkres] p. 93.
|- X = U.J   =>   |- (J e. Top -> X e. (Clsd` J))
Theorem	ntrval 7636	The interior of a subset of a topology's base set is the union of all the open sets it includes. Definition of interior of [Munkres] p. 94.
|- X = U.J   =>   |- ((J e. Top /\ S (_ X) -> ((int` J)` S) = U.{x e. J | x (_ S})
Theorem	clsval 7637	The closure of a subset of a topology's base set is the intersection of all the closed sets that include it. Definition of closure of [Munkres] p. 94.
|- X = U.J   =>   |- ((J e. Top /\ S (_ X) -> ((cls` J)` S) = |^|{x e. (Clsd` J) | S (_ x})
Theorem	0cld 7638	The empty set is closed. Part of Theorem 6.1(1) of [Munkres] p. 93.
|- (J e. Top -> (/) e. (Clsd` J))
Theorem	iincld 7639	The indexed intersection of a collection B(x) of closed sets is closed. Theorem 6.1(2) of [Munkres] p. 93.
|- ((J e. Top /\ A =/= (/) /\ A.x e. A B e. (Clsd` J)) -> |^|_x e. A B e. (Clsd` J))
Theorem	intcld 7640	The intersection of a set of closed sets is closed.
|- ((J e. Top /\ A =/= (/) /\ A (_ (Clsd` J)) -> |^|A e. (Clsd` J))
Theorem	uncld 7641	The union of two closed sets is closed. Equivalent to Theorem 6.1(3) of [Munkres] p. 93.
|- ((J e. Top /\ A e. (Clsd` J) /\ B e. (Clsd` J)) -> (A u. B) e. (Clsd` J))
Theorem	cldcls 7642	A closed subset equals its own closure.
|- ((J e. Top /\ S e. (Clsd` J)) -> ((cls` J)` S) = S)
Theorem	clscld 7643	The closure of a subset of a topology's underlying set is closed.
|- X = U.J   =>   |- ((J e. Top /\ S (_ X) -> ((cls` J)` S) e. (Clsd` J))
Theorem	ntropn 7644	The interior of a subset of a topology's underlying set is open.
|- X = U.J   =>   |- ((J e. Top /\ S (_ X) -> ((int` J)` S) e. J)
Theorem	clsval2 7645	Express closure in terms of interior.
|- X = U.J   =>   |- ((J e. Top /\ S (_ X) -> ((cls` J)` S) = (X \ ((int` J)` (X \ S))))
Theorem	ntrval2 7646	Interior expressed in terms of closure.
|- X = U.J   =>   |- ((J e. Top /\ S (_ X) -> ((int` J)` S) = (X \ ((cls` J)` (X \ S))))
Theorem	clsss 7647	Subset relationship for closure.
|- X = U.J   =>   |- ((J e. Top /\ S (_ X /\ T (_ S) -> ((cls` J)` T) (_ ((cls` J)` S))
Theorem	ntrss 7648	Subset relationship for interior.
|- X = U.J   =>   |- ((J e. Top /\ S (_ X /\ T (_ S) -> ((int` J)` T) (_ ((int` J)` S))
Theorem	sscls 7649	A subset of a topology's underlying set is included in its closure.
|- X = U.J   =>   |- ((J e. Top /\ S (_ X) -> S (_ ((cls` J)` S))
Theorem	ntrss2 7650	A subset includes its interior.
|- X = U.J   =>   |- ((J e. Top /\ S (_ X) -> ((int` J)` S) (_ S)
Theorem	clsss3 7651	The closure of a subset of a topological space is included in the space.
|- X = U.J   =>   |- ((J e. Top /\ S (_ X) -> ((cls` J)` S) (_ X)
Theorem	ntrss3 7652	The interior of a subset of a topological space is included in the space.
|- X = U.J   =>   |- ((J e. Top /\ S (_ X) -> ((int` J)` S) (_ X)
Theorem	cmclsopn 7653	The complement of a closure is open.
|- X = U.J   =>   |- ((J e. Top /\ S (_ X) -> (X \ ((cls` J)` S)) e. J)
Theorem	cmntrcld 7654	The complement of an interior is closed.
|- X = U.J   =>   |- ((J e. Top /\ S (_ X) -> (X \ ((int` J)` S)) e. (Clsd` J))
Theorem	iscld3 7655	A subset is closed iff it equals its own closure.
|- X = U.J   =>   |- ((J e. Top /\ S (_ X) -> (S e. (Clsd` J) <-> ((cls` J)` S) =