mmtheorems107 - 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 - 10601-10700 - Page 107 of 108

Type	Label	Description
Statement
Syntax	cflim2 10601
class fLim2
Definition	df-flim1OLD 10602	Define a function (indexed by a topology x) whose value is the limits of a filter a.
|- fLim1OLD = {<.x, y>. | (x e. Top /\ y = {<.a, b>. | (a e. (Fil i^i P~P~U.x) /\ b = {l e. U.x | ((nei` x)` {l}) (_ a})})}
Definition	df-flim1 10603
|- fLim1 = {<.x, y>. | (x e. Top /\ y = {<.a, b>. | (a e. Fil /\ U.a = U.x /\ b = {l e. U.x | ((nei` x)` {l}) (_ a})})}
Definition	df-flim2 10604	Define a function (indexed by a topology x and a filter y) whose values are the limits of a function a.
|- fLim2 = {<.<.x, y>., z>. | (x e. Top /\ y e. Fil /\ z = {<.a, b>. | (a:U.y-->U.x /\ b = {l | ((nei` x)` l) (_ (a"y)})})}
Theorem	sfvlim 10605	Functions whose values are the limits of the filters.
|- X = U.J   =>   |- (J e. Top -> (fLim1` J) = {<.a, b>. | (a e. Fil /\ U.a = X /\ b = {l e. X | ((nei` J)` {l}) (_ a})})
Theorem	sfvlimOLD 10606	Functions whose values are the limits of the filters.
|- X = U.J   =>   |- (J e. Top -> (fLim1OLD` J) = {<.a, b>. | (a e. (Fil i^i P~P~X) /\ b = {l e. X | ((nei` J)` {l}) (_ a})})
Theorem	limfillem1OLD 10607	The limits of a filter on X.
|- J e. Top   &   |- X = U.J   =>   |- (F e. (Fil i^i P~P~X) -> ((fLim1OLD` J)` F) = {l e. X | ((nei` J)` {l}) (_ F})
Theorem	limfillem2OLD 10608	The limits of a filter on X.
|- X = U.J   =>   |- ((J e. Top /\ F e. (Fil i^i P~P~X)) -> ((fLim1OLD` J)` F) = {l e. X | ((nei` J)` {l}) (_ F})
Theorem	plimfilOLD 10609	The predicate "is a limit of a filter".
|- X = U.J   =>   |- ((J e. Top /\ F e. (Fil i^i P~P~X) /\ L e. X) -> (L e. ((fLim1OLD` J)` F) <-> ((nei` J)` {L}) (_ F))
Separated spaces: T0, T1, T2 (Hausdorff) ...
Syntax	ct0 10610	Extend class notation to include T0-spaces.
class T0
Syntax	ct1 10611	Extend class notation to include T1-spaces.
class T1
Definition	df-t0 10612	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 10613	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 10614	The predicate J is T1.
|- X = U.J   =>   |- (J e. T1 <-> (J e. Top /\ A.a e. X {a} e. (Clsd` J)))
Theorem	dtopcl 10615	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 10616	A Hausdorff space is a T1 space.
|- (J e. Haus -> J e. T1)
Theorem	hst1 10617	A Hausdorff space is a T1 space.
|- Haus (_ T1
Theorem	dtt2 10618	A discrete topology is Hausdorff. Morris. Topology without tears. p.72. ex. 13.
|- A e. V   =>   |- P~A e. Haus
Theorem	dtt1 10619	A discrete topology is T1. Morris. Topology without tears.
|- A e. V   =>   |- P~A e. T1
Connectedness
Syntax	ccon 10620	Extend class notation with the the class of all connected topologies.
class Con
Definition	df-con 10621	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 10622	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 10623	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 10624	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 10625	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 10626	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 10627	Translation and inequality on the real line.
|- ((A e. RR /\ B e. RR+) -> (A - B) < A)
Theorem	ltaddpos2tb 10628	Translation and inequality on the real line.
|- ((A e. RR /\ B e. RR+) -> A < (A + B))
Theorem	mslb1 10629	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 10630	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 10631	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 10632	Lemma for iint 10634.
Theorem	iintlem2 10633	Lemma for iint 10634.
Theorem	iint 10634	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 10635	Domain of a translation.
|- F = (x e. RR |-> (x + A))   =>   |- (A e. RR -> dom F = RR)
Theorem	trran 10636	Range of a translation.
|- F = (x e. RR |-> (x + A))   =>   |- (A e. RR -> ran F = RR)
Theorem	trnij 10637	A translation is 1-1-onto.
|- F = (x e. RR |-> (x + A))   =>   |- (A e. RR -> F:RR-1-1-onto->RR)
Theorem	cnvtr 10638	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 10639	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 10640	Extend class notation with the class of directed multi graphs.
class Dgra
Definition	df-mgra 10641	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 10642	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 10643	Extend class notation with the class of structures used by Cat and Ded.
class Alg
Syntax	cdom_ 10644	Extend class notation with the function returning the function domain of a category.
class dom
Syntax	ccod_ 10645	Extend class notation with the function returning the function codomain of a category.
class cod
Syntax	cid_ 10646	Extend class notation with the function returning the function identity of a category.
class id
Syntax	co_ 10647	Extend class notation with the function returning the composition of morphisms of a category.
class o
Definition	df-alg 10648	Ded and Cat underlying structure. Metamath for internal reasons doesn't like too large definitions. Then Cat has been splitted giving birth to Ded and Alg. If Ded has a real mathematical use, Alg is only here to give relief to Metamath.
|- Alg = {x | E.dE.cE.jE.r(x = <.<.d, c>., <.j, r>.>. /\ (d:dom d-->dom j /\ c:dom d-->dom j /\ j:dom j-->dom d) /\ (Fun r /\ dom r (_ (dom d X. dom d) /\ ran r (_ dom d))}
Definition	df-doma 10649	Definition of dom.
|- dom = (1st o. 1st)
Definition	df-coda 10650	Definition of cod.
|- cod = (2nd o. 1st)
Definition	df-ida 10651	Definition of id.
|- id = (1st o. 2nd)
Definition	df-cmpa 10652	Definition of o.
|- o = (2nd o. 2nd)
Theorem	isalg 10653	The predicate "has the structure required by Alg and Ded."
|- M = dom D   &   |- O = dom J   =>   |- (((D e. A /\ C e. B /\ J e. F) /\ R e. G) -> (<.<.D, C>., <.J, R>.>. e. Alg <-> ((D:M-->O /\ C:M-->O /\ J:O-->M) /\ (Fun R /\ dom R (_ (M X. M) /\ ran R (_ M))))
Theorem	1alg 10654	Category 1 has the structure required by Ded and Alg.
|- A e. V   =>   |- <.<.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>., <.{<.A, <.A, A>.>.}, {<.<.<.A, A>., <.A, A>.>., <.A, A>.>.}>.>. e. Alg
Theorem	domval 10655	Value of the domain function expressed with the 1st function.
|- D = (dom` T)   =>   |- D = (1st` (1st` T))
Theorem	codval 10656	Value of the function codomain expressed with the 1st and 2nd functions.
|- C = (cod` T)   =>   |- C = (2nd` (1st` T))
Theorem	idval 10657	Value of the identity function expressed with the 1st and 2nd functions.
|- J = (id` T)   =>   |- J = (1st` (2nd` T))
Theorem