P. 214 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 21301-21400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	restutopopn 21301	The restriction of the topology induced by an uniform structure to an open set. (Contributed by Thierry Arnoux, 16-Dec-2017.)
|- ( ( U e. (UnifOn ` X ) /\ A e. (unifTop ` U ) ) -> ( (unifTop ` U ) ↾t A ) = (unifTop ` ( U ↾t ( A X. A ) ) ) )
Theorem	ustuqtoplem 21302*	Lemma for ustuqtop 21309. (Contributed by Thierry Arnoux, 11-Jan-2018.)
|- N = ( p e. X |-> ran ( v e. U |-> ( v " { p } ) ) )   =>    |- ( ( ( U e. (UnifOn ` X ) /\ P e. X ) /\ A e. V ) -> ( A e. ( N ` P ) <-> E. w e. U A = ( w " { P } ) ) )
Theorem	ustuqtop0 21303*	Lemma for ustuqtop 21309. (Contributed by Thierry Arnoux, 11-Jan-2018.)
|- N = ( p e. X |-> ran ( v e. U |-> ( v " { p } ) ) )   =>    |- ( U e. (UnifOn ` X ) -> N : X --> ~P ~P X )
Theorem	ustuqtop1 21304*	Lemma for ustuqtop 21309, similar to ssnei2 20180. (Contributed by Thierry Arnoux, 11-Jan-2018.)
|- N = ( p e. X |-> ran ( v e. U |-> ( v " { p } ) ) )   =>    |- ( ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) -> b e. ( N ` p ) )
Theorem	ustuqtop2 21305*	Lemma for ustuqtop 21309. (Contributed by Thierry Arnoux, 11-Jan-2018.)
|- N = ( p e. X |-> ran ( v e. U |-> ( v " { p } ) ) )   =>    |- ( ( U e. (UnifOn ` X ) /\ p e. X ) -> ( fi ` ( N ` p ) ) C_ ( N ` p ) )
Theorem	ustuqtop3 21306*	Lemma for ustuqtop 21309, similar to elnei 20175. (Contributed by Thierry Arnoux, 11-Jan-2018.)
|- N = ( p e. X |-> ran ( v e. U |-> ( v " { p } ) ) )   =>    |- ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) -> p e. a )
Theorem	ustuqtop4 21307*	Lemma for ustuqtop 21309. (Contributed by Thierry Arnoux, 11-Jan-2018.)
|- N = ( p e. X |-> ran ( v e. U |-> ( v " { p } ) ) )   =>    |- ( ( ( U e. (UnifOn ` X ) /\ p e. X ) /\ a e. ( N ` p ) ) -> E. b e. ( N ` p ) A. q e. b a e. ( N ` q ) )
Theorem	ustuqtop5 21308*	Lemma for ustuqtop 21309. (Contributed by Thierry Arnoux, 11-Jan-2018.)
|- N = ( p e. X |-> ran ( v e. U |-> ( v " { p } ) ) )   =>    |- ( ( U e. (UnifOn ` X ) /\ p e. X ) -> X e. ( N ` p ) )
Theorem	ustuqtop 21309*	For a given uniform structure U on a set X, there is a unique topology j such that the set ran ( v e. U |-> ( v " { p } ) ) is the filter of the neighborhoods of p for that topology. Proposition 1 of [BourbakiTop1] p. II.3. (Contributed by Thierry Arnoux, 11-Jan-2018.)
|- N = ( p e. X |-> ran ( v e. U |-> ( v " { p } ) ) )   =>    |- ( U e. (UnifOn ` X ) -> E! j e. (TopOn ` X ) A. p e. X ( N ` p ) = ( ( nei ` j ) ` { p } ) )
Theorem	utopsnneiplem 21310*	The neighborhoods of a point P for the topology induced by an uniform space U. (Contributed by Thierry Arnoux, 11-Jan-2018.)
|- J = (unifTop ` U )   &    |- K = { a e. ~P X | A. p e. a a e. ( N ` p ) }   &    |- N = ( p e. X |-> ran ( v e. U |-> ( v " { p } ) ) )   =>    |- ( ( U e. (UnifOn ` X ) /\ P e. X ) -> ( ( nei ` J ) ` { P } ) = ran ( v e. U |-> ( v " { P } ) ) )
Theorem	utopsnneip 21311*	The neighborhoods of a point P for the topology induced by an uniform space U. (Contributed by Thierry Arnoux, 13-Jan-2018.)
|- J = (unifTop ` U )   =>    |- ( ( U e. (UnifOn ` X ) /\ P e. X ) -> ( ( nei ` J ) ` { P } ) = ran ( v e. U |-> ( v " { P } ) ) )
Theorem	utopsnnei 21312	Images of singletons by entourages V are neighborhoods of those singletons. (Contributed by Thierry Arnoux, 13-Jan-2018.)
|- J = (unifTop ` U )   =>    |- ( ( U e. (UnifOn ` X ) /\ V e. U /\ P e. X ) -> ( V " { P } ) e. ( ( nei ` J ) ` { P } ) )
Theorem	utop2nei 21313	For any symmetrical entourage V and any relation M, build a neighborhood of M. First part of proposition 2 of [BourbakiTop1] p. II.4. (Contributed by Thierry Arnoux, 14-Jan-2018.)
|- J = (unifTop ` U )   =>    |- ( ( U e. (UnifOn ` X ) /\ ( V e. U /\ `' V = V ) /\ M C_ ( X X. X ) ) -> ( V o. ( M o. V ) ) e. ( ( nei ` ( J tX J ) ) ` M ) )
Theorem	utop3cls 21314	Relation between a topological closure and a symmetric entourage in an uniform space. Second part of proposition 2 of [BourbakiTop1] p. II.4. (Contributed by Thierry Arnoux, 17-Jan-2018.)
|- J = (unifTop ` U )   =>    |- ( ( ( U e. (UnifOn ` X ) /\ M C_ ( X X. X ) ) /\ ( V e. U /\ `' V = V ) ) -> ( ( cls ` ( J tX J ) ) ` M ) C_ ( V o. ( M o. V ) ) )
Theorem	utopreg 21315	All Hausdorff uniform spaces are regular. Proposition 3 of [BourbakiTop1] p. II.5. (Contributed by Thierry Arnoux, 16-Jan-2018.)
|- J = (unifTop ` U )   =>    |- ( ( U e. (UnifOn ` X ) /\ J e. Haus ) -> J e. Reg )
12.3.3  Uniform Spaces
Syntax	cuss 21316	Extend class notation with the Uniform Structure extractor function.
class UnifSt
Syntax	cusp 21317	Extend class notation with the class of uniform spaces.
class UnifSp
Syntax	ctus 21318	Extend class notation with the function mapping a uniform structure to a uniform space.
class toUnifSp
Definition	df-uss 21319	Define the uniform structure extractor function. Similarly with df-topn 15370 this differs from df-unif 15261 when a structure has been restricted using df-ress 15176; in this case the UnifSet component will still have a uniform set over the larger set, and this function fixes this by restricting the uniform set as well. (Contributed by Thierry Arnoux, 1-Dec-2017.)
|- UnifSt = ( f e. _V |-> ( ( UnifSet ` f ) ↾t ( ( Base ` f ) X. ( Base ` f ) ) ) )
Definition	df-usp 21320	Definition of a uniform space, i.e. a base set with an uniform structure and its induced topology. Derived from definition 3 of [BourbakiTop1] p. II.4. (Contributed by Thierry Arnoux, 17-Nov-2017.)
|- UnifSp = { f | ( (UnifSt ` f ) e. (UnifOn ` ( Base ` f ) ) /\ ( TopOpen ` f ) = (unifTop ` (UnifSt ` f ) ) ) }
Definition	df-tus 21321	Define the function mapping a uniform structure to a uniform space. (Contributed by Thierry Arnoux, 17-Nov-2017.)
|- toUnifSp = ( u e. U. ran UnifOn |-> ( { <. ( Base ` ndx ) , dom U. u >. , <. ( UnifSet ` ndx ) , u >. } sSet <. (TopSet ` ndx ) , (unifTop ` u ) >. ) )
Theorem	ussval 21322	The uniform structure on uniform space W. This proof uses a trick with fvprc 5881 to avoid requiring W to be a set. (Contributed by Thierry Arnoux, 3-Dec-2017.)
|- B = ( Base ` W )   &    |- U = ( UnifSet ` W )   =>    |- ( U ↾t ( B X. B ) ) = (UnifSt ` W )
Theorem	ussid 21323	In case the base of the UnifSt element of the uniform space is the base of its element structure, then UnifSt does not restrict it further. (Contributed by Thierry Arnoux, 4-Dec-2017.)
|- B = ( Base ` W )   &    |- U = ( UnifSet ` W )   =>    |- ( ( B X. B ) = U. U -> U = (UnifSt ` W ) )
Theorem	isusp 21324	The predicate W is a uniform space. (Contributed by Thierry Arnoux, 4-Dec-2017.)
|- B = ( Base ` W )   &    |- U = (UnifSt ` W )   &    |- J = ( TopOpen ` W )   =>    |- ( W e. UnifSp <-> ( U e. (UnifOn ` B ) /\ J = (unifTop ` U ) ) )
Theorem	ressunif 21325	UnifSet is unaffected by restriction. (Contributed by Thierry Arnoux, 7-Dec-2017.)
|- H = ( G ↾s A )   &    |- U = ( UnifSet ` G )   =>    |- ( A e. V -> U = ( UnifSet ` H ) )
Theorem	ressuss 21326	Value of the uniform structure of a restricted space. (Contributed by Thierry Arnoux, 12-Dec-2017.)
|- ( A e. V -> (UnifSt ` ( W ↾s A ) ) = ( (UnifSt ` W ) ↾t ( A X. A ) ) )
Theorem	ressust 21327	The uniform structure of a restricted space. (Contributed by Thierry Arnoux, 22-Jan-2018.)
|- X = ( Base ` W )   &    |- T = (UnifSt ` ( W ↾s A ) )   =>    |- ( ( W e. UnifSp /\ A C_ X ) -> T e. (UnifOn ` A ) )
Theorem	ressusp 21328	The restriction of a uniform topological space to an open set is a uniform space. (Contributed by Thierry Arnoux, 16-Dec-2017.)
|- B = ( Base ` W )   &    |- J = ( TopOpen ` W )   =>    |- ( ( W e. UnifSp /\ W e. TopSp /\ A e. J ) -> ( W ↾s A ) e. UnifSp )
Theorem	tusval 21329	The value of the uniform space mapping function. (Contributed by Thierry Arnoux, 5-Dec-2017.)
|- ( U e. (UnifOn ` X ) -> (toUnifSp ` U ) = ( { <. ( Base ` ndx ) , dom U. U >. , <. ( UnifSet ` ndx ) , U >. } sSet <. (TopSet ` ndx ) , (unifTop ` U ) >. ) )
Theorem	tuslem 21330	Lemma for tusbas 21331, tusunif 21332, and tustopn 21334. (Contributed by Thierry Arnoux, 5-Dec-2017.)
|- K = (toUnifSp ` U )   =>    |- ( U e. (UnifOn ` X ) -> ( X = ( Base ` K ) /\ U = ( UnifSet ` K ) /\ (unifTop ` U ) = ( TopOpen ` K ) ) )
Theorem	tusbas 21331	The base set of a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.)
|- K = (toUnifSp ` U )   =>    |- ( U e. (UnifOn ` X ) -> X = ( Base ` K ) )
Theorem	tusunif 21332	The uniform structure of a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.)
|- K = (toUnifSp ` U )   =>    |- ( U e. (UnifOn ` X ) -> U = ( UnifSet ` K ) )
Theorem	tususs 21333	The uniform structure of a constructed uniform space. (Contributed by Thierry Arnoux, 15-Dec-2017.)
|- K = (toUnifSp ` U )   =>    |- ( U e. (UnifOn ` X ) -> U = (UnifSt ` K ) )
Theorem	tustopn 21334	The topology induced by a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.)
|- K = (toUnifSp ` U )   &    |- J = (unifTop ` U )   =>    |- ( U e. (UnifOn ` X ) -> J = ( TopOpen ` K ) )
Theorem	tususp 21335	A constructed uniform space is an uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.)
|- K = (toUnifSp ` U )   =>    |- ( U e. (UnifOn ` X ) -> K e. UnifSp )
Theorem	tustps 21336	A constructed uniform space is a topological space. (Contributed by Thierry Arnoux, 25-Jan-2018.)
|- K = (toUnifSp ` U )   =>    |- ( U e. (UnifOn ` X ) -> K e. TopSp )
Theorem	uspreg 21337	If a uniform space is Hausdorff, it is regular. Proposition 3 of [BourbakiTop1] p. II.5. (Contributed by Thierry Arnoux, 4-Jan-2018.)
|- J = ( TopOpen ` W )   =>    |- ( ( W e. UnifSp /\ J e. Haus ) -> J e. Reg )
12.3.4  Uniform continuity
Syntax	cucn 21338	Extend class notation with the uniform continuity operation.
class Cnu
Definition	df-ucn 21339*	Define a function on two uniform structures which value is the set of uniformly continuous functions from the first uniform structure to the second. A function f is uniformly continuous if, roughly speaking, it is possible to guarantee that ( f ` x ) and ( f ` y ) be as close to each other as we please by requiring only that x and y are sufficiently close to each other; unlike ordinary continuity, the maximum distance between ( f ` x ) and ( f ` y ) cannot depend on x and y themselves. This formulation is the definition 1 of [BourbakiTop1] p. II.6. (Contributed by Thierry Arnoux, 16-Nov-2017.)
|- Cnu = ( u e. U. ran UnifOn , v e. U. ran UnifOn |-> { f e. ( dom U. v ^m dom U. u ) | A. s e. v E. r e. u A. x e. dom U. u A. y e. dom U. u ( x r y -> ( f ` x ) s ( f ` y ) ) } )
Theorem	ucnval 21340*	The set of all uniformly continuous function from uniform space U to uniform space V. (Contributed by Thierry Arnoux, 16-Nov-2017.)
|- ( ( U e. (UnifOn ` X ) /\ V e. (UnifOn ` Y ) ) -> ( U Cnu V ) = { f e. ( Y ^m X ) | A. s e. V E. r e. U A. x e. X A. y e. X ( x r y -> ( f ` x ) s ( f ` y ) ) } )
Theorem	isucn 21341*	The predicate " F is a uniformly continuous function from uniform space U to uniform space V." (Contributed by Thierry Arnoux, 16-Nov-2017.)
|- ( ( U e. (UnifOn ` X ) /\ V e. (UnifOn ` Y ) ) -> ( F e. ( U Cnu V ) <-> ( F : X --> Y /\ A. s e. V E. r e. U A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) ) ) )
Theorem	isucn2 21342*	The predicate " F is a uniformly continuous function from uniform space U to uniform space V." , expressed with filter bases for the entourages. (Contributed by Thierry Arnoux, 26-Jan-2018.)
|- U = ( ( X X. X ) filGen R )   &    |- V = ( ( Y X. Y ) filGen S )   &    |- ( ph -> U e. (UnifOn ` X ) )   &    |- ( ph -> V e. (UnifOn ` Y ) )   &    |- ( ph -> R e. ( fBas ` ( X X. X ) ) )   &    |- ( ph -> S e. ( fBas ` ( Y X. Y ) ) )   =>    |- ( ph -> ( F e. ( U Cnu V ) <-> ( F : X --> Y /\ A. s e. S E. r e. R A. x e. X A. y e. X ( x r y -> ( F ` x ) s ( F ` y ) ) ) ) )
Theorem	ucnimalem 21343*	Reformulate the G function as a mapping with one variable. (Contributed by Thierry Arnoux, 19-Nov-2017.)
|- ( ph -> U e. (UnifOn ` X ) )   &    |- ( ph -> V e. (UnifOn ` Y ) )   &    |- ( ph -> F e. ( U Cnu V ) )   &    |- ( ph -> W e. V )   &    |- G = ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. )   =>    |- G = ( p e. ( X X. X ) |-> <. ( F ` ( 1st ` p ) ) , ( F ` ( 2nd ` p ) ) >. )
Theorem	ucnima 21344*	An equivalent statement of the definition of uniformly continuous function. (Contributed by Thierry Arnoux, 19-Nov-2017.)
|- ( ph -> U e. (UnifOn ` X ) )   &    |- ( ph -> V e. (UnifOn ` Y ) )   &    |- ( ph -> F e. ( U Cnu V ) )   &    |- ( ph -> W e. V )   &    |- G = ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. )   =>    |- ( ph -> E. r e. U ( G " r ) C_ W )
Theorem	ucnprima 21345*	The preimage by a uniformly continuous function F of an entourage W of Y is an entourage of X. Note of the definition 1 of [BourbakiTop1] p. II.6. (Contributed by Thierry Arnoux, 19-Nov-2017.)
|- ( ph -> U e. (UnifOn ` X ) )   &    |- ( ph -> V e. (UnifOn ` Y ) )   &    |- ( ph -> F e. ( U Cnu V ) )   &    |- ( ph -> W e. V )   &    |- G = ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. )   =>    |- ( ph -> ( `' G " W ) e. U )
Theorem	iducn 21346	The identity is uniformly continuous from a uniform structure to itself. Example 1 of [BourbakiTop1] p. II.6. (Contributed by Thierry Arnoux, 16-Nov-2017.)
|- ( U e. (UnifOn ` X ) -> ( _I |` X ) e. ( U Cnu U ) )
Theorem	cstucnd 21347	A constant function is uniformly continuous. Deduction form. Example 1 of [BourbakiTop1] p. II.6. (Contributed by Thierry Arnoux, 16-Nov-2017.)
|- ( ph -> U e. (UnifOn ` X ) )   &    |- ( ph -> V e. (UnifOn ` Y ) )   &    |- ( ph -> A e. Y )   =>    |- ( ph -> ( X X. { A } ) e. ( U Cnu V ) )
Theorem	ucncn 21348	Uniform continuity implies continuity. Deduction form. Proposition 1 of [BourbakiTop1] p. II.6. (Contributed by Thierry Arnoux, 30-Nov-2017.)
|- J = ( TopOpen ` R )   &    |- K = ( TopOpen ` S )   &    |- ( ph -> R e. UnifSp )   &    |- ( ph -> S e. UnifSp )   &    |- ( ph -> R e. TopSp )   &    |- ( ph -> S e. TopSp )   &    |- ( ph -> F e. ( (UnifSt ` R ) Cnu (UnifSt ` S ) ) )   =>    |- ( ph -> F e. ( J Cn K ) )
12.3.5  Cauchy filters in uniform spaces
Syntax	ccfilu 21349	Extend class notation with the set of Cauchy filter bases.
class CauFilu
Definition	df-cfilu 21350*	Define the set of Cauchy filter bases on a uniform space. A Cauchy filter base is a filter base on the set such that for every entourage v, there is an element a of the filter "small enough in v " i.e. such that every pair { x , y } of points in a is related by v". Definition 2 of [BourbakiTop1] p. II.13. (Contributed by Thierry Arnoux, 16-Nov-2017.)
|- CauFilu = ( u e. U. ran UnifOn |-> { f e. ( fBas ` dom U. u ) | A. v e. u E. a e. f ( a X. a ) C_ v } )
Theorem	iscfilu 21351*	The predicate " F is a Cauchy filter base on uniform space U." (Contributed by Thierry Arnoux, 18-Nov-2017.)
|- ( U e. (UnifOn ` X ) -> ( F e. (CauFilu ` U ) <-> ( F e. ( fBas ` X ) /\ A. v e. U E. a e. F ( a X. a ) C_ v ) ) )
Theorem	cfilufbas 21352	A Cauchy filter base is a filter base. (Contributed by Thierry Arnoux, 19-Nov-2017.)
|- ( ( U e. (UnifOn ` X ) /\ F e. (CauFilu ` U ) ) -> F e. ( fBas ` X ) )
Theorem	cfiluexsm 21353*	For a Cauchy filter base and any entourage V, there is an element of the filter small in V. (Contributed by Thierry Arnoux, 19-Nov-2017.)
|- ( ( U e. (UnifOn ` X ) /\ F e. (CauFilu ` U ) /\ V e. U ) -> E. a e. F ( a X. a ) C_ V )
Theorem	fmucndlem 21354*	Lemma for fmucnd 21355. (Contributed by Thierry Arnoux, 19-Nov-2017.)
|- ( ( F Fn X /\ A C_ X ) -> ( ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) " ( A X. A ) ) = ( ( F " A ) X. ( F " A ) ) )
Theorem	fmucnd 21355*	The image of a Cauchy filter base by an uniformly continuous function is a Cauchy filter base. Deduction form. Proposition 3 of [BourbakiTop1] p. II.13. (Contributed by Thierry Arnoux, 18-Nov-2017.)
|- ( ph -> U e. (UnifOn ` X ) )   &    |- ( ph -> V e. (UnifOn ` Y ) )   &    |- ( ph -> F e. ( U Cnu V ) )   &    |- ( ph -> C e. (CauFilu ` U ) )   &    |- D = ran ( a e. C |-> ( F " a ) )   =>    |- ( ph -> D e. (CauFilu ` V ) )
Theorem	cfilufg 21356	The filter generated by a Cauchy filter base is still a Cauchy filter base. (Contributed by Thierry Arnoux, 24-Jan-2018.)
|- ( ( U e. (UnifOn ` X ) /\ F e. (CauFilu ` U ) ) -> ( X filGen F ) e. (CauFilu ` U ) )
Theorem	trcfilu 21357	Condition for the trace of a Cauchy filter base to be a Cauchy filter base for the restricted uniform structure. (Contributed by Thierry Arnoux, 24-Jan-2018.)
|- ( ( U e. (UnifOn ` X ) /\ ( F e. (CauFilu ` U ) /\ -. (/) e. ( F ↾t A ) ) /\ A C_ X ) -> ( F ↾t A ) e. (CauFilu ` ( U ↾t ( A X. A ) ) ) )
Theorem	cfiluweak 21358	A Cauchy filter base is also a Cauchy filter base on any coarser uniform structure. (Contributed by Thierry Arnoux, 24-Jan-2018.)
|- ( ( U e. (UnifOn ` X ) /\ A C_ X /\ F e. (CauFilu ` ( U ↾t ( A X. A ) ) ) ) -> F e. (CauFilu ` U ) )
Theorem	neipcfilu 21359	In an uniform space, a neighboring filter is a Cauchy filter base. (Contributed by Thierry Arnoux, 24-Jan-2018.)
|- X = ( Base ` W )   &    |- J = ( TopOpen ` W )   &    |- U = (UnifSt ` W )   =>    |- ( ( W e. UnifSp /\ W e. TopSp /\ P e. X ) -> ( ( nei ` J ) ` { P } ) e. (CauFilu ` U ) )
12.3.6  Complete uniform spaces
Syntax	ccusp 21360	Extend class notation with the class of all complete uniform spaces.
class CUnifSp
Definition	df-cusp 21361*	Define the class of all complete uniform spaces. Definition 3 of [BourbakiTop1] p. II.15. (Contributed by Thierry Arnoux, 1-Dec-2017.)
|- CUnifSp = { w e. UnifSp | A. c e. ( Fil ` ( Base ` w ) ) ( c e. (CauFilu ` (UnifSt ` w ) ) -> ( ( TopOpen ` w ) fLim c ) =/= (/) ) }
Theorem	iscusp 21362*	The predicate " W is a complete uniform space." (Contributed by Thierry Arnoux, 3-Dec-2017.)
|- ( W e. CUnifSp <-> ( W e. UnifSp /\ A. c e. ( Fil ` ( Base ` W ) ) ( c e. (CauFilu ` (UnifSt ` W ) ) -> ( ( TopOpen ` W ) fLim c ) =/= (/) ) ) )
Theorem	cuspusp 21363	A complete uniform space is an uniform space. (Contributed by Thierry Arnoux, 3-Dec-2017.)
|- ( W e. CUnifSp -> W e. UnifSp )
Theorem	cuspcvg 21364	In a complete uniform space, any Cauchy filter C has a limit. (Contributed by Thierry Arnoux, 3-Dec-2017.)
|- B = ( Base ` W )   &    |- J = ( TopOpen ` W )   =>    |- ( ( W e. CUnifSp /\ C e. (CauFilu ` (UnifSt ` W ) ) /\ C e. ( Fil ` B ) ) -> ( J fLim C ) =/= (/) )
Theorem	iscusp2 21365*	The predicate " W is a complete uniform space." (Contributed by Thierry Arnoux, 15-Dec-2017.)
|- B = ( Base ` W )   &    |- U = (UnifSt ` W )   &    |- J = ( TopOpen ` W )   =>    |- ( W e. CUnifSp <-> ( W e. UnifSp /\ A. c e. ( Fil ` B ) ( c e. (CauFilu ` U ) -> ( J fLim c ) =/= (/) ) ) )
Theorem	cnextucn 21366*	Extension by continuity. Proposition 11 of [BourbakiTop1] p. II.20. Given a topology J on X, a subset A dense in X, this states a condition for F from A to a space Y Hausdorff and complete to be extensible by continuity. (Contributed by Thierry Arnoux, 4-Dec-2017.)
|- X = ( Base ` V )   &    |- Y = ( Base ` W )   &    |- J = ( TopOpen ` V )   &    |- K = ( TopOpen ` W )   &    |- U = (UnifSt ` W )   &    |- ( ph -> V e. TopSp )   &    |- ( ph -> W e. TopSp )   &    |- ( ph -> W e. CUnifSp )   &    |- ( ph -> K e. Haus )   &    |- ( ph -> A C_ X )   &    |- ( ph -> F : A --> Y )   &    |- ( ph -> ( ( cls ` J ) ` A ) = X )   &    |- ( ( ph /\ x e. X ) -> ( ( Y FilMap F ) ` ( ( ( nei ` J ) ` { x } ) ↾t A ) ) e. (CauFilu ` U ) )   =>    |- ( ph -> ( ( JCnExt K ) ` F ) e. ( J Cn K ) )
Theorem	ucnextcn 21367	Extension by continuity. Theorem 2 of [BourbakiTop1] p. II.20. Given an uniform space on a set X, a subset A dense in X, and a function F uniformly continuous from A to Y, that function can be extended by continuity to the whole X, and its extension is uniformly continuous. (Contributed by Thierry Arnoux, 25-Jan-2018.)
|- X = ( Base ` V )   &    |- Y = ( Base ` W )   &    |- J = ( TopOpen ` V )   &    |- K = ( TopOpen ` W )   &    |- S = (UnifSt ` V )   &    |- T = (UnifSt ` ( V ↾s A ) )   &    |- U = (UnifSt ` W )   &    |- ( ph -> V e. TopSp )   &    |- ( ph -> V e. UnifSp )   &    |- ( ph -> W e. TopSp )   &    |- ( ph -> W e. CUnifSp )   &    |- ( ph -> K e. Haus )   &    |- ( ph -> A C_ X )   &    |- ( ph -> F e. ( T Cnu U ) )   &    |- ( ph -> ( ( cls ` J ) ` A ) = X )   =>    |- ( ph -> ( ( JCnExt K ) ` F ) e. ( J Cn K ) )
12.4  Metric spaces
12.4.1  Pseudometric spaces
Theorem	ispsmet 21368*	Express the predicate " D is a pseudometric." (Contributed by Thierry Arnoux, 7-Feb-2018.)
|- ( X e. V -> ( D e. (PsMet ` X ) <-> ( D : ( X X. X ) --> RR* /\ A. x e. X ( ( x D x ) = 0 /\ A. y e. X A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) ) )
Theorem	psmetdmdm 21369	Recover the base set from a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.)
|- ( D e. (PsMet ` X ) -> X = dom dom D )
Theorem	psmetf 21370	The distance function of a pseudometric as a function. (Contributed by Thierry Arnoux, 7-Feb-2018.)
|- ( D e. (PsMet ` X ) -> D : ( X X. X ) --> RR* )
Theorem	psmetcl 21371	Closure of the distance function of a pseudometric space. (Contributed by Thierry Arnoux, 7-Feb-2018.)
|- ( ( D e. (PsMet ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) e. RR* )
Theorem	psmet0 21372	The distance function of a pseudometric space is zero if its arguments are equal. (Contributed by Thierry Arnoux, 7-Feb-2018.)
|- ( ( D e. (PsMet ` X ) /\ A e. X ) -> ( A D A ) = 0 )
Theorem	psmettri2 21373	Triangle inequality for the distance function of a pseudometric. (Contributed by Thierry Arnoux, 11-Feb-2018.)
|- ( ( D e. (PsMet ` X ) /\ ( C e. X /\ A e. X /\ B e. X ) ) -> ( A D B ) <_ ( ( C D A ) +e ( C D B ) ) )
Theorem	psmetsym 21374	The distance function of a pseudometric is symmetrical. (Contributed by Thierry Arnoux, 7-Feb-2018.)
|- ( ( D e. (PsMet ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) = ( B D A ) )
Theorem	psmettri 21375	Triangle inequality for the distance function of a pseudometric space. (Contributed by Thierry Arnoux, 11-Feb-2018.)
|- ( ( D e. (PsMet ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D B ) <_ ( ( A D C ) +e ( C D B ) ) )
Theorem	psmetge0 21376	The distance function of a pseudometric space is nonnegative. (Contributed by Thierry Arnoux, 7-Feb-2018.)
|- ( ( D e. (PsMet ` X ) /\ A e. X /\ B e. X ) -> 0 <_ ( A D B ) )
Theorem	psmetxrge0 21377	The distance function of a pseudometric space is a function into the nonnegative extended real numbers. (Contributed by Thierry Arnoux, 24-Feb-2018.)
|- ( D e. (PsMet ` X ) -> D : ( X X. X ) --> ( 0 [,] +oo ) )
Theorem	psmetres2 21378	Restriction of a pseudometric. (Contributed by Thierry Arnoux, 11-Feb-2018.)
|- ( ( D e. (PsMet ` X ) /\ R C_ X ) -> ( D |` ( R X. R ) ) e. (PsMet ` R ) )
Theorem	psmetlecl 21379	Real closure of an extended metric value that is upper bounded by a real. (Contributed by Thierry Arnoux, 11-Mar-2018.)
|- ( ( D e. (PsMet ` X ) /\ ( A e. X /\ B e. X ) /\ ( C e. RR /\ ( A D B ) <_ C ) ) -> ( A D B ) e. RR )
12.4.2  Basic metric space properties
Syntax	cxme 21380	Extend class notation with the class of all extended metric spaces.
class *MetSp
Syntax	cmt 21381	Extend class notation with the class of all metric spaces.
class MetSp
Syntax	ctmt 21382	Extend class notation with the function mapping a metric to a metric space.
class toMetSp
Definition	df-xms 21383	Define the (proper) class of all extended metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- *MetSp = { f e. TopSp | ( TopOpen ` f ) = ( MetOpen ` ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) ) }
Definition	df-ms 21384	Define the (proper) class of all metric spaces. (Contributed by NM, 27-Aug-2006.)
|- MetSp = { f e. *MetSp | ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) e. ( Met ` ( Base ` f ) ) }
Definition	df-tms 21385	Define the function mapping a metric to a metric space. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- toMetSp = ( d e. U. ran *Met |-> ( { <. ( Base ` ndx ) , dom dom d >. , <. ( dist ` ndx ) , d >. } sSet <. (TopSet ` ndx ) , ( MetOpen ` d ) >. ) )
Theorem	ismet 21386*	Express the predicate " D is a metric." (Contributed by NM, 25-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- ( X e. A -> ( D e. ( Met ` X ) <-> ( D : ( X X. X ) --> RR /\ A. x e. X A. y e. X ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. X ( x D y ) <_ ( ( z D x ) + ( z D y ) ) ) ) ) )
Theorem	isxmet 21387*	Express the predicate " D is an extended metric." (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( X e. A -> ( D e. ( *Met ` X ) <-> ( D : ( X X. X ) --> RR* /\ A. x e. X A. y e. X ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) ) )
Theorem	ismeti 21388*	Properties that determine a metric. (Contributed by NM, 17-Nov-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- X e. _V   &    |- D : ( X X. X ) --> RR   &    |- ( ( x e. X /\ y e. X ) -> ( ( x D y ) = 0 <-> x = y ) )   &    |- ( ( x e. X /\ y e. X /\ z e. X ) -> ( x D y ) <_ ( ( z D x ) + ( z D y ) ) )   =>    |- D e. ( Met ` X )
Theorem	isxmetd 21389*	Properties that determine an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ph -> X e. _V )   &    |- ( ph -> D : ( X X. X ) --> RR* )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( ( x D y ) = 0 <-> x = y ) )   &    |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) )   =>    |- ( ph -> D e. ( *Met ` X ) )
Theorem	isxmet2d 21390*	It is safe to only require the triangle inequality when the values are real (so that we can use the standard addition over the reals), but in this case the nonnegativity constraint cannot be deduced and must be provided separately. (Counterexample: D ( x , y ) = if ( x = y , 0 , -oo ) satisfies all hypotheses except nonnegativity.) (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ph -> X e. _V )   &    |- ( ph -> D : ( X X. X ) --> RR* )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> 0 <_ ( x D y ) )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( ( x D y ) <_ 0 <-> x = y ) )   &    |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) /\ ( ( z D x ) e. RR /\ ( z D y ) e. RR ) ) -> ( x D y ) <_ ( ( z D x ) + ( z D y ) ) )   =>    |- ( ph -> D e. ( *Met ` X ) )
Theorem	metflem 21391*	Lemma for metf 21393 and others. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- ( D e. ( Met ` X ) -> ( D : ( X X. X ) --> RR /\ A. x e. X A. y e. X ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. X ( x D y ) <_ ( ( z D x ) + ( z D y ) ) ) ) )
Theorem	xmetf 21392	Mapping of the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( D e. ( *Met ` X ) -> D : ( X X. X ) --> RR* )
Theorem	metf 21393	Mapping of the distance function of a metric space. (Contributed by NM, 30-Aug-2006.)
|- ( D e. ( Met ` X ) -> D : ( X X. X ) --> RR )
Theorem	xmetcl 21394	Closure of the distance function of a metric space. Part of Property M1 of [Kreyszig] p. 3. (Contributed by NM, 30-Aug-2006.)
|- ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) e. RR* )
Theorem	metcl 21395	Closure of the distance function of a metric space. Part of Property M1 of [Kreyszig] p. 3. (Contributed by NM, 30-Aug-2006.)
|- ( ( D e. ( Met ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) e. RR )
Theorem	ismet2 21396	An extended metric is a metric exactly when it takes real values for all values of the arguments. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( D e. ( Met ` X ) <-> ( D e. ( *Met ` X ) /\ D : ( X X. X ) --> RR ) )
Theorem	metxmet 21397	A metric is an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
Theorem	xmetdmdm 21398	Recover the base set from an extended metric. (Contributed by Mario Carneiro, 23-Aug-2015.)
|- ( D e. ( *Met ` X ) -> X = dom dom D )
Theorem	metdmdm 21399	Recover the base set from a metric. (Contributed by Mario Carneiro, 23-Aug-2015.)
|- ( D e. ( Met ` X ) -> X = dom dom D )
Theorem	xmetunirn 21400	Two ways to express an extended metric on an unspecified base. (Contributed by Mario Carneiro, 13-Oct-2015.)
|- ( D e. U. ran *Met <-> D e. ( *Met ` dom dom D ) )