mmtheorems79 - 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 - 7801-7900 - Page 79 of 107

Type	Label	Description
Statement
Theorem	elbl 7801	Membership in a ball.
|- X = dom dom D   =>   |- (((D e. Met /\ P e. X) /\ (R e. RR /\ 0 < R)) -> (A e. (P( ball ` D)R) <-> (A e. X /\ (PDA) < R)))
Theorem	elbl2 7802	Membership in a ball.
|- X = dom dom D   =>   |- (((D e. Met /\ P e. X /\ A e. X) /\ (R e. RR /\ 0 < R)) -> (A e. (P( ball ` D)R) <-> (PDA) < R))
Theorem	elbl3 7803	Membership in a ball, with reversed distance function arguments.
|- X = dom dom D   =>   |- (((D e. Met /\ P e. X /\ A e. X) /\ (R e. RR /\ 0 < R)) -> (A e. (P( ball ` D)R) <-> (ADP) < R))
Theorem	blrn 7804	Membership in the range of the ball function. Note that ran ( ball ` D) is the collection of all balls for metric D.
|- X = dom dom D   =>   |- (D e. Met -> (B e. ran ( ball ` D) <-> E.x e. X E.y e. {w e. RR | 0 < w}B = {z e. X | (xDz) < y}))
Theorem	blrn2 7805	Membership in the range of the ball function. Note that ran ( ball ` D) is the collection of all balls for metric D.
|- X = dom dom D   =>   |- (D e. Met -> (B e. ran ( ball ` D) <-> E.x e. X E.y e. RR (0 < y /\ B = {z e. X | (xDz) < y})))
Theorem	bl2in 7806	Two balls are disjoint if they don't overlap.
|- X = dom dom D   =>   |- (((D e. Met /\ P e. X /\ Q e. X) /\ (R e. RR /\ 0 < R /\ R <_ ((PDQ) / 2))) -> ((P( ball ` D)R) i^i (Q( ball ` D)R)) = (/))
Theorem	blf 7807	Mapping of a ball.
|- X = dom dom D   =>   |- (D e. Met -> ( ball ` D):(X X. (0(,) +oo))-->P~X)
Theorem	blcntr 7808	A ball contains its center.
|- X = dom dom D   =>   |- (((D e. Met /\ P e. X) /\ (R e. RR /\ 0 < R)) -> P e. (P( ball ` D)R))
Theorem	blne0 7809	A ball is not empty.
|- X = dom dom D   =>   |- (((D e. Met /\ P e. X) /\ (R e. RR /\ 0 < R)) -> (P( ball ` D)R) =/= (/))
Theorem	blrn3 7810	Membership in the range of the ball function. Note that ran ( ball ` D) is the collection of all balls for metric D.
|- X = dom dom D   =>   |- (D e. Met -> (A e. ran ( ball ` D) <-> E.x e. X E.y e. RR (0 < y /\ A = (x( ball ` D)y))))
Theorem	blelrn 7811	A ball belongs to the set of balls of a metric space.
|- X = dom dom D   =>   |- (((D e. Met /\ P e. X) /\ (R e. RR /\ 0 < R)) -> (P( ball ` D)R) e. ran ( ball ` D))
Theorem	blex 7812	Any point in a metric space has a ball around it.
|- X = dom dom D   =>   |- ((D e. Met /\ P e. X) -> E.x e. ran ( ball ` D)P e. x)
Theorem	blssm 7813	A ball is a subset of the base set of a metric space.
|- X = dom dom D   =>   |- (((D e. Met /\ P e. X) /\ (R e. RR /\ 0 < R)) -> (P( ball ` D)R) (_ X)
Theorem	rnblssm 7814	A ball is a subset of the base set of a metric space.
|- X = dom dom D   =>   |- ((D e. Met /\ B e. ran ( ball ` D)) -> B (_ X)
Theorem	blin 7815	The intersection of two balls with the same center is the smaller of them.
|- X = dom dom D   =>   |- (((D e. Met /\ P e. X) /\ (R e. RR /\ 0 < R) /\ (S e. RR /\ 0 < S)) -> ((P( ball ` D)R) i^i (P( ball ` D)S)) = (P( ball ` D)if(R <_ S, R, S)))
Theorem	blss 7816	Any point P in a ball B can be centered in another ball that is a subset of B.
|- ((D e. Met /\ B e. ran ( ball ` D) /\ P e. B) -> E.x e. RR (0 < x /\ (P( ball ` D)x) (_ B))
Theorem	blssex 7817	Two ways to express the existence of a ball subset.
|- X = dom dom D   =>   |- ((D e. Met /\ P e. X) -> (E.x e. ran ( ball ` D)(P e. x /\ x (_ A) <-> E.y e. RR (0 < y /\ (P( ball ` D)y) (_ A)))
Theorem	ssbl 7818	The size of a ball increases monotonically with its radius.
|- X = dom dom D   =>   |- ((((D e. Met /\ P e. X) /\ (R e. RR /\ 0 < R) /\ (S e. RR /\ 0 < S)) /\ R <_ S) -> (P( ball ` D)R) (_ (P( ball ` D)S))
Theorem	ssblex 7819	A nested ball exists whose radius is less than any desired amount.
|- X = dom dom D   =>   |- (((D e. Met /\ P e. X) /\ (R e. RR /\ 0 < R) /\ (S e. RR /\ 0 < S)) -> E.x e. RR (0 < x /\ x < R /\ (P( ball ` D)x) (_ (P( ball ` D)S)))
Open sets of a metric space
Theorem	opnfval 7820	An open set is a subset of a metric space which includes a ball around each of its points. Definition 1.3-2 of [Kreyszig] p. 18. The object (Open` D) is the family of all open sets in the metric space determined by the metric D. By opntop 7833, the open sets of a metric space form a topology J, whose base set is U.J by uniopn 7824.
|- X = dom dom D   &   |- J = (Open` D)   =>   |- (D e. Met -> J = {x | (x (_ X /\ A.y e. x E.z e. ran ( ball ` D)(y e. z /\ z (_ x))})
Theorem	opnfss 7821	The family of open sets of a metric space is a collection of subsets of the base set.
|- X = dom dom D   &   |- J = (Open` D)   =>   |- (D e. Met -> J (_ P~X)
Theorem	isopn 7822	The defining property of an open set of a metric space.
|- X = dom dom D   &   |- J = (Open` D)   =>   |- (D e. Met -> (A e. J <-> (A (_ X /\ A.x e. A E.y e. ran ( ball ` D)(x e. y /\ y (_ A))))
Theorem	opnm 7823	The base set of a metric space is open. Part of Theorem T1 of [Kreyszig] p. 19.
|- X = dom dom D   &   |- J = (Open` D)   =>   |- (D e. Met -> X e. J)
Theorem	uniopn 7824	The union of all open sets in a metric space is its underlying set.
|- X = dom dom D   &   |- J = (Open` D)   =>   |- (D e. Met -> U.J = X)
Theorem	isopn4 7825	A defining property of an open set of a metric space.
|- X = dom dom D   &   |- J = (Open` D)   =>   |- (D e. Met -> (A e. J <-> (A (_ X /\ A.x e. A E.y e. RR (0 < y /\ (x( ball ` D)y) (_ A))))
Theorem	opnss 7826	An open set of a metric space is a subspace of its base set.
|- X = dom dom D   &   |- J = (Open` D)   =>   |- ((D e. Met /\ A e. J) -> A (_ X)
Theorem	opni 7827	An open set of a metric space includes a ball around each of its points.
|- J = (Open` D)   =>   |- ((D e. Met /\ A e. J /\ P e. A) -> E.x e. ran ( ball ` D)(P e. x /\ x (_ A))
Theorem	opni2 7828	An open set of a metric space includes a ball around each of its points.
|- J = (Open` D)   =>   |- ((D e. Met /\ A e. J /\ P e. A) -> E.x e. RR (0 < x /\ (P( ball ` D)x) (_ A))
Theorem	opni3 7829	An open set of a metric space includes an arbitrarily small ball around each of its points.
|- J = (Open` D)   =>   |- (((D e. Met /\ A e. J /\ P e. A) /\ (R e. RR /\ 0 < R)) -> E.x e. RR (0 < x /\ x < R /\ (P( ball ` D)x) (_ A))
Theorem	blssopn 7830	The balls of a metric space are open sets.
|- J = (Open` D)   =>   |- (D e. Met -> ran ( ball ` D) (_ J)
Theorem	opnuni 7831	The union of a collection of open sets of a metric space is open. Theorem T2 of [Kreyszig] p. 19.
|- J = (Open` D)   =>   |- ((D e. Met /\ A (_ J) -> U.A e. J)
Theorem	opnin 7832	The intersection of two open sets of a metric space is open.
|- J = (Open` D)   =>   |- ((D e. Met /\ A e. J /\ B e. J) -> (A i^i B) e. J)
Theorem	opntop 7833	The set of open sets of a metric space is a topology. Remark in [Kreyszig] p. 19. This theorem connects the two concepts and makes available the theorems for topologies for use with metric spaces.
|- J = (Open` D)   =>   |- (D e. Met -> J e. Top)
Theorem	tgbl 7834	The topology generated by the balls of a metric space is its open sets.
|- J = (Open` D)   =>   |- (D e. Met -> (topGen` ran ( ball ` D)) = J)
Theorem	blbas 7835	The balls of a metric space form a basis for a topology.
|- J = (Open` D)   =>   |- (D e. Met -> ran ( ball ` D) e. Bases)
Theorem	opn0 7836	The empty set is an open set of a metric space. Part of Theorem T1 of [Kreyszig] p. 19.
|- J = (Open` D)   =>   |- (D e. Met -> (/) e. J)
Theorem	rnblopn 7837	A ball of a metric space is an open set.
|- J = (Open` D)   =>   |- ((D e. Met /\ B e. ran ( ball ` D)) -> B e. J)
Theorem	unirnbl 7838	The union of the set of balls of a metric space is its base set.
|- X = dom dom D   =>   |- (D e. Met -> U.ran ( ball ` D) = X)
Theorem	blopn 7839	A ball of a metric space is an open set.
|- X = dom dom D   &   |- J = (Open` D)   =>   |- (((D e. Met /\ P e. X) /\ (R e. RR /\ 0 < R)) -> (P( ball ` D)R) e. J)
Theorem	neibl 7840	A neighborhood of a point defined in terms of balls.
|- X = dom dom D   &   |- J = (Open` D)   =>   |-