![]() |
Metamath
Proof Explorer Theorem List (p. 241 of 481) | < 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: | ![]() (1-30606) |
![]() (30607-32129) |
![]() (32130-48006) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | tdrgtmd 24001 | A topological division ring is a topological monoid. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑅 ∈ TopDRing → 𝑅 ∈ TopMnd) | ||
Theorem | tdrgtps 24002 | A topological division ring is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑅 ∈ TopDRing → 𝑅 ∈ TopSp) | ||
Theorem | istdrg2 24003 | A topological-ring division ring is a topological division ring iff the group of nonzero elements is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ TopDRing ↔ (𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ∧ (𝑀 ↾s (𝐵 ∖ { 0 })) ∈ TopGrp)) | ||
Theorem | mulrcn 24004 | The functionalization of the ring multiplication operation is a continuous function in a topological ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝐽 = (TopOpen‘𝑅) & ⊢ 𝑇 = (+𝑓‘(mulGrp‘𝑅)) ⇒ ⊢ (𝑅 ∈ TopRing → 𝑇 ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) | ||
Theorem | invrcn2 24005 | The multiplicative inverse function is a continuous function from the unit group (that is, the nonzero numbers) to itself. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝐽 = (TopOpen‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) ⇒ ⊢ (𝑅 ∈ TopDRing → 𝐼 ∈ ((𝐽 ↾t 𝑈) Cn (𝐽 ↾t 𝑈))) | ||
Theorem | invrcn 24006 | The multiplicative inverse function is a continuous function from the unit group (that is, the nonzero numbers) to the field. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝐽 = (TopOpen‘𝑅) & ⊢ 𝐼 = (invr‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) ⇒ ⊢ (𝑅 ∈ TopDRing → 𝐼 ∈ ((𝐽 ↾t 𝑈) Cn 𝐽)) | ||
Theorem | cnmpt1mulr 24007* | Continuity of ring multiplication; analogue of cnmpt12f 23491 which cannot be used directly because .r is not a function. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝐽 = (TopOpen‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ TopRing) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐾 Cn 𝐽)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐾 Cn 𝐽)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 · 𝐵)) ∈ (𝐾 Cn 𝐽)) | ||
Theorem | cnmpt2mulr 24008* | Continuity of ring multiplication; analogue of cnmpt22f 23500 which cannot be used directly because .r is not a function. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝐽 = (TopOpen‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ TopRing) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐾 ×t 𝐿) Cn 𝐽)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐾 ×t 𝐿) Cn 𝐽)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝐴 · 𝐵)) ∈ ((𝐾 ×t 𝐿) Cn 𝐽)) | ||
Theorem | dvrcn 24009 | 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 24010 | 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 24011 | 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 24012 | A topological module is a topological monoid. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopMnd) | ||
Theorem | tlmtps 24013 | A topological module is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopSp) | ||
Theorem | tlmlmod 24014 | A topological module is a left module. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ LMod) | ||
Theorem | tlmtrg 24015 | The scalar ring of a topological module is a topological ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ TopMod → 𝐹 ∈ TopRing) | ||
Theorem | tlmscatps 24016 | The scalar ring of a topological module is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ TopMod → 𝐹 ∈ TopSp) | ||
Theorem | istvc 24017 | 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 24018 | 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 24019* | Continuity of scalar multiplication; analogue of cnmpt12f 23491 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 24020* | Continuity of scalar multiplication; analogue of cnmpt22f 23500 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 24021 | A topological vector space is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopGrp) | ||
Theorem | tvctlm 24022 | A topological vector space is a topological module. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopVec → 𝑊 ∈ TopMod) | ||
Theorem | tvclmod 24023 | A topological vector space is a left module. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopVec → 𝑊 ∈ LMod) | ||
Theorem | tvclvec 24024 | A topological vector space is a vector space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopVec → 𝑊 ∈ LVec) | ||
Syntax | cust 24025 | Extend class notation with the class function of uniform structures. |
class UnifOn | ||
Definition | df-ust 24026* | 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 24027 | The defined uniform structure as a function. (Contributed by Thierry Arnoux, 15-Nov-2017.) |
⊢ UnifOn Fn V | ||
Theorem | ustval 24028* | 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 24029* | 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 24030 | Entourages are subsets of the Cartesian product of the base set. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → 𝑉 ⊆ (𝑋 × 𝑋)) | ||
Theorem | ustssel 24031 | 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 24032 | The full set is always an entourage. Condition FIIb of [BourbakiTop1] p. I.36. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 × 𝑋) ∈ 𝑈) | ||
Theorem | ustincl 24033 | 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 24034 | 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 24035 | 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 24036* | 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 24037 | The elements of uniform structures, called entourages, are relations. (Contributed by Thierry Arnoux, 15-Nov-2017.) |
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → Rel 𝑉) | ||
Theorem | ustfilxp 24038 | 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 24039 | A uniform structure cannot be empty. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 ≠ ∅) | ||
Theorem | ustssco 24040 | In an uniform structure, any entourage 𝑉 is a subset of its composition with itself. (Contributed by Thierry Arnoux, 5-Jan-2018.) |
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → 𝑉 ⊆ (𝑉 ∘ 𝑉)) | ||
Theorem | ustexsym 24041* | In an uniform structure, for any entourage 𝑉, there exists a smaller symmetrical entourage. (Contributed by Thierry Arnoux, 4-Jan-2018.) |
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → ∃𝑤 ∈ 𝑈 (◡𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑉)) | ||
Theorem | ustex2sym 24042* | 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 24043* | 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 24044 | Any element of the base set is "near" itself, i.e. entourages are reflexive. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝐴 ∈ 𝑋) → 𝐴𝑉𝐴) | ||
Theorem | ust0 24045 | 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 24046 | The empty set is not an uniform structure. (Contributed by Thierry Arnoux, 3-Dec-2017.) |
⊢ ¬ ∅ ∈ ∪ ran UnifOn | ||
Theorem | ustund 24047 | 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 24048 | Any point 𝐴 is near enough to itself. (Contributed by Thierry Arnoux, 18-Nov-2017.) |
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ (𝑉 “ {𝐴})) | ||
Theorem | ustneism 24049 | 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 24050 | Obsolete version of elfvunirn 6913 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 24051 | Second direction for ustbas 24053. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = dom ∪ 𝑈) | ||
Theorem | ustuni 24052 | The set union of a uniform structure is the Cartesian product of its base. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∪ 𝑈 = (𝑋 × 𝑋)) | ||
Theorem | ustbas 24053 | 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 24054 | Lemma for ustuqtop 24072. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝑃 ∈ 𝑋) → (𝑉 “ {𝑃}) ⊆ 𝑋) | ||
Theorem | trust 24055 | 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 24056 | Extend class notation with the function inducing a topology from a uniform structure. |
class unifTop | ||
Definition | df-utop 24057* | 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 24058* | The topology induced by a uniform structure 𝑈. (Contributed by Thierry Arnoux, 30-Nov-2017.) |
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑎}) | ||
Theorem | elutop 24059* | Open sets in the topology induced by an uniform structure 𝑈 on 𝑋 (Contributed by Thierry Arnoux, 30-Nov-2017.) |
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝐴 ∈ (unifTop‘𝑈) ↔ (𝐴 ⊆ 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝐴))) | ||
Theorem | utoptop 24060 | The topology induced by a uniform structure 𝑈 is a topology. (Contributed by Thierry Arnoux, 30-Nov-2017.) |
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) ∈ Top) | ||
Theorem | utopbas 24061 | The base of the topology induced by a uniform structure 𝑈. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = ∪ (unifTop‘𝑈)) | ||
Theorem | utoptopon 24062 | Topology induced by a uniform structure 𝑈 with its base set. (Contributed by Thierry Arnoux, 5-Jan-2018.) |
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) ∈ (TopOn‘𝑋)) | ||
Theorem | restutop 24063 | Restriction of a topology induced by an uniform structure. (Contributed by Thierry Arnoux, 12-Dec-2017.) |
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((unifTop‘𝑈) ↾t 𝐴) ⊆ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) | ||
Theorem | restutopopn 24064 | 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 24065* | Lemma for ustuqtop 24072. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))) ⇒ ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝐴 ∈ 𝑉) → (𝐴 ∈ (𝑁‘𝑃) ↔ ∃𝑤 ∈ 𝑈 𝐴 = (𝑤 “ {𝑃}))) | ||
Theorem | ustuqtop0 24066* | Lemma for ustuqtop 24072. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))) ⇒ ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑁:𝑋⟶𝒫 𝒫 𝑋) | ||
Theorem | ustuqtop1 24067* | Lemma for ustuqtop 24072, similar to ssnei2 22941. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))) ⇒ ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) | ||
Theorem | ustuqtop2 24068* | Lemma for ustuqtop 24072. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))) ⇒ ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝)) | ||
Theorem | ustuqtop3 24069* | Lemma for ustuqtop 24072, similar to elnei 22936. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))) ⇒ ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎) | ||
Theorem | ustuqtop4 24070* | Lemma for ustuqtop 24072. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))) ⇒ ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞)) | ||
Theorem | ustuqtop5 24071* | Lemma for ustuqtop 24072. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))) ⇒ ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝)) | ||
Theorem | ustuqtop 24072* | 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 24073* | 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 24074* | 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 24075 | Images of singletons by entourages 𝑉 are neighborhoods of those singletons. (Contributed by Thierry Arnoux, 13-Jan-2018.) |
⊢ 𝐽 = (unifTop‘𝑈) ⇒ ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝑃 ∈ 𝑋) → (𝑉 “ {𝑃}) ∈ ((nei‘𝐽)‘{𝑃})) | ||
Theorem | utop2nei 24076 | 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 24077 | 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 24078 | 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 24079 | Extend class notation with the Uniform Structure extractor function. |
class UnifSt | ||
Syntax | cusp 24080 | Extend class notation with the class of uniform spaces. |
class UnifSp | ||
Syntax | ctus 24081 | Extend class notation with the function mapping a uniform structure to a uniform space. |
class toUnifSp | ||
Definition | df-uss 24082 | Define the uniform structure extractor function. Similarly with df-topn 17367 this differs from df-unif 17218 when a structure has been restricted using df-ress 17172; 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 24083 | 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 24084 | 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 24085 | The uniform structure on uniform space 𝑊. This proof uses a trick with fvprc 6873 to avoid requiring 𝑊 to be a set. (Contributed by Thierry Arnoux, 3-Dec-2017.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝑈 = (UnifSet‘𝑊) ⇒ ⊢ (𝑈 ↾t (𝐵 × 𝐵)) = (UnifSt‘𝑊) | ||
Theorem | ussid 24086 | 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 24087 | The predicate 𝑊 is a uniform space. (Contributed by Thierry Arnoux, 4-Dec-2017.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝑈 = (UnifSt‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) ⇒ ⊢ (𝑊 ∈ UnifSp ↔ (𝑈 ∈ (UnifOn‘𝐵) ∧ 𝐽 = (unifTop‘𝑈))) | ||
Theorem | ressuss 24088 | Value of the uniform structure of a restricted space. (Contributed by Thierry Arnoux, 12-Dec-2017.) |
⊢ (𝐴 ∈ 𝑉 → (UnifSt‘(𝑊 ↾s 𝐴)) = ((UnifSt‘𝑊) ↾t (𝐴 × 𝐴))) | ||
Theorem | ressust 24089 | The uniform structure of a restricted space. (Contributed by Thierry Arnoux, 22-Jan-2018.) |
⊢ 𝑋 = (Base‘𝑊) & ⊢ 𝑇 = (UnifSt‘(𝑊 ↾s 𝐴)) ⇒ ⊢ ((𝑊 ∈ UnifSp ∧ 𝐴 ⊆ 𝑋) → 𝑇 ∈ (UnifOn‘𝐴)) | ||
Theorem | ressusp 24090 | 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 24091 | 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 24092 | Lemma for tusbas 24094, tusunif 24095, and tustopn 24097. (Contributed by Thierry Arnoux, 5-Dec-2017.) (Proof shortened by AV, 28-Oct-2024.) |
⊢ 𝐾 = (toUnifSp‘𝑈) ⇒ ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 = (Base‘𝐾) ∧ 𝑈 = (UnifSet‘𝐾) ∧ (unifTop‘𝑈) = (TopOpen‘𝐾))) | ||
Theorem | tuslemOLD 24093 | Obsolete proof of tuslem 24092 as of 28-Oct-2024. Lemma for tusbas 24094, tusunif 24095, and tustopn 24097. (Contributed by Thierry Arnoux, 5-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐾 = (toUnifSp‘𝑈) ⇒ ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 = (Base‘𝐾) ∧ 𝑈 = (UnifSet‘𝐾) ∧ (unifTop‘𝑈) = (TopOpen‘𝐾))) | ||
Theorem | tusbas 24094 | The base set of a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
⊢ 𝐾 = (toUnifSp‘𝑈) ⇒ ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = (Base‘𝐾)) | ||
Theorem | tusunif 24095 | The uniform structure of a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
⊢ 𝐾 = (toUnifSp‘𝑈) ⇒ ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 = (UnifSet‘𝐾)) | ||
Theorem | tususs 24096 | The uniform structure of a constructed uniform space. (Contributed by Thierry Arnoux, 15-Dec-2017.) |
⊢ 𝐾 = (toUnifSp‘𝑈) ⇒ ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 = (UnifSt‘𝐾)) | ||
Theorem | tustopn 24097 | The topology induced by a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
⊢ 𝐾 = (toUnifSp‘𝑈) & ⊢ 𝐽 = (unifTop‘𝑈) ⇒ ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐽 = (TopOpen‘𝐾)) | ||
Theorem | tususp 24098 | A constructed uniform space is an uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
⊢ 𝐾 = (toUnifSp‘𝑈) ⇒ ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐾 ∈ UnifSp) | ||
Theorem | tustps 24099 | A constructed uniform space is a topological space. (Contributed by Thierry Arnoux, 25-Jan-2018.) |
⊢ 𝐾 = (toUnifSp‘𝑈) ⇒ ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐾 ∈ TopSp) | ||
Theorem | uspreg 24100 | 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) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |