HomeTheorem List (p. 242 of 484)
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 484) | < 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-30767) |
Hilbert Space Explorer
(30768-32290) |
Users' Mathboxes
(32291-48346) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | dvrcn 24101 | The division function is continuous in a topological field. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| β’ π½ = (TopOpenβπ ) & β’ / = (/rβπ ) & β’ π = (Unitβπ ) β β’ (π β TopDRing β / β ((π½ Γt (π½ βΎt π)) Cn π½)) | ||
| Theorem | istlm 24102 | The predicate "π is a topological left module". (Contributed by Mario Carneiro, 5-Oct-2015.) |
| β’ Β· = ( Β·sf βπ) & β’ π½ = (TopOpenβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (TopOpenβπΉ) β β’ (π β TopMod β ((π β TopMnd β§ π β LMod β§ πΉ β TopRing) β§ Β· β ((πΎ Γt π½) Cn π½))) | ||
| Theorem | vscacn 24103 | The scalar multiplication is continuous in a topological module. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| β’ Β· = ( Β·sf βπ) & β’ π½ = (TopOpenβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (TopOpenβπΉ) β β’ (π β TopMod β Β· β ((πΎ Γt π½) Cn π½)) | ||
| Theorem | tlmtmd 24104 | A topological module is a topological monoid. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| β’ (π β TopMod β π β TopMnd) | ||
| Theorem | tlmtps 24105 | A topological module is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| β’ (π β TopMod β π β TopSp) | ||
| Theorem | tlmlmod 24106 | A topological module is a left module. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| β’ (π β TopMod β π β LMod) | ||
| Theorem | tlmtrg 24107 | The scalar ring of a topological module is a topological ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| β’ πΉ = (Scalarβπ) β β’ (π β TopMod β πΉ β TopRing) | ||
| Theorem | tlmscatps 24108 | The scalar ring of a topological module is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| β’ πΉ = (Scalarβπ) β β’ (π β TopMod β πΉ β TopSp) | ||
| Theorem | istvc 24109 | A topological vector space is a topological module over a topological division ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| β’ πΉ = (Scalarβπ) β β’ (π β TopVec β (π β TopMod β§ πΉ β TopDRing)) | ||
| Theorem | tvctdrg 24110 | The scalar field of a topological vector space is a topological division ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| β’ πΉ = (Scalarβπ) β β’ (π β TopVec β πΉ β TopDRing) | ||
| Theorem | cnmpt1vsca 24111* | Continuity of scalar multiplication; analogue of cnmpt12f 23583 which cannot be used directly because Β·π is not a function. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ π½ = (TopOpenβπ) & β’ πΎ = (TopOpenβπΉ) & β’ (π β π β TopMod) & β’ (π β πΏ β (TopOnβπ)) & β’ (π β (π₯ β π β¦ π΄) β (πΏ Cn πΎ)) & β’ (π β (π₯ β π β¦ π΅) β (πΏ Cn π½)) β β’ (π β (π₯ β π β¦ (π΄ Β· π΅)) β (πΏ Cn π½)) | ||
| Theorem | cnmpt2vsca 24112* | Continuity of scalar multiplication; analogue of cnmpt22f 23592 which cannot be used directly because Β·π is not a function. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ π½ = (TopOpenβπ) & β’ πΎ = (TopOpenβπΉ) & β’ (π β π β TopMod) & β’ (π β πΏ β (TopOnβπ)) & β’ (π β π β (TopOnβπ)) & β’ (π β (π₯ β π, π¦ β π β¦ π΄) β ((πΏ Γt π) Cn πΎ)) & β’ (π β (π₯ β π, π¦ β π β¦ π΅) β ((πΏ Γt π) Cn π½)) β β’ (π β (π₯ β π, π¦ β π β¦ (π΄ Β· π΅)) β ((πΏ Γt π) Cn π½)) | ||
| Theorem | tlmtgp 24113 | A topological vector space is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| β’ (π β TopMod β π β TopGrp) | ||
| Theorem | tvctlm 24114 | A topological vector space is a topological module. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| β’ (π β TopVec β π β TopMod) | ||
| Theorem | tvclmod 24115 | A topological vector space is a left module. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| β’ (π β TopVec β π β LMod) | ||
| Theorem | tvclvec 24116 | A topological vector space is a vector space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| β’ (π β TopVec β π β LVec) | ||
| Syntax | cust 24117 | Extend class notation with the class function of uniform structures. |
| class UnifOn | ||
| Definition | df-ust 24118* | 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 = (π₯ β V β¦ {π’ β£ (π’ β π« (π₯ Γ π₯) β§ (π₯ Γ π₯) β π’ β§ βπ£ β π’ (βπ€ β π« (π₯ Γ π₯)(π£ β π€ β π€ β π’) β§ βπ€ β π’ (π£ β© π€) β π’ β§ (( I βΎ π₯) β π£ β§ β‘π£ β π’ β§ βπ€ β π’ (π€ β π€) β π£)))}) | ||
| Theorem | ustfn 24119 | The defined uniform structure as a function. (Contributed by Thierry Arnoux, 15-Nov-2017.) |
| β’ UnifOn Fn V | ||
| Theorem | ustval 24120* | The class of all uniform structures for a base π. (Contributed by Thierry Arnoux, 15-Nov-2017.) (Revised by AV, 17-Sep-2021.) |
| β’ (π β π β (UnifOnβπ) = {π’ β£ (π’ β π« (π Γ π) β§ (π Γ π) β π’ β§ βπ£ β π’ (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π’) β§ βπ€ β π’ (π£ β© π€) β π’ β§ (( I βΎ π) β π£ β§ β‘π£ β π’ β§ βπ€ β π’ (π€ β π€) β π£)))}) | ||
| Theorem | isust 24121* | The predicate "π is a uniform structure with base π". (Contributed by Thierry Arnoux, 15-Nov-2017.) (Revised by AV, 17-Sep-2021.) |
| β’ (π β π β (π β (UnifOnβπ) β (π β π« (π Γ π) β§ (π Γ π) β π β§ βπ£ β π (βπ€ β π« (π Γ π)(π£ β π€ β π€ β π) β§ βπ€ β π (π£ β© π€) β π β§ (( I βΎ π) β π£ β§ β‘π£ β π β§ βπ€ β π (π€ β π€) β π£))))) | ||
| Theorem | ustssxp 24122 | Entourages are subsets of the Cartesian product of the base set. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
| β’ ((π β (UnifOnβπ) β§ π β π) β π β (π Γ π)) | ||
| Theorem | ustssel 24123 | 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 24124 | The full set is always an entourage. Condition FIIb of [BourbakiTop1] p. I.36. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
| β’ (π β (UnifOnβπ) β (π Γ π) β π) | ||
| Theorem | ustincl 24125 | 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 24126 | 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βπ) β§ π β π) β ( I βΎ π) β π) | ||
| Theorem | ustinvel 24127 | 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 24128* | 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 24129 | The elements of uniform structures, called entourages, are relations. (Contributed by Thierry Arnoux, 15-Nov-2017.) |
| β’ ((π β (UnifOnβπ) β§ π β π) β Rel π) | ||
| Theorem | ustfilxp 24130 | 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 24131 | A uniform structure cannot be empty. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
| β’ (π β (UnifOnβπ) β π β β ) | ||
| Theorem | ustssco 24132 | In an uniform structure, any entourage π is a subset of its composition with itself. (Contributed by Thierry Arnoux, 5-Jan-2018.) |
| β’ ((π β (UnifOnβπ) β§ π β π) β π β (π β π)) | ||
| Theorem | ustexsym 24133* | In an uniform structure, for any entourage π, there exists a smaller symmetrical entourage. (Contributed by Thierry Arnoux, 4-Jan-2018.) |
| β’ ((π β (UnifOnβπ) β§ π β π) β βπ€ β π (β‘π€ = π€ β§ π€ β π)) | ||
| Theorem | ustex2sym 24134* | 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 24135* | 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 24136 | Any element of the base set is "near" itself, i.e. entourages are reflexive. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
| β’ ((π β (UnifOnβπ) β§ π β π β§ π΄ β π) β π΄ππ΄) | ||
| Theorem | ust0 24137 | 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 24138 | The empty set is not an uniform structure. (Contributed by Thierry Arnoux, 3-Dec-2017.) |
| β’ Β¬ β β βͺ ran UnifOn | ||
| Theorem | ustund 24139 | 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 24140 | Any point π΄ is near enough to itself. (Contributed by Thierry Arnoux, 18-Nov-2017.) |
| β’ ((π β (UnifOnβπ) β§ π β π β§ π΄ β π) β π΄ β (π β {π΄})) | ||
| Theorem | ustneism 24141 | 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 24142 | Obsolete version of elfvunirn 6922 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 24143 | Second direction for ustbas 24145. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
| β’ (π β (UnifOnβπ) β π = dom βͺ π) | ||
| Theorem | ustuni 24144 | The set union of a uniform structure is the Cartesian product of its base. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
| β’ (π β (UnifOnβπ) β βͺ π = (π Γ π)) | ||
| Theorem | ustbas 24145 | 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 24146 | Lemma for ustuqtop 24164. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
| β’ ((π β (UnifOnβπ) β§ π β π β§ π β π) β (π β {π}) β π) | ||
| Theorem | trust 24147 | 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 24148 | Extend class notation with the function inducing a topology from a uniform structure. |
| class unifTop | ||
| Definition | df-utop 24149* | 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 24150* | The topology induced by a uniform structure π. (Contributed by Thierry Arnoux, 30-Nov-2017.) |
| β’ (π β (UnifOnβπ) β (unifTopβπ) = {π β π« π β£ βπ₯ β π βπ£ β π (π£ β {π₯}) β π}) | ||
| Theorem | elutop 24151* | Open sets in the topology induced by an uniform structure π on π (Contributed by Thierry Arnoux, 30-Nov-2017.) |
| β’ (π β (UnifOnβπ) β (π΄ β (unifTopβπ) β (π΄ β π β§ βπ₯ β π΄ βπ£ β π (π£ β {π₯}) β π΄))) | ||
| Theorem | utoptop 24152 | The topology induced by a uniform structure π is a topology. (Contributed by Thierry Arnoux, 30-Nov-2017.) |
| β’ (π β (UnifOnβπ) β (unifTopβπ) β Top) | ||
| Theorem | utopbas 24153 | The base of the topology induced by a uniform structure π. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
| β’ (π β (UnifOnβπ) β π = βͺ (unifTopβπ)) | ||
| Theorem | utoptopon 24154 | Topology induced by a uniform structure π with its base set. (Contributed by Thierry Arnoux, 5-Jan-2018.) |
| β’ (π β (UnifOnβπ) β (unifTopβπ) β (TopOnβπ)) | ||
| Theorem | restutop 24155 | Restriction of a topology induced by an uniform structure. (Contributed by Thierry Arnoux, 12-Dec-2017.) |
| β’ ((π β (UnifOnβπ) β§ π΄ β π) β ((unifTopβπ) βΎt π΄) β (unifTopβ(π βΎt (π΄ Γ π΄)))) | ||
| Theorem | restutopopn 24156 | 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 24157* | Lemma for ustuqtop 24164. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
| β’ π = (π β π β¦ ran (π£ β π β¦ (π£ β {π}))) β β’ (((π β (UnifOnβπ) β§ π β π) β§ π΄ β π) β (π΄ β (πβπ) β βπ€ β π π΄ = (π€ β {π}))) | ||
| Theorem | ustuqtop0 24158* | Lemma for ustuqtop 24164. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
| β’ π = (π β π β¦ ran (π£ β π β¦ (π£ β {π}))) β β’ (π β (UnifOnβπ) β π:πβΆπ« π« π) | ||
| Theorem | ustuqtop1 24159* | Lemma for ustuqtop 24164, similar to ssnei2 23033. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
| β’ π = (π β π β¦ ran (π£ β π β¦ (π£ β {π}))) β β’ ((((π β (UnifOnβπ) β§ π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β π β (πβπ)) | ||
| Theorem | ustuqtop2 24160* | Lemma for ustuqtop 24164. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
| β’ π = (π β π β¦ ran (π£ β π β¦ (π£ β {π}))) β β’ ((π β (UnifOnβπ) β§ π β π) β (fiβ(πβπ)) β (πβπ)) | ||
| Theorem | ustuqtop3 24161* | Lemma for ustuqtop 24164, similar to elnei 23028. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
| β’ π = (π β π β¦ ran (π£ β π β¦ (π£ β {π}))) β β’ (((π β (UnifOnβπ) β§ π β π) β§ π β (πβπ)) β π β π) | ||
| Theorem | ustuqtop4 24162* | Lemma for ustuqtop 24164. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
| β’ π = (π β π β¦ ran (π£ β π β¦ (π£ β {π}))) β β’ (((π β (UnifOnβπ) β§ π β π) β§ π β (πβπ)) β βπ β (πβπ)βπ β π π β (πβπ)) | ||
| Theorem | ustuqtop5 24163* | Lemma for ustuqtop 24164. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
| β’ π = (π β π β¦ ran (π£ β π β¦ (π£ β {π}))) β β’ ((π β (UnifOnβπ) β§ π β π) β π β (πβπ)) | ||
| Theorem | ustuqtop 24164* | 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 24165* | 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 24166* | 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 24167 | Images of singletons by entourages π are neighborhoods of those singletons. (Contributed by Thierry Arnoux, 13-Jan-2018.) |
| β’ π½ = (unifTopβπ) β β’ ((π β (UnifOnβπ) β§ π β π β§ π β π) β (π β {π}) β ((neiβπ½)β{π})) | ||
| Theorem | utop2nei 24168 | 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 24169 | 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 24170 | 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 24171 | Extend class notation with the Uniform Structure extractor function. |
| class UnifSt | ||
| Syntax | cusp 24172 | Extend class notation with the class of uniform spaces. |
| class UnifSp | ||
| Syntax | ctus 24173 | Extend class notation with the function mapping a uniform structure to a uniform space. |
| class toUnifSp | ||
| Definition | df-uss 24174 | Define the uniform structure extractor function. Similarly with df-topn 17399 this differs from df-unif 17250 when a structure has been restricted using df-ress 17204; 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 24175 | 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 24176 | 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 24177 | The uniform structure on uniform space π. This proof uses a trick with fvprc 6882 to avoid requiring π to be a set. (Contributed by Thierry Arnoux, 3-Dec-2017.) |
| β’ π΅ = (Baseβπ) & β’ π = (UnifSetβπ) β β’ (π βΎt (π΅ Γ π΅)) = (UnifStβπ) | ||
| Theorem | ussid 24178 | 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 24179 | The predicate π is a uniform space. (Contributed by Thierry Arnoux, 4-Dec-2017.) |
| β’ π΅ = (Baseβπ) & β’ π = (UnifStβπ) & β’ π½ = (TopOpenβπ) β β’ (π β UnifSp β (π β (UnifOnβπ΅) β§ π½ = (unifTopβπ))) | ||
| Theorem | ressuss 24180 | Value of the uniform structure of a restricted space. (Contributed by Thierry Arnoux, 12-Dec-2017.) |
| β’ (π΄ β π β (UnifStβ(π βΎs π΄)) = ((UnifStβπ) βΎt (π΄ Γ π΄))) | ||
| Theorem | ressust 24181 | The uniform structure of a restricted space. (Contributed by Thierry Arnoux, 22-Jan-2018.) |
| β’ π = (Baseβπ) & β’ π = (UnifStβ(π βΎs π΄)) β β’ ((π β UnifSp β§ π΄ β π) β π β (UnifOnβπ΄)) | ||
| Theorem | ressusp 24182 | 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 24183 | 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 24184 | Lemma for tusbas 24186, tusunif 24187, and tustopn 24189. (Contributed by Thierry Arnoux, 5-Dec-2017.) (Proof shortened by AV, 28-Oct-2024.) |
| β’ πΎ = (toUnifSpβπ) β β’ (π β (UnifOnβπ) β (π = (BaseβπΎ) β§ π = (UnifSetβπΎ) β§ (unifTopβπ) = (TopOpenβπΎ))) | ||
| Theorem | tuslemOLD 24185 | Obsolete proof of tuslem 24184 as of 28-Oct-2024. Lemma for tusbas 24186, tusunif 24187, and tustopn 24189. (Contributed by Thierry Arnoux, 5-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
| β’ πΎ = (toUnifSpβπ) β β’ (π β (UnifOnβπ) β (π = (BaseβπΎ) β§ π = (UnifSetβπΎ) β§ (unifTopβπ) = (TopOpenβπΎ))) | ||
| Theorem | tusbas 24186 | The base set of a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
| β’ πΎ = (toUnifSpβπ) β β’ (π β (UnifOnβπ) β π = (BaseβπΎ)) | ||
| Theorem | tusunif 24187 | The uniform structure of a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
| β’ πΎ = (toUnifSpβπ) β β’ (π β (UnifOnβπ) β π = (UnifSetβπΎ)) | ||
| Theorem | tususs 24188 | The uniform structure of a constructed uniform space. (Contributed by Thierry Arnoux, 15-Dec-2017.) |
| β’ πΎ = (toUnifSpβπ) β β’ (π β (UnifOnβπ) β π = (UnifStβπΎ)) | ||
| Theorem | tustopn 24189 | The topology induced by a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
| β’ πΎ = (toUnifSpβπ) & β’ π½ = (unifTopβπ) β β’ (π β (UnifOnβπ) β π½ = (TopOpenβπΎ)) | ||
| Theorem | tususp 24190 | A constructed uniform space is an uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
| β’ πΎ = (toUnifSpβπ) β β’ (π β (UnifOnβπ) β πΎ β UnifSp) | ||
| Theorem | tustps 24191 | A constructed uniform space is a topological space. (Contributed by Thierry Arnoux, 25-Jan-2018.) |
| β’ πΎ = (toUnifSpβπ) β β’ (π β (UnifOnβπ) β πΎ β TopSp) | ||
| Theorem | uspreg 24192 | 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 24193 | Extend class notation with the uniform continuity operation. |
| class Cnu | ||
| Definition | df-ucn 24194* | 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 24195* | 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 24196* | 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 24197* | 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 24198* | Reformulate the πΊ function as a mapping with one variable. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
| β’ (π β π β (UnifOnβπ)) & β’ (π β π β (UnifOnβπ)) & β’ (π β πΉ β (π Cnuπ)) & β’ (π β π β π) & β’ πΊ = (π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) β β’ πΊ = (π β (π Γ π) β¦ β¨(πΉβ(1st βπ)), (πΉβ(2nd βπ))β©) | ||
| Theorem | ucnima 24199* | An equivalent statement of the definition of uniformly continuous function. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
| β’ (π β π β (UnifOnβπ)) & β’ (π β π β (UnifOnβπ)) & β’ (π β πΉ β (π Cnuπ)) & β’ (π β π β π) & β’ πΊ = (π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) β β’ (π β βπ β π (πΊ β π) β π) | ||
| Theorem | ucnprima 24200* | 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π)) & β’ (π β π β π) & β’ πΊ = (π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) β β’ (π β (β‘πΊ β π) β π) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |