Home | Metamath
Proof Explorer Theorem List (p. 221 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | tvclmod 22001 | A topological vector space is a left module. (Contributed by Mario Carneiro, 5-Oct-2015.) |
Theorem | tvclvec 22002 | A topological vector space is a vector space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
Syntax | cust 22003 | Extend class notation with the class function of uniform structures. |
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 | ||
Theorem | ustfn 22005 | The defined uniform structure as a function. (Contributed by Thierry Arnoux, 15-Nov-2017.) |
UnifOn | ||
Theorem | ustval 22006* | The class of all uniform structures for a base . (Contributed by Thierry Arnoux, 15-Nov-2017.) (Revised by AV, 17-Sep-2021.) |
UnifOn | ||
Theorem | isust 22007* | The predicate " is a uniform structure with base ." (Contributed by Thierry Arnoux, 15-Nov-2017.) (Revised by AV, 17-Sep-2021.) |
UnifOn | ||
Theorem | ustssxp 22008 | Entourages are subsets of the Cartesian product of the base set. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
UnifOn | ||
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.) |
UnifOn | ||
Theorem | ustbasel 22010 | The full set is always an entourage. Condition FIIb of [BourbakiTop1] p. I.36. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
UnifOn | ||
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.) |
UnifOn | ||
Theorem | ustdiag 22012 | The diagonal set is included in any entourage, i.e. any point is -close to itself. Condition UI of [BourbakiTop1] p. II.1. (Contributed by Thierry Arnoux, 2-Dec-2017.) |
UnifOn | ||
Theorem | ustinvel 22013 | If is an entourage, so is its inverse. Condition UII of [BourbakiTop1] p. II.1. (Contributed by Thierry Arnoux, 2-Dec-2017.) |
UnifOn | ||
Theorem | ustexhalf 22014* | For each entourage there is an entourage that is "not more than half as large". Condition UIII of [BourbakiTop1] p. II.1. (Contributed by Thierry Arnoux, 2-Dec-2017.) |
UnifOn | ||
Theorem | ustrel 22015 | The elements of uniform structures, called entourages, are relations. (Contributed by Thierry Arnoux, 15-Nov-2017.) |
UnifOn | ||
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.) |
UnifOn | ||
Theorem | ustne0 22017 | A uniform structure cannot be empty. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
UnifOn | ||
Theorem | ustssco 22018 | In an uniform structure, any entourage is a subset of its composition with itself. (Contributed by Thierry Arnoux, 5-Jan-2018.) |
UnifOn | ||
Theorem | ustexsym 22019* | In an uniform structure, for any entourage , there exists a smaller symmetrical entourage. (Contributed by Thierry Arnoux, 4-Jan-2018.) |
UnifOn | ||
Theorem | ustex2sym 22020* | In an uniform structure, for any entourage , there exists a symmetrical entourage smaller than half . (Contributed by Thierry Arnoux, 16-Jan-2018.) |
UnifOn | ||
Theorem | ustex3sym 22021* | In an uniform structure, for any entourage , there exists a symmetrical entourage smaller than a third of . (Contributed by Thierry Arnoux, 16-Jan-2018.) |
UnifOn | ||
Theorem | ustref 22022 | Any element of the base set is "near" itself, i.e. entourages are reflexive. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
UnifOn | ||
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.) |
UnifOn | ||
Theorem | ustund 22025 | If two intersecting sets and are both small in , their union is small in . 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.) |
Theorem | ustelimasn 22026 | Any point is near enough to itself. (Contributed by Thierry Arnoux, 18-Nov-2017.) |
UnifOn | ||
Theorem | ustneism 22027 | For a point in , is small enough in . This proposition actually does not require any axiom of the definition of uniform structures. (Contributed by Thierry Arnoux, 18-Nov-2017.) |
Theorem | elrnust 22028 | First direction for ustbas 22031. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
UnifOn UnifOn | ||
Theorem | ustbas2 22029 | Second direction for ustbas 22031. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
UnifOn | ||
Theorem | ustuni 22030 | The set union of a uniform structure is the Cartesian product of its base. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
UnifOn | ||
Theorem | ustbas 22031 | Recover the base of an uniform structure . UnifOn is to UnifOn what is to TopOn. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
UnifOn UnifOn | ||
Theorem | ustimasn 22032 | Lemma for ustuqtop 22050. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
UnifOn | ||
Theorem | trust 22033 | The trace of a uniform structure on a subset is a uniform structure on . Definition 3 of [BourbakiTop1] p. II.9. (Contributed by Thierry Arnoux, 2-Dec-2017.) |
UnifOn ↾t UnifOn | ||
Syntax | cutop 22034 | Extend class notation with the function inducing a topology from a uniform structure. |
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 UnifOn | ||
Theorem | utopval 22036* | The topology induced by a uniform structure . (Contributed by Thierry Arnoux, 30-Nov-2017.) |
UnifOn unifTop | ||
Theorem | elutop 22037* | Open sets in the topology induced by an uniform structure on (Contributed by Thierry Arnoux, 30-Nov-2017.) |
UnifOn unifTop | ||
Theorem | utoptop 22038 | The topology induced by a uniform structure is a topology. (Contributed by Thierry Arnoux, 30-Nov-2017.) |
UnifOn unifTop | ||
Theorem | utopbas 22039 | The base of the topology induced by a uniform structure . (Contributed by Thierry Arnoux, 5-Dec-2017.) |
UnifOn unifTop | ||
Theorem | utoptopon 22040 | Topology induced by a uniform structure with its base set. (Contributed by Thierry Arnoux, 5-Jan-2018.) |
UnifOn unifTop TopOn | ||
Theorem | restutop 22041 | Restriction of a topology induced by an uniform structure. (Contributed by Thierry Arnoux, 12-Dec-2017.) |
UnifOn unifTop ↾t unifTop ↾t | ||
Theorem | restutopopn 22042 | The restriction of the topology induced by an uniform structure to an open set. (Contributed by Thierry Arnoux, 16-Dec-2017.) |
UnifOn unifTop unifTop ↾t unifTop ↾t | ||
Theorem | ustuqtoplem 22043* | Lemma for ustuqtop 22050. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
UnifOn | ||
Theorem | ustuqtop0 22044* | Lemma for ustuqtop 22050. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
UnifOn | ||
Theorem | ustuqtop1 22045* | Lemma for ustuqtop 22050, similar to ssnei2 20920. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
UnifOn | ||
Theorem | ustuqtop2 22046* | Lemma for ustuqtop 22050. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
UnifOn | ||
Theorem | ustuqtop3 22047* | Lemma for ustuqtop 22050, similar to elnei 20915. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
UnifOn | ||
Theorem | ustuqtop4 22048* | Lemma for ustuqtop 22050. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
UnifOn | ||
Theorem | ustuqtop5 22049* | Lemma for ustuqtop 22050. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
UnifOn | ||
Theorem | ustuqtop 22050* | For a given uniform structure on a set , there is a unique topology such that the set is the filter of the neighborhoods of for that topology. Proposition 1 of [BourbakiTop1] p. II.3. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
UnifOn TopOn | ||
Theorem | utopsnneiplem 22051* | The neighborhoods of a point for the topology induced by an uniform space . (Contributed by Thierry Arnoux, 11-Jan-2018.) |
unifTop UnifOn | ||
Theorem | utopsnneip 22052* | The neighborhoods of a point for the topology induced by an uniform space . (Contributed by Thierry Arnoux, 13-Jan-2018.) |
unifTop UnifOn | ||
Theorem | utopsnnei 22053 | Images of singletons by entourages are neighborhoods of those singletons. (Contributed by Thierry Arnoux, 13-Jan-2018.) |
unifTop UnifOn | ||
Theorem | utop2nei 22054 | For any symmetrical entourage and any relation , build a neighborhood of . First part of proposition 2 of [BourbakiTop1] p. II.4. (Contributed by Thierry Arnoux, 14-Jan-2018.) |
unifTop UnifOn | ||
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.) |
unifTop UnifOn | ||
Theorem | utopreg 22056 | All Hausdorff uniform spaces are regular. Proposition 3 of [BourbakiTop1] p. II.5. (Contributed by Thierry Arnoux, 16-Jan-2018.) |
unifTop UnifOn | ||
Syntax | cuss 22057 | Extend class notation with the Uniform Structure extractor function. |
UnifSt | ||
Syntax | cusp 22058 | Extend class notation with the class of uniform spaces. |
UnifSp | ||
Syntax | ctus 22059 | Extend class notation with the function mapping a uniform structure to a uniform space. |
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 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 ↾t | ||
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 UnifSt UnifOn unifTopUnifSt | ||
Definition | df-tus 22062 | Define the function mapping a uniform structure to a uniform space. (Contributed by Thierry Arnoux, 17-Nov-2017.) |
toUnifSp UnifOn sSet TopSet unifTop | ||
Theorem | ussval 22063 | The uniform structure on uniform space . This proof uses a trick with fvprc 6185 to avoid requiring to be a set. (Contributed by Thierry Arnoux, 3-Dec-2017.) |
↾t UnifSt | ||
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.) |
UnifSt | ||
Theorem | isusp 22065 | The predicate is a uniform space. (Contributed by Thierry Arnoux, 4-Dec-2017.) |
UnifSt UnifSp UnifOn unifTop | ||
Theorem | ressunif 22066 | is unaffected by restriction. (Contributed by Thierry Arnoux, 7-Dec-2017.) |
↾s | ||
Theorem | ressuss 22067 | Value of the uniform structure of a restricted space. (Contributed by Thierry Arnoux, 12-Dec-2017.) |
UnifSt ↾s UnifSt ↾t | ||
Theorem | ressust 22068 | The uniform structure of a restricted space. (Contributed by Thierry Arnoux, 22-Jan-2018.) |
UnifSt ↾s UnifSp UnifOn | ||
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.) |
UnifSp ↾s UnifSp | ||
Theorem | tusval 22070 | The value of the uniform space mapping function. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
UnifOn toUnifSp sSet TopSet unifTop | ||
Theorem | tuslem 22071 | Lemma for tusbas 22072, tusunif 22073, and tustopn 22075. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
toUnifSp UnifOn unifTop | ||
Theorem | tusbas 22072 | The base set of a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
toUnifSp UnifOn | ||
Theorem | tusunif 22073 | The uniform structure of a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
toUnifSp UnifOn | ||
Theorem | tususs 22074 | The uniform structure of a constructed uniform space. (Contributed by Thierry Arnoux, 15-Dec-2017.) |
toUnifSp UnifOn UnifSt | ||
Theorem | tustopn 22075 | The topology induced by a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
toUnifSp unifTop UnifOn | ||
Theorem | tususp 22076 | A constructed uniform space is an uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
toUnifSp UnifOn UnifSp | ||
Theorem | tustps 22077 | A constructed uniform space is a topological space. (Contributed by Thierry Arnoux, 25-Jan-2018.) |
toUnifSp UnifOn | ||
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.) |
UnifSp | ||
Syntax | cucn 22079 | Extend class notation with the uniform continuity operation. |
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 is uniformly continuous if, roughly speaking, it is possible to guarantee that and be as close to each other as we please by requiring only that and are sufficiently close to each other; unlike ordinary continuity, the maximum distance between and cannot depend on and themselves. This formulation is the definition 1 of [BourbakiTop1] p. II.6. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
Cnu UnifOn UnifOn | ||
Theorem | ucnval 22081* | The set of all uniformly continuous function from uniform space to uniform space . (Contributed by Thierry Arnoux, 16-Nov-2017.) |
UnifOn UnifOn Cnu | ||
Theorem | isucn 22082* | The predicate " is a uniformly continuous function from uniform space to uniform space ." (Contributed by Thierry Arnoux, 16-Nov-2017.) |
UnifOn UnifOn Cnu | ||
Theorem | isucn2 22083* | The predicate " is a uniformly continuous function from uniform space to uniform space ." , expressed with filter bases for the entourages. (Contributed by Thierry Arnoux, 26-Jan-2018.) |
UnifOn UnifOn Cnu | ||
Theorem | ucnimalem 22084* | Reformulate the function as a mapping with one variable. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
UnifOn UnifOn Cnu | ||
Theorem | ucnima 22085* | An equivalent statement of the definition of uniformly continuous function. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
UnifOn UnifOn Cnu | ||
Theorem | ucnprima 22086* | The preimage by a uniformly continuous function of an entourage of is an entourage of . Note of the definition 1 of [BourbakiTop1] p. II.6. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
UnifOn UnifOn Cnu | ||
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.) |
UnifOn Cnu | ||
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.) |
UnifOn UnifOn Cnu | ||
Theorem | ucncn 22089 | Uniform continuity implies continuity. Deduction form. Proposition 1 of [BourbakiTop1] p. II.6. (Contributed by Thierry Arnoux, 30-Nov-2017.) |
UnifSp UnifSp UnifSt CnuUnifSt | ||
Syntax | ccfilu 22090 | Extend class notation with the set of Cauchy filter bases. |
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 , there is an element of the filter "small enough in " i.e. such that every pair of points in is related by ". Definition 2 of [BourbakiTop1] p. II.13. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
CauFilu UnifOn | ||
Theorem | iscfilu 22092* | The predicate " is a Cauchy filter base on uniform space ." (Contributed by Thierry Arnoux, 18-Nov-2017.) |
UnifOn CauFilu | ||
Theorem | cfilufbas 22093 | A Cauchy filter base is a filter base. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
UnifOn CauFilu | ||
Theorem | cfiluexsm 22094* | For a Cauchy filter base and any entourage , there is an element of the filter small in . (Contributed by Thierry Arnoux, 19-Nov-2017.) |
UnifOn CauFilu | ||
Theorem | fmucndlem 22095* | Lemma for fmucnd 22096. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
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.) |
UnifOn UnifOn Cnu CauFilu CauFilu | ||
Theorem | cfilufg 22097 | The filter generated by a Cauchy filter base is still a Cauchy filter base. (Contributed by Thierry Arnoux, 24-Jan-2018.) |
UnifOn CauFilu CauFilu | ||
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.) |
UnifOn CauFilu ↾t ↾t CauFilu ↾t | ||
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.) |
UnifOn CauFilu ↾t CauFilu | ||
Theorem | neipcfilu 22100 | In an uniform space, a neighboring filter is a Cauchy filter base. (Contributed by Thierry Arnoux, 24-Jan-2018.) |
UnifSt UnifSp CauFilu |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |