P. 210 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 20901-21000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	utopval 20901*	The topology induced by a uniform structure U. (Contributed by Thierry Arnoux, 30-Nov-2017.)
|- ( U e. (UnifOn ` X ) -> (unifTop ` U ) = { a e. ~P X | A. x e. a E. v e. U ( v " { x } ) C_ a } )
Theorem	elutop 20902*	Open sets in the topology induced by an uniform structure U on X (Contributed by Thierry Arnoux, 30-Nov-2017.)
|- ( U e. (UnifOn ` X ) -> ( A e. (unifTop ` U ) <-> ( A C_ X /\ A. x e. A E. v e. U ( v " { x } ) C_ A ) ) )
Theorem	utoptop 20903	The topology induced by a uniform structure U is a topology. (Contributed by Thierry Arnoux, 30-Nov-2017.)
|- ( U e. (UnifOn ` X ) -> (unifTop ` U ) e. Top )
Theorem	utopbas 20904	The base of the topology induced by a uniform structure U. (Contributed by Thierry Arnoux, 5-Dec-2017.)
|- ( U e. (UnifOn ` X ) -> X = U. (unifTop ` U ) )
Theorem	utoptopon 20905	Topology induced by a uniform structure U with its base set. (Contributed by Thierry Arnoux, 5-Jan-2018.)
|- ( U e. (UnifOn ` X ) -> (unifTop ` U ) e. (TopOn ` X ) )
Theorem	restutop 20906	Restriction of a topology induced by an uniform structure (Contributed by Thierry Arnoux, 12-Dec-2017.)
|- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( (unifTop ` U ) ↾t A ) C_ (unifTop ` ( U ↾t ( A X. A ) ) ) )
Theorem	restutopopn 20907	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 20908*	Lemma for ustuqtop 20915 (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 20909*	Lemma for ustuqtop 20915 (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 20910*	Lemma for ustuqtop 20915, similar to ssnei2 19784 (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 20911*	Lemma for ustuqtop 20915 (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 20912*	Lemma for ustuqtop 20915, similar to elnei 19779 (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 20913*	Lemma for ustuqtop 20915 (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 20914*	Lemma for ustuqtop 20915 (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 20915*	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 20916*	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 20917*	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 20918	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 20919	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 20920	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 20921	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 20922	Extend class notation with the Uniform Structure extractor function.
class UnifSt
Syntax	cusp 20923	Extend class notation with the class of uniform spaces.
class UnifSp
Syntax	ctus 20924	Extend class notation with the function mapping a uniform structure to a uniform space.
class toUnifSp
Definition	df-uss 20925	Define the uniform structure extractor function. Similarly with df-topn 14913 this differs from df-unif 14807 when a structure has been restricted using df-ress 14723; 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 20926	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 20927	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 20928	The uniform structure on uniform space W. This proof uses a trick with fvprc 5842 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 20929	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 20930	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 20931	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 20932	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 20933	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 20934	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 20935	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 20936	Lemma for tusbas 20937, tusunif 20938, and tustopn 20940. (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 20937	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 20938	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 20939	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 20940	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 20941	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 20942	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 20943	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 20944	Extend class notation with the uniform continuity operation.
class Cnu
Definition	df-ucn 20945*	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 20946*	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 20947*	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 20948*	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 20949*	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 20950*	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 20951*	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 20952	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 20953	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 20954	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 20955	Extend class notation with the set of Cauchy filter bases.
class CauFilu
Definition	df-cfilu 20956*	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 20957*	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 20958	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 20959*	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 20960*	Lemma for fmucnd 20961. (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 20961*	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 20962	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 20963	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 20964	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 20965	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 20966	Extend class notation with the class of all complete uniform spaces.
class CUnifSp
Definition	df-cusp 20967*	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 20968*	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 20969	A complete uniform space is an uniform space. (Contributed by Thierry Arnoux, 3-Dec-2017.)
|- ( W e. CUnifSp -> W e. UnifSp )
Theorem	cuspcvg 20970	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 20971*	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 20972*	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 20973	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 20974*	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 20975	Recover the base set from a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.)
|- ( D e. (PsMet ` X ) -> X = dom dom D )
Theorem	psmetf 20976	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 20977	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 20978	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 20979	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 20980	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 20981	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 20982	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 20983	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 20984	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 20985	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 20986	Extend class notation with the class of all extended metric spaces.
class *MetSp
Syntax	cmt 20987	Extend class notation with the class of all metric spaces.
class MetSp
Syntax	ctmt 20988	Extend class notation with the function mapping a metric to a metric space.
class toMetSp
Definition	df-xms 20989	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 20990	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 20991	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 20992*	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 20993*	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 20994*	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 20995*	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 20996*	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 20997*	Lemma for metf 20999 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 20998	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 20999	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 21000	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* )