![]() |
Metamath
Proof Explorer Theorem List (p. 225 of 437) | < 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-28364) |
![]() (28365-29889) |
![]() (29890-43671) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mulrcn 22401 | 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 22402 | 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 22403 | 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 22404* | Continuity of ring multiplication; analogue of cnmpt12f 21889 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 22405* | Continuity of ring multiplication; analogue of cnmpt22f 21898 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 22406 | 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 22407 | 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 22408 | 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 22409 | A topological module is a topological monoid. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopMnd) | ||
Theorem | tlmtps 22410 | A topological module is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopSp) | ||
Theorem | tlmlmod 22411 | A topological module is a left module. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ LMod) | ||
Theorem | tlmtrg 22412 | The scalar ring of a topological module is a topological ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ TopMod → 𝐹 ∈ TopRing) | ||
Theorem | tlmscatps 22413 | The scalar ring of a topological module is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ TopMod → 𝐹 ∈ TopSp) | ||
Theorem | istvc 22414 | 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 22415 | 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 22416* | Continuity of scalar multiplication; analogue of cnmpt12f 21889 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 22417* | Continuity of scalar multiplication; analogue of cnmpt22f 21898 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 22418 | A topological vector space is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopGrp) | ||
Theorem | tvctlm 22419 | A topological vector space is a topological module. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopVec → 𝑊 ∈ TopMod) | ||
Theorem | tvclmod 22420 | A topological vector space is a left module. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopVec → 𝑊 ∈ LMod) | ||
Theorem | tvclvec 22421 | A topological vector space is a vector space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopVec → 𝑊 ∈ LVec) | ||
Syntax | cust 22422 | Extend class notation with the class function of uniform structures. |
class UnifOn | ||
Definition | df-ust 22423* | 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 22424 | The defined uniform structure as a function. (Contributed by Thierry Arnoux, 15-Nov-2017.) |
⊢ UnifOn Fn V | ||
Theorem | ustval 22425* | 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 22426* | 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 22427 | Entourages are subsets of the Cartesian product of the base set. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → 𝑉 ⊆ (𝑋 × 𝑋)) | ||
Theorem | ustssel 22428 | 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 22429 | The full set is always an entourage. Condition FIIb of [BourbakiTop1] p. I.36. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 × 𝑋) ∈ 𝑈) | ||
Theorem | ustincl 22430 | 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 22431 | 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 22432 | 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 22433* | 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 22434 | The elements of uniform structures, called entourages, are relations. (Contributed by Thierry Arnoux, 15-Nov-2017.) |
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → Rel 𝑉) | ||
Theorem | ustfilxp 22435 | 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 22436 | A uniform structure cannot be empty. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 ≠ ∅) | ||
Theorem | ustssco 22437 | In an uniform structure, any entourage 𝑉 is a subset of its composition with itself. (Contributed by Thierry Arnoux, 5-Jan-2018.) |
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → 𝑉 ⊆ (𝑉 ∘ 𝑉)) | ||
Theorem | ustexsym 22438* | In an uniform structure, for any entourage 𝑉, there exists a smaller symmetrical entourage. (Contributed by Thierry Arnoux, 4-Jan-2018.) |
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → ∃𝑤 ∈ 𝑈 (◡𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑉)) | ||
Theorem | ustex2sym 22439* | 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 22440* | 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 22441 | Any element of the base set is "near" itself, i.e. entourages are reflexive. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝐴 ∈ 𝑋) → 𝐴𝑉𝐴) | ||
Theorem | ust0 22442 | 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 22443 | The empty set is not an uniform structure. (Contributed by Thierry Arnoux, 3-Dec-2017.) |
⊢ ¬ ∅ ∈ ∪ ran UnifOn | ||
Theorem | ustund 22444 | 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 22445 | Any point 𝐴 is near enough to itself. (Contributed by Thierry Arnoux, 18-Nov-2017.) |
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ (𝑉 “ {𝐴})) | ||
Theorem | ustneism 22446 | 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 | elrnust 22447 | First direction for ustbas 22450. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 ∈ ∪ ran UnifOn) | ||
Theorem | ustbas2 22448 | Second direction for ustbas 22450. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = dom ∪ 𝑈) | ||
Theorem | ustuni 22449 | The set union of a uniform structure is the Cartesian product of its base. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∪ 𝑈 = (𝑋 × 𝑋)) | ||
Theorem | ustbas 22450 | 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 22451 | Lemma for ustuqtop 22469. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝑃 ∈ 𝑋) → (𝑉 “ {𝑃}) ⊆ 𝑋) | ||
Theorem | trust 22452 | 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 22453 | Extend class notation with the function inducing a topology from a uniform structure. |
class unifTop | ||
Definition | df-utop 22454* | 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 22455* | The topology induced by a uniform structure 𝑈. (Contributed by Thierry Arnoux, 30-Nov-2017.) |
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑎}) | ||
Theorem | elutop 22456* | Open sets in the topology induced by an uniform structure 𝑈 on 𝑋 (Contributed by Thierry Arnoux, 30-Nov-2017.) |
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝐴 ∈ (unifTop‘𝑈) ↔ (𝐴 ⊆ 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝐴))) | ||
Theorem | utoptop 22457 | The topology induced by a uniform structure 𝑈 is a topology. (Contributed by Thierry Arnoux, 30-Nov-2017.) |
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) ∈ Top) | ||
Theorem | utopbas 22458 | The base of the topology induced by a uniform structure 𝑈. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = ∪ (unifTop‘𝑈)) | ||
Theorem | utoptopon 22459 | Topology induced by a uniform structure 𝑈 with its base set. (Contributed by Thierry Arnoux, 5-Jan-2018.) |
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) ∈ (TopOn‘𝑋)) | ||
Theorem | restutop 22460 | Restriction of a topology induced by an uniform structure. (Contributed by Thierry Arnoux, 12-Dec-2017.) |
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((unifTop‘𝑈) ↾t 𝐴) ⊆ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) | ||
Theorem | restutopopn 22461 | 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 22462* | Lemma for ustuqtop 22469. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))) ⇒ ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝐴 ∈ 𝑉) → (𝐴 ∈ (𝑁‘𝑃) ↔ ∃𝑤 ∈ 𝑈 𝐴 = (𝑤 “ {𝑃}))) | ||
Theorem | ustuqtop0 22463* | Lemma for ustuqtop 22469. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))) ⇒ ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑁:𝑋⟶𝒫 𝒫 𝑋) | ||
Theorem | ustuqtop1 22464* | Lemma for ustuqtop 22469, similar to ssnei2 21339. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))) ⇒ ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) | ||
Theorem | ustuqtop2 22465* | Lemma for ustuqtop 22469. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))) ⇒ ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝)) | ||
Theorem | ustuqtop3 22466* | Lemma for ustuqtop 22469, similar to elnei 21334. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))) ⇒ ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎) | ||
Theorem | ustuqtop4 22467* | Lemma for ustuqtop 22469. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))) ⇒ ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞)) | ||
Theorem | ustuqtop5 22468* | Lemma for ustuqtop 22469. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))) ⇒ ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝)) | ||
Theorem | ustuqtop 22469* | 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 22470* | 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 22471* | 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 22472 | Images of singletons by entourages 𝑉 are neighborhoods of those singletons. (Contributed by Thierry Arnoux, 13-Jan-2018.) |
⊢ 𝐽 = (unifTop‘𝑈) ⇒ ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝑃 ∈ 𝑋) → (𝑉 “ {𝑃}) ∈ ((nei‘𝐽)‘{𝑃})) | ||
Theorem | utop2nei 22473 | 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 22474 | 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 22475 | 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 22476 | Extend class notation with the Uniform Structure extractor function. |
class UnifSt | ||
Syntax | cusp 22477 | Extend class notation with the class of uniform spaces. |
class UnifSp | ||
Syntax | ctus 22478 | Extend class notation with the function mapping a uniform structure to a uniform space. |
class toUnifSp | ||
Definition | df-uss 22479 | Define the uniform structure extractor function. Similarly with df-topn 16481 this differs from df-unif 16372 when a structure has been restricted using df-ress 16274; 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 22480 | 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 22481 | 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 22482 | The uniform structure on uniform space 𝑊. This proof uses a trick with fvprc 6441 to avoid requiring 𝑊 to be a set. (Contributed by Thierry Arnoux, 3-Dec-2017.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝑈 = (UnifSet‘𝑊) ⇒ ⊢ (𝑈 ↾t (𝐵 × 𝐵)) = (UnifSt‘𝑊) | ||
Theorem | ussid 22483 | 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 22484 | The predicate 𝑊 is a uniform space. (Contributed by Thierry Arnoux, 4-Dec-2017.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝑈 = (UnifSt‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) ⇒ ⊢ (𝑊 ∈ UnifSp ↔ (𝑈 ∈ (UnifOn‘𝐵) ∧ 𝐽 = (unifTop‘𝑈))) | ||
Theorem | ressunif 22485 | UnifSet is unaffected by restriction. (Contributed by Thierry Arnoux, 7-Dec-2017.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝑈 = (UnifSet‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝑈 = (UnifSet‘𝐻)) | ||
Theorem | ressuss 22486 | Value of the uniform structure of a restricted space. (Contributed by Thierry Arnoux, 12-Dec-2017.) |
⊢ (𝐴 ∈ 𝑉 → (UnifSt‘(𝑊 ↾s 𝐴)) = ((UnifSt‘𝑊) ↾t (𝐴 × 𝐴))) | ||
Theorem | ressust 22487 | The uniform structure of a restricted space. (Contributed by Thierry Arnoux, 22-Jan-2018.) |
⊢ 𝑋 = (Base‘𝑊) & ⊢ 𝑇 = (UnifSt‘(𝑊 ↾s 𝐴)) ⇒ ⊢ ((𝑊 ∈ UnifSp ∧ 𝐴 ⊆ 𝑋) → 𝑇 ∈ (UnifOn‘𝐴)) | ||
Theorem | ressusp 22488 | 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 22489 | 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 22490 | Lemma for tusbas 22491, tusunif 22492, and tustopn 22494. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
⊢ 𝐾 = (toUnifSp‘𝑈) ⇒ ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 = (Base‘𝐾) ∧ 𝑈 = (UnifSet‘𝐾) ∧ (unifTop‘𝑈) = (TopOpen‘𝐾))) | ||
Theorem | tusbas 22491 | The base set of a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
⊢ 𝐾 = (toUnifSp‘𝑈) ⇒ ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = (Base‘𝐾)) | ||
Theorem | tusunif 22492 | The uniform structure of a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
⊢ 𝐾 = (toUnifSp‘𝑈) ⇒ ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 = (UnifSet‘𝐾)) | ||
Theorem | tususs 22493 | The uniform structure of a constructed uniform space. (Contributed by Thierry Arnoux, 15-Dec-2017.) |
⊢ 𝐾 = (toUnifSp‘𝑈) ⇒ ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 = (UnifSt‘𝐾)) | ||
Theorem | tustopn 22494 | The topology induced by a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
⊢ 𝐾 = (toUnifSp‘𝑈) & ⊢ 𝐽 = (unifTop‘𝑈) ⇒ ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐽 = (TopOpen‘𝐾)) | ||
Theorem | tususp 22495 | A constructed uniform space is an uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
⊢ 𝐾 = (toUnifSp‘𝑈) ⇒ ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐾 ∈ UnifSp) | ||
Theorem | tustps 22496 | A constructed uniform space is a topological space. (Contributed by Thierry Arnoux, 25-Jan-2018.) |
⊢ 𝐾 = (toUnifSp‘𝑈) ⇒ ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐾 ∈ TopSp) | ||
Theorem | uspreg 22497 | 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 22498 | Extend class notation with the uniform continuity operation. |
class Cnu | ||
Definition | df-ucn 22499* | 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 ∪ 𝑣 ↑𝑚 dom ∪ 𝑢) ∣ ∀𝑠 ∈ 𝑣 ∃𝑟 ∈ 𝑢 ∀𝑥 ∈ dom ∪ 𝑢∀𝑦 ∈ dom ∪ 𝑢(𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))}) | ||
Theorem | ucnval 22500* | The set of all uniformly continuous function from uniform space 𝑈 to uniform space 𝑉. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝑈 Cnu𝑉) = {𝑓 ∈ (𝑌 ↑𝑚 𝑋) ∣ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |