HomeTheorem List (p. 242 of 482)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 242 of 482) | < Previous Next > |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-30715) |
Hilbert Space Explorer
(30716-32238) |
Users' Mathboxes
(32239-48161) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | ustinvel 24101 | 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 24102* | 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 24103 | The elements of uniform structures, called entourages, are relations. (Contributed by Thierry Arnoux, 15-Nov-2017.) |
| β’ ((π β (UnifOnβπ) β§ π β π) β Rel π) | ||
| Theorem | ustfilxp 24104 | A uniform structure on a nonempty base is a filter. Remark 3 of [BourbakiTop1] p. II.2. (Contributed by Thierry Arnoux, 15-Nov-2017.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
| β’ ((π β β β§ π β (UnifOnβπ)) β π β (Filβ(π Γ π))) | ||
| Theorem | ustne0 24105 | A uniform structure cannot be empty. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
| β’ (π β (UnifOnβπ) β π β β ) | ||
| Theorem | ustssco 24106 | In an uniform structure, any entourage π is a subset of its composition with itself. (Contributed by Thierry Arnoux, 5-Jan-2018.) |
| β’ ((π β (UnifOnβπ) β§ π β π) β π β (π β π)) | ||
| Theorem | ustexsym 24107* | In an uniform structure, for any entourage π, there exists a smaller symmetrical entourage. (Contributed by Thierry Arnoux, 4-Jan-2018.) |
| β’ ((π β (UnifOnβπ) β§ π β π) β βπ€ β π (β‘π€ = π€ β§ π€ β π)) | ||
| Theorem | ustex2sym 24108* | 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 24109* | 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 24110 | Any element of the base set is "near" itself, i.e. entourages are reflexive. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
| β’ ((π β (UnifOnβπ) β§ π β π β§ π΄ β π) β π΄ππ΄) | ||
| Theorem | ust0 24111 | 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 24112 | The empty set is not an uniform structure. (Contributed by Thierry Arnoux, 3-Dec-2017.) |
| β’ Β¬ β β βͺ ran UnifOn | ||
| Theorem | ustund 24113 | If two intersecting sets π΄ and π΅ are both small in π, their union is small in (πβ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.) |
| β’ (π β (π΄ Γ π΄) β π) & β’ (π β (π΅ Γ π΅) β π) & β’ (π β (π΄ β© π΅) β β ) β β’ (π β ((π΄ βͺ π΅) Γ (π΄ βͺ π΅)) β (π β π)) | ||
| Theorem | ustelimasn 24114 | Any point π΄ is near enough to itself. (Contributed by Thierry Arnoux, 18-Nov-2017.) |
| β’ ((π β (UnifOnβπ) β§ π β π β§ π΄ β π) β π΄ β (π β {π΄})) | ||
| Theorem | ustneism 24115 | 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 | elrnustOLD 24116 | Obsolete version of elfvunirn 6923 as of 12-Jan-2025. (Contributed by Thierry Arnoux, 16-Nov-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
| β’ (π β (UnifOnβπ) β π β βͺ ran UnifOn) | ||
| Theorem | ustbas2 24117 | Second direction for ustbas 24119. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
| β’ (π β (UnifOnβπ) β π = dom βͺ π) | ||
| Theorem | ustuni 24118 | The set union of a uniform structure is the Cartesian product of its base. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
| β’ (π β (UnifOnβπ) β βͺ π = (π Γ π)) | ||
| Theorem | ustbas 24119 | Recover the base of an uniform structure π. βͺ ran UnifOn is to UnifOn what Top is to TopOn. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
| β’ π = dom βͺ π β β’ (π β βͺ ran UnifOn β π β (UnifOnβπ)) | ||
| Theorem | ustimasn 24120 | Lemma for ustuqtop 24138. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
| β’ ((π β (UnifOnβπ) β§ π β π β§ π β π) β (π β {π}) β π) | ||
| Theorem | trust 24121 | 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 24122 | Extend class notation with the function inducing a topology from a uniform structure. |
| class unifTop | ||
| Definition | df-utop 24123* | Definition of a topology induced by a uniform structure. Definition 3 of [BourbakiTop1] p. II.4. (Contributed by Thierry Arnoux, 17-Nov-2017.) |
| β’ unifTop = (π’ β βͺ ran UnifOn β¦ {π β π« dom βͺ π’ β£ βπ₯ β π βπ£ β π’ (π£ β {π₯}) β π}) | ||
| Theorem | utopval 24124* | The topology induced by a uniform structure π. (Contributed by Thierry Arnoux, 30-Nov-2017.) |
| β’ (π β (UnifOnβπ) β (unifTopβπ) = {π β π« π β£ βπ₯ β π βπ£ β π (π£ β {π₯}) β π}) | ||
| Theorem | elutop 24125* | Open sets in the topology induced by an uniform structure π on π (Contributed by Thierry Arnoux, 30-Nov-2017.) |
| β’ (π β (UnifOnβπ) β (π΄ β (unifTopβπ) β (π΄ β π β§ βπ₯ β π΄ βπ£ β π (π£ β {π₯}) β π΄))) | ||
| Theorem | utoptop 24126 | The topology induced by a uniform structure π is a topology. (Contributed by Thierry Arnoux, 30-Nov-2017.) |
| β’ (π β (UnifOnβπ) β (unifTopβπ) β Top) | ||
| Theorem | utopbas 24127 | The base of the topology induced by a uniform structure π. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
| β’ (π β (UnifOnβπ) β π = βͺ (unifTopβπ)) | ||
| Theorem | utoptopon 24128 | Topology induced by a uniform structure π with its base set. (Contributed by Thierry Arnoux, 5-Jan-2018.) |
| β’ (π β (UnifOnβπ) β (unifTopβπ) β (TopOnβπ)) | ||
| Theorem | restutop 24129 | Restriction of a topology induced by an uniform structure. (Contributed by Thierry Arnoux, 12-Dec-2017.) |
| β’ ((π β (UnifOnβπ) β§ π΄ β π) β ((unifTopβπ) βΎt π΄) β (unifTopβ(π βΎt (π΄ Γ π΄)))) | ||
| Theorem | restutopopn 24130 | 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 24131* | Lemma for ustuqtop 24138. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
| β’ π = (π β π β¦ ran (π£ β π β¦ (π£ β {π}))) β β’ (((π β (UnifOnβπ) β§ π β π) β§ π΄ β π) β (π΄ β (πβπ) β βπ€ β π π΄ = (π€ β {π}))) | ||
| Theorem | ustuqtop0 24132* | Lemma for ustuqtop 24138. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
| β’ π = (π β π β¦ ran (π£ β π β¦ (π£ β {π}))) β β’ (π β (UnifOnβπ) β π:πβΆπ« π« π) | ||
| Theorem | ustuqtop1 24133* | Lemma for ustuqtop 24138, similar to ssnei2 23007. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
| β’ π = (π β π β¦ ran (π£ β π β¦ (π£ β {π}))) β β’ ((((π β (UnifOnβπ) β§ π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β π β (πβπ)) | ||
| Theorem | ustuqtop2 24134* | Lemma for ustuqtop 24138. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
| β’ π = (π β π β¦ ran (π£ β π β¦ (π£ β {π}))) β β’ ((π β (UnifOnβπ) β§ π β π) β (fiβ(πβπ)) β (πβπ)) | ||
| Theorem | ustuqtop3 24135* | Lemma for ustuqtop 24138, similar to elnei 23002. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
| β’ π = (π β π β¦ ran (π£ β π β¦ (π£ β {π}))) β β’ (((π β (UnifOnβπ) β§ π β π) β§ π β (πβπ)) β π β π) | ||
| Theorem | ustuqtop4 24136* | Lemma for ustuqtop 24138. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
| β’ π = (π β π β¦ ran (π£ β π β¦ (π£ β {π}))) β β’ (((π β (UnifOnβπ) β§ π β π) β§ π β (πβπ)) β βπ β (πβπ)βπ β π π β (πβπ)) | ||
| Theorem | ustuqtop5 24137* | Lemma for ustuqtop 24138. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
| β’ π = (π β π β¦ ran (π£ β π β¦ (π£ β {π}))) β β’ ((π β (UnifOnβπ) β§ π β π) β π β (πβπ)) | ||
| Theorem | ustuqtop 24138* | For a given uniform structure π on a set π, there is a unique topology π such that the set ran (π£ β π β¦ (π£ β {π})) is the filter of the neighborhoods of π for that topology. Proposition 1 of [BourbakiTop1] p. II.3. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
| β’ π = (π β π β¦ ran (π£ β π β¦ (π£ β {π}))) β β’ (π β (UnifOnβπ) β β!π β (TopOnβπ)βπ β π (πβπ) = ((neiβπ)β{π})) | ||
| Theorem | utopsnneiplem 24139* | The neighborhoods of a point π for the topology induced by an uniform space π. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
| β’ π½ = (unifTopβπ) & β’ πΎ = {π β π« π β£ βπ β π π β (πβπ)} & β’ π = (π β π β¦ ran (π£ β π β¦ (π£ β {π}))) β β’ ((π β (UnifOnβπ) β§ π β π) β ((neiβπ½)β{π}) = ran (π£ β π β¦ (π£ β {π}))) | ||
| Theorem | utopsnneip 24140* | The neighborhoods of a point π for the topology induced by an uniform space π. (Contributed by Thierry Arnoux, 13-Jan-2018.) |
| β’ π½ = (unifTopβπ) β β’ ((π β (UnifOnβπ) β§ π β π) β ((neiβπ½)β{π}) = ran (π£ β π β¦ (π£ β {π}))) | ||
| Theorem | utopsnnei 24141 | Images of singletons by entourages π are neighborhoods of those singletons. (Contributed by Thierry Arnoux, 13-Jan-2018.) |
| β’ π½ = (unifTopβπ) β β’ ((π β (UnifOnβπ) β§ π β π β§ π β π) β (π β {π}) β ((neiβπ½)β{π})) | ||
| Theorem | utop2nei 24142 | 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βπ) β§ (π β π β§ β‘π = π) β§ π β (π Γ π)) β (π β (π β π)) β ((neiβ(π½ Γt π½))βπ)) | ||
| Theorem | utop3cls 24143 | 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βπ) β§ π β (π Γ π)) β§ (π β π β§ β‘π = π)) β ((clsβ(π½ Γt π½))βπ) β (π β (π β π))) | ||
| Theorem | utopreg 24144 | All Hausdorff uniform spaces are regular. Proposition 3 of [BourbakiTop1] p. II.5. (Contributed by Thierry Arnoux, 16-Jan-2018.) |
| β’ π½ = (unifTopβπ) β β’ ((π β (UnifOnβπ) β§ π½ β Haus) β π½ β Reg) | ||
| Syntax | cuss 24145 | Extend class notation with the Uniform Structure extractor function. |
| class UnifSt | ||
| Syntax | cusp 24146 | Extend class notation with the class of uniform spaces. |
| class UnifSp | ||
| Syntax | ctus 24147 | Extend class notation with the function mapping a uniform structure to a uniform space. |
| class toUnifSp | ||
| Definition | df-uss 24148 | Define the uniform structure extractor function. Similarly with df-topn 17396 this differs from df-unif 17247 when a structure has been restricted using df-ress 17201; 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 = (π β V β¦ ((UnifSetβπ) βΎt ((Baseβπ) Γ (Baseβπ)))) | ||
| Definition | df-usp 24149 | 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β(Baseβπ)) β§ (TopOpenβπ) = (unifTopβ(UnifStβπ)))} | ||
| Definition | df-tus 24150 | Define the function mapping a uniform structure to a uniform space. (Contributed by Thierry Arnoux, 17-Nov-2017.) |
| β’ toUnifSp = (π’ β βͺ ran UnifOn β¦ ({β¨(Baseβndx), dom βͺ π’β©, β¨(UnifSetβndx), π’β©} sSet β¨(TopSetβndx), (unifTopβπ’)β©)) | ||
| Theorem | ussval 24151 | The uniform structure on uniform space π. This proof uses a trick with fvprc 6883 to avoid requiring π to be a set. (Contributed by Thierry Arnoux, 3-Dec-2017.) |
| β’ π΅ = (Baseβπ) & β’ π = (UnifSetβπ) β β’ (π βΎt (π΅ Γ π΅)) = (UnifStβπ) | ||
| Theorem | ussid 24152 | 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.) |
| β’ π΅ = (Baseβπ) & β’ π = (UnifSetβπ) β β’ ((π΅ Γ π΅) = βͺ π β π = (UnifStβπ)) | ||
| Theorem | isusp 24153 | The predicate π is a uniform space. (Contributed by Thierry Arnoux, 4-Dec-2017.) |
| β’ π΅ = (Baseβπ) & β’ π = (UnifStβπ) & β’ π½ = (TopOpenβπ) β β’ (π β UnifSp β (π β (UnifOnβπ΅) β§ π½ = (unifTopβπ))) | ||
| Theorem | ressuss 24154 | Value of the uniform structure of a restricted space. (Contributed by Thierry Arnoux, 12-Dec-2017.) |
| β’ (π΄ β π β (UnifStβ(π βΎs π΄)) = ((UnifStβπ) βΎt (π΄ Γ π΄))) | ||
| Theorem | ressust 24155 | The uniform structure of a restricted space. (Contributed by Thierry Arnoux, 22-Jan-2018.) |
| β’ π = (Baseβπ) & β’ π = (UnifStβ(π βΎs π΄)) β β’ ((π β UnifSp β§ π΄ β π) β π β (UnifOnβπ΄)) | ||
| Theorem | ressusp 24156 | The restriction of a uniform topological space to an open set is a uniform space. (Contributed by Thierry Arnoux, 16-Dec-2017.) |
| β’ π΅ = (Baseβπ) & β’ π½ = (TopOpenβπ) β β’ ((π β UnifSp β§ π β TopSp β§ π΄ β π½) β (π βΎs π΄) β UnifSp) | ||
| Theorem | tusval 24157 | The value of the uniform space mapping function. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
| β’ (π β (UnifOnβπ) β (toUnifSpβπ) = ({β¨(Baseβndx), dom βͺ πβ©, β¨(UnifSetβndx), πβ©} sSet β¨(TopSetβndx), (unifTopβπ)β©)) | ||
| Theorem | tuslem 24158 | Lemma for tusbas 24160, tusunif 24161, and tustopn 24163. (Contributed by Thierry Arnoux, 5-Dec-2017.) (Proof shortened by AV, 28-Oct-2024.) |
| β’ πΎ = (toUnifSpβπ) β β’ (π β (UnifOnβπ) β (π = (BaseβπΎ) β§ π = (UnifSetβπΎ) β§ (unifTopβπ) = (TopOpenβπΎ))) | ||
| Theorem | tuslemOLD 24159 | Obsolete proof of tuslem 24158 as of 28-Oct-2024. Lemma for tusbas 24160, tusunif 24161, and tustopn 24163. (Contributed by Thierry Arnoux, 5-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
| β’ πΎ = (toUnifSpβπ) β β’ (π β (UnifOnβπ) β (π = (BaseβπΎ) β§ π = (UnifSetβπΎ) β§ (unifTopβπ) = (TopOpenβπΎ))) | ||
| Theorem | tusbas 24160 | The base set of a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
| β’ πΎ = (toUnifSpβπ) β β’ (π β (UnifOnβπ) β π = (BaseβπΎ)) | ||
| Theorem | tusunif 24161 | The uniform structure of a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
| β’ πΎ = (toUnifSpβπ) β β’ (π β (UnifOnβπ) β π = (UnifSetβπΎ)) | ||
| Theorem | tususs 24162 | The uniform structure of a constructed uniform space. (Contributed by Thierry Arnoux, 15-Dec-2017.) |
| β’ πΎ = (toUnifSpβπ) β β’ (π β (UnifOnβπ) β π = (UnifStβπΎ)) | ||
| Theorem | tustopn 24163 | The topology induced by a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
| β’ πΎ = (toUnifSpβπ) & β’ π½ = (unifTopβπ) β β’ (π β (UnifOnβπ) β π½ = (TopOpenβπΎ)) | ||
| Theorem | tususp 24164 | A constructed uniform space is an uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
| β’ πΎ = (toUnifSpβπ) β β’ (π β (UnifOnβπ) β πΎ β UnifSp) | ||
| Theorem | tustps 24165 | A constructed uniform space is a topological space. (Contributed by Thierry Arnoux, 25-Jan-2018.) |
| β’ πΎ = (toUnifSpβπ) β β’ (π β (UnifOnβπ) β πΎ β TopSp) | ||
| Theorem | uspreg 24166 | If a uniform space is Hausdorff, it is regular. Proposition 3 of [BourbakiTop1] p. II.5. (Contributed by Thierry Arnoux, 4-Jan-2018.) |
| β’ π½ = (TopOpenβπ) β β’ ((π β UnifSp β§ π½ β Haus) β π½ β Reg) | ||
| Syntax | cucn 24167 | Extend class notation with the uniform continuity operation. |
| class Cnu | ||
| Definition | df-ucn 24168* | 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 = (π’ β βͺ ran UnifOn, π£ β βͺ ran UnifOn β¦ {π β (dom βͺ π£ βm dom βͺ π’) β£ βπ β π£ βπ β π’ βπ₯ β dom βͺ π’βπ¦ β dom βͺ π’(π₯ππ¦ β (πβπ₯)π (πβπ¦))}) | ||
| Theorem | ucnval 24169* | The set of all uniformly continuous function from uniform space π to uniform space π. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
| β’ ((π β (UnifOnβπ) β§ π β (UnifOnβπ)) β (π Cnuπ) = {π β (π βm π) β£ βπ β π βπ β π βπ₯ β π βπ¦ β π (π₯ππ¦ β (πβπ₯)π (πβπ¦))}) | ||
| Theorem | isucn 24170* | 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 24171* | 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.) |
| β’ π = ((π Γ π)filGenπ ) & β’ π = ((π Γ π)filGenπ) & β’ (π β π β (UnifOnβπ)) & β’ (π β π β (UnifOnβπ)) & β’ (π β π β (fBasβ(π Γ π))) & β’ (π β π β (fBasβ(π Γ π))) β β’ (π β (πΉ β (π Cnuπ) β (πΉ:πβΆπ β§ βπ β π βπ β π βπ₯ β π βπ¦ β π (π₯ππ¦ β (πΉβπ₯)π (πΉβπ¦))))) | ||
| Theorem | ucnimalem 24172* | Reformulate the πΊ function as a mapping with one variable. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
| β’ (π β π β (UnifOnβπ)) & β’ (π β π β (UnifOnβπ)) & β’ (π β πΉ β (π Cnuπ)) & β’ (π β π β π) & β’ πΊ = (π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) β β’ πΊ = (π β (π Γ π) β¦ β¨(πΉβ(1st βπ)), (πΉβ(2nd βπ))β©) | ||
| Theorem | ucnima 24173* | An equivalent statement of the definition of uniformly continuous function. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
| β’ (π β π β (UnifOnβπ)) & β’ (π β π β (UnifOnβπ)) & β’ (π β πΉ β (π Cnuπ)) & β’ (π β π β π) & β’ πΊ = (π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) β β’ (π β βπ β π (πΊ β π) β π) | ||
| Theorem | ucnprima 24174* | 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 24175 | 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βπ) β ( I βΎ π) β (π Cnuπ)) | ||
| Theorem | cstucnd 24176 | 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 24177 | Uniform continuity implies continuity. Deduction form. Proposition 1 of [BourbakiTop1] p. II.6. (Contributed by Thierry Arnoux, 30-Nov-2017.) |
| β’ π½ = (TopOpenβπ ) & β’ πΎ = (TopOpenβπ) & β’ (π β π β UnifSp) & β’ (π β π β UnifSp) & β’ (π β π β TopSp) & β’ (π β π β TopSp) & β’ (π β πΉ β ((UnifStβπ ) Cnu(UnifStβπ))) β β’ (π β πΉ β (π½ Cn πΎ)) | ||
| Syntax | ccfilu 24178 | Extend class notation with the set of Cauchy filter bases. |
| class CauFilu | ||
| Definition | df-cfilu 24179* | 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 = (π’ β βͺ ran UnifOn β¦ {π β (fBasβdom βͺ π’) β£ βπ£ β π’ βπ β π (π Γ π) β π£}) | ||
| Theorem | iscfilu 24180* | The predicate "πΉ is a Cauchy filter base on uniform space π". (Contributed by Thierry Arnoux, 18-Nov-2017.) |
| β’ (π β (UnifOnβπ) β (πΉ β (CauFiluβπ) β (πΉ β (fBasβπ) β§ βπ£ β π βπ β πΉ (π Γ π) β π£))) | ||
| Theorem | cfilufbas 24181 | A Cauchy filter base is a filter base. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
| β’ ((π β (UnifOnβπ) β§ πΉ β (CauFiluβπ)) β πΉ β (fBasβπ)) | ||
| Theorem | cfiluexsm 24182* | 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 24183* | Lemma for fmucnd 24184. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
| β’ ((πΉ Fn π β§ π΄ β π) β ((π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) β (π΄ Γ π΄)) = ((πΉ β π΄) Γ (πΉ β π΄))) | ||
| Theorem | fmucnd 24184* | 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βπ)) & β’ π· = ran (π β πΆ β¦ (πΉ β π)) β β’ (π β π· β (CauFiluβπ)) | ||
| Theorem | cfilufg 24185 | The filter generated by a Cauchy filter base is still a Cauchy filter base. (Contributed by Thierry Arnoux, 24-Jan-2018.) |
| β’ ((π β (UnifOnβπ) β§ πΉ β (CauFiluβπ)) β (πfilGenπΉ) β (CauFiluβπ)) | ||
| Theorem | trcfilu 24186 | 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 24187 | 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 24188 | In an uniform space, a neighboring filter is a Cauchy filter base. (Contributed by Thierry Arnoux, 24-Jan-2018.) |
| β’ π = (Baseβπ) & β’ π½ = (TopOpenβπ) & β’ π = (UnifStβπ) β β’ ((π β UnifSp β§ π β TopSp β§ π β π) β ((neiβπ½)β{π}) β (CauFiluβπ)) | ||
| Syntax | ccusp 24189 | Extend class notation with the class of all complete uniform spaces. |
| class CUnifSp | ||
| Definition | df-cusp 24190* | Define the class of all complete uniform spaces. Definition 3 of [BourbakiTop1] p. II.15. (Contributed by Thierry Arnoux, 1-Dec-2017.) |
| β’ CUnifSp = {π€ β UnifSp β£ βπ β (Filβ(Baseβπ€))(π β (CauFiluβ(UnifStβπ€)) β ((TopOpenβπ€) fLim π) β β )} | ||
| Theorem | iscusp 24191* | The predicate "π is a complete uniform space." (Contributed by Thierry Arnoux, 3-Dec-2017.) |
| β’ (π β CUnifSp β (π β UnifSp β§ βπ β (Filβ(Baseβπ))(π β (CauFiluβ(UnifStβπ)) β ((TopOpenβπ) fLim π) β β ))) | ||
| Theorem | cuspusp 24192 | A complete uniform space is an uniform space. (Contributed by Thierry Arnoux, 3-Dec-2017.) |
| β’ (π β CUnifSp β π β UnifSp) | ||
| Theorem | cuspcvg 24193 | In a complete uniform space, any Cauchy filter πΆ has a limit. (Contributed by Thierry Arnoux, 3-Dec-2017.) |
| β’ π΅ = (Baseβπ) & β’ π½ = (TopOpenβπ) β β’ ((π β CUnifSp β§ πΆ β (CauFiluβ(UnifStβπ)) β§ πΆ β (Filβπ΅)) β (π½ fLim πΆ) β β ) | ||
| Theorem | iscusp2 24194* | The predicate "π is a complete uniform space." (Contributed by Thierry Arnoux, 15-Dec-2017.) |
| β’ π΅ = (Baseβπ) & β’ π = (UnifStβπ) & β’ π½ = (TopOpenβπ) β β’ (π β CUnifSp β (π β UnifSp β§ βπ β (Filβπ΅)(π β (CauFiluβπ) β (π½ fLim π) β β ))) | ||
| Theorem | cnextucn 24195* | Extension by continuity. Proposition 11 of [BourbakiTop1] p. II.20. Given a topology π½ on π, a subset π΄ dense in π, this states a condition for πΉ from π΄ to a space π Hausdorff and complete to be extensible by continuity. (Contributed by Thierry Arnoux, 4-Dec-2017.) |
| β’ π = (Baseβπ) & β’ π = (Baseβπ) & β’ π½ = (TopOpenβπ) & β’ πΎ = (TopOpenβπ) & β’ π = (UnifStβπ) & β’ (π β π β TopSp) & β’ (π β π β TopSp) & β’ (π β π β CUnifSp) & β’ (π β πΎ β Haus) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ) & β’ (π β ((clsβπ½)βπ΄) = π) & β’ ((π β§ π₯ β π) β ((π FilMap πΉ)β(((neiβπ½)β{π₯}) βΎt π΄)) β (CauFiluβπ)) β β’ (π β ((π½CnExtπΎ)βπΉ) β (π½ Cn πΎ)) | ||
| Theorem | ucnextcn 24196 | Extension by continuity. Theorem 2 of [BourbakiTop1] p. II.20. Given an uniform space on a set π, a subset π΄ dense in π, and a function πΉ uniformly continuous from π΄ to π, that function can be extended by continuity to the whole π, and its extension is uniformly continuous. (Contributed by Thierry Arnoux, 25-Jan-2018.) |
| β’ π = (Baseβπ) & β’ π = (Baseβπ) & β’ π½ = (TopOpenβπ) & β’ πΎ = (TopOpenβπ) & β’ π = (UnifStβπ) & β’ π = (UnifStβ(π βΎs π΄)) & β’ π = (UnifStβπ) & β’ (π β π β TopSp) & β’ (π β π β UnifSp) & β’ (π β π β TopSp) & β’ (π β π β CUnifSp) & β’ (π β πΎ β Haus) & β’ (π β π΄ β π) & β’ (π β πΉ β (π Cnuπ)) & β’ (π β ((clsβπ½)βπ΄) = π) β β’ (π β ((π½CnExtπΎ)βπΉ) β (π½ Cn πΎ)) | ||
| Theorem | ispsmet 24197* | Express the predicate "π· is a pseudometric." (Contributed by Thierry Arnoux, 7-Feb-2018.) |
| β’ (π β π β (π· β (PsMetβπ) β (π·:(π Γ π)βΆβ* β§ βπ₯ β π ((π₯π·π₯) = 0 β§ βπ¦ β π βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)))))) | ||
| Theorem | psmetdmdm 24198 | Recover the base set from a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
| β’ (π· β (PsMetβπ) β π = dom dom π·) | ||
| Theorem | psmetf 24199 | The distance function of a pseudometric as a function. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
| β’ (π· β (PsMetβπ) β π·:(π Γ π)βΆβ*) | ||
| Theorem | psmetcl 24200 | Closure of the distance function of a pseudometric space. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
| β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) β β*) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |