![]() |
Metamath
Proof Explorer Theorem List (p. 226 of 443) | < 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-28477) |
![]() (28478-30002) |
![]() (30003-44274) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | tlmtmd 22501 | A topological module is a topological monoid. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopMnd) | ||
Theorem | tlmtps 22502 | A topological module is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopSp) | ||
Theorem | tlmlmod 22503 | A topological module is a left module. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ LMod) | ||
Theorem | tlmtrg 22504 | The scalar ring of a topological module is a topological ring. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ TopMod → 𝐹 ∈ TopRing) | ||
Theorem | tlmscatps 22505 | The scalar ring of a topological module is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ (𝑊 ∈ TopMod → 𝐹 ∈ TopSp) | ||
Theorem | istvc 22506 | 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 22507 | 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 22508* | Continuity of scalar multiplication; analogue of cnmpt12f 21981 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 22509* | Continuity of scalar multiplication; analogue of cnmpt22f 21990 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 22510 | A topological vector space is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopGrp) | ||
Theorem | tvctlm 22511 | A topological vector space is a topological module. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopVec → 𝑊 ∈ TopMod) | ||
Theorem | tvclmod 22512 | A topological vector space is a left module. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopVec → 𝑊 ∈ LMod) | ||
Theorem | tvclvec 22513 | A topological vector space is a vector space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ (𝑊 ∈ TopVec → 𝑊 ∈ LVec) | ||
Syntax | cust 22514 | Extend class notation with the class function of uniform structures. |
class UnifOn | ||
Definition | df-ust 22515* | 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 22516 | The defined uniform structure as a function. (Contributed by Thierry Arnoux, 15-Nov-2017.) |
⊢ UnifOn Fn V | ||
Theorem | ustval 22517* | 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 22518* | 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 22519 | Entourages are subsets of the Cartesian product of the base set. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → 𝑉 ⊆ (𝑋 × 𝑋)) | ||
Theorem | ustssel 22520 | 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 22521 | The full set is always an entourage. Condition FIIb of [BourbakiTop1] p. I.36. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 × 𝑋) ∈ 𝑈) | ||
Theorem | ustincl 22522 | 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 22523 | 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 22524 | 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 22525* | 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 22526 | The elements of uniform structures, called entourages, are relations. (Contributed by Thierry Arnoux, 15-Nov-2017.) |
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → Rel 𝑉) | ||
Theorem | ustfilxp 22527 | 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 22528 | A uniform structure cannot be empty. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 ≠ ∅) | ||
Theorem | ustssco 22529 | In an uniform structure, any entourage 𝑉 is a subset of its composition with itself. (Contributed by Thierry Arnoux, 5-Jan-2018.) |
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → 𝑉 ⊆ (𝑉 ∘ 𝑉)) | ||
Theorem | ustexsym 22530* | In an uniform structure, for any entourage 𝑉, there exists a smaller symmetrical entourage. (Contributed by Thierry Arnoux, 4-Jan-2018.) |
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → ∃𝑤 ∈ 𝑈 (◡𝑤 = 𝑤 ∧ 𝑤 ⊆ 𝑉)) | ||
Theorem | ustex2sym 22531* | 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 22532* | 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 22533 | Any element of the base set is "near" itself, i.e. entourages are reflexive. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝐴 ∈ 𝑋) → 𝐴𝑉𝐴) | ||
Theorem | ust0 22534 | 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 22535 | The empty set is not an uniform structure. (Contributed by Thierry Arnoux, 3-Dec-2017.) |
⊢ ¬ ∅ ∈ ∪ ran UnifOn | ||
Theorem | ustund 22536 | 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 22537 | Any point 𝐴 is near enough to itself. (Contributed by Thierry Arnoux, 18-Nov-2017.) |
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ (𝑉 “ {𝐴})) | ||
Theorem | ustneism 22538 | 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 22539 | First direction for ustbas 22542. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 ∈ ∪ ran UnifOn) | ||
Theorem | ustbas2 22540 | Second direction for ustbas 22542. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = dom ∪ 𝑈) | ||
Theorem | ustuni 22541 | The set union of a uniform structure is the Cartesian product of its base. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∪ 𝑈 = (𝑋 × 𝑋)) | ||
Theorem | ustbas 22542 | 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 22543 | Lemma for ustuqtop 22561. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝑃 ∈ 𝑋) → (𝑉 “ {𝑃}) ⊆ 𝑋) | ||
Theorem | trust 22544 | 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 22545 | Extend class notation with the function inducing a topology from a uniform structure. |
class unifTop | ||
Definition | df-utop 22546* | 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 22547* | The topology induced by a uniform structure 𝑈. (Contributed by Thierry Arnoux, 30-Nov-2017.) |
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑎}) | ||
Theorem | elutop 22548* | Open sets in the topology induced by an uniform structure 𝑈 on 𝑋 (Contributed by Thierry Arnoux, 30-Nov-2017.) |
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝐴 ∈ (unifTop‘𝑈) ↔ (𝐴 ⊆ 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝐴))) | ||
Theorem | utoptop 22549 | The topology induced by a uniform structure 𝑈 is a topology. (Contributed by Thierry Arnoux, 30-Nov-2017.) |
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) ∈ Top) | ||
Theorem | utopbas 22550 | The base of the topology induced by a uniform structure 𝑈. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = ∪ (unifTop‘𝑈)) | ||
Theorem | utoptopon 22551 | Topology induced by a uniform structure 𝑈 with its base set. (Contributed by Thierry Arnoux, 5-Jan-2018.) |
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) ∈ (TopOn‘𝑋)) | ||
Theorem | restutop 22552 | Restriction of a topology induced by an uniform structure. (Contributed by Thierry Arnoux, 12-Dec-2017.) |
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((unifTop‘𝑈) ↾t 𝐴) ⊆ (unifTop‘(𝑈 ↾t (𝐴 × 𝐴)))) | ||
Theorem | restutopopn 22553 | 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 22554* | Lemma for ustuqtop 22561. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))) ⇒ ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝐴 ∈ 𝑉) → (𝐴 ∈ (𝑁‘𝑃) ↔ ∃𝑤 ∈ 𝑈 𝐴 = (𝑤 “ {𝑃}))) | ||
Theorem | ustuqtop0 22555* | Lemma for ustuqtop 22561. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))) ⇒ ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑁:𝑋⟶𝒫 𝒫 𝑋) | ||
Theorem | ustuqtop1 22556* | Lemma for ustuqtop 22561, similar to ssnei2 21431. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))) ⇒ ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) | ||
Theorem | ustuqtop2 22557* | Lemma for ustuqtop 22561. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))) ⇒ ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝)) | ||
Theorem | ustuqtop3 22558* | Lemma for ustuqtop 22561, similar to elnei 21426. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))) ⇒ ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎) | ||
Theorem | ustuqtop4 22559* | Lemma for ustuqtop 22561. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))) ⇒ ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞)) | ||
Theorem | ustuqtop5 22560* | Lemma for ustuqtop 22561. (Contributed by Thierry Arnoux, 11-Jan-2018.) |
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))) ⇒ ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝)) | ||
Theorem | ustuqtop 22561* | 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 22562* | 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 22563* | 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 22564 | Images of singletons by entourages 𝑉 are neighborhoods of those singletons. (Contributed by Thierry Arnoux, 13-Jan-2018.) |
⊢ 𝐽 = (unifTop‘𝑈) ⇒ ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝑃 ∈ 𝑋) → (𝑉 “ {𝑃}) ∈ ((nei‘𝐽)‘{𝑃})) | ||
Theorem | utop2nei 22565 | 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 22566 | 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 22567 | 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 22568 | Extend class notation with the Uniform Structure extractor function. |
class UnifSt | ||
Syntax | cusp 22569 | Extend class notation with the class of uniform spaces. |
class UnifSp | ||
Syntax | ctus 22570 | Extend class notation with the function mapping a uniform structure to a uniform space. |
class toUnifSp | ||
Definition | df-uss 22571 | Define the uniform structure extractor function. Similarly with df-topn 16556 this differs from df-unif 16447 when a structure has been restricted using df-ress 16350; 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 22572 | 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 22573 | 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 22574 | The uniform structure on uniform space 𝑊. This proof uses a trick with fvprc 6494 to avoid requiring 𝑊 to be a set. (Contributed by Thierry Arnoux, 3-Dec-2017.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝑈 = (UnifSet‘𝑊) ⇒ ⊢ (𝑈 ↾t (𝐵 × 𝐵)) = (UnifSt‘𝑊) | ||
Theorem | ussid 22575 | 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 22576 | The predicate 𝑊 is a uniform space. (Contributed by Thierry Arnoux, 4-Dec-2017.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝑈 = (UnifSt‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) ⇒ ⊢ (𝑊 ∈ UnifSp ↔ (𝑈 ∈ (UnifOn‘𝐵) ∧ 𝐽 = (unifTop‘𝑈))) | ||
Theorem | ressunif 22577 | UnifSet is unaffected by restriction. (Contributed by Thierry Arnoux, 7-Dec-2017.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝑈 = (UnifSet‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝑈 = (UnifSet‘𝐻)) | ||
Theorem | ressuss 22578 | Value of the uniform structure of a restricted space. (Contributed by Thierry Arnoux, 12-Dec-2017.) |
⊢ (𝐴 ∈ 𝑉 → (UnifSt‘(𝑊 ↾s 𝐴)) = ((UnifSt‘𝑊) ↾t (𝐴 × 𝐴))) | ||
Theorem | ressust 22579 | The uniform structure of a restricted space. (Contributed by Thierry Arnoux, 22-Jan-2018.) |
⊢ 𝑋 = (Base‘𝑊) & ⊢ 𝑇 = (UnifSt‘(𝑊 ↾s 𝐴)) ⇒ ⊢ ((𝑊 ∈ UnifSp ∧ 𝐴 ⊆ 𝑋) → 𝑇 ∈ (UnifOn‘𝐴)) | ||
Theorem | ressusp 22580 | 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 22581 | 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 22582 | Lemma for tusbas 22583, tusunif 22584, and tustopn 22586. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
⊢ 𝐾 = (toUnifSp‘𝑈) ⇒ ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 = (Base‘𝐾) ∧ 𝑈 = (UnifSet‘𝐾) ∧ (unifTop‘𝑈) = (TopOpen‘𝐾))) | ||
Theorem | tusbas 22583 | The base set of a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
⊢ 𝐾 = (toUnifSp‘𝑈) ⇒ ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = (Base‘𝐾)) | ||
Theorem | tusunif 22584 | The uniform structure of a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
⊢ 𝐾 = (toUnifSp‘𝑈) ⇒ ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 = (UnifSet‘𝐾)) | ||
Theorem | tususs 22585 | The uniform structure of a constructed uniform space. (Contributed by Thierry Arnoux, 15-Dec-2017.) |
⊢ 𝐾 = (toUnifSp‘𝑈) ⇒ ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 = (UnifSt‘𝐾)) | ||
Theorem | tustopn 22586 | The topology induced by a constructed uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
⊢ 𝐾 = (toUnifSp‘𝑈) & ⊢ 𝐽 = (unifTop‘𝑈) ⇒ ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐽 = (TopOpen‘𝐾)) | ||
Theorem | tususp 22587 | A constructed uniform space is an uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.) |
⊢ 𝐾 = (toUnifSp‘𝑈) ⇒ ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐾 ∈ UnifSp) | ||
Theorem | tustps 22588 | A constructed uniform space is a topological space. (Contributed by Thierry Arnoux, 25-Jan-2018.) |
⊢ 𝐾 = (toUnifSp‘𝑈) ⇒ ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐾 ∈ TopSp) | ||
Theorem | uspreg 22589 | 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 22590 | Extend class notation with the uniform continuity operation. |
class Cnu | ||
Definition | df-ucn 22591* | 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 22592* | The set of all uniformly continuous function from uniform space 𝑈 to uniform space 𝑉. (Contributed by Thierry Arnoux, 16-Nov-2017.) |
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ (UnifOn‘𝑌)) → (𝑈 Cnu𝑉) = {𝑓 ∈ (𝑌 ↑𝑚 𝑋) ∣ ∀𝑠 ∈ 𝑉 ∃𝑟 ∈ 𝑈 ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑟𝑦 → (𝑓‘𝑥)𝑠(𝑓‘𝑦))}) | ||
Theorem | isucn 22593* | 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 22594* | 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 22595* | Reformulate the 𝐺 function as a mapping with one variable. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋)) & ⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌)) & ⊢ (𝜑 → 𝐹 ∈ (𝑈 Cnu𝑉)) & ⊢ (𝜑 → 𝑊 ∈ 𝑉) & ⊢ 𝐺 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ⇒ ⊢ 𝐺 = (𝑝 ∈ (𝑋 × 𝑋) ↦ 〈(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))〉) | ||
Theorem | ucnima 22596* | An equivalent statement of the definition of uniformly continuous function. (Contributed by Thierry Arnoux, 19-Nov-2017.) |
⊢ (𝜑 → 𝑈 ∈ (UnifOn‘𝑋)) & ⊢ (𝜑 → 𝑉 ∈ (UnifOn‘𝑌)) & ⊢ (𝜑 → 𝐹 ∈ (𝑈 Cnu𝑉)) & ⊢ (𝜑 → 𝑊 ∈ 𝑉) & ⊢ 𝐺 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ⇒ ⊢ (𝜑 → ∃𝑟 ∈ 𝑈 (𝐺 “ 𝑟) ⊆ 𝑊) | ||
Theorem | ucnprima 22597* | 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 22598 | 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 22599 | 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 22600 | 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 𝐾)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |