P. 224 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 22301-22400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	unimopn 22301	The union of a collection of open sets of a metric space is open. Theorem T2 of [Kreyszig] p. 19. (Contributed by NM, 4-Sep-2006.) (Revised by Mario Carneiro, 23-Dec-2013.)
|- J = ( MetOpen ` D )   =>    |- ( ( D e. ( *Met ` X ) /\ A C_ J ) -> U. A e. J )
Theorem	mopnin 22302	The intersection of two open sets of a metric space is open. (Contributed by NM, 4-Sep-2006.) (Revised by Mario Carneiro, 23-Dec-2013.)
|- J = ( MetOpen ` D )   =>    |- ( ( D e. ( *Met ` X ) /\ A e. J /\ B e. J ) -> ( A i^i B ) e. J )
Theorem	mopn0 22303	The empty set is an open set of a metric space. Part of Theorem T1 of [Kreyszig] p. 19. (Contributed by NM, 4-Sep-2006.)
|- J = ( MetOpen ` D )   =>    |- ( D e. ( *Met ` X ) -> (/) e. J )
Theorem	rnblopn 22304	A ball of a metric space is an open set. (Contributed by NM, 12-Sep-2006.)
|- J = ( MetOpen ` D )   =>    |- ( ( D e. ( *Met ` X ) /\ B e. ran ( ball ` D ) ) -> B e. J )
Theorem	blopn 22305	A ball of a metric space is an open set. (Contributed by NM, 9-Mar-2007.) (Revised by Mario Carneiro, 12-Nov-2013.)
|- J = ( MetOpen ` D )   =>    |- ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( P ( ball ` D ) R ) e. J )
Theorem	neibl 22306*	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. (Contributed by NM, 8-Nov-2007.) (Revised by Mario Carneiro, 23-Dec-2013.)
|- J = ( MetOpen ` D )   =>    |- ( ( D e. ( *Met ` X ) /\ P e. X ) -> ( N e. ( ( nei ` J ) ` { P } ) <-> ( N C_ X /\ E. r e. RR+ ( P ( ball ` D ) r ) C_ N ) ) )
Theorem	blnei 22307	A ball around a point is a neighborhood of the point. (Contributed by NM, 8-Nov-2007.) (Revised by Mario Carneiro, 24-Aug-2015.)
|- J = ( MetOpen ` D )   =>    |- ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR+ ) -> ( P ( ball ` D ) R ) e. ( ( nei ` J ) ` { P } ) )
Theorem	lpbl 22308*	Every ball around a limit point P of a subset S includes a member of S (even if P e/ S). (Contributed by NM, 9-Nov-2007.) (Revised by Mario Carneiro, 23-Dec-2013.)
|- J = ( MetOpen ` D )   =>    |- ( ( ( D e. ( *Met ` X ) /\ S C_ X /\ P e. ( ( limPt ` J ) ` S ) ) /\ R e. RR+ ) -> E. x e. S x e. ( P ( ball ` D ) R ) )
Theorem	blsscls2 22309*	A smaller closed ball is contained in a larger open ball. (Contributed by Mario Carneiro, 10-Jan-2014.)
|- J = ( MetOpen ` D )   &    |- S = { z e. X | ( P D z ) <_ R }   =>    |- ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR* /\ T e. RR* /\ R < T ) ) -> S C_ ( P ( ball ` D ) T ) )
Theorem	blcld 22310*	A "closed ball" in a metric space is actually closed. (Contributed by Mario Carneiro, 31-Dec-2013.) (Revised by Mario Carneiro, 24-Aug-2015.)
|- J = ( MetOpen ` D )   &    |- S = { z e. X | ( P D z ) <_ R }   =>    |- ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> S e. ( Clsd ` J ) )
Theorem	blcls 22311*	The closure of an open ball in a metric space is contained in the corresponding closed ball. (Equality need not hold; for example, with the discrete metric, the closed ball of radius 1 is the whole space, but the open ball of radius 1 is just a point, whose closure is also a point.) (Contributed by Mario Carneiro, 31-Dec-2013.)
|- J = ( MetOpen ` D )   &    |- S = { z e. X | ( P D z ) <_ R }   =>    |- ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( ( cls ` J ) ` ( P ( ball ` D ) R ) ) C_ S )
Theorem	blsscls 22312	If two concentric balls have different radii, the closure of the smaller one is contained in the larger one. (Contributed by Mario Carneiro, 5-Jan-2014.)
|- J = ( MetOpen ` D )   =>    |- ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* /\ R < S ) ) -> ( ( cls ` J ) ` ( P ( ball ` D ) R ) ) C_ ( P ( ball ` D ) S ) )
Theorem	metss 22313*	Two ways of saying that metric D generates a finer topology than metric C. (Contributed by Mario Carneiro, 12-Nov-2013.) (Revised by Mario Carneiro, 24-Aug-2015.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) -> ( J C_ K <-> A. x e. X A. r e. RR+ E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) ) )
Theorem	metequiv 22314*	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 Jeff Hankins, 21-Jun-2009.) (Revised by Mario Carneiro, 12-Nov-2013.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) -> ( J = K <-> A. x e. X ( A. r e. RR+ E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) /\ A. a e. RR+ E. b e. RR+ ( x ( ball ` C ) b ) C_ ( x ( ball ` D ) a ) ) ) )
Theorem	metequiv2 22315*	If there is a sequence of radii approaching zero for which the balls of both metrics coincide, then the generated topologies are equivalent. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) -> ( A. x e. X A. r e. RR+ E. s e. RR+ ( s <_ r /\ ( x ( ball ` C ) s ) = ( x ( ball ` D ) s ) ) -> J = K ) )
Theorem	metss2lem 22316*	Lemma for metss2 22317. (Contributed by Mario Carneiro, 14-Sep-2015.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   &    |- ( ph -> C e. ( Met ` X ) )   &    |- ( ph -> D e. ( Met ` X ) )   &    |- ( ph -> R e. RR+ )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x C y ) <_ ( R x. ( x D y ) ) )   =>    |- ( ( ph /\ ( x e. X /\ S e. RR+ ) ) -> ( x ( ball ` D ) ( S / R ) ) C_ ( x ( ball ` C ) S ) )
Theorem	metss2 22317*	If the metric D is "strongly finer" than C (meaning that there is a positive real constant R such that C ( x , y ) <_ R x. D ( x , y )), then D generates a finer topology. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then they generate the same topology.) (Contributed by Mario Carneiro, 14-Sep-2015.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   &    |- ( ph -> C e. ( Met ` X ) )   &    |- ( ph -> D e. ( Met ` X ) )   &    |- ( ph -> R e. RR+ )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x C y ) <_ ( R x. ( x D y ) ) )   =>    |- ( ph -> J C_ K )
Theorem	comet 22318*	The composition of an extended metric with a monotonic subadditive function is an extended metric. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- ( ph -> D e. ( *Met ` X ) )   &    |- ( ph -> F : ( 0 [,] +oo ) --> RR* )   &    |- ( ( ph /\ x e. ( 0 [,] +oo ) ) -> ( ( F ` x ) = 0 <-> x = 0 ) )   &    |- ( ( ph /\ ( x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) ) ) -> ( x <_ y -> ( F ` x ) <_ ( F ` y ) ) )   &    |- ( ( ph /\ ( x e. ( 0 [,] +oo ) /\ y e. ( 0 [,] +oo ) ) ) -> ( F ` ( x +e y ) ) <_ ( ( F ` x ) +e ( F ` y ) ) )   =>    |- ( ph -> ( F o. D ) e. ( *Met ` X ) )
Theorem	stdbdmetval 22319*	Value of the standard bounded metric. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- D = ( x e. X , y e. X |-> if ( ( x C y ) <_ R , ( x C y ) , R ) )   =>    |- ( ( R e. V /\ A e. X /\ B e. X ) -> ( A D B ) = if ( ( A C B ) <_ R , ( A C B ) , R ) )
Theorem	stdbdxmet 22320*	The standard bounded metric is an extended metric given an extended metric and a positive extended real cutoff. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- D = ( x e. X , y e. X |-> if ( ( x C y ) <_ R , ( x C y ) , R ) )   =>    |- ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) -> D e. ( *Met ` X ) )
Theorem	stdbdmet 22321*	The standard bounded metric is a proper metric given an extended metric and a positive real cutoff. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- D = ( x e. X , y e. X |-> if ( ( x C y ) <_ R , ( x C y ) , R ) )   =>    |- ( ( C e. ( *Met ` X ) /\ R e. RR+ ) -> D e. ( Met ` X ) )
Theorem	stdbdbl 22322*	The standard bounded metric corresponding to C generates the same balls as C for radii less than R. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- D = ( x e. X , y e. X |-> if ( ( x C y ) <_ R , ( x C y ) , R ) )   =>    |- ( ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) /\ ( P e. X /\ S e. RR* /\ S <_ R ) ) -> ( P ( ball ` D ) S ) = ( P ( ball ` C ) S ) )
Theorem	stdbdmopn 22323*	The standard bounded metric corresponding to C generates the same topology as C. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- D = ( x e. X , y e. X |-> if ( ( x C y ) <_ R , ( x C y ) , R ) )   &    |- J = ( MetOpen ` C )   =>    |- ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) -> J = ( MetOpen ` D ) )
Theorem	mopnex 22324*	The topology generated by an extended metric can also be generated by a true metric. Thus, "metrizable topologies" can equivalently be defined in terms of metrics or extended metrics. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- J = ( MetOpen ` D )   =>    |- ( D e. ( *Met ` X ) -> E. d e. ( Met ` X ) J = ( MetOpen ` d ) )
Theorem	methaus 22325	The topology generated by a metric space is Hausdorff. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 26-Aug-2015.)
|- J = ( MetOpen ` D )   =>    |- ( D e. ( *Met ` X ) -> J e. Haus )
Theorem	met1stc 22326	The topology generated by a metric space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- J = ( MetOpen ` D )   =>    |- ( D e. ( *Met ` X ) -> J e. 1stc )
Theorem	met2ndci 22327	A separable metric space (a metric space with a countable dense subset) is second-countable. (Contributed by Mario Carneiro, 13-Apr-2015.)
|- J = ( MetOpen ` D )   =>    |- ( ( D e. ( *Met ` X ) /\ ( A C_ X /\ A ~<_ om /\ ( ( cls ` J ) ` A ) = X ) ) -> J e. 2ndc )
Theorem	met2ndc 22328*	A metric space is second-countable iff it is separable (has a countable dense subset). (Contributed by Mario Carneiro, 13-Apr-2015.)
|- J = ( MetOpen ` D )   =>    |- ( D e. ( *Met ` X ) -> ( J e. 2ndc <-> E. x e. ~P X ( x ~<_ om /\ ( ( cls ` J ) ` x ) = X ) ) )
Theorem	metrest 22329	Two alternate formulations of a subspace topology of a metric space topology. (Contributed by Jeff Hankins, 19-Aug-2009.) (Proof shortened by Mario Carneiro, 5-Jan-2014.)
|- D = ( C |` ( Y X. Y ) )   &    |- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( C e. ( *Met ` X ) /\ Y C_ X ) -> ( J ↾t Y ) = K )
Theorem	ressxms 22330	The restriction of a metric space is a metric space. (Contributed by Mario Carneiro, 24-Aug-2015.)
|- ( ( K e. *MetSp /\ A e. V ) -> ( K ↾s A ) e. *MetSp )
Theorem	ressms 22331	The restriction of a metric space is a metric space. (Contributed by Mario Carneiro, 24-Aug-2015.)
|- ( ( K e. MetSp /\ A e. V ) -> ( K ↾s A ) e. MetSp )
Theorem	prdsmslem1 22332	Lemma for prdsms 22336. The distance function of a product structure is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- Y = ( S X_s R )   &    |- ( ph -> S e. W )   &    |- ( ph -> I e. Fin )   &    |- D = ( dist ` Y )   &    |- B = ( Base ` Y )   &    |- ( ph -> R : I --> MetSp )   =>    |- ( ph -> D e. ( Met ` B ) )
Theorem	prdsxmslem1 22333	Lemma for prdsms 22336. The distance function of a product structure is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- Y = ( S X_s R )   &    |- ( ph -> S e. W )   &    |- ( ph -> I e. Fin )   &    |- D = ( dist ` Y )   &    |- B = ( Base ` Y )   &    |- ( ph -> R : I --> *MetSp )   =>    |- ( ph -> D e. ( *Met ` B ) )
Theorem	prdsxmslem2 22334*	Lemma for prdsxms 22335. The topology generated by the supremum metric is the same as the product topology, when the index set is finite. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- Y = ( S X_s R )   &    |- ( ph -> S e. W )   &    |- ( ph -> I e. Fin )   &    |- D = ( dist ` Y )   &    |- B = ( Base ` Y )   &    |- ( ph -> R : I --> *MetSp )   &    |- J = ( TopOpen ` Y )   &    |- V = ( Base ` ( R ` k ) )   &    |- E = ( ( dist ` ( R ` k ) ) |` ( V X. V ) )   &    |- K = ( TopOpen ` ( R ` k ) )   &    |- C = { x | E. g ( ( g Fn I /\ A. k e. I ( g ` k ) e. ( ( TopOpen o. R ) ` k ) /\ E. z e. Fin A. k e. ( I \ z ) ( g ` k ) = U. ( ( TopOpen o. R ) ` k ) ) /\ x = X_ k e. I ( g ` k ) ) }   =>    |- ( ph -> J = ( MetOpen ` D ) )
Theorem	prdsxms 22335	The indexed product structure is an extended metric space when the index set is finite. (Although the extended metric is still valid when the index set is infinite, it no longer agrees with the product topology, which is not metrizable in any case.) (Contributed by Mario Carneiro, 28-Aug-2015.)
|- Y = ( S X_s R )   =>    |- ( ( S e. W /\ I e. Fin /\ R : I --> *MetSp ) -> Y e. *MetSp )
Theorem	prdsms 22336	The indexed product structure is a metric space when the index set is finite. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- Y = ( S X_s R )   =>    |- ( ( S e. W /\ I e. Fin /\ R : I --> MetSp ) -> Y e. MetSp )
Theorem	pwsxms 22337	The product of a finite family of metric spaces is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- Y = ( R ^s I )   =>    |- ( ( R e. *MetSp /\ I e. Fin ) -> Y e. *MetSp )
Theorem	pwsms 22338	The product of a finite family of metric spaces is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- Y = ( R ^s I )   =>    |- ( ( R e. MetSp /\ I e. Fin ) -> Y e. MetSp )
Theorem	xpsxms 22339	A binary product of metric spaces is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- T = ( R X.s S )   =>    |- ( ( R e. *MetSp /\ S e. *MetSp ) -> T e. *MetSp )
Theorem	xpsms 22340	A binary product of metric spaces is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- T = ( R X.s S )   =>    |- ( ( R e. MetSp /\ S e. MetSp ) -> T e. MetSp )
Theorem	tmsxps 22341	Express the product of two metrics as another metric. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- P = ( dist ` ( (toMetSp ` M ) X.s (toMetSp ` N ) ) )   &    |- ( ph -> M e. ( *Met ` X ) )   &    |- ( ph -> N e. ( *Met ` Y ) )   =>    |- ( ph -> P e. ( *Met ` ( X X. Y ) ) )
Theorem	tmsxpsmopn 22342	Express the product of two metrics as another metric. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- P = ( dist ` ( (toMetSp ` M ) X.s (toMetSp ` N ) ) )   &    |- ( ph -> M e. ( *Met ` X ) )   &    |- ( ph -> N e. ( *Met ` Y ) )   &    |- J = ( MetOpen ` M )   &    |- K = ( MetOpen ` N )   &    |- L = ( MetOpen ` P )   =>    |- ( ph -> L = ( J tX K ) )
Theorem	tmsxpsval 22343	Value of the product of two metrics. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- P = ( dist ` ( (toMetSp ` M ) X.s (toMetSp ` N ) ) )   &    |- ( ph -> M e. ( *Met ` X ) )   &    |- ( ph -> N e. ( *Met ` Y ) )   &    |- ( ph -> A e. X )   &    |- ( ph -> B e. Y )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   =>    |- ( ph -> ( <. A , B >. P <. C , D >. ) = sup ( { ( A M C ) , ( B N D ) } , RR* , < ) )
Theorem	tmsxpsval2 22344	Value of the product of two metrics. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- P = ( dist ` ( (toMetSp ` M ) X.s (toMetSp ` N ) ) )   &    |- ( ph -> M e. ( *Met ` X ) )   &    |- ( ph -> N e. ( *Met ` Y ) )   &    |- ( ph -> A e. X )   &    |- ( ph -> B e. Y )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   =>    |- ( ph -> ( <. A , B >. P <. C , D >. ) = if ( ( A M C ) <_ ( B N D ) , ( B N D ) , ( A M C ) ) )
12.4.5  Continuity in metric spaces
Theorem	metcnp3 22345*	Two ways to express that F is continuous at P for metric spaces. Proposition 14-4.2 of [Gleason] p. 240. (Contributed by NM, 17-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. RR+ E. z e. RR+ ( F " ( P ( ball ` C ) z ) ) C_ ( ( F ` P ) ( ball ` D ) y ) ) ) )
Theorem	metcnp 22346*	Two ways to say a mapping from metric C to metric D is continuous at point P. (Contributed by NM, 11-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. RR+ E. z e. RR+ A. w e. X ( ( P C w ) < z -> ( ( F ` P ) D ( F ` w ) ) < y ) ) ) )
Theorem	metcnp2 22347*	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 22346 (and Munkres' metcn 22348) for compatibility with df-lm 21033. Definition 1.3-3 of [Kreyszig] p. 20. (Contributed by NM, 4-Jun-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. RR+ E. z e. RR+ A. w e. X ( ( w C P ) < z -> ( ( F ` w ) D ( F ` P ) ) < y ) ) ) )
Theorem	metcn 22348*	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. (Contributed by NM, 15-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. x e. X A. y e. RR+ E. z e. RR+ A. w e. X ( ( x C w ) < z -> ( ( F ` x ) D ( F ` w ) ) < y ) ) ) )
Theorem	metcnpi 22349*	Epsilon-delta property of a continuous metric space function, with function arguments as in metcnp 22346. (Contributed by NM, 17-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) -> E. x e. RR+ A. y e. X ( ( P C y ) < x -> ( ( F ` P ) D ( F ` y ) ) < A ) )
Theorem	metcnpi2 22350*	Epsilon-delta property of a continuous metric space function, with swapped distance function arguments as in metcnp2 22347. (Contributed by NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) -> E. x e. RR+ A. y e. X ( ( y C P ) < x -> ( ( F ` y ) D ( F ` P ) ) < A ) )
Theorem	metcnpi3 22351*	Epsilon-delta property of a metric space function continuous at P. A variation of metcnpi2 22350 with non-strict ordering. (Contributed by NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   =>    |- ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) ) /\ ( F e. ( ( J CnP K ) ` P ) /\ A e. RR+ ) ) -> E. x e. RR+ A. y e. X ( ( y C P ) <_ x -> ( ( F ` y ) D ( F ` P ) ) <_ A ) )
Theorem	txmetcnp 22352*	Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   &    |- L = ( MetOpen ` E )   =>    |- ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) /\ ( A e. X /\ B e. Y ) ) -> ( F e. ( ( ( J tX K ) CnP L ) ` <. A , B >. ) <-> ( F : ( X X. Y ) --> Z /\ A. z e. RR+ E. w e. RR+ A. u e. X A. v e. Y ( ( ( A C u ) < w /\ ( B D v ) < w ) -> ( ( A F B ) E ( u F v ) ) < z ) ) ) )
Theorem	txmetcn 22353*	Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- J = ( MetOpen ` C )   &    |- K = ( MetOpen ` D )   &    |- L = ( MetOpen ` E )   =>    |- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` Y ) /\ E e. ( *Met ` Z ) ) -> ( F e. ( ( J tX K ) Cn L ) <-> ( F : ( X X. Y ) --> Z /\ A. x e. X A. y e. Y A. z e. RR+ E. w e. RR+ A. u e. X A. v e. Y ( ( ( x C u ) < w /\ ( y D v ) < w ) -> ( ( x F y ) E ( u F v ) ) < z ) ) ) )
12.4.6  The uniform structure generated by a metric
Theorem	metuval 22354*	Value of the uniform structure generated by metric D. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- ( D e. (PsMet ` X ) -> (metUnif ` D ) = ( ( X X. X ) filGen ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) ) )
Theorem	metustel 22355*	Define a filter base F generated by a metric D. (Contributed by Thierry Arnoux, 22-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )   =>    |- ( D e. (PsMet ` X ) -> ( B e. F <-> E. a e. RR+ B = ( `' D " ( 0 [,) a ) ) ) )
Theorem	metustss 22356*	Range of the elements of the filter base generated by the metric D. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )   =>    |- ( ( D e. (PsMet ` X ) /\ A e. F ) -> A C_ ( X X. X ) )
Theorem	metustrel 22357*	Elements of the filter base generated by the metric D are relations. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )   =>    |- ( ( D e. (PsMet ` X ) /\ A e. F ) -> Rel A )
Theorem	metustto 22358*	Any two elements of the filter base generated by the metric D can be compared, like for RR+ (i.e. it's totally ordered). (Contributed by Thierry Arnoux, 22-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )   =>    |- ( ( D e. (PsMet ` X ) /\ A e. F /\ B e. F ) -> ( A C_ B \/ B C_ A ) )
Theorem	metustid 22359*	The identity diagonal is included in all elements of the filter base generated by the metric D. (Contributed by Thierry Arnoux, 22-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )   =>    |- ( ( D e. (PsMet ` X ) /\ A e. F ) -> ( _I |` X ) C_ A )
Theorem	metustsym 22360*	Elements of the filter base generated by the metric D are symmetric. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )   =>    |- ( ( D e. (PsMet ` X ) /\ A e. F ) -> `' A = A )
Theorem	metustexhalf 22361*	For any element A of the filter base generated by the metric D, the half element (corresponding to half the distance) is also in this base. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )   =>    |- ( ( ( X =/= (/) /\ D e. (PsMet ` X ) ) /\ A e. F ) -> E. v e. F ( v o. v ) C_ A )
Theorem	metustfbas 22362*	The filter base generated by a metric D. (Contributed by Thierry Arnoux, 26-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )   =>    |- ( ( X =/= (/) /\ D e. (PsMet ` X ) ) -> F e. ( fBas ` ( X X. X ) ) )
Theorem	metust 22363*	The uniform structure generated by a metric D. (Contributed by Thierry Arnoux, 26-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )   =>    |- ( ( X =/= (/) /\ D e. (PsMet ` X ) ) -> ( ( X X. X ) filGen F ) e. (UnifOn ` X ) )
Theorem	cfilucfil 22364*	Given a metric D and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the filter bases which contain balls of any pre-chosen size. See iscfil 23063. (Contributed by Thierry Arnoux, 29-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- F = ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) )   =>    |- ( ( X =/= (/) /\ D e. (PsMet ` X ) ) -> ( C e. (CauFilu ` ( ( X X. X ) filGen F ) ) <-> ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) )
Theorem	metuust 22365	The uniform structure generated by metric D is a uniform structure. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- ( ( X =/= (/) /\ D e. (PsMet ` X ) ) -> (metUnif ` D ) e. (UnifOn ` X ) )
Theorem	cfilucfil2 22366*	Given a metric D and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the filter bases which contain balls of any pre-chosen size. See iscfil 23063. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- ( ( X =/= (/) /\ D e. (PsMet ` X ) ) -> ( C e. (CauFilu ` (metUnif ` D ) ) <-> ( C e. ( fBas ` X ) /\ A. x e. RR+ E. y e. C ( D " ( y X. y ) ) C_ ( 0 [,) x ) ) ) )
Theorem	blval2 22367	The ball around a point P, alternative definition. (Contributed by Thierry Arnoux, 7-Dec-2017.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|- ( ( D e. (PsMet ` X ) /\ P e. X /\ R e. RR+ ) -> ( P ( ball ` D ) R ) = ( ( `' D " ( 0 [,) R ) ) " { P } ) )
Theorem	elbl4 22368	Membership in a ball, alternative definition. (Contributed by Thierry Arnoux, 26-Jan-2018.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|- ( ( ( D e. (PsMet ` X ) /\ R e. RR+ ) /\ ( A e. X /\ B e. X ) ) -> ( B e. ( A ( ball ` D ) R ) <-> B ( `' D " ( 0 [,) R ) ) A ) )
Theorem	metuel 22369*	Elementhood in the uniform structure generated by a metric D (Contributed by Thierry Arnoux, 8-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- ( ( X =/= (/) /\ D e. (PsMet ` X ) ) -> ( V e. (metUnif ` D ) <-> ( V C_ ( X X. X ) /\ E. w e. ran ( a e. RR+ |-> ( `' D " ( 0 [,) a ) ) ) w C_ V ) ) )
Theorem	metuel2 22370*	Elementhood in the uniform structure generated by a metric D (Contributed by Thierry Arnoux, 24-Jan-2018.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- U = (metUnif ` D )   =>    |- ( ( X =/= (/) /\ D e. (PsMet ` X ) ) -> ( V e. U <-> ( V C_ ( X X. X ) /\ E. d e. RR+ A. x e. X A. y e. X ( ( x D y ) < d -> x V y ) ) ) )
Theorem	metustbl 22371*	The "section" image of an entourage at a point P always contains a ball (centered on this point). (Contributed by Thierry Arnoux, 8-Dec-2017.)
|- ( ( D e. (PsMet ` X ) /\ V e. (metUnif ` D ) /\ P e. X ) -> E. a e. ran ( ball ` D ) ( P e. a /\ a C_ ( V " { P } ) ) )
Theorem	psmetutop 22372	The topology induced by a uniform structure generated by a metric D is generated by that metric's open balls. (Contributed by Thierry Arnoux, 6-Dec-2017.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|- ( ( X =/= (/) /\ D e. (PsMet ` X ) ) -> (unifTop ` (metUnif ` D ) ) = ( topGen ` ran ( ball ` D ) ) )
Theorem	xmetutop 22373	The topology induced by a uniform structure generated by an extended metric D is that metric's open sets. (Contributed by Thierry Arnoux, 11-Mar-2018.)
|- ( ( X =/= (/) /\ D e. ( *Met ` X ) ) -> (unifTop ` (metUnif ` D ) ) = ( MetOpen ` D ) )
Theorem	xmsusp 22374	If the uniform set of a metric space is the uniform structure generated by its metric, then it is a uniform space. (Contributed by Thierry Arnoux, 14-Dec-2017.)
|- X = ( Base ` F )   &    |- D = ( ( dist ` F ) |` ( X X. X ) )   &    |- U = (UnifSt ` F )   =>    |- ( ( X =/= (/) /\ F e. *MetSp /\ U = (metUnif ` D ) ) -> F e. UnifSp )
Theorem	restmetu 22375	The uniform structure generated by the restriction of a metric is its trace. (Contributed by Thierry Arnoux, 18-Dec-2017.)
|- ( ( A =/= (/) /\ D e. (PsMet ` X ) /\ A C_ X ) -> ( (metUnif ` D ) ↾t ( A X. A ) ) = (metUnif ` ( D |` ( A X. A ) ) ) )
Theorem	metucn 22376*	Uniform continuity in metric spaces. Compare the order of the quantifiers with metcn 22348. (Contributed by Thierry Arnoux, 26-Jan-2018.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- U = (metUnif ` C )   &    |- V = (metUnif ` D )   &    |- ( ph -> X =/= (/) )   &    |- ( ph -> Y =/= (/) )   &    |- ( ph -> C e. (PsMet ` X ) )   &    |- ( ph -> D e. (PsMet ` Y ) )   =>    |- ( ph -> ( F e. ( U Cnu V ) <-> ( F : X --> Y /\ A. d e. RR+ E. c e. RR+ A. x e. X A. y e. X ( ( x C y ) < c -> ( ( F ` x ) D ( F ` y ) ) < d ) ) ) )
12.4.7  Examples of metric spaces
Theorem	dscmet 22377*	The discrete metric on any set X. Definition 1.1-8 of [Kreyszig] p. 8. (Contributed by FL, 12-Oct-2006.)
|- D = ( x e. X , y e. X |-> if ( x = y , 0 , 1 ) )   =>    |- ( X e. V -> D e. ( Met ` X ) )
Theorem	dscopn 22378*	The discrete metric generates the discrete topology. In particular, the discrete topology is metrizable. (Contributed by Mario Carneiro, 29-Jan-2014.)
|- D = ( x e. X , y e. X |-> if ( x = y , 0 , 1 ) )   =>    |- ( X e. V -> ( MetOpen ` D ) = ~P X )
Theorem	nrmmetd 22379*	Show that a group norm generates a metric. Part of Definition 2.2-1 of [Kreyszig] p. 58. (Contributed by NM, 4-Dec-2006.) (Revised by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` G )   &    |- .- = ( -g ` G )   &    |- .0. = ( 0g ` G )   &    |- ( ph -> G e. Grp )   &    |- ( ph -> F : X --> RR )   &    |- ( ( ph /\ x e. X ) -> ( ( F ` x ) = 0 <-> x = .0. ) )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( F ` ( x .- y ) ) <_ ( ( F ` x ) + ( F ` y ) ) )   =>    |- ( ph -> ( F o. .- ) e. ( Met ` X ) )
Theorem	abvmet 22380	An absolute value F generates a metric defined by d ( x , y ) = F ( x - y ), analogously to cnmet 22575. (In fact, the ring structure is not needed at all; the group properties abveq0 18826 and abvtri 18830, abvneg 18834 are sufficient.) (Contributed by Mario Carneiro, 9-Sep-2014.) (Revised by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` R )   &    |- A = (AbsVal ` R )   &    |- .- = ( -g ` R )   =>    |- ( F e. A -> ( F o. .- ) e. ( Met ` X ) )
12.4.8  Normed algebraic structures In the following, the norm of a normed algebraic structure (group, left module, vector space) is defined by the (given) distance function (the norm N of an element is its distance D from the zero element, see nmval 22394: ( N ` A ) = ( A D .0. )). By this definition, the norm function N is actually a norm (satisfying the properties of being a function into the reals, subadditivity/triangle inequality ( n(x+y) <_ n(x)+n(y) ), absolute homogeneity ( n(sx) = |s| n(x) ) [Remark: for group norms, some authors (e.g. Juris Steprans in "A characterization of free abelian groups") demand that n(sx) = |s| n(x) for all s in ZZ, whereas other authors (e.g. N. H. Bingham and A. J. Ostaszewski in "Normed versus topological groups: Dichotomy and duality") only require inversion symmetry, i.e. n(-x) = n(x). The definition df-ngp 22388 of a group norm follows the second aproach, see nminv 22425.] and positive definiteness/point-separating ( n(x) = 0 <-> x = 0 ) if the structure is a metric space with a right-translation-invariant metric (see nmf 22419, nmtri 22430, nmvs 22480 and nmeq0 22422). An alternate definition of a normed group (i.e. a group equipped with a norm) without using the properties of a metric space is given by theorem tngngp3 22460. For a structure being a group, the (arbitrary) distance function can be restricted to the elements of the group without affecting the norm, see nmfval2 22395. Usually, however, the norm of a normed structure is given, and the corresponding metric ("induced metric") is achieved by defining a distance function based on the norm (the distance D between two elements is the norm N of their difference, see ngpds 22408: ( A D B ) = ( N ` ( A .- B ) )). The operation toNrmGrp does exactly this, i.e. it adds a distance function (and a topology) to a structure (which should be at least a group) corresponding to a given norm in the just shown way: ( dist ` T ) = ( N o. .- ), see also tngds 22452. By this, the enhanced structure becomes a normed structure if the induced metric is in fact a metric (see tngngp2 22456) resp. if the norm is in fact a norm (see tngngpd 22457). If the norm is derived from a given metric, as done with df-nm 22387, the induced metric is the original metric restricted to the base set: ( dist ` T ) = ( ( dist ` G ) |` ( X X. X ) ), see nrmtngdist 22461, and the norm remains the same: ( norm ` T ) = ( norm ` G ), see nrmtngnrm 22462.
Syntax	cnm 22381	Norm of a normed ring.
class norm
Syntax	cngp 22382	The class of all normed groups.
class NrmGrp
Syntax	ctng 22383	Make a normed group from a norm and a group.
class toNrmGrp
Syntax	cnrg 22384	Normed ring.
class NrmRing
Syntax	cnlm 22385	Normed module.
class NrmMod
Syntax	cnvc 22386	Normed vector space.
class NrmVec
Definition	df-nm 22387*	Define the norm on a group or ring (when it makes sense) in terms of the distance to zero. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- norm = ( w e. _V |-> ( x e. ( Base ` w ) |-> ( x ( dist ` w ) ( 0g ` w ) ) ) )
Definition	df-ngp 22388	Define a normed group, which is a group with a right-translation-invariant metric. This is not a standard notion, but is helpful as the most general context in which a metric-like norm makes sense. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- NrmGrp = { g e. ( Grp i^i MetSp ) | ( ( norm ` g ) o. ( -g ` g ) ) C_ ( dist ` g ) }
Definition	df-tng 22389*	Define a function that fills in the topology and metric components of a structure given a group and a norm on it. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- toNrmGrp = ( g e. _V , f e. _V |-> ( ( g sSet <. ( dist ` ndx ) , ( f o. ( -g ` g ) ) >. ) sSet <. (TopSet ` ndx ) , ( MetOpen ` ( f o. ( -g ` g ) ) ) >. ) )
Definition	df-nrg 22390	A normed ring is a ring with an induced topology and metric such that the metric is translation-invariant and the norm (distance from 0) is an absolute value on the ring. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- NrmRing = { w e. NrmGrp | ( norm ` w ) e. (AbsVal ` w ) }
Definition	df-nlm 22391*	A normed (left) module is a module which is also a normed group over a normed ring, such that the norm distributes over scalar multiplication. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- NrmMod = { w e. (NrmGrp i^i LMod ) | [. (Scalar ` w ) / f ]. ( f e. NrmRing /\ A. x e. ( Base ` f ) A. y e. ( Base ` w ) ( ( norm ` w ) ` ( x ( .s ` w ) y ) ) = ( ( ( norm ` f ) ` x ) x. ( ( norm ` w ) ` y ) ) ) }
Definition	df-nvc 22392	A normed vector space is a normed module which is also a vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- NrmVec = (NrmMod i^i LVec )
Theorem	nmfval 22393*	The value of the norm function. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- N = ( norm ` W )   &    |- X = ( Base ` W )   &    |- .0. = ( 0g ` W )   &    |- D = ( dist ` W )   =>    |- N = ( x e. X |-> ( x D .0. ) )
Theorem	nmval 22394	The value of the norm function. Problem 1 of [Kreyszig] p. 63. (Contributed by NM, 4-Dec-2006.) (Revised by Mario Carneiro, 2-Oct-2015.)
|- N = ( norm ` W )   &    |- X = ( Base ` W )   &    |- .0. = ( 0g ` W )   &    |- D = ( dist ` W )   =>    |- ( A e. X -> ( N ` A ) = ( A D .0. ) )
Theorem	nmfval2 22395*	The value of the norm function using a restricted metric. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- N = ( norm ` W )   &    |- X = ( Base ` W )   &    |- .0. = ( 0g ` W )   &    |- D = ( dist ` W )   &    |- E = ( D |` ( X X. X ) )   =>    |- ( W e. Grp -> N = ( x e. X |-> ( x E .0. ) ) )
Theorem	nmval2 22396	The value of the norm function using a restricted metric. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- N = ( norm ` W )   &    |- X = ( Base ` W )   &    |- .0. = ( 0g ` W )   &    |- D = ( dist ` W )   &    |- E = ( D |` ( X X. X ) )   =>    |- ( ( W e. Grp /\ A e. X ) -> ( N ` A ) = ( A E .0. ) )
Theorem	nmf2 22397	The norm is a function from the base set into the reals. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- N = ( norm ` W )   &    |- X = ( Base ` W )   &    |- D = ( dist ` W )   &    |- E = ( D |` ( X X. X ) )   =>    |- ( ( W e. Grp /\ E e. ( Met ` X ) ) -> N : X --> RR )
Theorem	nmpropd 22398	Weak property deduction for a norm. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( ph -> ( Base ` K ) = ( Base ` L ) )   &    |- ( ph -> ( +g ` K ) = ( +g ` L ) )   &    |- ( ph -> ( dist ` K ) = ( dist ` L ) )   =>    |- ( ph -> ( norm ` K ) = ( norm ` L ) )
Theorem	nmpropd2 22399*	Strong property deduction for a norm. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ph -> K e. Grp )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )   &    |- ( ph -> ( ( dist ` K ) |` ( B X. B ) ) = ( ( dist ` L ) |` ( B X. B ) ) )   =>    |- ( ph -> ( norm ` K ) = ( norm ` L ) )
Theorem	isngp 22400	The property of being a normed group. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- N = ( norm ` G )   &    |- .- = ( -g ` G )   &    |- D = ( dist ` G )   =>    |- ( G e. NrmGrp <-> ( G e. Grp /\ G e. MetSp /\ ( N o. .- ) C_ D ) )