HomeTheorem List (p. 238 of 479)
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. 238 of 479) | < 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-30171) |
Hilbert Space Explorer
(30172-31694) |
Users' Mathboxes
(31695-47852) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | tvctlm 23701 | A topological vector space is a topological module. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| β’ (π β TopVec β π β TopMod) | ||
| Theorem | tvclmod 23702 | A topological vector space is a left module. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| β’ (π β TopVec β π β LMod) | ||
| Theorem | tvclvec 23703 | A topological vector space is a vector space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| β’ (π β TopVec β π β LVec) | ||
| Syntax | cust 23704 | Extend class notation with the class function of uniform structures. |
| class UnifOn | ||
| Definition | df-ust 23705* | 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 23706 | The defined uniform structure as a function. (Contributed by Thierry Arnoux, 15-Nov-2017.) |
| β’ UnifOn Fn V | ||
| Theorem | ustval 23707* | 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 23708* | 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 23709 | Entourages are subsets of the Cartesian product of the base set. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
| β’ ((π β (UnifOnβπ) β§ π β π) β π β (π Γ π)) | ||
| Theorem | ustssel 23710 | 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 23711 | The full set is always an entourage. Condition FIIb of [BourbakiTop1] p. I.36. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
| β’ (π β (UnifOnβπ) β (π Γ π) β π) | ||
| Theorem | ustincl 23712 | 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 23713 | 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 23714 | 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 23715* | 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 23716 | The elements of uniform structures, called entourages, are relations. (Contributed by Thierry Arnoux, 15-Nov-2017.) |
| β’ ((π β (UnifOnβπ) β§ π β π) β Rel π) | ||
| Theorem | ustfilxp 23717 | 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 23718 | A uniform structure cannot be empty. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
| β’ (π β (UnifOnβπ) β π β β ) | ||
| Theorem | ustssco 23719 | In an uniform structure, any entourage π is a subset of its composition with itself. (Contributed by Thierry Arnoux, 5-Jan-2018.) |
| β’ ((π β (UnifOnβπ) β§ π β π) β π β (π β π)) | ||
| Theorem | ustexsym 23720* | In an uniform structure, for any entourage π, there exists a smaller symmetrical entourage. (Contributed by Thierry Arnoux, 4-Jan-2018.) |
| β’ ((π β (UnifOnβπ) β§ π β π) β βπ€ β π (β‘π€ = π€ β§ π€ β π)) | ||
| Theorem | ustex2sym 23721* | 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 23722* | 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 23723 | Any element of the base set is "near" itself, i.e. entourages are reflexive. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
| β’ ((π β (UnifOnβπ) β§ π β π β§ π΄ β π) β π΄ππ΄) | ||
| Theorem | ust0 23724 | 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 23725 | The empty set is not an uniform structure. (Contributed by Thierry Arnoux, 3-Dec-2017.) |
| β’ Β¬ β β βͺ ran UnifOn | ||
| Theorem | ustund 23726 | 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 23727 | Any point π΄ is near enough to itself. (Contributed by Thierry Arnoux, 18-Nov-2017.) |
| β’ ((π β (UnifOnβπ) β§ π β π β§ π΄ β π) β π΄ β (π β {π΄})) | ||
| Theorem | ustneism 23728 | 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 23729 | Obsolete version of elfvunirn 6924 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 23730 | Second direction for ustbas 23732. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
| β’ (π β (UnifOnβπ) β π = dom βͺ π) | ||
| Theorem | ustuni 23731 | The set union of a uniform structure is the Cartesian product of its base. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
| β’ (π β (UnifOnβπ) β βͺ π = (π Γ π)) | ||
| Theorem | ustbas 23732 | 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 23733 | Lemma for ustuqtop 23751. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
| β’ ((π β (UnifOnβπ) β§ π β π β§ π β π) β (π β {π}) β π) | ||
| Theorem | trust 23734 | 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 23735 | Extend class notation with the function inducing a topology from a uniform structure. |
| class unifTop | ||
| Definition | df-utop 23736* | 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 23737* | The topology induced by a uniform structure π. (Contributed by Thierry Arnoux, 30-Nov-2017.) |
| β’ (π β (UnifOnβπ) β (unifTopβπ) = {π β π« π β£ βπ₯ β π βπ£ β π (π£ β {π₯}) β π}) | ||
| Theorem | elutop 23738* | Open sets in the topology induced by an uniform structure π on π (Contributed by Thierry Arnoux, 30-Nov-2017.) |
| β’ (π β (UnifOnβπ) β (π΄ β (unifTopβπ) β (π΄ β π β§ βπ₯ β π΄ βπ£ β π (π£ β {π₯}) β π΄))) | ||
| Theorem | utoptop 23739 | The topology induced by a uniform structure π is a topology. (Contributed by Thierry Arnoux, 30-Nov-2017.) |
| β’ (π β (UnifOnβπ) β (unifTopβπ) β Top) | ||
| Theorem | utopbas 23740 | The base of the topology induced by a uniform structure π. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
| β’ (π β (UnifOnβπ) β π = βͺ (unifTopβπ)) | ||
| Theorem | utoptopon 23741 | Topology induced by a uniform structure π with its base set. (Contributed by Thierry Arnoux, 5-Jan-2018.) |
| β’ (π β (UnifOnβπ) β (unifTopβπ) β (TopOnβπ)) | ||
| Theorem | restutop 23742 | Restriction of a topology induced by an uniform structure. (Contributed by Thierry Arnoux, 12-Dec-2017.) |
| β’ ((π β (UnifOnβπ) β§ π΄ β π) β ((unifTopβπ) βΎt π΄) β (unifTopβ(π βΎt (π΄ Γ π΄)))) | ||
| Theorem | restutopopn 23743 | 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 23744* | Lemma for ustuqtop 23751. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
| β’ π = (π β π β¦ ran (π£ β π β¦ (π£ β {π}))) β β’ (((π β (UnifOnβπ) β§ π β π) β§ π΄ β π) β (π΄ β (πβπ) β βπ€ β π π΄ = (π€ β {π}))) | ||
| Theorem | ustuqtop0 23745* | Lemma for ustuqtop 23751. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
| β’ π = (π β π β¦ ran (π£ β π β¦ (π£ β {π}))) β β’ (π β (UnifOnβπ) β π:πβΆπ« π« π) | ||
| Theorem | ustuqtop1 23746* | Lemma for ustuqtop 23751, similar to ssnei2 22620. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
| β’ π = (π β π β¦ ran (π£ β π β¦ (π£ β {π}))) β β’ ((((π β (UnifOnβπ) β§ π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β π β (πβπ)) | ||
| Theorem | ustuqtop2 23747* | Lemma for ustuqtop 23751. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
| β’ π = (π β π β¦ ran (π£ β π β¦ (π£ β {π}))) β β’ ((π β (UnifOnβπ) β§ π β π) β (fiβ(πβπ)) β (πβπ)) | ||
| Theorem | ustuqtop3 23748* | Lemma for ustuqtop 23751, similar to elnei 22615. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
| β’ π = (π β π β¦ ran (π£ β π β¦ (π£ β {π}))) β β’ (((π β (UnifOnβπ) β§ π β π) β§ π β (πβπ)) β π β π) | ||
| Theorem | ustuqtop4 23749* | Lemma for ustuqtop 23751. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
| β’ π = (π β π β¦ ran (π£ β π β¦ (π£ β {π}))) β β’ (((π β (UnifOnβπ) β§ π β π) β§ π β (πβπ)) β βπ β (πβπ)βπ β π π β (πβπ)) | ||
| Theorem | ustuqtop5 23750* | Lemma for ustuqtop 23751. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
| β’ π = (π β π β¦ ran (π£ β π β¦ (π£ β {π}))) β β’ ((π β (UnifOnβπ) β§ π β π) β π β (πβπ)) | ||
| Theorem | ustuqtop 23751* | 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 23752* | 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 23753* | 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 23754 | Images of singletons by entourages π are neighborhoods of those singletons. (Contributed by Thierry Arnoux, 13-Jan-2018.) |
| β’ π½ = (unifTopβπ) β β’ ((π β (UnifOnβπ) β§ π β π β§ π β π) β (π β {π}) β ((neiβπ½)β{π})) | ||
| Theorem | utop2nei 23755 | 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 23756 | 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 23757 | 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 23758 | Extend class notation with the Uniform Structure extractor function. |
| class UnifSt | ||
| Syntax | cusp 23759 | Extend class notation with the class of uniform spaces. |
| class UnifSp | ||
| Syntax | ctus 23760 | Extend class notation with the function mapping a uniform structure to a uniform space. |
| class toUnifSp | ||
| Definition | df-uss 23761 | Define the uniform structure extractor function. Similarly with df-topn 17369 this differs from df-unif 17220 when a structure has been restricted using df-ress 17174; 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 23762 | 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 23763 | 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 23764 | The uniform structure on uniform space π. This proof uses a trick with fvprc 6884 to avoid requiring π to be a set. (Contributed by Thierry Arnoux, 3-Dec-2017.) |
| β’ π΅ = (Baseβπ) & β’ π = (UnifSetβπ) β β’ (π βΎt (π΅ Γ π΅)) = (UnifStβπ) | ||
| Theorem | ussid 23765 | 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 23766 | The predicate π is a uniform space. (Contributed by Thierry Arnoux, 4-Dec-2017.) |
| β’ π΅ = (Baseβπ) & β’ π = (UnifStβπ) & β’ π½ = (TopOpenβπ) β β’ (π β UnifSp β (π β (UnifOnβπ΅) β§ π½ = (unifTopβπ))) | ||
| Theorem | ressuss 23767 | Value of the uniform structure of a restricted space. (Contributed by Thierry Arnoux, 12-Dec-2017.) |
| β’ (π΄ β π β (UnifStβ(π βΎs π΄)) = ((UnifStβπ) βΎt (π΄ Γ π΄))) | ||
| Theorem | ressust 23768 | The uniform structure of a restricted space. (Contributed by Thierry Arnoux, 22-Jan-2018.) |
| β’ π = (Baseβπ) & β’ π = (UnifStβ(π βΎs π΄)) β β’ ((π β UnifSp β§ π΄ β π) β π β (UnifOnβπ΄)) | ||
| Theorem | ressusp 23769 | 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 23770 | 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 23771 | Lemma for tusbas 23773, tusunif 23774, and tustopn 23776. (Contributed by Thierry Arnoux, 5-Dec-2017.) (Proof shortened by AV, 28-Oct-2024.) |
| β’ πΎ = (toUnifSpβπ) β β’ (π β (UnifOnβπ) β (π = (BaseβπΎ) β§ π = (UnifSetβπΎ) β§ (unifTopβπ) = (TopOpenβπΎ))) | ||
| Theorem | tuslemOLD 23772 | Obsolete proof of tuslem 23771 as of 28-Oct-2024. Lemma for tusbas 23773, tusunif 23774, and tustopn 23776. (Contributed by Thierry Arnoux, 5-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
| β’ πΎ = (toUnifSpβπ) β β’ (π β (UnifOnβπ) β (π = (BaseβπΎ) β§ π = (UnifSetβπΎ) β§ (unifTopβπ) = (TopOpenβπΎ))) | ||
| Theorem | tusbas 23773 | The base set of a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
| β’ πΎ = (toUnifSpβπ) β β’ (π β (UnifOnβπ) β π = (BaseβπΎ)) | ||
| Theorem | tusunif 23774 | The uniform structure of a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
| β’ πΎ = (toUnifSpβπ) β β’ (π β (UnifOnβπ) β π = (UnifSetβπΎ)) | ||
| Theorem | tususs 23775 | The uniform structure of a constructed uniform space. (Contributed by Thierry Arnoux, 15-Dec-2017.) |
| β’ πΎ = (toUnifSpβπ) β β’ (π β (UnifOnβπ) β π = (UnifStβπΎ)) | ||
| Theorem | tustopn 23776 | The topology induced by a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
| β’ πΎ = (toUnifSpβπ) & β’ π½ = (unifTopβπ) β β’ (π β (UnifOnβπ) β π½ = (TopOpenβπΎ)) | ||
| Theorem | tususp 23777 | A constructed uniform space is an uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
| β’ πΎ = (toUnifSpβπ) β β’ (π β (UnifOnβπ) β πΎ β UnifSp) | ||
| Theorem | tustps 23778 | A constructed uniform space is a topological space. (Contributed by Thierry Arnoux, 25-Jan-2018.) |
| β’ πΎ = (toUnifSpβπ) β β’ (π β (UnifOnβπ) β πΎ β TopSp) | ||
| Theorem | uspreg 23779 | 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 23780 | Extend class notation with the uniform continuity operation. |
| class Cnu | ||
| Definition | df-ucn 23781* | 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 23782* | 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 23783* | 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 23784* | 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 23785* | Reformulate the πΊ function as a mapping with one variable. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
| β’ (π β π β (UnifOnβπ)) & β’ (π β π β (UnifOnβπ)) & β’ (π β πΉ β (π Cnuπ)) & β’ (π β π β π) & β’ πΊ = (π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) β β’ πΊ = (π β (π Γ π) β¦ β¨(πΉβ(1st βπ)), (πΉβ(2nd βπ))β©) | ||
| Theorem | ucnima 23786* | An equivalent statement of the definition of uniformly continuous function. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
| β’ (π β π β (UnifOnβπ)) & β’ (π β π β (UnifOnβπ)) & β’ (π β πΉ β (π Cnuπ)) & β’ (π β π β π) & β’ πΊ = (π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) β β’ (π β βπ β π (πΊ β π) β π) | ||
| Theorem | ucnprima 23787* | 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 23788 | 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 23789 | 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 23790 | 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 23791 | Extend class notation with the set of Cauchy filter bases. |
| class CauFilu | ||
| Definition | df-cfilu 23792* | 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 23793* | The predicate "πΉ is a Cauchy filter base on uniform space π". (Contributed by Thierry Arnoux, 18-Nov-2017.) |
| β’ (π β (UnifOnβπ) β (πΉ β (CauFiluβπ) β (πΉ β (fBasβπ) β§ βπ£ β π βπ β πΉ (π Γ π) β π£))) | ||
| Theorem | cfilufbas 23794 | A Cauchy filter base is a filter base. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
| β’ ((π β (UnifOnβπ) β§ πΉ β (CauFiluβπ)) β πΉ β (fBasβπ)) | ||
| Theorem | cfiluexsm 23795* | 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 23796* | Lemma for fmucnd 23797. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
| β’ ((πΉ Fn π β§ π΄ β π) β ((π₯ β π, π¦ β π β¦ β¨(πΉβπ₯), (πΉβπ¦)β©) β (π΄ Γ π΄)) = ((πΉ β π΄) Γ (πΉ β π΄))) | ||
| Theorem | fmucnd 23797* | 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 23798 | 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 23799 | 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 23800 | 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βπ)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |