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