P. 149 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14801-14900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	blrnps 14801*	Membership in the range of the ball function. Note that ran ( ball ` D ) is the collection of all balls for metric D. (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|- ( D e. (PsMet ` X ) -> ( A e. ran ( ball ` D ) <-> E. x e. X E. r e. RR* A = ( x ( ball ` D ) r ) ) )
Theorem	blrn 14802*	Membership in the range of the ball function. Note that ran ( ball ` D ) is the collection of all balls for metric D. (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
|- ( D e. ( *Met ` X ) -> ( A e. ran ( ball ` D ) <-> E. x e. X E. r e. RR* A = ( x ( ball ` D ) r ) ) )
Theorem	xblcntrps 14803	A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|- ( ( D e. (PsMet ` X ) /\ P e. X /\ ( R e. RR* /\ 0 < R ) ) -> P e. ( P ( ball ` D ) R ) )
Theorem	xblcntr 14804	A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
|- ( ( D e. ( *Met ` X ) /\ P e. X /\ ( R e. RR* /\ 0 < R ) ) -> P e. ( P ( ball ` D ) R ) )
Theorem	blcntrps 14805	A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|- ( ( D e. (PsMet ` X ) /\ P e. X /\ R e. RR+ ) -> P e. ( P ( ball ` D ) R ) )
Theorem	blcntr 14806	A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
|- ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR+ ) -> P e. ( P ( ball ` D ) R ) )
Theorem	xblm 14807*	A ball is inhabited iff the radius is positive. (Contributed by Mario Carneiro, 23-Aug-2015.)
|- ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( E. x x e. ( P ( ball ` D ) R ) <-> 0 < R ) )
Theorem	bln0 14808	A ball is not empty. It is also inhabited, as seen at blcntr 14806. (Contributed by NM, 6-Oct-2007.) (Revised by Mario Carneiro, 12-Nov-2013.)
|- ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR+ ) -> ( P ( ball ` D ) R ) =/= (/) )
Theorem	blelrnps 14809	A ball belongs to the set of balls of a metric space. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|- ( ( D e. (PsMet ` X ) /\ P e. X /\ R e. RR* ) -> ( P ( ball ` D ) R ) e. ran ( ball ` D ) )
Theorem	blelrn 14810	A ball belongs to the set of balls of a metric space. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
|- ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( P ( ball ` D ) R ) e. ran ( ball ` D ) )
Theorem	blssm 14811	A ball is a subset of the base set of a metric space. (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
|- ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( P ( ball ` D ) R ) C_ X )
Theorem	unirnblps 14812	The union of the set of balls of a metric space is its base set. (Contributed by NM, 12-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|- ( D e. (PsMet ` X ) -> U. ran ( ball ` D ) = X )
Theorem	unirnbl 14813	The union of the set of balls of a metric space is its base set. (Contributed by NM, 12-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
|- ( D e. ( *Met ` X ) -> U. ran ( ball ` D ) = X )
Theorem	blininf 14814	The intersection of two balls with the same center is the smaller of them. (Contributed by NM, 1-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
|- ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* ) ) -> ( ( P ( ball ` D ) R ) i^i ( P ( ball ` D ) S ) ) = ( P ( ball ` D )inf ( { R , S } , RR* , < ) ) )
Theorem	ssblps 14815	The size of a ball increases monotonically with its radius. (Contributed by NM, 20-Sep-2007.) (Revised by Mario Carneiro, 24-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|- ( ( ( D e. (PsMet ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* ) /\ R <_ S ) -> ( P ( ball ` D ) R ) C_ ( P ( ball ` D ) S ) )
Theorem	ssbl 14816	The size of a ball increases monotonically with its radius. (Contributed by NM, 20-Sep-2007.) (Revised by Mario Carneiro, 24-Aug-2015.)
|- ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR* /\ S e. RR* ) /\ R <_ S ) -> ( P ( ball ` D ) R ) C_ ( P ( ball ` D ) S ) )
Theorem	blssps 14817*	Any point P in a ball B can be centered in another ball that is a subset of B. (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 24-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|- ( ( D e. (PsMet ` X ) /\ B e. ran ( ball ` D ) /\ P e. B ) -> E. x e. RR+ ( P ( ball ` D ) x ) C_ B )
Theorem	blss 14818*	Any point P in a ball B can be centered in another ball that is a subset of B. (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 24-Aug-2015.)
|- ( ( D e. ( *Met ` X ) /\ B e. ran ( ball ` D ) /\ P e. B ) -> E. x e. RR+ ( P ( ball ` D ) x ) C_ B )
Theorem	blssexps 14819*	Two ways to express the existence of a ball subset. (Contributed by NM, 5-May-2007.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|- ( ( D e. (PsMet ` X ) /\ P e. X ) -> ( E. x e. ran ( ball ` D ) ( P e. x /\ x C_ A ) <-> E. r e. RR+ ( P ( ball ` D ) r ) C_ A ) )
Theorem	blssex 14820*	Two ways to express the existence of a ball subset. (Contributed by NM, 5-May-2007.) (Revised by Mario Carneiro, 12-Nov-2013.)
|- ( ( D e. ( *Met ` X ) /\ P e. X ) -> ( E. x e. ran ( ball ` D ) ( P e. x /\ x C_ A ) <-> E. r e. RR+ ( P ( ball ` D ) r ) C_ A ) )
Theorem	ssblex 14821*	A nested ball exists whose radius is less than any desired amount. (Contributed by NM, 20-Sep-2007.) (Revised by Mario Carneiro, 12-Nov-2013.)
|- ( ( ( D e. ( *Met ` X ) /\ P e. X ) /\ ( R e. RR+ /\ S e. RR+ ) ) -> E. x e. RR+ ( x < R /\ ( P ( ball ` D ) x ) C_ ( P ( ball ` D ) S ) ) )
Theorem	blin2 14822*	Given any two balls and a point in their intersection, there is a ball contained in the intersection with the given center point. (Contributed by Mario Carneiro, 12-Nov-2013.)
|- ( ( ( D e. ( *Met ` X ) /\ P e. ( B i^i C ) ) /\ ( B e. ran ( ball ` D ) /\ C e. ran ( ball ` D ) ) ) -> E. x e. RR+ ( P ( ball ` D ) x ) C_ ( B i^i C ) )
Theorem	blbas 14823	The balls of a metric space form a basis for a topology. (Contributed by NM, 12-Sep-2006.) (Revised by Mario Carneiro, 15-Jan-2014.)
|- ( D e. ( *Met ` X ) -> ran ( ball ` D ) e. TopBases )
Theorem	blres 14824	A ball in a restricted metric space. (Contributed by Mario Carneiro, 5-Jan-2014.)
|- C = ( D |` ( Y X. Y ) )   =>    |- ( ( D e. ( *Met ` X ) /\ P e. ( X i^i Y ) /\ R e. RR* ) -> ( P ( ball ` C ) R ) = ( ( P ( ball ` D ) R ) i^i Y ) )
Theorem	xmeterval 14825	Value of the "finitely separated" relation. (Contributed by Mario Carneiro, 24-Aug-2015.)
|- .~ = ( `' D " RR )   =>    |- ( D e. ( *Met ` X ) -> ( A .~ B <-> ( A e. X /\ B e. X /\ ( A D B ) e. RR ) ) )
Theorem	xmeter 14826	The "finitely separated" relation is an equivalence relation. (Contributed by Mario Carneiro, 24-Aug-2015.)
|- .~ = ( `' D " RR )   =>    |- ( D e. ( *Met ` X ) -> .~ Er X )
Theorem	xmetec 14827	The equivalence classes under the finite separation equivalence relation are infinity balls. (Contributed by Mario Carneiro, 24-Aug-2015.)
|- .~ = ( `' D " RR )   =>    |- ( ( D e. ( *Met ` X ) /\ P e. X ) -> [ P ] .~ = ( P ( ball ` D ) +oo ) )
Theorem	blssec 14828	A ball centered at P is contained in the set of points finitely separated from P. This is just an application of ssbl 14816 to the infinity ball. (Contributed by Mario Carneiro, 24-Aug-2015.)
|- .~ = ( `' D " RR )   =>    |- ( ( D e. ( *Met ` X ) /\ P e. X /\ S e. RR* ) -> ( P ( ball ` D ) S ) C_ [ P ] .~ )
Theorem	blpnfctr 14829	The infinity ball in an extended metric acts like an ultrametric ball in that every point in the ball is also its center. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- ( ( D e. ( *Met ` X ) /\ P e. X /\ A e. ( P ( ball ` D ) +oo ) ) -> ( P ( ball ` D ) +oo ) = ( A ( ball ` D ) +oo ) )
Theorem	xmetresbl 14830	An extended metric restricted to any ball (in particular the infinity ball) is a proper metric. Together with xmetec 14827, this shows that any extended metric space can be "factored" into the disjoint union of proper metric spaces, with points in the same region measured by that region's metric, and points in different regions being distance +oo from each other. (Contributed by Mario Carneiro, 23-Aug-2015.)
|- B = ( P ( ball ` D ) R )   =>    |- ( ( D e. ( *Met ` X ) /\ P e. X /\ R e. RR* ) -> ( D |` ( B X. B ) ) e. ( Met ` B ) )
9.2.4  Open sets of a metric space
Theorem	mopnrel 14831	The class of open sets of a metric space is a relation. (Contributed by Jim Kingdon, 5-May-2023.)
|- Rel MetOpen
Theorem	mopnval 14832	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 ( MetOpen ` D ) is the family of all open sets in the metric space determined by the metric D. By mopntop 14834, the open sets of a metric space form a topology J, whose base set is U. J by mopnuni 14835. (Contributed by NM, 1-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
|- J = ( MetOpen ` D )   =>    |- ( D e. ( *Met ` X ) -> J = ( topGen ` ran ( ball ` D ) ) )
Theorem	mopntopon 14833	The set of open sets of a metric space X is a topology on X. Remark in [Kreyszig] p. 19. This theorem connects the two concepts and makes available the theorems for topologies for use with metric spaces. (Contributed by Mario Carneiro, 24-Aug-2015.)
|- J = ( MetOpen ` D )   =>    |- ( D e. ( *Met ` X ) -> J e. (TopOn ` X ) )
Theorem	mopntop 14834	The set of open sets of a metric space is a topology. (Contributed by NM, 28-Aug-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
|- J = ( MetOpen ` D )   =>    |- ( D e. ( *Met ` X ) -> J e. Top )
Theorem	mopnuni 14835	The union of all open sets in a metric space is its underlying set. (Contributed by NM, 4-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
|- J = ( MetOpen ` D )   =>    |- ( D e. ( *Met ` X ) -> X = U. J )
Theorem	elmopn 14836*	The defining property of an open set of a metric space. (Contributed by NM, 1-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
|- J = ( MetOpen ` D )   =>    |- ( D e. ( *Met ` X ) -> ( A e. J <-> ( A C_ X /\ A. x e. A E. y e. ran ( ball ` D ) ( x e. y /\ y C_ A ) ) ) )
Theorem	mopnfss 14837	The family of open sets of a metric space is a collection of subsets of the base set. (Contributed by NM, 3-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
|- J = ( MetOpen ` D )   =>    |- ( D e. ( *Met ` X ) -> J C_ ~P X )
Theorem	mopnm 14838	The base set of a metric space is open. Part of Theorem T1 of [Kreyszig] p. 19. (Contributed by NM, 4-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
|- J = ( MetOpen ` D )   =>    |- ( D e. ( *Met ` X ) -> X e. J )
Theorem	elmopn2 14839*	A defining property of an open set of a metric space. (Contributed by NM, 5-May-2007.) (Revised by Mario Carneiro, 12-Nov-2013.)
|- J = ( MetOpen ` D )   =>    |- ( D e. ( *Met ` X ) -> ( A e. J <-> ( A C_ X /\ A. x e. A E. y e. RR+ ( x ( ball ` D ) y ) C_ A ) ) )
Theorem	mopnss 14840	An open set of a metric space is a subspace of its base set. (Contributed by NM, 3-Sep-2006.)
|- J = ( MetOpen ` D )   =>    |- ( ( D e. ( *Met ` X ) /\ A e. J ) -> A C_ X )
Theorem	isxms 14841	Express the predicate " <. X , D >. is an extended metric space" with underlying set X and distance function D. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- J = ( TopOpen ` K )   &    |- X = ( Base ` K )   &    |- D = ( ( dist ` K ) |` ( X X. X ) )   =>    |- ( K e. *MetSp <-> ( K e. TopSp /\ J = ( MetOpen ` D ) ) )
Theorem	isxms2 14842	Express the predicate " <. X , D >. is an extended metric space" with underlying set X and distance function D. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- J = ( TopOpen ` K )   &    |- X = ( Base ` K )   &    |- D = ( ( dist ` K ) |` ( X X. X ) )   =>    |- ( K e. *MetSp <-> ( D e. ( *Met ` X ) /\ J = ( MetOpen ` D ) ) )
Theorem	isms 14843	Express the predicate " <. X , D >. is a metric space" with underlying set X and distance function D. (Contributed by NM, 27-Aug-2006.) (Revised by Mario Carneiro, 24-Aug-2015.)
|- J = ( TopOpen ` K )   &    |- X = ( Base ` K )   &    |- D = ( ( dist ` K ) |` ( X X. X ) )   =>    |- ( K e. MetSp <-> ( K e. *MetSp /\ D e. ( Met ` X ) ) )
Theorem	isms2 14844	Express the predicate " <. X , D >. is a metric space" with underlying set X and distance function D. (Contributed by NM, 27-Aug-2006.) (Revised by Mario Carneiro, 24-Aug-2015.)
|- J = ( TopOpen ` K )   &    |- X = ( Base ` K )   &    |- D = ( ( dist ` K ) |` ( X X. X ) )   =>    |- ( K e. MetSp <-> ( D e. ( Met ` X ) /\ J = ( MetOpen ` D ) ) )
Theorem	xmstopn 14845	The topology component of an extended metric space coincides with the topology generated by the metric component. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- J = ( TopOpen ` K )   &    |- X = ( Base ` K )   &    |- D = ( ( dist ` K ) |` ( X X. X ) )   =>    |- ( K e. *MetSp -> J = ( MetOpen ` D ) )
Theorem	mstopn 14846	The topology component of a metric space coincides with the topology generated by the metric component. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- J = ( TopOpen ` K )   &    |- X = ( Base ` K )   &    |- D = ( ( dist ` K ) |` ( X X. X ) )   =>    |- ( K e. MetSp -> J = ( MetOpen ` D ) )
Theorem	xmstps 14847	An extended metric space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- ( M e. *MetSp -> M e. TopSp )
Theorem	msxms 14848	A metric space is an extended metric space. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- ( M e. MetSp -> M e. *MetSp )
Theorem	mstps 14849	A metric space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- ( M e. MetSp -> M e. TopSp )
Theorem	xmsxmet 14850	The distance function, suitably truncated, is an extended metric on X. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- X = ( Base ` M )   &    |- D = ( ( dist ` M ) |` ( X X. X ) )   =>    |- ( M e. *MetSp -> D e. ( *Met ` X ) )
Theorem	msmet 14851	The distance function, suitably truncated, is a metric on X. (Contributed by Mario Carneiro, 12-Nov-2013.)
|- X = ( Base ` M )   &    |- D = ( ( dist ` M ) |` ( X X. X ) )   =>    |- ( M e. MetSp -> D e. ( Met ` X ) )
Theorem	msf 14852	The distance function of a metric space is a function into the real numbers. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
|- X = ( Base ` M )   &    |- D = ( ( dist ` M ) |` ( X X. X ) )   =>    |- ( M e. MetSp -> D : ( X X. X ) --> RR )
Theorem	xmsxmet2 14853	The distance function, suitably truncated, is an extended metric on X. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` M )   &    |- D = ( dist ` M )   =>    |- ( M e. *MetSp -> ( D |` ( X X. X ) ) e. ( *Met ` X ) )
Theorem	msmet2 14854	The distance function, suitably truncated, is a metric on X. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` M )   &    |- D = ( dist ` M )   =>    |- ( M e. MetSp -> ( D |` ( X X. X ) ) e. ( Met ` X ) )
Theorem	mscl 14855	Closure of the distance function of a metric space. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` M )   &    |- D = ( dist ` M )   =>    |- ( ( M e. MetSp /\ A e. X /\ B e. X ) -> ( A D B ) e. RR )
Theorem	xmscl 14856	Closure of the distance function of an extended metric space. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` M )   &    |- D = ( dist ` M )   =>    |- ( ( M e. *MetSp /\ A e. X /\ B e. X ) -> ( A D B ) e. RR* )
Theorem	xmsge0 14857	The distance function in an extended metric space is nonnegative. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- X = ( Base ` M )   &    |- D = ( dist ` M )   =>    |- ( ( M e. *MetSp /\ A e. X /\ B e. X ) -> 0 <_ ( A D B ) )
Theorem	xmseq0 14858	The distance between two points in an extended metric space is zero iff the two points are identical. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` M )   &    |- D = ( dist ` M )   =>    |- ( ( M e. *MetSp /\ A e. X /\ B e. X ) -> ( ( A D B ) = 0 <-> A = B ) )
Theorem	xmssym 14859	The distance function in an extended metric space is symmetric. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` M )   &    |- D = ( dist ` M )   =>    |- ( ( M e. *MetSp /\ A e. X /\ B e. X ) -> ( A D B ) = ( B D A ) )
Theorem	xmstri2 14860	Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` M )   &    |- D = ( dist ` M )   =>    |- ( ( M e. *MetSp /\ ( C e. X /\ A e. X /\ B e. X ) ) -> ( A D B ) <_ ( ( C D A ) +e ( C D B ) ) )
Theorem	mstri2 14861	Triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` M )   &    |- D = ( dist ` M )   =>    |- ( ( M e. MetSp /\ ( C e. X /\ A e. X /\ B e. X ) ) -> ( A D B ) <_ ( ( C D A ) + ( C D B ) ) )
Theorem	xmstri 14862	Triangle inequality for the distance function of a metric space. Definition 14-1.1(d) of [Gleason] p. 223. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` M )   &    |- D = ( dist ` M )   =>    |- ( ( M e. *MetSp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D B ) <_ ( ( A D C ) +e ( C D B ) ) )
Theorem	mstri 14863	Triangle inequality for the distance function of a metric space. Definition 14-1.1(d) of [Gleason] p. 223. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` M )   &    |- D = ( dist ` M )   =>    |- ( ( M e. MetSp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D B ) <_ ( ( A D C ) + ( C D B ) ) )
Theorem	xmstri3 14864	Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` M )   &    |- D = ( dist ` M )   =>    |- ( ( M e. *MetSp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D B ) <_ ( ( A D C ) +e ( B D C ) ) )
Theorem	mstri3 14865	Triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- X = ( Base ` M )   &    |- D = ( dist ` M )   =>    |- ( ( M e. MetSp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D B ) <_ ( ( A D C ) + ( B D C ) ) )
Theorem	msrtri 14866	Reverse triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- X = ( Base ` M )   &    |- D = ( dist ` M )   =>    |- ( ( M e. MetSp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( abs ` ( ( A D C ) - ( B D C ) ) ) <_ ( A D B ) )
Theorem	xmspropd 14867	Property deduction for an extended metric space. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ph -> ( ( dist ` K ) |` ( B X. B ) ) = ( ( dist ` L ) |` ( B X. B ) ) )   &    |- ( ph -> ( TopOpen ` K ) = ( TopOpen ` L ) )   =>    |- ( ph -> ( K e. *MetSp <-> L e. *MetSp ) )
Theorem	mspropd 14868	Property deduction for a metric space. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ph -> ( ( dist ` K ) |` ( B X. B ) ) = ( ( dist ` L ) |` ( B X. B ) ) )   &    |- ( ph -> ( TopOpen ` K ) = ( TopOpen ` L ) )   =>    |- ( ph -> ( K e. MetSp <-> L e. MetSp ) )
Theorem	setsmsbasg 14869	The base set of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- ( ph -> X = ( Base ` M ) )   &    |- ( ph -> D = ( ( dist ` M ) |` ( X X. X ) ) )   &    |- ( ph -> K = ( M sSet <. (TopSet ` ndx ) , ( MetOpen ` D ) >. ) )   &    |- ( ph -> M e. V )   &    |- ( ph -> ( MetOpen ` D ) e. W )   =>    |- ( ph -> X = ( Base ` K ) )
Theorem	setsmsdsg 14870	The distance function of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
|- ( ph -> X = ( Base ` M ) )   &    |- ( ph -> D = ( ( dist ` M ) |` ( X X. X ) ) )   &    |- ( ph -> K = ( M sSet <. (TopSet ` ndx ) , ( MetOpen ` D ) >. ) )   &    |- ( ph -> M e. V )   &    |- ( ph -> ( MetOpen ` D ) e. W )   =>    |- ( ph -> ( dist ` M ) = ( dist ` K ) )
Theorem	setsmstsetg 14871	The topology of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) (Revised by Jim Kingdon, 7-May-2023.)
|- ( ph -> X = ( Base ` M ) )   &    |- ( ph -> D = ( ( dist ` M ) |` ( X X. X ) ) )   &    |- ( ph -> K = ( M sSet <. (TopSet ` ndx ) , ( MetOpen ` D ) >. ) )   &    |- ( ph -> M e. V )   &    |- ( ph -> ( MetOpen ` D ) e. W )   =>    |- ( ph -> ( MetOpen ` D ) = (TopSet ` K ) )
Theorem	mopni 14872*	An open set of a metric space includes a ball around each of its points. (Contributed by NM, 3-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
|- J = ( MetOpen ` D )   =>    |- ( ( D e. ( *Met ` X ) /\ A e. J /\ P e. A ) -> E. x e. ran ( ball ` D ) ( P e. x /\ x C_ A ) )
Theorem	mopni2 14873*	An open set of a metric space includes a ball around each of its points. (Contributed by NM, 2-May-2007.) (Revised by Mario Carneiro, 12-Nov-2013.)
|- J = ( MetOpen ` D )   =>    |- ( ( D e. ( *Met ` X ) /\ A e. J /\ P e. A ) -> E. x e. RR+ ( P ( ball ` D ) x ) C_ A )
Theorem	mopni3 14874*	An open set of a metric space includes an arbitrarily small ball around each of its points. (Contributed by NM, 20-Sep-2007.) (Revised by Mario Carneiro, 12-Nov-2013.)
|- J = ( MetOpen ` D )   =>    |- ( ( ( D e. ( *Met ` X ) /\ A e. J /\ P e. A ) /\ R e. RR+ ) -> E. x e. RR+ ( x < R /\ ( P ( ball ` D ) x ) C_ A ) )
Theorem	blssopn 14875	The balls of a metric space are open sets. (Contributed by NM, 12-Sep-2006.) (Revised by Mario Carneiro, 23-Dec-2013.)
|- J = ( MetOpen ` D )   =>    |- ( D e. ( *Met ` X ) -> ran ( ball ` D ) C_ J )
Theorem	unimopn 14876	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 14877	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 14878	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 14879	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 14880	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 14881*	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 14882	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	blsscls2 14883*	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	metss 14884*	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 14885*	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 14886*	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 14887*	Lemma for metss2 14888. (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 14888*	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 14889*	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	bdmetval 14890*	Value of the standard bounded metric. (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 9-May-2023.)
|- D = ( x e. X , y e. X |-> inf ( { ( x C y ) , R } , RR* , < ) )   =>    |- ( ( ( C : ( X X. X ) --> RR* /\ R e. RR* ) /\ ( A e. X /\ B e. X ) ) -> ( A D B ) = inf ( { ( A C B ) , R } , RR* , < ) )
Theorem	bdxmet 14891*	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.) (Revised by Jim Kingdon, 9-May-2023.)
|- D = ( x e. X , y e. X |-> inf ( { ( x C y ) , R } , RR* , < ) )   =>    |- ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) -> D e. ( *Met ` X ) )
Theorem	bdmet 14892*	The standard bounded metric is a proper metric given an extended metric and a positive real cutoff. (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 19-May-2023.)
|- D = ( x e. X , y e. X |-> inf ( { ( x C y ) , R } , RR* , < ) )   =>    |- ( ( C e. ( *Met ` X ) /\ R e. RR+ ) -> D e. ( Met ` X ) )
Theorem	bdbl 14893*	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.) (Revised by Jim Kingdon, 19-May-2023.)
|- D = ( x e. X , y e. X |-> inf ( { ( x C y ) , R } , RR* , < ) )   =>    |- ( ( ( 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	bdmopn 14894*	The standard bounded metric corresponding to C generates the same topology as C. (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 19-May-2023.)
|- D = ( x e. X , y e. X |-> inf ( { ( x C y ) , R } , RR* , < ) )   &    |- J = ( MetOpen ` C )   =>    |- ( ( C e. ( *Met ` X ) /\ R e. RR* /\ 0 < R ) -> J = ( MetOpen ` D ) )
Theorem	mopnex 14895*	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	metrest 14896	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	xmetxp 14897*	The maximum metric (Chebyshev distance) on the product of two sets. (Contributed by Jim Kingdon, 11-Oct-2023.)
|- P = ( u e. ( X X. Y ) , v e. ( X X. Y ) |-> sup ( { ( ( 1st ` u ) M ( 1st ` v ) ) , ( ( 2nd ` u ) N ( 2nd ` v ) ) } , RR* , < ) )   &    |- ( ph -> M e. ( *Met ` X ) )   &    |- ( ph -> N e. ( *Met ` Y ) )   =>    |- ( ph -> P e. ( *Met ` ( X X. Y ) ) )
Theorem	xmetxpbl 14898*	The maximum metric (Chebyshev distance) on the product of two sets, expressed in terms of balls centered on a point C with radius R. (Contributed by Jim Kingdon, 22-Oct-2023.)
|- P = ( u e. ( X X. Y ) , v e. ( X X. Y ) |-> sup ( { ( ( 1st ` u ) M ( 1st ` v ) ) , ( ( 2nd ` u ) N ( 2nd ` v ) ) } , RR* , < ) )   &    |- ( ph -> M e. ( *Met ` X ) )   &    |- ( ph -> N e. ( *Met ` Y ) )   &    |- ( ph -> R e. RR* )   &    |- ( ph -> C e. ( X X. Y ) )   =>    |- ( ph -> ( C ( ball ` P ) R ) = ( ( ( 1st ` C ) ( ball ` M ) R ) X. ( ( 2nd ` C ) ( ball ` N ) R ) ) )
Theorem	xmettxlem 14899*	Lemma for xmettx 14900. (Contributed by Jim Kingdon, 15-Oct-2023.)
|- P = ( u e. ( X X. Y ) , v e. ( X X. Y ) |-> sup ( { ( ( 1st ` u ) M ( 1st ` v ) ) , ( ( 2nd ` u ) N ( 2nd ` v ) ) } , RR* , < ) )   &    |- ( ph -> M e. ( *Met ` X ) )   &    |- ( ph -> N e. ( *Met ` Y ) )   &    |- J = ( MetOpen ` M )   &    |- K = ( MetOpen ` N )   &    |- L = ( MetOpen ` P )   =>    |- ( ph -> L C_ ( J tX K ) )
Theorem	xmettx 14900*	The maximum metric (Chebyshev distance) on the product of two sets, expressed as a binary topological product. (Contributed by Jim Kingdon, 11-Oct-2023.)
|- P = ( u e. ( X X. Y ) , v e. ( X X. Y ) |-> sup ( { ( ( 1st ` u ) M ( 1st ` v ) ) , ( ( 2nd ` u ) N ( 2nd ` v ) ) } , RR* , < ) )   &    |- ( ph -> M e. ( *Met ` X ) )   &    |- ( ph -> N e. ( *Met ` Y ) )   &    |- J = ( MetOpen ` M )   &    |- K = ( MetOpen ` N )   &    |- L = ( MetOpen ` P )   =>    |- ( ph -> L = ( J tX K ) )