P. 221 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 22001-22100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tvclmod 22001	A topological vector space is a left module. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- ( W e. TopVec -> W e. LMod )
Theorem	tvclvec 22002	A topological vector space is a vector space. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- ( W e. TopVec -> W e. LVec )
12.3  Uniform Structures and Spaces
12.3.1  Uniform structures
Syntax	cust 22003	Extend class notation with the class function of uniform structures.
class UnifOn
Definition	df-ust 22004*	Definition of a uniform structure. Definition 1 of [BourbakiTop1] p. II.1. A uniform structure is used to give a generalization of the idea of Cauchy's sequence. This definition is analogous to TopOn. Elements of an uniform structure are called entourages. (Contributed by FL, 29-May-2014.) (Revised by Thierry Arnoux, 15-Nov-2017.)
|- UnifOn = ( x e. _V |-> { u | ( u C_ ~P ( x X. x ) /\ ( x X. x ) e. u /\ A. v e. u ( A. w e. ~P ( x X. x ) ( v C_ w -> w e. u ) /\ A. w e. u ( v i^i w ) e. u /\ ( ( _I |` x ) C_ v /\ `' v e. u /\ E. w e. u ( w o. w ) C_ v ) ) ) } )
Theorem	ustfn 22005	The defined uniform structure as a function. (Contributed by Thierry Arnoux, 15-Nov-2017.)
|- UnifOn Fn _V
Theorem	ustval 22006*	The class of all uniform structures for a base X. (Contributed by Thierry Arnoux, 15-Nov-2017.) (Revised by AV, 17-Sep-2021.)
|- ( X e. V -> (UnifOn ` X ) = { u | ( u C_ ~P ( X X. X ) /\ ( X X. X ) e. u /\ A. v e. u ( A. w e. ~P ( X X. X ) ( v C_ w -> w e. u ) /\ A. w e. u ( v i^i w ) e. u /\ ( ( _I |` X ) C_ v /\ `' v e. u /\ E. w e. u ( w o. w ) C_ v ) ) ) } )
Theorem	isust 22007*	The predicate " U is a uniform structure with base X." (Contributed by Thierry Arnoux, 15-Nov-2017.) (Revised by AV, 17-Sep-2021.)
|- ( X e. V -> ( U e. (UnifOn ` X ) <-> ( U C_ ~P ( X X. X ) /\ ( X X. X ) e. U /\ A. v e. U ( A. w e. ~P ( X X. X ) ( v C_ w -> w e. U ) /\ A. w e. U ( v i^i w ) e. U /\ ( ( _I |` X ) C_ v /\ `' v e. U /\ E. w e. U ( w o. w ) C_ v ) ) ) ) )
Theorem	ustssxp 22008	Entourages are subsets of the Cartesian product of the base set. (Contributed by Thierry Arnoux, 19-Nov-2017.)
|- ( ( U e. (UnifOn ` X ) /\ V e. U ) -> V C_ ( X X. X ) )
Theorem	ustssel 22009	A uniform structure is upward closed. Condition FI of [BourbakiTop1] p. I.36. (Contributed by Thierry Arnoux, 19-Nov-2017.) (Proof shortened by AV, 17-Sep-2021.)
|- ( ( U e. (UnifOn ` X ) /\ V e. U /\ W C_ ( X X. X ) ) -> ( V C_ W -> W e. U ) )
Theorem	ustbasel 22010	The full set is always an entourage. Condition FIIb of [BourbakiTop1] p. I.36. (Contributed by Thierry Arnoux, 19-Nov-2017.)
|- ( U e. (UnifOn ` X ) -> ( X X. X ) e. U )
Theorem	ustincl 22011	A uniform structure is closed under finite intersection. Condition FII of [BourbakiTop1] p. I.36. (Contributed by Thierry Arnoux, 30-Nov-2017.)
|- ( ( U e. (UnifOn ` X ) /\ V e. U /\ W e. U ) -> ( V i^i W ) e. U )
Theorem	ustdiag 22012	The diagonal set is included in any entourage, i.e. any point is V -close to itself. Condition UI of [BourbakiTop1] p. II.1. (Contributed by Thierry Arnoux, 2-Dec-2017.)
|- ( ( U e. (UnifOn ` X ) /\ V e. U ) -> ( _I |` X ) C_ V )
Theorem	ustinvel 22013	If V is an entourage, so is its inverse. Condition UII of [BourbakiTop1] p. II.1. (Contributed by Thierry Arnoux, 2-Dec-2017.)
|- ( ( U e. (UnifOn ` X ) /\ V e. U ) -> `' V e. U )
Theorem	ustexhalf 22014*	For each entourage V there is an entourage w that is "not more than half as large". Condition UIII of [BourbakiTop1] p. II.1. (Contributed by Thierry Arnoux, 2-Dec-2017.)
|- ( ( U e. (UnifOn ` X ) /\ V e. U ) -> E. w e. U ( w o. w ) C_ V )
Theorem	ustrel 22015	The elements of uniform structures, called entourages, are relations. (Contributed by Thierry Arnoux, 15-Nov-2017.)
|- ( ( U e. (UnifOn ` X ) /\ V e. U ) -> Rel V )
Theorem	ustfilxp 22016	A uniform structure on a nonempty base is a filter. Remark 3 of [BourbakiTop1] p. II.2. (Contributed by Thierry Arnoux, 15-Nov-2017.)
|- ( ( X =/= (/) /\ U e. (UnifOn ` X ) ) -> U e. ( Fil ` ( X X. X ) ) )
Theorem	ustne0 22017	A uniform structure cannot be empty. (Contributed by Thierry Arnoux, 16-Nov-2017.)
|- ( U e. (UnifOn ` X ) -> U =/= (/) )
Theorem	ustssco 22018	In an uniform structure, any entourage V is a subset of its composition with itself. (Contributed by Thierry Arnoux, 5-Jan-2018.)
|- ( ( U e. (UnifOn ` X ) /\ V e. U ) -> V C_ ( V o. V ) )
Theorem	ustexsym 22019*	In an uniform structure, for any entourage V, there exists a smaller symmetrical entourage. (Contributed by Thierry Arnoux, 4-Jan-2018.)
|- ( ( U e. (UnifOn ` X ) /\ V e. U ) -> E. w e. U ( `' w = w /\ w C_ V ) )
Theorem	ustex2sym 22020*	In an uniform structure, for any entourage V, there exists a symmetrical entourage smaller than half V. (Contributed by Thierry Arnoux, 16-Jan-2018.)
|- ( ( U e. (UnifOn ` X ) /\ V e. U ) -> E. w e. U ( `' w = w /\ ( w o. w ) C_ V ) )
Theorem	ustex3sym 22021*	In an uniform structure, for any entourage V, there exists a symmetrical entourage smaller than a third of V. (Contributed by Thierry Arnoux, 16-Jan-2018.)
|- ( ( U e. (UnifOn ` X ) /\ V e. U ) -> E. w e. U ( `' w = w /\ ( w o. ( w o. w ) ) C_ V ) )
Theorem	ustref 22022	Any element of the base set is "near" itself, i.e. entourages are reflexive. (Contributed by Thierry Arnoux, 16-Nov-2017.)
|- ( ( U e. (UnifOn ` X ) /\ V e. U /\ A e. X ) -> A V A )
Theorem	ust0 22023	The unique uniform structure of the empty set is the empty set. Remark 3 of [BourbakiTop1] p. II.2. (Contributed by Thierry Arnoux, 15-Nov-2017.)
|- (UnifOn ` (/) ) = { { (/) } }
Theorem	ustn0 22024	The empty set is not an uniform structure. (Contributed by Thierry Arnoux, 3-Dec-2017.)
|- -. (/) e. U. ran UnifOn
Theorem	ustund 22025	If two intersecting sets A and B are both small in V, their union is small in ( V ^ 2 ). Proposition 1 of [BourbakiTop1] p. II.12. This proposition actually does not require any axiom of the definition of uniform structures. (Contributed by Thierry Arnoux, 17-Nov-2017.)
|- ( ph -> ( A X. A ) C_ V )   &    |- ( ph -> ( B X. B ) C_ V )   &    |- ( ph -> ( A i^i B ) =/= (/) )   =>    |- ( ph -> ( ( A u. B ) X. ( A u. B ) ) C_ ( V o. V ) )
Theorem	ustelimasn 22026	Any point A is near enough to itself. (Contributed by Thierry Arnoux, 18-Nov-2017.)
|- ( ( U e. (UnifOn ` X ) /\ V e. U /\ A e. X ) -> A e. ( V " { A } ) )
Theorem	ustneism 22027	For a point A in X, ( V " { A } ) is small enough in ( V o. `' V ). This proposition actually does not require any axiom of the definition of uniform structures. (Contributed by Thierry Arnoux, 18-Nov-2017.)
|- ( ( V C_ ( X X. X ) /\ A e. X ) -> ( ( V " { A } ) X. ( V " { A } ) ) C_ ( V o. `' V ) )
Theorem	elrnust 22028	First direction for ustbas 22031. (Contributed by Thierry Arnoux, 16-Nov-2017.)
|- ( U e. (UnifOn ` X ) -> U e. U. ran UnifOn )
Theorem	ustbas2 22029	Second direction for ustbas 22031. (Contributed by Thierry Arnoux, 16-Nov-2017.)
|- ( U e. (UnifOn ` X ) -> X = dom U. U )
Theorem	ustuni 22030	The set union of a uniform structure is the Cartesian product of its base. (Contributed by Thierry Arnoux, 5-Dec-2017.)
|- ( U e. (UnifOn ` X ) -> U. U = ( X X. X ) )
Theorem	ustbas 22031	Recover the base of an uniform structure U. U. ran UnifOn is to UnifOn what Top is to TopOn. (Contributed by Thierry Arnoux, 16-Nov-2017.)
|- X = dom U. U   =>    |- ( U e. U. ran UnifOn <-> U e. (UnifOn ` X ) )
Theorem	ustimasn 22032	Lemma for ustuqtop 22050. (Contributed by Thierry Arnoux, 5-Dec-2017.)
|- ( ( U e. (UnifOn ` X ) /\ V e. U /\ P e. X ) -> ( V " { P } ) C_ X )
Theorem	trust 22033	The trace of a uniform structure U on a subset A is a uniform structure on A. Definition 3 of [BourbakiTop1] p. II.9. (Contributed by Thierry Arnoux, 2-Dec-2017.)
|- ( ( U e. (UnifOn ` X ) /\ A C_ X ) -> ( U ↾t ( A X. A ) ) e. (UnifOn ` A ) )
12.3.2  The topology induced by an uniform structure
Syntax	cutop 22034	Extend class notation with the function inducing a topology from a uniform structure.
class unifTop
Definition	df-utop 22035*	Definition of a topology induced by a uniform structure. Definition 3 of [BourbakiTop1] p. II.4. (Contributed by Thierry Arnoux, 17-Nov-2017.)
|- unifTop = ( u e. U. ran UnifOn |-> { a e. ~P dom U. u | A. x e. a E. v e. u ( v " { x } ) C_ a } )
Theorem	utopval 22036*	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 22037*	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 22038	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 22039	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 22040	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 22041	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 22042	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 22043*	Lemma for ustuqtop 22050. (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 22044*	Lemma for ustuqtop 22050. (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 22045*	Lemma for ustuqtop 22050, similar to ssnei2 20920. (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 22046*	Lemma for ustuqtop 22050. (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 22047*	Lemma for ustuqtop 22050, similar to elnei 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 ) ) -> p e. a )
Theorem	ustuqtop4 22048*	Lemma for ustuqtop 22050. (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 22049*	Lemma for ustuqtop 22050. (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 22050*	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 22051*	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 22052*	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 22053	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 22054	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 22055	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 22056	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 22057	Extend class notation with the Uniform Structure extractor function.
class UnifSt
Syntax	cusp 22058	Extend class notation with the class of uniform spaces.
class UnifSp
Syntax	ctus 22059	Extend class notation with the function mapping a uniform structure to a uniform space.
class toUnifSp
Definition	df-uss 22060	Define the uniform structure extractor function. Similarly with df-topn 16084 this differs from df-unif 15965 when a structure has been restricted using df-ress 15865; 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 22061	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 22062	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 22063	The uniform structure on uniform space W. This proof uses a trick with fvprc 6185 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 22064	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 22065	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 22066	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 22067	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 22068	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 22069	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 22070	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 22071	Lemma for tusbas 22072, tusunif 22073, and tustopn 22075. (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 22072	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 22073	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 22074	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 22075	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 22076	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 22077	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 22078	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 22079	Extend class notation with the uniform continuity operation.
class Cnu
Definition	df-ucn 22080*	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 22081*	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 22082*	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 22083*	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 22084*	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 22085*	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 22086*	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 22087	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 22088	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 22089	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 22090	Extend class notation with the set of Cauchy filter bases.
class CauFilu
Definition	df-cfilu 22091*	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 22092*	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 22093	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 22094*	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 22095*	Lemma for fmucnd 22096. (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 22096*	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 22097	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 22098	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 22099	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 22100	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 ) )