mmtheorems106 - 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-10687

Statement List for Metamath Proof Explorer - 10501-10600 - Page 106 of 107

Type	Label	Description
Statement
Filters
Syntax	cfil 10501	Extend class notation with the class of all filters.
class Fil
Definition	df-fil 10502	The class of all filters. Bourbaki TG I.36 def. 1 axioms FI, FIIa, FIIb, FIII. This concept is used to define the concept of limit in the general case. The notion was invented by Cartan in 1937 and made famous by Bourbaki in his treatise. A notion similar to the notion of filter is the concept of net invented by Moore and Smith in 1922.
|- Fil = {f | ((-. (/) e. f /\ U.f e. f) /\ A.xA.y((x e. f /\ y (_ U.f /\ x (_ y) -> y e. f) /\ A.x e. f A.y e. f (x i^i y) e. f)}
Theorem	isfil 10503	The predicate "is a filter."
|- X = U.F   =>   |- (F e. A -> (F e. Fil <-> ((-. (/) e. F /\ X e. F) /\ A.xA.y((x e. F /\ y (_ X /\ x (_ y) -> y e. F) /\ A.x e. F A.y e. F (x i^i y) e. F)))
Theorem	filesn 10504	The empty set doesn't belong to a filter.
|- (F e. Fil -> -. (/) e. F)
Theorem	fillsb 10505	A filter is closed under taking supersets.
|- X = U.F   =>   |- (F e. Fil -> ((A e. F /\ B (_ X /\ A (_ B) -> B e. F))
Theorem	filusb 10506	The underlying set belongs to the filter.
|- X = U.F   =>   |- (F e. Fil -> X e. F)
Theorem	filint 10507	A filter is closed under taking intersections.
|- ((F e. Fil /\ A e. F /\ B e. F) -> (A i^i B) e. F)
Theorem	fipfil 10508	The intersection of two elements of a filter can't be empty.
|- (F e. Fil -> ((A e. F /\ B e. F) -> (A i^i B) =/= (/)))
Theorem	fipfil2 10509	A filter has the finite intersection property. Bourbaki TG I.36 note of def. 1.
|- (F e. Fil -> ((A (_ F /\ A =/= (/) /\ E.x e. om A ~~ x) -> |^|A =/= (/)))
Theorem	emnfil 10510	The empty set is not a filter. Bourbaki TG I.36 def 1 note.
|- -. (/) e. Fil
Theorem	oefil2 10511	A singleton is a filter. Bourbaki TG I.36, example 1.
|- ((A e. B /\ A =/= (/)) -> {A} e. Fil)
Theorem	neifil 10512	The neighborhoods of a non empty set is a filter. Bourbaki TG I.36, example 2.
|- X = U.J   =>   |- ((J e. Top /\ S (_ X /\ S =/= (/)) -> ((nei` J)` S) e. Fil)
Theorem	filintf 10513	The intersection of two filters is a filter. Use fiint 4551 to extend this property to the intersection of a finite set of filters. Bourbaki TG I.36 par. 3.
|- ((F e. Fil /\ G e. Fil /\ U.F = U.G) -> (F i^i G) e. Fil)
Theorem	fgsb 10514	Filter generated by a subbasis A. Bourbaki TG I.37 paragraph above prop. 1. The theorem has been slightly modified because the definitions of the empty set are different in Bourbaki and Metamath. )
|- B = {x | E.y(y (_ A /\ E.z e. om y ~~ z /\ x = |^|y)}   =>   |- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> (-. (/) e. B -> {x e. P~X | E.y e. B y (_ x} e. Fil))
Theorem	efilcp 10515	A filter containing a set A exists iff A has the finite intersection property (i.e. no finite intersection of elements of A is empty). Bourbaki TG I.37 prop. 1.
|- B = {z | E.y(y (_ A /\ E.u e. om y ~~ u /\ z = |^|y)}   =>   |- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> (-. (/) e. B <-> E.x e. Fil A (_ x))
Theorem	filint2 10516	A filter is closed under taking finite intersections.
|- (F e. Fil -> ((A (_ F /\ A =/= (/) /\ E.x e. om A ~~ x) -> |^|A e. F))
Theorem	fisub 10517	If a set has the finite intersection property, its subsets have also this property.
|- B = {z | E.y(y (_ A /\ E.u e. om y ~~ u /\ z = |^|y)}   &   |- D = {z | E.y(y (_ C /\ E.u e. om y ~~ u /\ z = |^|y)}   =>   |- (C (_ A -> (-. (/) e. B -> -. (/) e. D))
Theorem	infi 10518	The intersection of two finite intersections is a finite intersection.
|- (C e. D -> ((A e. (fi` C) /\ B e. (fi` C)) -> (A i^i B) e. (fi` C)))
Theorem	fgsb2 10519	Filter generated by a subbasis A. Bourbaki TG I.37 paragraph above prop. 1. (The theorem has been slightly modified because the definitions of the empty set are different in Bourbaki and Metamath.)
|- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> (-. (/) e. (fi` A) -> {x e. P~X | E.y e. (fi` A)y (_ x} e. Fil))
Theorem	efilcp2 10520	A filter containing a set A exists iff A has the finite intersection property (i.e. no finite intersection of elements of A is empty). Bourbaki TG I.37 prop. 1.
|- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> (-. (/) e. (fi` A) <-> E.x e. Fil A (_ x))
Theorem	cnfilca 10521	Condition to have a filter finer than a given filter and containing a set A. Bourbaki T.G. I.37 cor. 1
|- ((F e. Fil /\ A (_ U.F /\ A =/= (/)) -> (E.g e. Fil (A e. g /\ F (_ g) <-> A.x e. F (x i^i A) =/= (/)))
Limits
Syntax	cflim2 10522	Extend class notation with the class of all functions on topologies whose value is a relation between filters and their limits.
class fLim
Definition	df-flim 10523	Define a function on topologies whose value is a relation between filters and their limits.
|- fLim = {<.j, x>. | (j e. Top /\ x = {<.f, y>. | (f e. Fil /\ U.f = U.j /\ ((nei` j)` y) (_ f)})}
Separated spaces: T0, T1, T2 (Hausdorff) ...
Syntax	ct0 10524	Extend class notation to include T0-spaces.
class T0
Syntax	ct1 10525	Extend class notation to include T1-spaces.
class T1
Definition	df-t0 10526	The class of all T0-spaces also called Kolmogorov spaces. Morris. Topology without tears. p. 30 ex. 5.
|- T0 = {x e. Top | A.a e. U.xA.b e. U.xE.u e. x ((a e. u /\ -. b e. u) \/ (-. a e. u /\ b e. u))}
Definition	df-t1 10527	The class of all T1-spaces also called Frechet spaces. Morris. Topology without tears. p. 30 ex. 3.
|- T1 = {x e. Top | A.a e. U.x{a} e. (Clsd` x)}
Theorem	ist1 10528	The predicate J is T1.
|- X = U.J   =>   |- (J e. T1 <-> (J e. Top /\ A.a e. X {a} e. (Clsd` J)))
Theorem	dtopcl 10529	The open sets of a discrete topology are closed and its closed sets are open.
|- A e. V   =>   |- P~A = (Clsd` P~A)
Theorem	t2t1 10530	A Hausdorff space is a T1 space.
|- (J e. Haus -> J e. T1)
Theorem	hst1 10531	A Hausdorff space is a T1 space.
|- Haus (_ T1
Theorem	dtt2 10532	A discrete topology is Hausdorff. Morris. Topology without tears. p.72. ex. 13.
|- A e. V   =>   |- P~A e. Haus
Theorem	dtt1 10533	A discrete topology is T1. Morris. Topology without tears.
|- A e. V   =>   |- P~A e. T1
Connectedness
Syntax	ccon 10534	Extend class notation with the the class of all connected topologies.
class Con
Definition	df-con 10535	Topologies are connected when only (/) and U.j are both open and closed.
|- Con = {j e. Top | (j i^i (Clsd` j)) = {(/), U.j}}
Standard topology on RR
Theorem	clicls 10536	Closed intervals are closed sets of the standard topology on RR.
|- ((A e. RR /\ B e. RR) -> (A[,]B) e. (Clsd` (topGen` ran (,))))
Pre-calculus and Cartesian geometry
Theorem	dmse1 10537	Distance between the middle of a segment and one of its extremities is a positive real.
|- ((A e. RR /\ B e. RR /\ A =/= B) -> ((abs` (A - B)) / 2) e. RR+)
Theorem	dmse2 10538	Distance between the middle of a segment and one of its extremities is a positive real.
|- ((A e. RR /\ B e. RR /\ A < B) -> ((abs` (A - B)) / 2) e. RR+)
Theorem	msr3 10539	The midpoint of a segment AB of the real line is a real.
|- ((A e. RR /\ B e. RR) -> (B - ((abs` (A - B)) / 2)) e. RR)
Theorem	msr4 10540	The midpoint of a segment AB of the real line is a real.
|- ((A e. RR /\ B e. RR) -> (A + ((abs` (B - A)) / 2)) e. RR)
Theorem	ltsubpostb 10541	Translation and inequality on the real line.
|- ((A e. RR /\ B e. RR+) -> (A - B) < A)
Theorem	ltaddpos2tb 10542	Translation and inequality on the real line.
|- ((A e. RR /\ B e. RR+) -> A < (A + B))
Theorem	mslb1 10543	The midpoint of a segment AB of the real line is on the "left" of B.
|- ((A e. RR /\ B e. RR /\ A < B) -> (A + ((abs` (B - A)) / 2)) < B)
Theorem	2wsms 10544	Two ways to state the midpoint of a segment.
|- ((A e. RR /\ B e. RR /\ A < B) -> ((A + B) / 2) = (B - ((abs` (A - B)) / 2)))
Theorem	msra3 10545	The midpoint of a segment AB of the real line is on the "right" of A.
|- ((A e. RR /\ B e. RR /\ A < B) -> A < (B - ((abs` (A - B)) / 2)))
Theorem	iintlem1 10546	Lemma for iint 10548.
Theorem	iintlem2 10547	Lemma for iint 10548.
Theorem	iint 10548	Indexed intersection of a set of open intervals centered on A. This theorem is a rough justification for taking finite intersections in the definition of a topology. If we consider we are in the standard topology of RR this theorem means a non finite intersection of open sets can result in a closed set.
|- (A e. RR -> |^|_x e. RR+ ((A - x)(,)(A + x)) = {A})
Theorem	trdom 10549	Domain of a translation.
|- F = (x e. RR |-> (x + A))   =>   |- (A e. RR -> dom F = RR)
Theorem	trran 10550	Range of a translation.
|- F = (x e. RR |-> (x + A))   =>   |- (A e. RR -> ran F = RR)
Theorem	trnij 10551	A translation is 1-1-onto.
|- F = (x e. RR |-> (x + A))   =>   |- (A e. RR -> F:RR-1-1-onto->RR)
Theorem	cnvtr 10552	Converse of a translation.
|- (A e. RR -> `'(x e. RR |-> (x + A)) = (x e. RR |-> (x - A)))
Standard topology of intervals of RR
Theorem	stoi 10553	The underlying set of the standard topology on an open interval is the open interval itself.
|- <.(A(,)B), (subSp` <.(A(,)B), (topGen` ran (,))>.)>. e. TopSp
Directed multi graphs
Syntax	cmgra 10554	Extend class notation with the class of directed multi graphs.
class Dgra
Definition	df-mgra 10555	Definition of a directed multi graph. Loops are allowed and there may be more than one edge between the same pair of vertices. Isolated points are allowed.
|- Dgra = {<.<.d, c>., u>. | (d:dom d-->u /\ c:dom d-->u)}
Theorem	ismgra 10556	The predicate "is a directed multi graph".
|- ((D e. A /\ C e. B /\ U e. F) -> (<.<.D, C>., U>. e. Dgra <-> (D:dom D-->U /\ C:dom D-->U)))
Category and deductive system underlying "structure"
Syntax	calg 10557	Extend class notation with the class of structures used by Cat and Ded.