HomeTheorem List (p. 245 of 482)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 245 of 482) | < 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-30715) |
Hilbert Space Explorer
(30716-32238) |
Users' Mathboxes
(32239-48161) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | blcld 24401* | 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 24402* | 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 24403 | 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 24404* | 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 24405* | 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 24406* | 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 24407* | Lemma for metss2 24408. (Contributed by Mario Carneiro, 14-Sep-2015.) |
| ⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐶 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐶𝑦) ≤ (𝑅 · (𝑥𝐷𝑦))) ⇒ ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) → (𝑥(ball‘𝐷)(𝑆 / 𝑅)) ⊆ (𝑥(ball‘𝐶)𝑆)) | ||
| Theorem | metss2 24408* | 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 24409* | 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 24410* | Value of the standard bounded metric. (Contributed by Mario Carneiro, 26-Aug-2015.) |
| ⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ if((𝑥𝐶𝑦) ≤ 𝑅, (𝑥𝐶𝑦), 𝑅)) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = if((𝐴𝐶𝐵) ≤ 𝑅, (𝐴𝐶𝐵), 𝑅)) | ||
| Theorem | stdbdxmet 24411* | 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 24412* | 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 24413* | 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 24414* | 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 24415* | 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 24416 | 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 24417 | The topology generated by a metric space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
| ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ 1stω) | ||
| Theorem | met2ndci 24418 | 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 24419* | 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 24420 | 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 24421 | The restriction of a metric space is a metric space. (Contributed by Mario Carneiro, 24-Aug-2015.) |
| ⊢ ((𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉) → (𝐾 ↾s 𝐴) ∈ ∞MetSp) | ||
| Theorem | ressms 24422 | The restriction of a metric space is a metric space. (Contributed by Mario Carneiro, 24-Aug-2015.) |
| ⊢ ((𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉) → (𝐾 ↾s 𝐴) ∈ MetSp) | ||
| Theorem | prdsmslem1 24423 | Lemma for prdsms 24427. 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 24424 | Lemma for prdsms 24427. 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 24425* | Lemma for prdsxms 24426. 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 24426 | 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 24427 | 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 24428 | A power of an extended metric space is an extended metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| ⊢ 𝑌 = (𝑅 ↑s 𝐼) ⇒ ⊢ ((𝑅 ∈ ∞MetSp ∧ 𝐼 ∈ Fin) → 𝑌 ∈ ∞MetSp) | ||
| Theorem | pwsms 24429 | A power of a metric space is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| ⊢ 𝑌 = (𝑅 ↑s 𝐼) ⇒ ⊢ ((𝑅 ∈ MetSp ∧ 𝐼 ∈ Fin) → 𝑌 ∈ MetSp) | ||
| Theorem | xpsxms 24430 | A binary product of metric spaces is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| ⊢ 𝑇 = (𝑅 ×s 𝑆) ⇒ ⊢ ((𝑅 ∈ ∞MetSp ∧ 𝑆 ∈ ∞MetSp) → 𝑇 ∈ ∞MetSp) | ||
| Theorem | xpsms 24431 | A binary product of metric spaces is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| ⊢ 𝑇 = (𝑅 ×s 𝑆) ⇒ ⊢ ((𝑅 ∈ MetSp ∧ 𝑆 ∈ MetSp) → 𝑇 ∈ MetSp) | ||
| Theorem | tmsxps 24432 | 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 24433 | 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 24434 | Value of the product of two metrics. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| ⊢ 𝑃 = (dist‘((toMetSp‘𝑀) ×s (toMetSp‘𝑁))) & ⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌)) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑌) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑌) ⇒ ⊢ (𝜑 → (⟨𝐴, 𝐵⟩𝑃⟨𝐶, 𝐷⟩) = sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < )) | ||
| Theorem | tmsxpsval2 24435 | Value of the product of two metrics. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| ⊢ 𝑃 = (dist‘((toMetSp‘𝑀) ×s (toMetSp‘𝑁))) & ⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌)) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑌) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑌) ⇒ ⊢ (𝜑 → (⟨𝐴, 𝐵⟩𝑃⟨𝐶, 𝐷⟩) = if((𝐴𝑀𝐶) ≤ (𝐵𝑁𝐷), (𝐵𝑁𝐷), (𝐴𝑀𝐶))) | ||
| Theorem | metcnp3 24436* | 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 24437* | 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 24438* | Two ways to say a mapping from metric 𝐶 to metric 𝐷 is continuous at point 𝑃. The distance arguments are swapped compared to metcnp 24437 (and Munkres' metcn 24439) for compatibility with df-lm 23120. 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 24439* | 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 24440* | Epsilon-delta property of a continuous metric space function, with function arguments as in metcnp 24437. (Contributed by NM, 17-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
| ⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷) ⇒ ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌)) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐴 ∈ ℝ+)) → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝑋 ((𝑃𝐶𝑦) < 𝑥 → ((𝐹‘𝑃)𝐷(𝐹‘𝑦)) < 𝐴)) | ||
| Theorem | metcnpi2 24441* | Epsilon-delta property of a continuous metric space function, with swapped distance function arguments as in metcnp2 24438. (Contributed by NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
| ⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷) ⇒ ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌)) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐴 ∈ ℝ+)) → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝑋 ((𝑦𝐶𝑃) < 𝑥 → ((𝐹‘𝑦)𝐷(𝐹‘𝑃)) < 𝐴)) | ||
| Theorem | metcnpi3 24442* | Epsilon-delta property of a metric space function continuous at 𝑃. A variation of metcnpi2 24441 with non-strict ordering. (Contributed by NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
| ⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷) ⇒ ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌)) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐴 ∈ ℝ+)) → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝑋 ((𝑦𝐶𝑃) ≤ 𝑥 → ((𝐹‘𝑦)𝐷(𝐹‘𝑃)) ≤ 𝐴)) | ||
| Theorem | txmetcnp 24443* | 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 24444* | 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 24445* | 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 24446* | 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 24447* | 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 24448* | 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 24449* | 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 24450* | 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.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
| ⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))) ⇒ ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) → ( I ↾ 𝑋) ⊆ 𝐴) | ||
| Theorem | metustsym 24451* | 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 24452* | 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 24453* | The filter base generated by a metric 𝐷. (Contributed by Thierry Arnoux, 26-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
| ⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))) ⇒ ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → 𝐹 ∈ (fBas‘(𝑋 × 𝑋))) | ||
| Theorem | metust 24454* | 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 24455* | 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 25180. (Contributed by Thierry Arnoux, 29-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
| ⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))) ⇒ ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹)) ↔ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))) | ||
| Theorem | metuust 24456 | 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 24457* | 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 25180. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
| ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐶 ∈ (CauFilu‘(metUnif‘𝐷)) ↔ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))) | ||
| Theorem | blval2 24458 | 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 24459 | 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 24460* | 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 24461* | 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 24462* | 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 24463 | 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 24464 | 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 24465 | 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 24466 | 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 24467* | Uniform continuity in metric spaces. Compare the order of the quantifiers with metcn 24439. (Contributed by Thierry Arnoux, 26-Jan-2018.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
| ⊢ 𝑈 = (metUnif‘𝐶) & ⊢ 𝑉 = (metUnif‘𝐷) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝑌 ≠ ∅) & ⊢ (𝜑 → 𝐶 ∈ (PsMet‘𝑋)) & ⊢ (𝜑 → 𝐷 ∈ (PsMet‘𝑌)) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑑 ∈ ℝ+ ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐶𝑦) < 𝑐 → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) < 𝑑)))) | ||
| Theorem | dscmet 24468* | 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 24469* | 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 24470* | 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 24471 | An absolute value 𝐹 generates a metric defined by 𝑑(𝑥, 𝑦) = 𝐹(𝑥 − 𝑦), analogously to cnmet 24675. (In fact, the ring structure is not needed at all; the group properties abveq0 20695 and abvtri 20699, abvneg 20703 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 24485: (𝑁‘𝐴) = (𝐴𝐷 0 )). By this definition, the norm function 𝑁 is actually a norm (satisfying the properties: being a function into the reals; subadditivity/triangle inequality (𝑁‘(𝑥 + 𝑦)) ≤ ((𝑁‘𝑥) + (𝑁‘𝑦)); 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 𝑠 ∈ ℤ, 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., (𝑁‘( − 𝑥) = 𝑁‘𝑥). The definition df-ngp 24479 of a group norm follows the second aproach, see nminv 24517.] and positive definiteness/point-separation ((𝑁‘𝑥) = 0 ↔ 𝑥 = 0)) if the structure is a metric space with a right-translation-invariant metric (see nmf 24511, nmtri 24522, nmvs 24580 and nmeq0 24514). An alternate definition of a normed group (i.e., a group equipped with a norm) not using the properties of a metric space is given by Theorem tngngp3 24560. The norm can be expressed as the distance to zero (nmfval 24484), so in a structure with a zero (a "pointed set", for instance a monoid or a group), the norm can be expressed as the distance restricted to the elements of the base set to zero (nmfval0 24486). Usually, however, the norm of a normed structure is given, and the corresponding metric ("induced metric") is defined as the distance function based on the norm (the distance 𝐷 between two elements is the norm 𝑁 of their difference, see ngpds 24500: (𝐴𝐷𝐵) = (𝑁‘(𝐴 − 𝐵))). 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 for the difference of two elements to make sense) corresponding to a given norm as explained above: (dist‘𝑇) = (𝑁 ∘ − ), see also tngds 24551. By this, the enhanced structure becomes a normed structure if the induced metric is in fact a metric (see tngngp2 24556) or a norm (see tngngpd 24557). If the norm is derived from a given metric, as done with df-nm 24478, the induced metric is the original metric restricted to the base set: (dist‘𝑇) = ((dist‘𝐺) ↾ (𝑋 × 𝑋)), see nrmtngdist 24561, and the norm remains the same: (norm‘𝑇) = (norm‘𝐺), see nrmtngnrm 24562. | ||
| Syntax | cnm 24472 | Norm of a normed ring. |
| class norm | ||
| Syntax | cngp 24473 | The class of all normed groups. |
| class NrmGrp | ||
| Syntax | ctng 24474 | Make a normed group from a norm and a group. |
| class toNrmGrp | ||
| Syntax | cnrg 24475 | Normed ring. |
| class NrmRing | ||
| Syntax | cnlm 24476 | Normed module. |
| class NrmMod | ||
| Syntax | cnvc 24477 | Normed vector space. |
| class NrmVec | ||
| Definition | df-nm 24478* | 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 24479 | 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 24480* | 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 24481 | 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 24482* | 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 24483 | 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 24484* | The value of the norm function as the distance to zero. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| ⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝑋 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐷 = (dist‘𝑊) ⇒ ⊢ 𝑁 = (𝑥 ∈ 𝑋 ↦ (𝑥𝐷 0 )) | ||
| Theorem | nmval 24485 | The value of the norm as the distance to zero. 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 | nmfval0 24486* | The value of the norm function on a structure containing a zero as the distance restricted to the elements of the base set to zero. Examples of structures containing a "zero" are groups (see nmfval2 24487 proved from this theorem and grpidcl 18913) or more generally monoids (see mndidcl 18700), or pointed sets). (Contributed by Mario Carneiro, 2-Oct-2015.) Extract this result from the proof of nmfval2 24487. (Revised by BJ, 27-Aug-2024.) |
| ⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝑋 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐷 = (dist‘𝑊) & ⊢ 𝐸 = (𝐷 ↾ (𝑋 × 𝑋)) ⇒ ⊢ ( 0 ∈ 𝑋 → 𝑁 = (𝑥 ∈ 𝑋 ↦ (𝑥𝐸 0 ))) | ||
| Theorem | nmfval2 24487* | The value of the norm function on a group as the distance restricted to the elements of the base set to zero. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| ⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝑋 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐷 = (dist‘𝑊) & ⊢ 𝐸 = (𝐷 ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝑊 ∈ Grp → 𝑁 = (𝑥 ∈ 𝑋 ↦ (𝑥𝐸 0 ))) | ||
| Theorem | nmval2 24488 | The value of the norm on a group as the distance restricted to the elements of the base set to zero. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| ⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝑋 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝐷 = (dist‘𝑊) & ⊢ 𝐸 = (𝐷 ↾ (𝑋 × 𝑋)) ⇒ ⊢ ((𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) = (𝐴𝐸 0 )) | ||
| Theorem | nmf2 24489 | The norm on a metric group is a function from the base set into the reals. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| ⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝑋 = (Base‘𝑊) & ⊢ 𝐷 = (dist‘𝑊) & ⊢ 𝐸 = (𝐷 ↾ (𝑋 × 𝑋)) ⇒ ⊢ ((𝑊 ∈ Grp ∧ 𝐸 ∈ (Met‘𝑋)) → 𝑁:𝑋⟶ℝ) | ||
| Theorem | nmpropd 24490 | Weak property deduction for a norm. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿)) & ⊢ (𝜑 → (+g‘𝐾) = (+g‘𝐿)) & ⊢ (𝜑 → (dist‘𝐾) = (dist‘𝐿)) ⇒ ⊢ (𝜑 → (norm‘𝐾) = (norm‘𝐿)) | ||
| Theorem | nmpropd2 24491* | Strong property deduction for a norm. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → 𝐾 ∈ Grp) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵))) ⇒ ⊢ (𝜑 → (norm‘𝐾) = (norm‘𝐿)) | ||
| Theorem | isngp 24492 | The property of being a normed group. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| ⊢ 𝑁 = (norm‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) ⇒ ⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ (𝑁 ∘ − ) ⊆ 𝐷)) | ||
| Theorem | isngp2 24493 | The property of being a normed group. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| ⊢ 𝑁 = (norm‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = (𝐷 ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ (𝑁 ∘ − ) = 𝐸)) | ||
| Theorem | isngp3 24494* | The property of being a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑁 = (norm‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) & ⊢ 𝑋 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ NrmGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ MetSp ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐷𝑦) = (𝑁‘(𝑥 − 𝑦)))) | ||
| Theorem | ngpgrp 24495 | A normed group is a group. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| ⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ Grp) | ||
| Theorem | ngpms 24496 | A normed group is a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| ⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ MetSp) | ||
| Theorem | ngpxms 24497 | A normed group is an extended metric space. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| ⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ ∞MetSp) | ||
| Theorem | ngptps 24498 | A normed group is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| ⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ TopSp) | ||
| Theorem | ngpmet 24499 | The (induced) metric of a normed group is a metric. Part of Definition 2.2-1 of [Kreyszig] p. 58. (Contributed by NM, 4-Dec-2006.) (Revised by AV, 14-Oct-2021.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐷 = ((dist‘𝐺) ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝐺 ∈ NrmGrp → 𝐷 ∈ (Met‘𝑋)) | ||
| Theorem | ngpds 24500 | Value of the distance function in terms of the norm of a normed group. Equation 1 of [Kreyszig] p. 59. (Contributed by NM, 28-Nov-2006.) (Revised by Mario Carneiro, 2-Oct-2015.) |
| ⊢ 𝑁 = (norm‘𝐺) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝐷 = (dist‘𝐺) ⇒ ⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝑁‘(𝐴 − 𝐵))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |