mmtheorems81 - 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-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12229

Statement List for Metamath Proof Explorer - 8001-8100 - Page 81 of 123

Type	Label	Description
Statement
Syntax	cbl 8001	Extend class notation with the metric space ball function.
class ball
Syntax	copn 8002	Extend class notation with a function mapping each metric space to the family of its open sets.
class Open
Definition	df-met 8003	Define the (proper) class of all metrics. (A metric space is the metric's base set paired with the metric; see df-ms 8004. However, we will often also call the metric itself a "metric space.") Equivalent to Definition 14-1.1 of [Gleason] p. 223. See ismsg 8010 for the property "is a metric space." The 4 properties in Gleason's definition are shown by met0 8025, metgt0 8030, metsym 8026, and mettri 8027.
|- Met = {x | E.y(x:(y X. y)-->RR /\ A.z e. y A.w e. y (((zxw) = 0 <-> z = w) /\ A.v e. y (zxw) <_ ((vxz) + (vxw))))}
Definition	df-ms 8004	Define the (proper) class of all metric spaces.
|- MetSp = {<.x, y>. | (y e. Met /\ x = dom dom y)}
Definition	df-bl 8005	Define the metric space ball function. See blval 8047 for its value.
|- ball = {<.x, y>. | (x e. Met /\ y = {<.<.z, w>., v>. | ((z e. dom dom x /\ w e. RR) /\ (0 < w /\ v = {u e. dom dom x | (zxu) < w}))})}
Definition	df-opn 8006	Define a function whose value is the family of open sets of a metric space. See isopn 8069 for its main property.
|- Open = {<.x, y>. | (x e. Met /\ y = {z | (z (_ dom dom x /\ A.w e. z E.v e. ran ( ball ` x)(w e. v /\ v (_ z))})}
Theorem	msrel 8007	The class of all metric spaces is a relation.
|- Rel MetSp
Theorem	ismet 8008	Express the predicate "D is a metric."
|- X = dom dom D   =>   |- (D e. A -> (D e. Met <-> (D:(X X. X)-->RR /\ A.x e. X A.y e. X (((xDy) = 0 <-> x = y) /\ A.z e. X (xDy) <_ ((zDx) + (zDy))))))
Theorem	dfms2 8009	Alternate definition for the class of all metric spaces (replaces old version of df-ms 8004).
|- MetSp = {<.x, y>. | (y:(x X. x)-->RR /\ A.z e. x A.w e. x (((zyw) = 0 <-> z = w) /\ A.v e. x (zyw) <_ ((vyz) + (vyw))))}
Theorem	ismsg 8010	Express the predicate "<.X, D>. is a metric space" with underlying set X and distance function D.
|- (D e. A -> (<.X, D>. e. MetSp <-> (D:(X X. X)-->RR /\ A.x e. X A.y e. X (((xDy) = 0 <-> x = y) /\ A.z e. X (xDy) <_ ((zDx) + (zDy))))))
Theorem	ismsi 8011	Properties that determine a metric space.
|- D e. V   &   |- D:(X X. X)-->RR   &   |- ((x e. X /\ y e. X) -> ((xDy) = 0 <-> x = y))   &   |- ((x e. X /\ y e. X /\ z e. X) -> (xDy) <_ ((zDx) + (zDy)))   &   |- M = <.X, D>.   =>   |- M e. MetSp
Theorem	ismeti 8012	Properties that determine a metric.
|- X e. V   &   |- D:(X X. X)-->RR   &   |- ((x e. X /\ y e. X) -> ((xDy) = 0 <-> x = y))   &   |- ((x e. X /\ y e. X /\ z e. X) -> (xDy) <_ ((zDx) + (zDy)))   =>   |- D e. Met
Theorem	msflem 8013	Lemma for msf 8014 and others.
Theorem	msf 8014	Mapping of the distance function of a metric space.
|- X = (1st` M)   &   |- D = (2nd` M)   =>   |- (M e. MetSp -> D:(X X. X)-->RR)
Theorem	mscl 8015	Closure of the distance function of a metric space.
|- X = (1st` M)   &   |- D = (2nd` M)   =>   |- ((M e. MetSp /\ A e. X /\ B e. X) -> (ADB) e. RR)
Theorem	metflem 8016	Lemma for metf 8017 and others.
Theorem	metf 8017	Mapping of the distance function of a metric space.
|- X = dom dom D   =>   |- (D e. Met -> D:(X X. X)-->RR)
Theorem	metdmdm 8018	The base set of a metric space in terms of its distance function.
|- X = dom dom D   =>   |- (D e. Met -> X = dom dom D)
Theorem	metssba 8019	The base set of a metric subspace.
|- X = dom dom D   =>   |- (D e. Met -> (X i^i Y) = dom dom ( D |` (Y X. Y)))
Theorem	metssba2 8020	The base set of a metric subspace.
|- X = dom dom D   =>   |- ((D e. Met /\ Y (_ X) -> Y = dom dom ( D |` (Y X. Y)))
Theorem	metcl 8021	Closure of the distance function of a metric space. Part of Property M1 of [Kreyszig] p. 3.
|- X = dom dom D   =>   |- ((D e. Met /\ A e. X /\ B e. X) -> (ADB) e. RR)
Theorem	meteq0 8022	The value of a metric is zero iff its arguments are equal. Property M2 of [Kreyszig] p. 4.
|- X = dom dom D   =>   |- ((D e. Met /\ A e. X /\ B e. X) -> ((ADB) = 0 <-> A = B))
Theorem	mettri2 8023	Triangle inequality for the distance function of a metric space.
|- X = dom dom D   =>   |- ((D e. Met /\ (C e. X /\ A e. X /\ B e. X)) -> (ADB) <_ ((CDA) + (CDB)))
Theorem	mettri4 8024	Triangle inequality for the distance function of a metric space.
|- X = dom dom D   =>   |- (((D e. Met /\ A e. X) /\ (B e. X /\ C e. X)) -> (ADB) <_ ((CDA) + (CDB)))
Theorem	met0 8025	The distance function of a metric space is zero if its arguments are equal. Definition 14-1.1(a) of [Gleason] p. 223.
|- X = dom dom D   =>   |- ((D e. Met /\ A e. X) -> (ADA) = 0)
Theorem	metsym 8026	The distance function of a metric space is symmetric. Definition 14-1.1(c) of [Gleason] p. 223.
|- X = dom dom D   =>   |- ((D e. Met /\ A e. X /\ B e. X) -> (ADB) = (BDA))
Theorem	mettri 8027	Triangle inequality for the distance function of a metric space. Definition 14-1.1(d) of [Gleason] p. 223.
|- X = dom dom D   =>   |- ((D e. Met /\ (A e. X /\ B e. X /\ C e. X)) -> (ADB) <_ ((ADC) + (CDB)))
Theorem	mettri3 8028	Triangle inequality for the distance function of a metric space.
|- X = dom dom D   =>   |- ((D e. Met /\ (A e. X /\ B e. X /\ C e. X)) -> (ADB) <_ ((ADC) + (BDC)))
Theorem	metge0 8029	The distance function of a metric space is nonnegative.
|- X = dom dom D   =>   |- ((D e. Met /\ A e. X /\ B e. X) -> 0 <_ (ADB))
Theorem	metgt0 8030	The distance function of a metric space is positive for unequal points. Definition 14-1.1(b) of [Gleason] p. 223 and its converse.
|- X = dom dom D   =>   |- ((D e. Met /\ A e. X /\ B e. X) -> (A =/= B <-> 0 < (ADB)))
Theorem	metn0 8031	A metric space is nonempty iff its base set is nonempty.
|- X = dom dom D   =>   |- (D e. Met -> (D =/= (/) <-> X =/= (/)))
Theorem	metreslem 8032	Lemma for metres 8033. (Contributed by FL, 10-Nov-2006.)
Theorem	metres 8033	A restriction of a metric is a metric.
|- (D e. Met -> (D |` (R X. R)) e. Met)
Theorem	metss 8034	If two metrics are in a subset relationship, so are their base sets.
|- X = dom dom C   &   |- Y = dom dom D   =>   |- (C (_ D -> X (_ Y)
Theorem	0met 8035	The empty metric.
|- (/) e. Met
Theorem	metxplem1 8036	Lemma for metxp 8044.
Theorem	metxplem2 8037	Lemma for metxp 8044.
Theorem	metxplem3 8038	Lemma for metxp 8044.
Theorem	metxpdval 8039	Value of the distance function of the direct product of two metric spaces. Based on Definition 14-1.5 of [Gleason] p. 225.
|- X = dom dom B   &   |- Y = dom dom C   &   |- B e. Met   &   |- C e. Met   &   |- D = {<.<.x, y>., z>. | ((x e. (X X. Y) /\ y e. (X X. Y)) /\ z = sup({((1st` x)B(1st` y)), ((2nd` x)C(2nd` y))}, RR, < ))}   &   |- F = (1st` R)   &   |- G = (2nd` R)   &   |- H = (1st` S)   &   |- J = (2nd` S)   =>   |- ((R e. (X X. Y) /\ S e. (X X. Y)) -> (RDS) = if((GCJ) < (FBH), (FBH), (GCJ)))
Theorem	metxptval 8040	One case of the value of the distance function of the direct product of two metric spaces. Based on Definition 14-1.5 of [Gleason] p. 225.
|- X = dom dom B   &   |- Y = dom dom C   &   |- B e. Met   &   |- C e. Met   &   |- D = {<.<.x, y>., z>. | ((x e. (X X. Y) /\ y e. (X X. Y)) /\ z = sup({((1st` x)B(1st` y)), ((2nd` x)C(2nd` y))}, RR, < ))}   &   |- F = (1st` R)   &   |- G = (2nd` R)   &   |- H = (1st` S)   &   |- J = (2nd` S)   =>   |- (((R e. (X X. Y) /\ S e. (X X. Y)) /\ (GCJ) <_ (FBH)) -> (RDS) = (FBH))
Theorem	metxpfval 8041	One case of the value of the distance function of the direct product of two metric spaces. Based on Definition 14-1.5 of [Gleason] p. 225.
|- X = dom dom B   &   |- Y = dom dom C   &   |- B e. Met   &   |- C e. Met   &   |- D = {<.<.x, y>., z>. | ((x e. (X X. Y) /\ y e. (X X. Y)) /\ z = sup({((1st` x)B(1st` y)), ((2nd` x)C(2nd` y))}, RR, < ))}   &   |- F = (1st` R)   &   |- G = (2nd` R)   &   |- H = (1st` S)   &   |- J = (2nd` S)   =>   |- (((R e. (X X. Y) /\ S e. (X X. Y)) /\ (FBH) <_ (GCJ)) -> (RDS) = (GCJ))
Theorem	metxpcl 8042	Closure of the distance function of the direct product of two metric spaces. Based on Definition 14-1.5 of [Gleason] p. 225.
|- X = dom dom B   &   |- Y = dom dom C   &   |- B e. Met   &   |- C e. Met   &   |- D = {<.<.x, y>., z>. | ((x e. (X X. Y) /\ y e. (X X. Y)) /\ z = sup({((1st` x)B(1st` y)), ((2nd` x)C(2nd` y))}, RR, < ))}   =>   |- ((R e. (X X. Y) /\ S e. (X X. Y)) -> (RDS) e. RR)
Theorem	metxplem4 8043	Lemma for metxp 8044. Triangle inequality. Warning: The HTML proof page is 0.6 megabyte in size.
Theorem	metxp 8044	The direct product of two metric spaces. Definition 14-1.5 of [Gleason] p. 225.
|- X = dom dom B   &   |- Y = dom dom C   &   |- B e. Met   &   |- C e. Met   &   |- D = {<.<.x, y>., z>. | ((x e. (X X. Y) /\ y e. (X X. Y)) /\ z = sup({((1st` x)B(1st` y)), ((2nd` x)C(2nd` y))}, RR, < ))}   =>   |- D e. Met
Metric space balls
Theorem	blfval 8045	The value of the ball function.
|- X = dom dom D   =>   |- (D e. Met -> ( ball ` D) = {<.<.x, y>., z>. | ((x e. X /\ y e. RR) /\ (0 < y /\ z = {w e. X | (xDw) < y}))})
Theorem	blfval2 8046	Alternate value of the ball function that simplifies its use with operation theorems.
|- X = dom dom D   =>   |- (D e. Met -> ( ball ` D) = {<.<.x, y>., z>. | ((x e. X /\ y e. {v e. RR | 0 < v}) /\ z = {w e. X | (xDw) < y})})
Theorem	blval 8047	The ball around a point P is the set of all points whose distance from P is less than the ball's radius R.
|- X = dom dom D   =>   |- (((D e. Met /\ P e. X) /\ (R e. RR /\ 0 < R)) -> (P( ball ` D)R) = {x e. X | (PDx) < R})
Theorem	elbl 8048	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 8049	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 8050	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 8051	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 8052	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 8053	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 8054	Mapping of a ball.
|- X = dom dom D   =>   |- (D e. Met -> ( ball ` D):(X X. (0(,) +oo))-->P~X)
Theorem	blcntr 8055	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	bln0 8056	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 8057	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 8058	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 8059	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 8060	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 8061	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 8062	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 8063	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 8064	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 8065	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 8066	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 8067	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 8080, the open sets of a metric space form a topology J, whose base set is U.J by uniopn2 8071.
|- 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 8068	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 8069	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 8070	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	uniopn2 8071	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 8072	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 8073	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 8074	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 8075	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 8076	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 8077	The balls of a metric space are open sets.
|- J = (Open` D)   =>   |- (D e. Met -> ran ( ball ` D) (_ J)
Theorem	opnuni 8078	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 8079	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 8080	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 8081	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 8082	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 8083	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 8084	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 8085	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 8086	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 8087	A neighborhood of a point defined in terms of balls.
|- X = dom dom D   &   |- J = (Open` D)   =>   |- ((D e. Met /\ P e. X) -> (N e. ((nei` J)` {P}) <-> (N (_ X /\ E.r e. RR (0 < r /\ (P( ball ` D)r) (_ N))))
Theorem	metnei 8088	The neighborhoods around a point P of a metric space are those subsets containing a ball around P. Definition of neighborhood in [Kreyszig] p. 19.
|- X = dom dom D   &   |- J = (Open` D)   =>   |- ((D e. Met /\ P e. X) -> ((nei` J)` {P}) = {x | (x (_ X /\ E.r e. RR (0 < r /\ (P( ball ` D)r) (_ x))})
Theorem	blnei 8089	A ball around a point is a neighborhood of the point.
|- X = dom dom D   &   |- J = (Open` D)   =>   |- (((D e. Met /\ P e. X) /\ (R e. RR /\ 0 < R)) -> (P( ball ` D)R) e. ((nei` J)` {P}))
Theorem	lpbl 8090	Every ball around a limit point P of a subset S includes a member of S (even if P e/ S).
|- X = dom dom D   &   |- J = (Open` D)   =>   |- (((D e. Met /\ S (_ X /\ P e. ((limPt` J)` S)) /\ (R e. RR /\ 0 < R)) -> E.x e. S x e. (P( ball ` D)R))
Theorem	metequiv 8091	Two ways of saying that two metrics generate the same topology. Two metrics satisfying the right-hand side are said to be (topologically) equivalent. (Contributed by Jeffrey Hankins, 21-Jun-2009.)
|- X = dom dom C   &   |- Y = dom dom D   &   |- J = (Open` C)   &   |- K = (Open` D)   =>   |- ((C e. Met /\ D e. Met) -> (J = K <-> (X = Y /\ A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) (_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) (_ (x( ball ` D)s)))))))
Theorem	methausi 8092	The topology generated by a metric space is Hausdorff. Remark in [Munkres] p. 126.
|- D e. Met   &   |- J = (Open` D)   =>   |- J e. Haus
Theorem	methaus 8093	The topology generated by a metric space is Hausdorff. Remark in [Munkres] p. 126.
|- J = (Open` D)   =>   |- (D e. Met -> J e. Haus)
Continuity in metric spaces
Theorem	metcnpf 8094	A continuous function at point P is a mapping (metric space version of cnpf 7973).
|- X = dom dom C   &   |- Y = dom dom D   &   |- J = (Open` C)   &   |- K = (Open` D)   =>   |- (((C e. Met /\ D e. Met /\ P e. X) /\ F e. ((J CnP K)` P)) -> F:X-->Y)
Theorem	metcnf 8095	A continuous function is a mapping (metric space version of cnf 7972).
|- X = dom dom C   &   |- Y = dom dom D   &   |- J = (Open` C)   &   |- K = (Open` D)   =>   |- ((C e. Met /\ D e. Met /\ F e. (J Cn K)) -> F:X-->Y)
Theorem	metcnconst 8096	A constant function is continuous (metric space version of cnconst 7990).
|- X = dom dom C   &   |- Y = dom dom D   &   |- J = (Open` C)   &   |- K = (Open` D)   =>   |- (((C e. Met /\ D e. Met) /\ (B e. Y /\ F:X-->{B})) -> F e. (J Cn K))
Theorem	metcnplem 8097	Lemma for metcnp 8098.
Theorem	metcnp 8098	Two ways to say a mapping from metric C to metric D is continuous at point P. Warning: The HTML proof page is 0.6 megabyte in size.
|- X = dom dom C   &   |- J = (Open` C)   &   |- Y = dom dom D   &   |- K = (Open` D)   =>   |- ((C e. Met /\ D e. Met /\ P e. X) -> (F e. ((J CnP K)` P) <-> (F:X-->Y /\ A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. X ((PCw) < z -> ((F` P)D(F` w)) < y))))))
Theorem	metcnp2 8099	Two ways to say a mapping from metric C to metric D is continuous at point P. The distance arguments are swapped compared to metcnp 8098 (and Munkres' metcn 8100) for compatibility with df-lm 8133. Definition 1.3-3 of [Kreyszig] p. 20.
|- X = dom dom C   &   |- J = (Open` C)   &   |- Y = dom dom D   &   |- K = (Open` D)   =>   |- ((C e. Met /\ D e. Met /\ P e. X) -> (F e. ((J CnP K)` P) <-> (F:X-->Y /\ A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. X ((wCP) < z -> ((F` w)D(F` P)) < y))))))
Theorem	metcn 8100	Two ways to say a mapping from metric C to metric D is continuous. Theorem 10.1 of [Munkres] p. 127. The second biconditional argument says that for every positive "epsilon" y there is a positive "delta" z such that a distance less than delta in C maps to a distance less than epsilon in D.
|- X = dom dom C   &   |- J = (Open` C)   &   |- Y = dom dom D   &   |- K = (Open` D)   =>   |- ((C e. Met /\ D e. Met) -> (F e. (J Cn K) <-> (F:X-->Y /\ A.x e. X A.y e. RR (0 < y -> E.z e. RR (0 < z /\ A.w e. X ((xCw) < z -> ((F` x)D(F` w)) < y))))))