Home | Metamath
Proof Explorer Theorem List (p. 224 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | unimopn 22301 | The union of a collection of open sets of a metric space is open. Theorem T2 of [Kreyszig] p. 19. (Contributed by NM, 4-Sep-2006.) (Revised by Mario Carneiro, 23-Dec-2013.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ⊆ 𝐽) → ∪ 𝐴 ∈ 𝐽) | ||
Theorem | mopnin 22302 | The intersection of two open sets of a metric space is open. (Contributed by NM, 4-Sep-2006.) (Revised by Mario Carneiro, 23-Dec-2013.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽) → (𝐴 ∩ 𝐵) ∈ 𝐽) | ||
Theorem | mopn0 22303 | The empty set is an open set of a metric space. Part of Theorem T1 of [Kreyszig] p. 19. (Contributed by NM, 4-Sep-2006.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → ∅ ∈ 𝐽) | ||
Theorem | rnblopn 22304 | A ball of a metric space is an open set. (Contributed by NM, 12-Sep-2006.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ ran (ball‘𝐷)) → 𝐵 ∈ 𝐽) | ||
Theorem | blopn 22305 | A ball of a metric space is an open set. (Contributed by NM, 9-Mar-2007.) (Revised by Mario Carneiro, 12-Nov-2013.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) ∈ 𝐽) | ||
Theorem | neibl 22306* | The neighborhoods around a point 𝑃 of a metric space are those subsets containing a ball around 𝑃. Definition of neighborhood in [Kreyszig] p. 19. (Contributed by NM, 8-Nov-2007.) (Revised by Mario Carneiro, 23-Dec-2013.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) ↔ (𝑁 ⊆ 𝑋 ∧ ∃𝑟 ∈ ℝ+ (𝑃(ball‘𝐷)𝑟) ⊆ 𝑁))) | ||
Theorem | blnei 22307 | A ball around a point is a neighborhood of the point. (Contributed by NM, 8-Nov-2007.) (Revised by Mario Carneiro, 24-Aug-2015.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → (𝑃(ball‘𝐷)𝑅) ∈ ((nei‘𝐽)‘{𝑃})) | ||
Theorem | lpbl 22308* | Every ball around a limit point 𝑃 of a subset 𝑆 includes a member of 𝑆 (even if 𝑃 ∉ 𝑆). (Contributed by NM, 9-Nov-2007.) (Revised by Mario Carneiro, 23-Dec-2013.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ((limPt‘𝐽)‘𝑆)) ∧ 𝑅 ∈ ℝ+) → ∃𝑥 ∈ 𝑆 𝑥 ∈ (𝑃(ball‘𝐷)𝑅)) | ||
Theorem | blsscls2 22309* | A smaller closed ball is contained in a larger open ball. (Contributed by Mario Carneiro, 10-Jan-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝑆 = {𝑧 ∈ 𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅} ⇒ ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑇 ∈ ℝ* ∧ 𝑅 < 𝑇)) → 𝑆 ⊆ (𝑃(ball‘𝐷)𝑇)) | ||
Theorem | blcld 22310* | A "closed ball" in a metric space is actually closed. (Contributed by Mario Carneiro, 31-Dec-2013.) (Revised by Mario Carneiro, 24-Aug-2015.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝑆 = {𝑧 ∈ 𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅} ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → 𝑆 ∈ (Clsd‘𝐽)) | ||
Theorem | blcls 22311* | The closure of an open ball in a metric space is contained in the corresponding closed ball. (Equality need not hold; for example, with the discrete metric, the closed ball of radius 1 is the whole space, but the open ball of radius 1 is just a point, whose closure is also a point.) (Contributed by Mario Carneiro, 31-Dec-2013.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝑆 = {𝑧 ∈ 𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅} ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → ((cls‘𝐽)‘(𝑃(ball‘𝐷)𝑅)) ⊆ 𝑆) | ||
Theorem | blsscls 22312 | If two concentric balls have different radii, the closure of the smaller one is contained in the larger one. (Contributed by Mario Carneiro, 5-Jan-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ 𝑅 < 𝑆)) → ((cls‘𝐽)‘(𝑃(ball‘𝐷)𝑅)) ⊆ (𝑃(ball‘𝐷)𝑆)) | ||
Theorem | metss 22313* | Two ways of saying that metric 𝐷 generates a finer topology than metric 𝐶. (Contributed by Mario Carneiro, 12-Nov-2013.) (Revised by Mario Carneiro, 24-Aug-2015.) |
⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) → (𝐽 ⊆ 𝐾 ↔ ∀𝑥 ∈ 𝑋 ∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟))) | ||
Theorem | metequiv 22314* | Two ways of saying that two metrics generate the same topology. Two metrics satisfying the right-hand side are said to be (topologically) equivalent. (Contributed by Jeff Hankins, 21-Jun-2009.) (Revised by Mario Carneiro, 12-Nov-2013.) |
⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) → (𝐽 = 𝐾 ↔ ∀𝑥 ∈ 𝑋 (∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟) ∧ ∀𝑎 ∈ ℝ+ ∃𝑏 ∈ ℝ+ (𝑥(ball‘𝐶)𝑏) ⊆ (𝑥(ball‘𝐷)𝑎)))) | ||
Theorem | metequiv2 22315* | If there is a sequence of radii approaching zero for which the balls of both metrics coincide, then the generated topologies are equivalent. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) → (∀𝑥 ∈ 𝑋 ∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+ (𝑠 ≤ 𝑟 ∧ (𝑥(ball‘𝐶)𝑠) = (𝑥(ball‘𝐷)𝑠)) → 𝐽 = 𝐾)) | ||
Theorem | metss2lem 22316* | Lemma for metss2 22317. (Contributed by Mario Carneiro, 14-Sep-2015.) |
⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐶 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐶𝑦) ≤ (𝑅 · (𝑥𝐷𝑦))) ⇒ ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) → (𝑥(ball‘𝐷)(𝑆 / 𝑅)) ⊆ (𝑥(ball‘𝐶)𝑆)) | ||
Theorem | metss2 22317* | If the metric 𝐷 is "strongly finer" than 𝐶 (meaning that there is a positive real constant 𝑅 such that 𝐶(𝑥, 𝑦) ≤ 𝑅 · 𝐷(𝑥, 𝑦)), then 𝐷 generates a finer topology. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then they generate the same topology.) (Contributed by Mario Carneiro, 14-Sep-2015.) |
⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐶 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐶𝑦) ≤ (𝑅 · (𝑥𝐷𝑦))) ⇒ ⊢ (𝜑 → 𝐽 ⊆ 𝐾) | ||
Theorem | comet 22318* | The composition of an extended metric with a monotonic subadditive function is an extended metric. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝐹:(0[,]+∞)⟶ℝ*) & ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞)) → ((𝐹‘𝑥) = 0 ↔ 𝑥 = 0)) & ⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞))) → (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦))) & ⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞))) → (𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦))) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝐷) ∈ (∞Met‘𝑋)) | ||
Theorem | stdbdmetval 22319* | Value of the standard bounded metric. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ if((𝑥𝐶𝑦) ≤ 𝑅, (𝑥𝐶𝑦), 𝑅)) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = if((𝐴𝐶𝐵) ≤ 𝑅, (𝐴𝐶𝐵), 𝑅)) | ||
Theorem | stdbdxmet 22320* | The standard bounded metric is an extended metric given an extended metric and a positive extended real cutoff. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ if((𝑥𝐶𝑦) ≤ 𝑅, (𝑥𝐶𝑦), 𝑅)) ⇒ ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) → 𝐷 ∈ (∞Met‘𝑋)) | ||
Theorem | stdbdmet 22321* | The standard bounded metric is a proper metric given an extended metric and a positive real cutoff. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ if((𝑥𝐶𝑦) ≤ 𝑅, (𝑥𝐶𝑦), 𝑅)) ⇒ ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ+) → 𝐷 ∈ (Met‘𝑋)) | ||
Theorem | stdbdbl 22322* | The standard bounded metric corresponding to 𝐶 generates the same balls as 𝐶 for radii less than 𝑅. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ if((𝑥𝐶𝑦) ≤ 𝑅, (𝑥𝐶𝑦), 𝑅)) ⇒ ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ* ∧ 𝑆 ≤ 𝑅)) → (𝑃(ball‘𝐷)𝑆) = (𝑃(ball‘𝐶)𝑆)) | ||
Theorem | stdbdmopn 22323* | The standard bounded metric corresponding to 𝐶 generates the same topology as 𝐶. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ if((𝑥𝐶𝑦) ≤ 𝑅, (𝑥𝐶𝑦), 𝑅)) & ⊢ 𝐽 = (MetOpen‘𝐶) ⇒ ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) → 𝐽 = (MetOpen‘𝐷)) | ||
Theorem | mopnex 22324* | The topology generated by an extended metric can also be generated by a true metric. Thus, "metrizable topologies" can equivalently be defined in terms of metrics or extended metrics. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → ∃𝑑 ∈ (Met‘𝑋)𝐽 = (MetOpen‘𝑑)) | ||
Theorem | methaus 22325 | The topology generated by a metric space is Hausdorff. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Haus) | ||
Theorem | met1stc 22326 | The topology generated by a metric space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ 1st𝜔) | ||
Theorem | met2ndci 22327 | A separable metric space (a metric space with a countable dense subset) is second-countable. (Contributed by Mario Carneiro, 13-Apr-2015.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → 𝐽 ∈ 2nd𝜔) | ||
Theorem | met2ndc 22328* | A metric space is second-countable iff it is separable (has a countable dense subset). (Contributed by Mario Carneiro, 13-Apr-2015.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐽 ∈ 2nd𝜔 ↔ ∃𝑥 ∈ 𝒫 𝑋(𝑥 ≼ ω ∧ ((cls‘𝐽)‘𝑥) = 𝑋))) | ||
Theorem | metrest 22329 | Two alternate formulations of a subspace topology of a metric space topology. (Contributed by Jeff Hankins, 19-Aug-2009.) (Proof shortened by Mario Carneiro, 5-Jan-2014.) |
⊢ 𝐷 = (𝐶 ↾ (𝑌 × 𝑌)) & ⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝐽 ↾t 𝑌) = 𝐾) | ||
Theorem | ressxms 22330 | The restriction of a metric space is a metric space. (Contributed by Mario Carneiro, 24-Aug-2015.) |
⊢ ((𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉) → (𝐾 ↾s 𝐴) ∈ ∞MetSp) | ||
Theorem | ressms 22331 | The restriction of a metric space is a metric space. (Contributed by Mario Carneiro, 24-Aug-2015.) |
⊢ ((𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉) → (𝐾 ↾s 𝐴) ∈ MetSp) | ||
Theorem | prdsmslem1 22332 | Lemma for prdsms 22336. The distance function of a product structure is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ 𝐷 = (dist‘𝑌) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ (𝜑 → 𝑅:𝐼⟶MetSp) ⇒ ⊢ (𝜑 → 𝐷 ∈ (Met‘𝐵)) | ||
Theorem | prdsxmslem1 22333 | Lemma for prdsms 22336. The distance function of a product structure is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ 𝐷 = (dist‘𝑌) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ (𝜑 → 𝑅:𝐼⟶∞MetSp) ⇒ ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝐵)) | ||
Theorem | prdsxmslem2 22334* | Lemma for prdsxms 22335. The topology generated by the supremum metric is the same as the product topology, when the index set is finite. (Contributed by Mario Carneiro, 28-Aug-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ 𝐷 = (dist‘𝑌) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ (𝜑 → 𝑅:𝐼⟶∞MetSp) & ⊢ 𝐽 = (TopOpen‘𝑌) & ⊢ 𝑉 = (Base‘(𝑅‘𝑘)) & ⊢ 𝐸 = ((dist‘(𝑅‘𝑘)) ↾ (𝑉 × 𝑉)) & ⊢ 𝐾 = (TopOpen‘(𝑅‘𝑘)) & ⊢ 𝐶 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))} ⇒ ⊢ (𝜑 → 𝐽 = (MetOpen‘𝐷)) | ||
Theorem | prdsxms 22335 | The indexed product structure is an extended metric space when the index set is finite. (Although the extended metric is still valid when the index set is infinite, it no longer agrees with the product topology, which is not metrizable in any case.) (Contributed by Mario Carneiro, 28-Aug-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) ⇒ ⊢ ((𝑆 ∈ 𝑊 ∧ 𝐼 ∈ Fin ∧ 𝑅:𝐼⟶∞MetSp) → 𝑌 ∈ ∞MetSp) | ||
Theorem | prdsms 22336 | The indexed product structure is a metric space when the index set is finite. (Contributed by Mario Carneiro, 28-Aug-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) ⇒ ⊢ ((𝑆 ∈ 𝑊 ∧ 𝐼 ∈ Fin ∧ 𝑅:𝐼⟶MetSp) → 𝑌 ∈ MetSp) | ||
Theorem | pwsxms 22337 | The product of a finite family of metric spaces is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) ⇒ ⊢ ((𝑅 ∈ ∞MetSp ∧ 𝐼 ∈ Fin) → 𝑌 ∈ ∞MetSp) | ||
Theorem | pwsms 22338 | The product of a finite family of metric spaces is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) ⇒ ⊢ ((𝑅 ∈ MetSp ∧ 𝐼 ∈ Fin) → 𝑌 ∈ MetSp) | ||
Theorem | xpsxms 22339 | A binary product of metric spaces is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) ⇒ ⊢ ((𝑅 ∈ ∞MetSp ∧ 𝑆 ∈ ∞MetSp) → 𝑇 ∈ ∞MetSp) | ||
Theorem | xpsms 22340 | A binary product of metric spaces is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) ⇒ ⊢ ((𝑅 ∈ MetSp ∧ 𝑆 ∈ MetSp) → 𝑇 ∈ MetSp) | ||
Theorem | tmsxps 22341 | Express the product of two metrics as another metric. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ 𝑃 = (dist‘((toMetSp‘𝑀) ×s (toMetSp‘𝑁))) & ⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌)) ⇒ ⊢ (𝜑 → 𝑃 ∈ (∞Met‘(𝑋 × 𝑌))) | ||
Theorem | tmsxpsmopn 22342 | Express the product of two metrics as another metric. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ 𝑃 = (dist‘((toMetSp‘𝑀) ×s (toMetSp‘𝑁))) & ⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌)) & ⊢ 𝐽 = (MetOpen‘𝑀) & ⊢ 𝐾 = (MetOpen‘𝑁) & ⊢ 𝐿 = (MetOpen‘𝑃) ⇒ ⊢ (𝜑 → 𝐿 = (𝐽 ×t 𝐾)) | ||
Theorem | tmsxpsval 22343 | Value of the product of two metrics. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ 𝑃 = (dist‘((toMetSp‘𝑀) ×s (toMetSp‘𝑁))) & ⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌)) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑌) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑌) ⇒ ⊢ (𝜑 → (〈𝐴, 𝐵〉𝑃〈𝐶, 𝐷〉) = sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < )) | ||
Theorem | tmsxpsval2 22344 | Value of the product of two metrics. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ 𝑃 = (dist‘((toMetSp‘𝑀) ×s (toMetSp‘𝑁))) & ⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌)) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑌) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑌) ⇒ ⊢ (𝜑 → (〈𝐴, 𝐵〉𝑃〈𝐶, 𝐷〉) = if((𝐴𝑀𝐶) ≤ (𝐵𝑁𝐷), (𝐵𝑁𝐷), (𝐴𝑀𝐶))) | ||
Theorem | metcnp3 22345* | Two ways to express that 𝐹 is continuous at 𝑃 for metric spaces. Proposition 14-4.2 of [Gleason] p. 240. (Contributed by NM, 17-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.) |
⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌) ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ (𝐹 “ (𝑃(ball‘𝐶)𝑧)) ⊆ ((𝐹‘𝑃)(ball‘𝐷)𝑦)))) | ||
Theorem | metcnp 22346* | Two ways to say a mapping from metric 𝐶 to metric 𝐷 is continuous at point 𝑃. (Contributed by NM, 11-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.) |
⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌) ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝑋 ((𝑃𝐶𝑤) < 𝑧 → ((𝐹‘𝑃)𝐷(𝐹‘𝑤)) < 𝑦)))) | ||
Theorem | metcnp2 22347* | Two ways to say a mapping from metric 𝐶 to metric 𝐷 is continuous at point 𝑃. The distance arguments are swapped compared to metcnp 22346 (and Munkres' metcn 22348) for compatibility with df-lm 21033. Definition 1.3-3 of [Kreyszig] p. 20. (Contributed by NM, 4-Jun-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌) ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝑋 ((𝑤𝐶𝑃) < 𝑧 → ((𝐹‘𝑤)𝐷(𝐹‘𝑃)) < 𝑦)))) | ||
Theorem | metcn 22348* | Two ways to say a mapping from metric 𝐶 to metric 𝐷 is continuous. Theorem 10.1 of [Munkres] p. 127. The second biconditional argument says that for every positive "epsilon" 𝑦 there is a positive "delta" 𝑧 such that a distance less than delta in 𝐶 maps to a distance less than epsilon in 𝐷. (Contributed by NM, 15-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.) |
⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝐹‘𝑥)𝐷(𝐹‘𝑤)) < 𝑦)))) | ||
Theorem | metcnpi 22349* | Epsilon-delta property of a continuous metric space function, with function arguments as in metcnp 22346. (Contributed by NM, 17-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷) ⇒ ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌)) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐴 ∈ ℝ+)) → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝑋 ((𝑃𝐶𝑦) < 𝑥 → ((𝐹‘𝑃)𝐷(𝐹‘𝑦)) < 𝐴)) | ||
Theorem | metcnpi2 22350* | Epsilon-delta property of a continuous metric space function, with swapped distance function arguments as in metcnp2 22347. (Contributed by NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷) ⇒ ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌)) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐴 ∈ ℝ+)) → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝑋 ((𝑦𝐶𝑃) < 𝑥 → ((𝐹‘𝑦)𝐷(𝐹‘𝑃)) < 𝐴)) | ||
Theorem | metcnpi3 22351* | Epsilon-delta property of a metric space function continuous at 𝑃. A variation of metcnpi2 22350 with non-strict ordering. (Contributed by NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷) ⇒ ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌)) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐴 ∈ ℝ+)) → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝑋 ((𝑦𝐶𝑃) ≤ 𝑥 → ((𝐹‘𝑦)𝐷(𝐹‘𝑃)) ≤ 𝐴)) | ||
Theorem | txmetcnp 22352* | Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷) & ⊢ 𝐿 = (MetOpen‘𝐸) ⇒ ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌) ∧ 𝐸 ∈ (∞Met‘𝑍)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐹 ∈ (((𝐽 ×t 𝐾) CnP 𝐿)‘〈𝐴, 𝐵〉) ↔ (𝐹:(𝑋 × 𝑌)⟶𝑍 ∧ ∀𝑧 ∈ ℝ+ ∃𝑤 ∈ ℝ+ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑌 (((𝐴𝐶𝑢) < 𝑤 ∧ (𝐵𝐷𝑣) < 𝑤) → ((𝐴𝐹𝐵)𝐸(𝑢𝐹𝑣)) < 𝑧)))) | ||
Theorem | txmetcn 22353* | Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷) & ⊢ 𝐿 = (MetOpen‘𝐸) ⇒ ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌) ∧ 𝐸 ∈ (∞Met‘𝑍)) → (𝐹 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ↔ (𝐹:(𝑋 × 𝑌)⟶𝑍 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ∀𝑧 ∈ ℝ+ ∃𝑤 ∈ ℝ+ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑌 (((𝑥𝐶𝑢) < 𝑤 ∧ (𝑦𝐷𝑣) < 𝑤) → ((𝑥𝐹𝑦)𝐸(𝑢𝐹𝑣)) < 𝑧)))) | ||
Theorem | metuval 22354* | Value of the uniform structure generated by metric 𝐷. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
⊢ (𝐷 ∈ (PsMet‘𝑋) → (metUnif‘𝐷) = ((𝑋 × 𝑋)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))))) | ||
Theorem | metustel 22355* | Define a filter base 𝐹 generated by a metric 𝐷. (Contributed by Thierry Arnoux, 22-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))) ⇒ ⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝐵 ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ+ 𝐵 = (◡𝐷 “ (0[,)𝑎)))) | ||
Theorem | metustss 22356* | Range of the elements of the filter base generated by the metric 𝐷. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))) ⇒ ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) → 𝐴 ⊆ (𝑋 × 𝑋)) | ||
Theorem | metustrel 22357* | Elements of the filter base generated by the metric 𝐷 are relations. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))) ⇒ ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) → Rel 𝐴) | ||
Theorem | metustto 22358* | Any two elements of the filter base generated by the metric 𝐷 can be compared, like for RR+ (i.e. it's totally ordered). (Contributed by Thierry Arnoux, 22-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))) ⇒ ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐹) → (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴)) | ||
Theorem | metustid 22359* | The identity diagonal is included in all elements of the filter base generated by the metric 𝐷. (Contributed by Thierry Arnoux, 22-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))) ⇒ ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) → ( I ↾ 𝑋) ⊆ 𝐴) | ||
Theorem | metustsym 22360* | Elements of the filter base generated by the metric 𝐷 are symmetric. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))) ⇒ ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) → ◡𝐴 = 𝐴) | ||
Theorem | metustexhalf 22361* | For any element 𝐴 of the filter base generated by the metric 𝐷, the half element (corresponding to half the distance) is also in this base. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))) ⇒ ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) → ∃𝑣 ∈ 𝐹 (𝑣 ∘ 𝑣) ⊆ 𝐴) | ||
Theorem | metustfbas 22362* | The filter base generated by a metric 𝐷. (Contributed by Thierry Arnoux, 26-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))) ⇒ ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → 𝐹 ∈ (fBas‘(𝑋 × 𝑋))) | ||
Theorem | metust 22363* | The uniform structure generated by a metric 𝐷. (Contributed by Thierry Arnoux, 26-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))) ⇒ ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋)) | ||
Theorem | cfilucfil 22364* | Given a metric 𝐷 and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the filter bases which contain balls of any pre-chosen size. See iscfil 23063. (Contributed by Thierry Arnoux, 29-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))) ⇒ ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹)) ↔ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))) | ||
Theorem | metuust 22365 | The uniform structure generated by metric 𝐷 is a uniform structure. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (metUnif‘𝐷) ∈ (UnifOn‘𝑋)) | ||
Theorem | cfilucfil2 22366* | Given a metric 𝐷 and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the filter bases which contain balls of any pre-chosen size. See iscfil 23063. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐶 ∈ (CauFilu‘(metUnif‘𝐷)) ↔ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))) | ||
Theorem | blval2 22367 | The ball around a point 𝑃, alternative definition. (Contributed by Thierry Arnoux, 7-Dec-2017.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → (𝑃(ball‘𝐷)𝑅) = ((◡𝐷 “ (0[,)𝑅)) “ {𝑃})) | ||
Theorem | elbl4 22368 | Membership in a ball, alternative definition. (Contributed by Thierry Arnoux, 26-Jan-2018.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ∈ ℝ+) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐵 ∈ (𝐴(ball‘𝐷)𝑅) ↔ 𝐵(◡𝐷 “ (0[,)𝑅))𝐴)) | ||
Theorem | metuel 22369* | Elementhood in the uniform structure generated by a metric 𝐷 (Contributed by Thierry Arnoux, 8-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝑉 ∈ (metUnif‘𝐷) ↔ (𝑉 ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))𝑤 ⊆ 𝑉))) | ||
Theorem | metuel2 22370* | Elementhood in the uniform structure generated by a metric 𝐷 (Contributed by Thierry Arnoux, 24-Jan-2018.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
⊢ 𝑈 = (metUnif‘𝐷) ⇒ ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝑉 ∈ 𝑈 ↔ (𝑉 ⊆ (𝑋 × 𝑋) ∧ ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐷𝑦) < 𝑑 → 𝑥𝑉𝑦)))) | ||
Theorem | metustbl 22371* | The "section" image of an entourage at a point 𝑃 always contains a ball (centered on this point). (Contributed by Thierry Arnoux, 8-Dec-2017.) |
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑉 ∈ (metUnif‘𝐷) ∧ 𝑃 ∈ 𝑋) → ∃𝑎 ∈ ran (ball‘𝐷)(𝑃 ∈ 𝑎 ∧ 𝑎 ⊆ (𝑉 “ {𝑃}))) | ||
Theorem | psmetutop 22372 | The topology induced by a uniform structure generated by a metric 𝐷 is generated by that metric's open balls. (Contributed by Thierry Arnoux, 6-Dec-2017.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (unifTop‘(metUnif‘𝐷)) = (topGen‘ran (ball‘𝐷))) | ||
Theorem | xmetutop 22373 | The topology induced by a uniform structure generated by an extended metric 𝐷 is that metric's open sets. (Contributed by Thierry Arnoux, 11-Mar-2018.) |
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (∞Met‘𝑋)) → (unifTop‘(metUnif‘𝐷)) = (MetOpen‘𝐷)) | ||
Theorem | xmsusp 22374 | If the uniform set of a metric space is the uniform structure generated by its metric, then it is a uniform space. (Contributed by Thierry Arnoux, 14-Dec-2017.) |
⊢ 𝑋 = (Base‘𝐹) & ⊢ 𝐷 = ((dist‘𝐹) ↾ (𝑋 × 𝑋)) & ⊢ 𝑈 = (UnifSt‘𝐹) ⇒ ⊢ ((𝑋 ≠ ∅ ∧ 𝐹 ∈ ∞MetSp ∧ 𝑈 = (metUnif‘𝐷)) → 𝐹 ∈ UnifSp) | ||
Theorem | restmetu 22375 | The uniform structure generated by the restriction of a metric is its trace. (Contributed by Thierry Arnoux, 18-Dec-2017.) |
⊢ ((𝐴 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((metUnif‘𝐷) ↾t (𝐴 × 𝐴)) = (metUnif‘(𝐷 ↾ (𝐴 × 𝐴)))) | ||
Theorem | metucn 22376* | Uniform continuity in metric spaces. Compare the order of the quantifiers with metcn 22348. (Contributed by Thierry Arnoux, 26-Jan-2018.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
⊢ 𝑈 = (metUnif‘𝐶) & ⊢ 𝑉 = (metUnif‘𝐷) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝑌 ≠ ∅) & ⊢ (𝜑 → 𝐶 ∈ (PsMet‘𝑋)) & ⊢ (𝜑 → 𝐷 ∈ (PsMet‘𝑌)) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑑 ∈ ℝ+ ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐶𝑦) < 𝑐 → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) < 𝑑)))) | ||
Theorem | dscmet 22377* | The discrete metric on any set 𝑋. Definition 1.1-8 of [Kreyszig] p. 8. (Contributed by FL, 12-Oct-2006.) |
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ if(𝑥 = 𝑦, 0, 1)) ⇒ ⊢ (𝑋 ∈ 𝑉 → 𝐷 ∈ (Met‘𝑋)) | ||
Theorem | dscopn 22378* | The discrete metric generates the discrete topology. In particular, the discrete topology is metrizable. (Contributed by Mario Carneiro, 29-Jan-2014.) |
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ if(𝑥 = 𝑦, 0, 1)) ⇒ ⊢ (𝑋 ∈ 𝑉 → (MetOpen‘𝐷) = 𝒫 𝑋) | ||
Theorem | nrmmetd 22379* | Show that a group norm generates a metric. Part of Definition 2.2-1 of [Kreyszig] p. 58. (Contributed by NM, 4-Dec-2006.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐹:𝑋⟶ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝐹‘𝑥) = 0 ↔ 𝑥 = 0 )) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝐹‘(𝑥 − 𝑦)) ≤ ((𝐹‘𝑥) + (𝐹‘𝑦))) ⇒ ⊢ (𝜑 → (𝐹 ∘ − ) ∈ (Met‘𝑋)) | ||
Theorem | abvmet 22380 | An absolute value 𝐹 generates a metric defined by 𝑑(𝑥, 𝑦) = 𝐹(𝑥 − 𝑦), analogously to cnmet 22575. (In fact, the ring structure is not needed at all; the group properties abveq0 18826 and abvtri 18830, abvneg 18834 are sufficient.) (Contributed by Mario Carneiro, 9-Sep-2014.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝐴 = (AbsVal‘𝑅) & ⊢ − = (-g‘𝑅) ⇒ ⊢ (𝐹 ∈ 𝐴 → (𝐹 ∘ − ) ∈ (Met‘𝑋)) | ||
In the following, the norm of a normed algebraic structure (group, left module, vector space) is defined by the (given) distance function (the norm 𝑁 of an element is its distance 𝐷 from the zero element, see nmval 22394: (𝑁‘𝐴) = (𝐴𝐷 0 )). By this definition, the norm function 𝑁 is actually a norm (satisfying the properties of being a function into the reals, subadditivity/triangle inequality ( n(x+y) <_ n(x)+n(y) ), absolute homogeneity ( n(sx) = |s| n(x) ) [Remark: for group norms, some authors (e.g. Juris Steprans in "A characterization of free abelian groups") demand that n(sx) = |s| n(x) for all s in ZZ, whereas other authors (e.g. N. H. Bingham and A. J. Ostaszewski in "Normed versus topological groups: Dichotomy and duality") only require inversion symmetry, i.e. n(-x) = n(x). The definition df-ngp 22388 of a group norm follows the second aproach, see nminv 22425.] and positive definiteness/point-separating ( n(x) = 0 <-> x = 0 ) if the structure is a metric space with a right-translation-invariant metric (see nmf 22419, nmtri 22430, nmvs 22480 and nmeq0 22422). An alternate definition of a normed group (i.e. a group equipped with a norm) without using the properties of a metric space is given by theorem tngngp3 22460. For a structure being a group, the (arbitrary) distance function can be restricted to the elements of the group without affecting the norm, see nmfval2 22395. Usually, however, the norm of a normed structure is given, and the corresponding metric ("induced metric") is achieved by defining a distance function based on the norm (the distance 𝐷 between two elements is the norm 𝑁 of their difference, see ngpds 22408: (𝐴𝐷𝐵) = (𝑁‘(𝐴 − 𝐵))). The operation toNrmGrp does exactly this, i.e. it adds a distance function (and a topology) to a structure (which should be at least a group) corresponding to a given norm in the just shown way: (dist‘𝑇) = (𝑁 ∘ − ), see also tngds 22452. By this, the enhanced structure becomes a normed structure if the induced metric is in fact a metric (see tngngp2 22456) resp. if the norm is in fact a norm (see tngngpd 22457). If the norm is derived from a given metric, as done with df-nm 22387, the induced metric is the original metric restricted to the base set: (dist‘𝑇) = ((dist‘𝐺) ↾ (𝑋 × 𝑋)), see nrmtngdist 22461, and the norm remains the same: (norm‘𝑇) = (norm‘𝐺), see nrmtngnrm 22462. | ||
Syntax | cnm 22381 | Norm of a normed ring. |
class norm | ||
Syntax | cngp 22382 | The class of all normed groups. |
class NrmGrp | ||
Syntax | ctng 22383 | Make a normed group from a norm and a group. |
class toNrmGrp | ||
Syntax | cnrg 22384 | Normed ring. |
class NrmRing | ||
Syntax | cnlm 22385 | Normed module. |
class NrmMod | ||
Syntax | cnvc 22386 | Normed vector space. |
class NrmVec | ||
Definition | df-nm 22387* | Define the norm on a group or ring (when it makes sense) in terms of the distance to zero. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ norm = (𝑤 ∈ V ↦ (𝑥 ∈ (Base‘𝑤) ↦ (𝑥(dist‘𝑤)(0g‘𝑤)))) | ||
Definition | df-ngp 22388 | Define a normed group, which is a group with a right-translation-invariant metric. This is not a standard notion, but is helpful as the most general context in which a metric-like norm makes sense. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ NrmGrp = {𝑔 ∈ (Grp ∩ MetSp) ∣ ((norm‘𝑔) ∘ (-g‘𝑔)) ⊆ (dist‘𝑔)} | ||
Definition | df-tng 22389* | Define a function that fills in the topology and metric components of a structure given a group and a norm on it. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ toNrmGrp = (𝑔 ∈ V, 𝑓 ∈ V ↦ ((𝑔 sSet 〈(dist‘ndx), (𝑓 ∘ (-g‘𝑔))〉) sSet 〈(TopSet‘ndx), (MetOpen‘(𝑓 ∘ (-g‘𝑔)))〉)) | ||
Definition | df-nrg 22390 | A normed ring is a ring with an induced topology and metric such that the metric is translation-invariant and the norm (distance from 0) is an absolute value on the ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ NrmRing = {𝑤 ∈ NrmGrp ∣ (norm‘𝑤) ∈ (AbsVal‘𝑤)} | ||
Definition | df-nlm 22391* | A normed (left) module is a module which is also a normed group over a normed ring, such that the norm distributes over scalar multiplication. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ NrmMod = {𝑤 ∈ (NrmGrp ∩ LMod) ∣ [(Scalar‘𝑤) / 𝑓](𝑓 ∈ NrmRing ∧ ∀𝑥 ∈ (Base‘𝑓)∀𝑦 ∈ (Base‘𝑤)((norm‘𝑤)‘(𝑥( ·𝑠 ‘𝑤)𝑦)) = (((norm‘𝑓)‘𝑥) · ((norm‘𝑤)‘𝑦)))} | ||
Definition | df-nvc 22392 | A normed vector space is a normed module which is also a vector space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ NrmVec = (NrmMod ∩ LVec) | ||
Theorem | nmfval 22393* | The value of the norm function. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝑋 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐷 = (dist‘𝑊) ⇒ ⊢ 𝑁 = (𝑥 ∈ 𝑋 ↦ (𝑥𝐷 0 )) | ||
Theorem | nmval 22394 | The value of the norm function. Problem 1 of [Kreyszig] p. 63. (Contributed by NM, 4-Dec-2006.) (Revised by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝑋 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐷 = (dist‘𝑊) ⇒ ⊢ (𝐴 ∈ 𝑋 → (𝑁‘𝐴) = (𝐴𝐷 0 )) | ||
Theorem | nmfval2 22395* | The value of the norm function using a restricted metric. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝑋 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐷 = (dist‘𝑊) & ⊢ 𝐸 = (𝐷 ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝑊 ∈ Grp → 𝑁 = (𝑥 ∈ 𝑋 ↦ (𝑥𝐸 0 ))) | ||
Theorem | nmval2 22396 | The value of the norm function using a restricted metric. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝑋 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐷 = (dist‘𝑊) & ⊢ 𝐸 = (𝐷 ↾ (𝑋 × 𝑋)) ⇒ ⊢ ((𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) = (𝐴𝐸 0 )) | ||
Theorem | nmf2 22397 | The norm is a function from the base set into the reals. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝑋 = (Base‘𝑊) & ⊢ 𝐷 = (dist‘𝑊) & ⊢ 𝐸 = (𝐷 ↾ (𝑋 × 𝑋)) ⇒ ⊢ ((𝑊 ∈ Grp ∧ 𝐸 ∈ (Met‘𝑋)) → 𝑁:𝑋⟶ℝ) | ||
Theorem | nmpropd 22398 | Weak property deduction for a norm. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿)) & ⊢ (𝜑 → (+g‘𝐾) = (+g‘𝐿)) & ⊢ (𝜑 → (dist‘𝐾) = (dist‘𝐿)) ⇒ ⊢ (𝜑 → (norm‘𝐾) = (norm‘𝐿)) | ||
Theorem | nmpropd2 22399* | Strong property deduction for a norm. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → 𝐾 ∈ Grp) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵))) ⇒ ⊢ (𝜑 → (norm‘𝐾) = (norm‘𝐿)) | ||
Theorem | isngp 22400 | The property of being a normed group. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑁 = (norm‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) ⇒ ⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ (𝑁 ∘ − ) ⊆ 𝐷)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |