![]() |
Metamath
Proof Explorer Theorem List (p. 228 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-28347) |
![]() (28348-29872) |
![]() (29873-43639) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | imasf1obl 22701 | The image of a metric space ball. (Contributed by Mario Carneiro, 28-Aug-2015.) |
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝐵) & ⊢ (𝜑 → 𝑅 ∈ 𝑍) & ⊢ 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉)) & ⊢ 𝐷 = (dist‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ (∞Met‘𝑉)) & ⊢ (𝜑 → 𝑃 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ ℝ*) ⇒ ⊢ (𝜑 → ((𝐹‘𝑃)(ball‘𝐷)𝑆) = (𝐹 “ (𝑃(ball‘𝐸)𝑆))) | ||
Theorem | imasf1oxms 22702 | The image of a metric space is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝐵) & ⊢ (𝜑 → 𝑅 ∈ ∞MetSp) ⇒ ⊢ (𝜑 → 𝑈 ∈ ∞MetSp) | ||
Theorem | imasf1oms 22703 | The image of a metric space is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝐵) & ⊢ (𝜑 → 𝑅 ∈ MetSp) ⇒ ⊢ (𝜑 → 𝑈 ∈ MetSp) | ||
Theorem | prdsbl 22704* |
A ball in the product metric for finite index set is the Cartesian
product of balls in all coordinates. For infinite index set this is no
longer true; instead the correct statement is that a *closed ball* is
the product of closed balls in each coordinate (where closed ball means
a set of the form in blcld 22718) - for a counterexample the point 𝑝 in
ℝ↑ℕ whose 𝑛-th
coordinate is 1 − 1 / 𝑛 is in
X𝑛 ∈ ℕball(0, 1) but is not
in the 1-ball of the
product (since 𝑑(0, 𝑝) = 1).
The last assumption, 0 < 𝐴, is needed only in the case 𝐼 = ∅, when the right side evaluates to {∅} and the left evaluates to ∅ if 𝐴 ≤ 0 and {∅} if 0 < 𝐴. (Contributed by Mario Carneiro, 28-Aug-2015.) |
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ 𝑉 = (Base‘𝑅) & ⊢ 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉)) & ⊢ 𝐷 = (dist‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ 𝑍) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉)) & ⊢ (𝜑 → 𝑃 ∈ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ ℝ*) & ⊢ (𝜑 → 0 < 𝐴) ⇒ ⊢ (𝜑 → (𝑃(ball‘𝐷)𝐴) = X𝑥 ∈ 𝐼 ((𝑃‘𝑥)(ball‘𝐸)𝐴)) | ||
Theorem | mopni 22705* | An open set of a metric space includes a ball around each of its points. (Contributed by NM, 3-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝐽 ∧ 𝑃 ∈ 𝐴) → ∃𝑥 ∈ ran (ball‘𝐷)(𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴)) | ||
Theorem | mopni2 22706* | An open set of a metric space includes a ball around each of its points. (Contributed by NM, 2-May-2007.) (Revised by Mario Carneiro, 12-Nov-2013.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝐽 ∧ 𝑃 ∈ 𝐴) → ∃𝑥 ∈ ℝ+ (𝑃(ball‘𝐷)𝑥) ⊆ 𝐴) | ||
Theorem | mopni3 22707* | An open set of a metric space includes an arbitrarily small ball around each of its points. (Contributed by NM, 20-Sep-2007.) (Revised by Mario Carneiro, 12-Nov-2013.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝐽 ∧ 𝑃 ∈ 𝐴) ∧ 𝑅 ∈ ℝ+) → ∃𝑥 ∈ ℝ+ (𝑥 < 𝑅 ∧ (𝑃(ball‘𝐷)𝑥) ⊆ 𝐴)) | ||
Theorem | blssopn 22708 | The balls of a metric space are open sets. (Contributed by NM, 12-Sep-2006.) (Revised by Mario Carneiro, 23-Dec-2013.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → ran (ball‘𝐷) ⊆ 𝐽) | ||
Theorem | unimopn 22709 | 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 22710 | 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 22711 | 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 22712 | A ball of a metric space is an open set. (Contributed by NM, 12-Sep-2006.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ ran (ball‘𝐷)) → 𝐵 ∈ 𝐽) | ||
Theorem | blopn 22713 | 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 22714* | 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 22715 | 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 22716* | 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 22717* | A smaller closed ball is contained in a larger open ball. (Contributed by Mario Carneiro, 10-Jan-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝑆 = {𝑧 ∈ 𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅} ⇒ ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑇 ∈ ℝ* ∧ 𝑅 < 𝑇)) → 𝑆 ⊆ (𝑃(ball‘𝐷)𝑇)) | ||
Theorem | blcld 22718* | 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 22719* | 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 22720 | 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 22721* | 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 22722* | 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 22723* | 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 22724* | Lemma for metss2 22725. (Contributed by Mario Carneiro, 14-Sep-2015.) |
⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐶 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐶𝑦) ≤ (𝑅 · (𝑥𝐷𝑦))) ⇒ ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) → (𝑥(ball‘𝐷)(𝑆 / 𝑅)) ⊆ (𝑥(ball‘𝐶)𝑆)) | ||
Theorem | metss2 22725* | 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 22726* | 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 22727* | Value of the standard bounded metric. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ if((𝑥𝐶𝑦) ≤ 𝑅, (𝑥𝐶𝑦), 𝑅)) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = if((𝐴𝐶𝐵) ≤ 𝑅, (𝐴𝐶𝐵), 𝑅)) | ||
Theorem | stdbdxmet 22728* | 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 22729* | 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 22730* | 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 22731* | 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 22732* | 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 22733 | 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 22734 | The topology generated by a metric space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ 1st𝜔) | ||
Theorem | met2ndci 22735 | 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 22736* | 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 22737 | 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 22738 | The restriction of a metric space is a metric space. (Contributed by Mario Carneiro, 24-Aug-2015.) |
⊢ ((𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉) → (𝐾 ↾s 𝐴) ∈ ∞MetSp) | ||
Theorem | ressms 22739 | The restriction of a metric space is a metric space. (Contributed by Mario Carneiro, 24-Aug-2015.) |
⊢ ((𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉) → (𝐾 ↾s 𝐴) ∈ MetSp) | ||
Theorem | prdsmslem1 22740 | Lemma for prdsms 22744. 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 22741 | Lemma for prdsms 22744. 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 22742* | Lemma for prdsxms 22743. 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 22743 | 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 22744 | 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 22745 | 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 22746 | 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 22747 | A binary product of metric spaces is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) ⇒ ⊢ ((𝑅 ∈ ∞MetSp ∧ 𝑆 ∈ ∞MetSp) → 𝑇 ∈ ∞MetSp) | ||
Theorem | xpsms 22748 | A binary product of metric spaces is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) ⇒ ⊢ ((𝑅 ∈ MetSp ∧ 𝑆 ∈ MetSp) → 𝑇 ∈ MetSp) | ||
Theorem | tmsxps 22749 | 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 22750 | 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 22751 | Value of the product of two metrics. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ 𝑃 = (dist‘((toMetSp‘𝑀) ×s (toMetSp‘𝑁))) & ⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌)) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑌) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑌) ⇒ ⊢ (𝜑 → (〈𝐴, 𝐵〉𝑃〈𝐶, 𝐷〉) = sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < )) | ||
Theorem | tmsxpsval2 22752 | Value of the product of two metrics. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ 𝑃 = (dist‘((toMetSp‘𝑀) ×s (toMetSp‘𝑁))) & ⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌)) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑌) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑌) ⇒ ⊢ (𝜑 → (〈𝐴, 𝐵〉𝑃〈𝐶, 𝐷〉) = if((𝐴𝑀𝐶) ≤ (𝐵𝑁𝐷), (𝐵𝑁𝐷), (𝐴𝑀𝐶))) | ||
Theorem | metcnp3 22753* | 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 22754* | 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 22755* | Two ways to say a mapping from metric 𝐶 to metric 𝐷 is continuous at point 𝑃. The distance arguments are swapped compared to metcnp 22754 (and Munkres' metcn 22756) for compatibility with df-lm 21441. 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 22756* | 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 22757* | Epsilon-delta property of a continuous metric space function, with function arguments as in metcnp 22754. (Contributed by NM, 17-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷) ⇒ ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌)) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐴 ∈ ℝ+)) → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝑋 ((𝑃𝐶𝑦) < 𝑥 → ((𝐹‘𝑃)𝐷(𝐹‘𝑦)) < 𝐴)) | ||
Theorem | metcnpi2 22758* | Epsilon-delta property of a continuous metric space function, with swapped distance function arguments as in metcnp2 22755. (Contributed by NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷) ⇒ ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌)) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐴 ∈ ℝ+)) → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝑋 ((𝑦𝐶𝑃) < 𝑥 → ((𝐹‘𝑦)𝐷(𝐹‘𝑃)) < 𝐴)) | ||
Theorem | metcnpi3 22759* | Epsilon-delta property of a metric space function continuous at 𝑃. A variation of metcnpi2 22758 with non-strict ordering. (Contributed by NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷) ⇒ ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌)) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐴 ∈ ℝ+)) → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝑋 ((𝑦𝐶𝑃) ≤ 𝑥 → ((𝐹‘𝑦)𝐷(𝐹‘𝑃)) ≤ 𝐴)) | ||
Theorem | txmetcnp 22760* | 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 22761* | 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 22762* | 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 22763* | 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 22764* | 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 22765* | 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 22766* | 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 22767* | 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 22768* | 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 22769* | 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 22770* | 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 22771* | 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 22772* | 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 23471. (Contributed by Thierry Arnoux, 29-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎))) ⇒ ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹)) ↔ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))) | ||
Theorem | metuust 22773 | 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 22774* | 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 23471. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐶 ∈ (CauFilu‘(metUnif‘𝐷)) ↔ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))) | ||
Theorem | blval2 22775 | 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 22776 | 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 22777* | 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 22778* | 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 22779* | 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 22780 | 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 22781 | 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 22782 | 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 22783 | 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 22784* | Uniform continuity in metric spaces. Compare the order of the quantifiers with metcn 22756. (Contributed by Thierry Arnoux, 26-Jan-2018.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
⊢ 𝑈 = (metUnif‘𝐶) & ⊢ 𝑉 = (metUnif‘𝐷) & ⊢ (𝜑 → 𝑋 ≠ ∅) & ⊢ (𝜑 → 𝑌 ≠ ∅) & ⊢ (𝜑 → 𝐶 ∈ (PsMet‘𝑋)) & ⊢ (𝜑 → 𝐷 ∈ (PsMet‘𝑌)) ⇒ ⊢ (𝜑 → (𝐹 ∈ (𝑈 Cnu𝑉) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑑 ∈ ℝ+ ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐶𝑦) < 𝑐 → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) < 𝑑)))) | ||
Theorem | dscmet 22785* | 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 22786* | 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 22787* | 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 22788 | An absolute value 𝐹 generates a metric defined by 𝑑(𝑥, 𝑦) = 𝐹(𝑥 − 𝑦), analogously to cnmet 22983. (In fact, the ring structure is not needed at all; the group properties abveq0 19218 and abvtri 19222, abvneg 19226 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 22802: (𝑁‘𝐴) = (𝐴𝐷 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 22796 of a group norm follows the second aproach, see nminv 22833.] 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 22827, nmtri 22838, nmvs 22888 and nmeq0 22830). 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 22868. 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 22803. 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 22816: (𝐴𝐷𝐵) = (𝑁‘(𝐴 − 𝐵))). 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 22860. By this, the enhanced structure becomes a normed structure if the induced metric is in fact a metric (see tngngp2 22864) resp. if the norm is in fact a norm (see tngngpd 22865). If the norm is derived from a given metric, as done with df-nm 22795, the induced metric is the original metric restricted to the base set: (dist‘𝑇) = ((dist‘𝐺) ↾ (𝑋 × 𝑋)), see nrmtngdist 22869, and the norm remains the same: (norm‘𝑇) = (norm‘𝐺), see nrmtngnrm 22870. | ||
Syntax | cnm 22789 | Norm of a normed ring. |
class norm | ||
Syntax | cngp 22790 | The class of all normed groups. |
class NrmGrp | ||
Syntax | ctng 22791 | Make a normed group from a norm and a group. |
class toNrmGrp | ||
Syntax | cnrg 22792 | Normed ring. |
class NrmRing | ||
Syntax | cnlm 22793 | Normed module. |
class NrmMod | ||
Syntax | cnvc 22794 | Normed vector space. |
class NrmVec | ||
Definition | df-nm 22795* | 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 22796 | 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 22797* | 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 22798 | 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 22799* | 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 22800 | A normed vector space is a normed module which is also a vector space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ NrmVec = (NrmMod ∩ LVec) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |