| Metamath
Proof Explorer Theorem List (p. 245 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | elbl3ps 24401 | Membership in a ball, with reversed distance function arguments. (Contributed by NM, 10-Nov-2007.) |
| ⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝐴𝐷𝑃) < 𝑅)) | ||
| Theorem | elbl3 24402 | Membership in a ball, with reversed distance function arguments. (Contributed by NM, 10-Nov-2007.) |
| ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝐴𝐷𝑃) < 𝑅)) | ||
| Theorem | blcomps 24403 | Commute the arguments to the ball function. (Contributed by Mario Carneiro, 22-Jan-2014.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
| ⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ 𝑃 ∈ (𝐴(ball‘𝐷)𝑅))) | ||
| Theorem | blcom 24404 | Commute the arguments to the ball function. (Contributed by Mario Carneiro, 22-Jan-2014.) |
| ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ 𝑃 ∈ (𝐴(ball‘𝐷)𝑅))) | ||
| Theorem | xblpnfps 24405 | The infinity ball in an extended metric is the set of all points that are a finite distance from the center. (Contributed by Mario Carneiro, 23-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
| ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝐴 ∈ (𝑃(ball‘𝐷)+∞) ↔ (𝐴 ∈ 𝑋 ∧ (𝑃𝐷𝐴) ∈ ℝ))) | ||
| Theorem | xblpnf 24406 | The infinity ball in an extended metric is the set of all points that are a finite distance from the center. (Contributed by Mario Carneiro, 23-Aug-2015.) |
| ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝐴 ∈ (𝑃(ball‘𝐷)+∞) ↔ (𝐴 ∈ 𝑋 ∧ (𝑃𝐷𝐴) ∈ ℝ))) | ||
| Theorem | blpnf 24407 | The infinity ball in a standard metric is just the whole space. (Contributed by Mario Carneiro, 23-Aug-2015.) |
| ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝑃(ball‘𝐷)+∞) = 𝑋) | ||
| Theorem | bldisj 24408 | Two balls are disjoint if the center-to-center distance is more than the sum of the radii. (Contributed by Mario Carneiro, 30-Dec-2013.) |
| ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ (𝑅 +𝑒 𝑆) ≤ (𝑃𝐷𝑄))) → ((𝑃(ball‘𝐷)𝑅) ∩ (𝑄(ball‘𝐷)𝑆)) = ∅) | ||
| Theorem | blgt0 24409 | A nonempty ball implies that the radius is positive. (Contributed by NM, 11-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.) |
| ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) ∧ 𝐴 ∈ (𝑃(ball‘𝐷)𝑅)) → 0 < 𝑅) | ||
| Theorem | bl2in 24410 | Two balls are disjoint if they don't overlap. (Contributed by NM, 11-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.) |
| ⊢ (((𝐷 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ ∧ 𝑅 ≤ ((𝑃𝐷𝑄) / 2))) → ((𝑃(ball‘𝐷)𝑅) ∩ (𝑄(ball‘𝐷)𝑅)) = ∅) | ||
| Theorem | xblss2ps 24411 | One ball is contained in another if the center-to-center distance is less than the difference of the radii. In this version of blss2 24414 for extended metrics, we have to assume the balls are a finite distance apart, or else 𝑃 will not even be in the infinity ball around 𝑄. (Contributed by Mario Carneiro, 23-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
| ⊢ (𝜑 → 𝐷 ∈ (PsMet‘𝑋)) & ⊢ (𝜑 → 𝑃 ∈ 𝑋) & ⊢ (𝜑 → 𝑄 ∈ 𝑋) & ⊢ (𝜑 → 𝑅 ∈ ℝ*) & ⊢ (𝜑 → 𝑆 ∈ ℝ*) & ⊢ (𝜑 → (𝑃𝐷𝑄) ∈ ℝ) & ⊢ (𝜑 → (𝑃𝐷𝑄) ≤ (𝑆 +𝑒 -𝑒𝑅)) ⇒ ⊢ (𝜑 → (𝑃(ball‘𝐷)𝑅) ⊆ (𝑄(ball‘𝐷)𝑆)) | ||
| Theorem | xblss2 24412 | One ball is contained in another if the center-to-center distance is less than the difference of the radii. In this version of blss2 24414 for extended metrics, we have to assume the balls are a finite distance apart, or else 𝑃 will not even be in the infinity ball around 𝑄. (Contributed by Mario Carneiro, 23-Aug-2015.) |
| ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑃 ∈ 𝑋) & ⊢ (𝜑 → 𝑄 ∈ 𝑋) & ⊢ (𝜑 → 𝑅 ∈ ℝ*) & ⊢ (𝜑 → 𝑆 ∈ ℝ*) & ⊢ (𝜑 → (𝑃𝐷𝑄) ∈ ℝ) & ⊢ (𝜑 → (𝑃𝐷𝑄) ≤ (𝑆 +𝑒 -𝑒𝑅)) ⇒ ⊢ (𝜑 → (𝑃(ball‘𝐷)𝑅) ⊆ (𝑄(ball‘𝐷)𝑆)) | ||
| Theorem | blss2ps 24413 | One ball is contained in another if the center-to-center distance is less than the difference of the radii. (Contributed by Mario Carneiro, 15-Jan-2014.) (Revised by Mario Carneiro, 23-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
| ⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ (𝑃𝐷𝑄) ≤ (𝑆 − 𝑅))) → (𝑃(ball‘𝐷)𝑅) ⊆ (𝑄(ball‘𝐷)𝑆)) | ||
| Theorem | blss2 24414 | One ball is contained in another if the center-to-center distance is less than the difference of the radii. (Contributed by Mario Carneiro, 15-Jan-2014.) (Revised by Mario Carneiro, 23-Aug-2015.) |
| ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) ∧ (𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ (𝑃𝐷𝑄) ≤ (𝑆 − 𝑅))) → (𝑃(ball‘𝐷)𝑅) ⊆ (𝑄(ball‘𝐷)𝑆)) | ||
| Theorem | blhalf 24415 | A ball of radius 𝑅 / 2 is contained in a ball of radius 𝑅 centered at any point inside the smaller ball. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 14-Jan-2014.) |
| ⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑌 ∈ 𝑋) ∧ (𝑅 ∈ ℝ ∧ 𝑍 ∈ (𝑌(ball‘𝑀)(𝑅 / 2)))) → (𝑌(ball‘𝑀)(𝑅 / 2)) ⊆ (𝑍(ball‘𝑀)𝑅)) | ||
| Theorem | blfps 24416 | Mapping of a ball. (Contributed by NM, 7-May-2007.) (Revised by Mario Carneiro, 23-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
| ⊢ (𝐷 ∈ (PsMet‘𝑋) → (ball‘𝐷):(𝑋 × ℝ*)⟶𝒫 𝑋) | ||
| Theorem | blf 24417 | Mapping of a ball. (Contributed by NM, 7-May-2007.) (Revised by Mario Carneiro, 23-Aug-2015.) |
| ⊢ (𝐷 ∈ (∞Met‘𝑋) → (ball‘𝐷):(𝑋 × ℝ*)⟶𝒫 𝑋) | ||
| Theorem | blrnps 24418* | Membership in the range of the ball function. Note that ran (ball‘𝐷) is the collection of all balls for metric 𝐷. (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
| ⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝐴 ∈ ran (ball‘𝐷) ↔ ∃𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ* 𝐴 = (𝑥(ball‘𝐷)𝑟))) | ||
| Theorem | blrn 24419* | Membership in the range of the ball function. Note that ran (ball‘𝐷) is the collection of all balls for metric 𝐷. (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| ⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐴 ∈ ran (ball‘𝐷) ↔ ∃𝑥 ∈ 𝑋 ∃𝑟 ∈ ℝ* 𝐴 = (𝑥(ball‘𝐷)𝑟))) | ||
| Theorem | xblcntrps 24420 | A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
| ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ (𝑅 ∈ ℝ* ∧ 0 < 𝑅)) → 𝑃 ∈ (𝑃(ball‘𝐷)𝑅)) | ||
| Theorem | xblcntr 24421 | A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ (𝑅 ∈ ℝ* ∧ 0 < 𝑅)) → 𝑃 ∈ (𝑃(ball‘𝐷)𝑅)) | ||
| Theorem | blcntrps 24422 | A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
| ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → 𝑃 ∈ (𝑃(ball‘𝐷)𝑅)) | ||
| Theorem | blcntr 24423 | A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → 𝑃 ∈ (𝑃(ball‘𝐷)𝑅)) | ||
| Theorem | xbln0 24424 | A ball is nonempty iff the radius is positive. (Contributed by Mario Carneiro, 23-Aug-2015.) |
| ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → ((𝑃(ball‘𝐷)𝑅) ≠ ∅ ↔ 0 < 𝑅)) | ||
| Theorem | bln0 24425 | A ball is not empty. (Contributed by NM, 6-Oct-2007.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → (𝑃(ball‘𝐷)𝑅) ≠ ∅) | ||
| Theorem | blelrnps 24426 | A ball belongs to the set of balls of a metric space. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
| ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) ∈ ran (ball‘𝐷)) | ||
| Theorem | blelrn 24427 | A ball belongs to the set of balls of a metric space. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) ∈ ran (ball‘𝐷)) | ||
| Theorem | blssm 24428 | A ball is a subset of the base set of a metric space. (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) ⊆ 𝑋) | ||
| Theorem | unirnblps 24429 | The union of the set of balls of a metric space is its base set. (Contributed by NM, 12-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
| ⊢ (𝐷 ∈ (PsMet‘𝑋) → ∪ ran (ball‘𝐷) = 𝑋) | ||
| Theorem | unirnbl 24430 | The union of the set of balls of a metric space is its base set. (Contributed by NM, 12-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| ⊢ (𝐷 ∈ (∞Met‘𝑋) → ∪ ran (ball‘𝐷) = 𝑋) | ||
| Theorem | blin 24431 | The intersection of two balls with the same center is the smaller of them. (Contributed by NM, 1-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*)) → ((𝑃(ball‘𝐷)𝑅) ∩ (𝑃(ball‘𝐷)𝑆)) = (𝑃(ball‘𝐷)if(𝑅 ≤ 𝑆, 𝑅, 𝑆))) | ||
| Theorem | ssblps 24432 | The size of a ball increases monotonically with its radius. (Contributed by NM, 20-Sep-2007.) (Revised by Mario Carneiro, 24-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
| ⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*) ∧ 𝑅 ≤ 𝑆) → (𝑃(ball‘𝐷)𝑅) ⊆ (𝑃(ball‘𝐷)𝑆)) | ||
| Theorem | ssbl 24433 | The size of a ball increases monotonically with its radius. (Contributed by NM, 20-Sep-2007.) (Revised by Mario Carneiro, 24-Aug-2015.) |
| ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ*) ∧ 𝑅 ≤ 𝑆) → (𝑃(ball‘𝐷)𝑅) ⊆ (𝑃(ball‘𝐷)𝑆)) | ||
| Theorem | blssps 24434* | Any point 𝑃 in a ball 𝐵 can be centered in another ball that is a subset of 𝐵. (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 24-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
| ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐵 ∈ ran (ball‘𝐷) ∧ 𝑃 ∈ 𝐵) → ∃𝑥 ∈ ℝ+ (𝑃(ball‘𝐷)𝑥) ⊆ 𝐵) | ||
| Theorem | blss 24435* | Any point 𝑃 in a ball 𝐵 can be centered in another ball that is a subset of 𝐵. (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 24-Aug-2015.) |
| ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ ran (ball‘𝐷) ∧ 𝑃 ∈ 𝐵) → ∃𝑥 ∈ ℝ+ (𝑃(ball‘𝐷)𝑥) ⊆ 𝐵) | ||
| Theorem | blssexps 24436* | Two ways to express the existence of a ball subset. (Contributed by NM, 5-May-2007.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
| ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋) → (∃𝑥 ∈ ran (ball‘𝐷)(𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴) ↔ ∃𝑟 ∈ ℝ+ (𝑃(ball‘𝐷)𝑟) ⊆ 𝐴)) | ||
| Theorem | blssex 24437* | Two ways to express the existence of a ball subset. (Contributed by NM, 5-May-2007.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → (∃𝑥 ∈ ran (ball‘𝐷)(𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴) ↔ ∃𝑟 ∈ ℝ+ (𝑃(ball‘𝐷)𝑟) ⊆ 𝐴)) | ||
| Theorem | ssblex 24438* | A nested ball exists whose radius is less than any desired amount. (Contributed by NM, 20-Sep-2007.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ+ ∧ 𝑆 ∈ ℝ+)) → ∃𝑥 ∈ ℝ+ (𝑥 < 𝑅 ∧ (𝑃(ball‘𝐷)𝑥) ⊆ (𝑃(ball‘𝐷)𝑆))) | ||
| Theorem | blin2 24439* | Given any two balls and a point in their intersection, there is a ball contained in the intersection with the given center point. (Contributed by Mario Carneiro, 12-Nov-2013.) |
| ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ (𝐵 ∩ 𝐶)) ∧ (𝐵 ∈ ran (ball‘𝐷) ∧ 𝐶 ∈ ran (ball‘𝐷))) → ∃𝑥 ∈ ℝ+ (𝑃(ball‘𝐷)𝑥) ⊆ (𝐵 ∩ 𝐶)) | ||
| Theorem | blbas 24440 | The balls of a metric space form a basis for a topology. (Contributed by NM, 12-Sep-2006.) (Revised by Mario Carneiro, 15-Jan-2014.) |
| ⊢ (𝐷 ∈ (∞Met‘𝑋) → ran (ball‘𝐷) ∈ TopBases) | ||
| Theorem | blres 24441 | A ball in a restricted metric space. (Contributed by Mario Carneiro, 5-Jan-2014.) |
| ⊢ 𝐶 = (𝐷 ↾ (𝑌 × 𝑌)) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ (𝑋 ∩ 𝑌) ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐶)𝑅) = ((𝑃(ball‘𝐷)𝑅) ∩ 𝑌)) | ||
| Theorem | xmeterval 24442 | Value of the "finitely separated" relation. (Contributed by Mario Carneiro, 24-Aug-2015.) |
| ⊢ ∼ = (◡𝐷 “ ℝ) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐴 ∼ 𝐵 ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (𝐴𝐷𝐵) ∈ ℝ))) | ||
| Theorem | xmeter 24443 | The "finitely separated" relation is an equivalence relation. (Contributed by Mario Carneiro, 24-Aug-2015.) |
| ⊢ ∼ = (◡𝐷 “ ℝ) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → ∼ Er 𝑋) | ||
| Theorem | xmetec 24444 | The equivalence classes under the finite separation equivalence relation are infinity balls. Thus, by erdisj 8799, infinity balls are either identical or disjoint, quite unlike the usual situation with Euclidean balls which admit many kinds of overlap. (Contributed by Mario Carneiro, 24-Aug-2015.) |
| ⊢ ∼ = (◡𝐷 “ ℝ) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → [𝑃] ∼ = (𝑃(ball‘𝐷)+∞)) | ||
| Theorem | blssec 24445 | A ball centered at 𝑃 is contained in the set of points finitely separated from 𝑃. This is just an application of ssbl 24433 to the infinity ball. (Contributed by Mario Carneiro, 24-Aug-2015.) |
| ⊢ ∼ = (◡𝐷 “ ℝ) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑆) ⊆ [𝑃] ∼ ) | ||
| Theorem | blpnfctr 24446 | The infinity ball in an extended metric acts like an ultrametric ball in that every point in the ball is also its center. (Contributed by Mario Carneiro, 21-Aug-2015.) |
| ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝐴 ∈ (𝑃(ball‘𝐷)+∞)) → (𝑃(ball‘𝐷)+∞) = (𝐴(ball‘𝐷)+∞)) | ||
| Theorem | xmetresbl 24447 | An extended metric restricted to any ball (in particular the infinity ball) is a proper metric. Together with xmetec 24444, this shows that any extended metric space can be "factored" into the disjoint union of proper metric spaces, with points in the same region measured by that region's metric, and points in different regions being distance +∞ from each other. (Contributed by Mario Carneiro, 23-Aug-2015.) |
| ⊢ 𝐵 = (𝑃(ball‘𝐷)𝑅) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝐷 ↾ (𝐵 × 𝐵)) ∈ (Met‘𝐵)) | ||
| Theorem | mopnval 24448 | An open set is a subset of a metric space which includes a ball around each of its points. Definition 1.3-2 of [Kreyszig] p. 18. The object (MetOpen‘𝐷) is the family of all open sets in the metric space determined by the metric 𝐷. By mopntop 24450, the open sets of a metric space form a topology 𝐽, whose base set is ∪ 𝐽 by mopnuni 24451. (Contributed by NM, 1-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 = (topGen‘ran (ball‘𝐷))) | ||
| Theorem | mopntopon 24449 | The set of open sets of a metric space 𝑋 is a topology on 𝑋. Remark in [Kreyszig] p. 19. This theorem connects the two concepts and makes available the theorems for topologies for use with metric spaces. (Contributed by Mario Carneiro, 24-Aug-2015.) |
| ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ (TopOn‘𝑋)) | ||
| Theorem | mopntop 24450 | The set of open sets of a metric space is a topology. (Contributed by NM, 28-Aug-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top) | ||
| Theorem | mopnuni 24451 | The union of all open sets in a metric space is its underlying set. (Contributed by NM, 4-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽) | ||
| Theorem | elmopn 24452* | The defining property of an open set of a metric space. (Contributed by NM, 1-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐴 ∈ 𝐽 ↔ (𝐴 ⊆ 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ran (ball‘𝐷)(𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴)))) | ||
| Theorem | mopnfss 24453 | The family of open sets of a metric space is a collection of subsets of the base set. (Contributed by NM, 3-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ⊆ 𝒫 𝑋) | ||
| Theorem | mopnm 24454 | The base set of a metric space is open. Part of Theorem T1 of [Kreyszig] p. 19. (Contributed by NM, 4-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 ∈ 𝐽) | ||
| Theorem | elmopn2 24455* | A defining property of an open set of a metric space. (Contributed by NM, 5-May-2007.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐴 ∈ 𝐽 ↔ (𝐴 ⊆ 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ℝ+ (𝑥(ball‘𝐷)𝑦) ⊆ 𝐴))) | ||
| Theorem | mopnss 24456 | An open set of a metric space is a subspace of its base set. (Contributed by NM, 3-Sep-2006.) |
| ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝑋) | ||
| Theorem | isxms 24457 | Express the predicate "〈𝑋, 𝐷〉 is an extended metric space" with underlying set 𝑋 and distance function 𝐷. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| ⊢ 𝐽 = (TopOpen‘𝐾) & ⊢ 𝑋 = (Base‘𝐾) & ⊢ 𝐷 = ((dist‘𝐾) ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝐾 ∈ ∞MetSp ↔ (𝐾 ∈ TopSp ∧ 𝐽 = (MetOpen‘𝐷))) | ||
| Theorem | isxms2 24458 | Express the predicate "〈𝑋, 𝐷〉 is an extended metric space" with underlying set 𝑋 and distance function 𝐷. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| ⊢ 𝐽 = (TopOpen‘𝐾) & ⊢ 𝑋 = (Base‘𝐾) & ⊢ 𝐷 = ((dist‘𝐾) ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝐾 ∈ ∞MetSp ↔ (𝐷 ∈ (∞Met‘𝑋) ∧ 𝐽 = (MetOpen‘𝐷))) | ||
| Theorem | isms 24459 | Express the predicate "〈𝑋, 𝐷〉 is a metric space" with underlying set 𝑋 and distance function 𝐷. (Contributed by NM, 27-Aug-2006.) (Revised by Mario Carneiro, 24-Aug-2015.) |
| ⊢ 𝐽 = (TopOpen‘𝐾) & ⊢ 𝑋 = (Base‘𝐾) & ⊢ 𝐷 = ((dist‘𝐾) ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝐾 ∈ MetSp ↔ (𝐾 ∈ ∞MetSp ∧ 𝐷 ∈ (Met‘𝑋))) | ||
| Theorem | isms2 24460 | Express the predicate "〈𝑋, 𝐷〉 is a metric space" with underlying set 𝑋 and distance function 𝐷. (Contributed by NM, 27-Aug-2006.) (Revised by Mario Carneiro, 24-Aug-2015.) |
| ⊢ 𝐽 = (TopOpen‘𝐾) & ⊢ 𝑋 = (Base‘𝐾) & ⊢ 𝐷 = ((dist‘𝐾) ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝐾 ∈ MetSp ↔ (𝐷 ∈ (Met‘𝑋) ∧ 𝐽 = (MetOpen‘𝐷))) | ||
| Theorem | xmstopn 24461 | The topology component of an extended metric space coincides with the topology generated by the metric component. (Contributed by Mario Carneiro, 26-Aug-2015.) |
| ⊢ 𝐽 = (TopOpen‘𝐾) & ⊢ 𝑋 = (Base‘𝐾) & ⊢ 𝐷 = ((dist‘𝐾) ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝐾 ∈ ∞MetSp → 𝐽 = (MetOpen‘𝐷)) | ||
| Theorem | mstopn 24462 | The topology component of a metric space coincides with the topology generated by the metric component. (Contributed by Mario Carneiro, 26-Aug-2015.) |
| ⊢ 𝐽 = (TopOpen‘𝐾) & ⊢ 𝑋 = (Base‘𝐾) & ⊢ 𝐷 = ((dist‘𝐾) ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝐾 ∈ MetSp → 𝐽 = (MetOpen‘𝐷)) | ||
| Theorem | xmstps 24463 | An extended metric space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.) |
| ⊢ (𝑀 ∈ ∞MetSp → 𝑀 ∈ TopSp) | ||
| Theorem | msxms 24464 | A metric space is an extended metric space. (Contributed by Mario Carneiro, 26-Aug-2015.) |
| ⊢ (𝑀 ∈ MetSp → 𝑀 ∈ ∞MetSp) | ||
| Theorem | mstps 24465 | A metric space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.) |
| ⊢ (𝑀 ∈ MetSp → 𝑀 ∈ TopSp) | ||
| Theorem | xmsxmet 24466 | The distance function, suitably truncated, is an extended metric on 𝑋. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| ⊢ 𝑋 = (Base‘𝑀) & ⊢ 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝑀 ∈ ∞MetSp → 𝐷 ∈ (∞Met‘𝑋)) | ||
| Theorem | msmet 24467 | The distance function, suitably truncated, is a metric on 𝑋. (Contributed by Mario Carneiro, 12-Nov-2013.) |
| ⊢ 𝑋 = (Base‘𝑀) & ⊢ 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝑀 ∈ MetSp → 𝐷 ∈ (Met‘𝑋)) | ||
| Theorem | msf 24468 | The distance function of a metric space is a function into the real numbers. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
| ⊢ 𝑋 = (Base‘𝑀) & ⊢ 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝑀 ∈ MetSp → 𝐷:(𝑋 × 𝑋)⟶ℝ) | ||
| Theorem | xmsxmet2 24469 | The distance function, suitably truncated, is an extended metric on 𝑋. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝑀) & ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ (𝑀 ∈ ∞MetSp → (𝐷 ↾ (𝑋 × 𝑋)) ∈ (∞Met‘𝑋)) | ||
| Theorem | msmet2 24470 | The distance function, suitably truncated, is a metric on 𝑋. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝑀) & ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ (𝑀 ∈ MetSp → (𝐷 ↾ (𝑋 × 𝑋)) ∈ (Met‘𝑋)) | ||
| Theorem | mscl 24471 | Closure of the distance function of a metric space. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 2-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝑀) & ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ MetSp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ ℝ) | ||
| Theorem | xmscl 24472 | Closure of the distance function of an extended metric space. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝑀) & ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ ℝ*) | ||
| Theorem | xmsge0 24473 | The distance function in an extended metric space is nonnegative. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝑀) & ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝐵)) | ||
| Theorem | xmseq0 24474 | The distance between two points in an extended metric space is zero iff the two points are identical. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝑀) & ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝐷𝐵) = 0 ↔ 𝐴 = 𝐵)) | ||
| Theorem | xmssym 24475 | The distance function in an extended metric space is symmetric. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝑀) & ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴)) | ||
| Theorem | xmstri2 24476 | Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝑀) & ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ ∞MetSp ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) +𝑒 (𝐶𝐷𝐵))) | ||
| Theorem | mstri2 24477 | Triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝑀) & ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ MetSp ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) + (𝐶𝐷𝐵))) | ||
| Theorem | xmstri 24478 | Triangle inequality for the distance function of a metric space. Definition 14-1.1(d) of [Gleason] p. 223. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝑀) & ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ ∞MetSp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) +𝑒 (𝐶𝐷𝐵))) | ||
| Theorem | mstri 24479 | Triangle inequality for the distance function of a metric space. Definition 14-1.1(d) of [Gleason] p. 223. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝑀) & ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ MetSp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) + (𝐶𝐷𝐵))) | ||
| Theorem | xmstri3 24480 | Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝑀) & ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ ∞MetSp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) +𝑒 (𝐵𝐷𝐶))) | ||
| Theorem | mstri3 24481 | Triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝑀) & ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ MetSp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) + (𝐵𝐷𝐶))) | ||
| Theorem | msrtri 24482 | Reverse triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑋 = (Base‘𝑀) & ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ MetSp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (abs‘((𝐴𝐷𝐶) − (𝐵𝐷𝐶))) ≤ (𝐴𝐷𝐵)) | ||
| Theorem | xmspropd 24483 | Property deduction for an extended metric space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵))) & ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿)) ⇒ ⊢ (𝜑 → (𝐾 ∈ ∞MetSp ↔ 𝐿 ∈ ∞MetSp)) | ||
| Theorem | mspropd 24484 | Property deduction for a metric space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵))) & ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿)) ⇒ ⊢ (𝜑 → (𝐾 ∈ MetSp ↔ 𝐿 ∈ MetSp)) | ||
| Theorem | setsmsbas 24485 | The base set of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) (Proof shortened by AV, 12-Nov-2024.) |
| ⊢ (𝜑 → 𝑋 = (Base‘𝑀)) & ⊢ (𝜑 → 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋))) & ⊢ (𝜑 → 𝐾 = (𝑀 sSet 〈(TopSet‘ndx), (MetOpen‘𝐷)〉)) ⇒ ⊢ (𝜑 → 𝑋 = (Base‘𝐾)) | ||
| Theorem | setsmsbasOLD 24486 | Obsolete version of setsmsbas 24485 as of 12-Nov-2024. The base set of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝑋 = (Base‘𝑀)) & ⊢ (𝜑 → 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋))) & ⊢ (𝜑 → 𝐾 = (𝑀 sSet 〈(TopSet‘ndx), (MetOpen‘𝐷)〉)) ⇒ ⊢ (𝜑 → 𝑋 = (Base‘𝐾)) | ||
| Theorem | setsmsds 24487 | The distance function of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) (Proof shortened by AV, 11-Nov-2024.) |
| ⊢ (𝜑 → 𝑋 = (Base‘𝑀)) & ⊢ (𝜑 → 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋))) & ⊢ (𝜑 → 𝐾 = (𝑀 sSet 〈(TopSet‘ndx), (MetOpen‘𝐷)〉)) ⇒ ⊢ (𝜑 → (dist‘𝑀) = (dist‘𝐾)) | ||
| Theorem | setsmsdsOLD 24488 | Obsolete version of setsmsds 24487 as of 11-Nov-2024. The distance function of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝜑 → 𝑋 = (Base‘𝑀)) & ⊢ (𝜑 → 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋))) & ⊢ (𝜑 → 𝐾 = (𝑀 sSet 〈(TopSet‘ndx), (MetOpen‘𝐷)〉)) ⇒ ⊢ (𝜑 → (dist‘𝑀) = (dist‘𝐾)) | ||
| Theorem | setsmstset 24489 | The topology of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| ⊢ (𝜑 → 𝑋 = (Base‘𝑀)) & ⊢ (𝜑 → 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋))) & ⊢ (𝜑 → 𝐾 = (𝑀 sSet 〈(TopSet‘ndx), (MetOpen‘𝐷)〉)) & ⊢ (𝜑 → 𝑀 ∈ 𝑉) ⇒ ⊢ (𝜑 → (MetOpen‘𝐷) = (TopSet‘𝐾)) | ||
| Theorem | setsmstopn 24490 | The topology of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| ⊢ (𝜑 → 𝑋 = (Base‘𝑀)) & ⊢ (𝜑 → 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋))) & ⊢ (𝜑 → 𝐾 = (𝑀 sSet 〈(TopSet‘ndx), (MetOpen‘𝐷)〉)) & ⊢ (𝜑 → 𝑀 ∈ 𝑉) ⇒ ⊢ (𝜑 → (MetOpen‘𝐷) = (TopOpen‘𝐾)) | ||
| Theorem | setsxms 24491 | The constructed metric space is a metric space iff the provided distance function is a metric. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| ⊢ (𝜑 → 𝑋 = (Base‘𝑀)) & ⊢ (𝜑 → 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋))) & ⊢ (𝜑 → 𝐾 = (𝑀 sSet 〈(TopSet‘ndx), (MetOpen‘𝐷)〉)) & ⊢ (𝜑 → 𝑀 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐾 ∈ ∞MetSp ↔ 𝐷 ∈ (∞Met‘𝑋))) | ||
| Theorem | setsms 24492 | The constructed metric space is a metric space iff the provided distance function is a metric. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| ⊢ (𝜑 → 𝑋 = (Base‘𝑀)) & ⊢ (𝜑 → 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋))) & ⊢ (𝜑 → 𝐾 = (𝑀 sSet 〈(TopSet‘ndx), (MetOpen‘𝐷)〉)) & ⊢ (𝜑 → 𝑀 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐾 ∈ MetSp ↔ 𝐷 ∈ (Met‘𝑋))) | ||
| Theorem | tmsval 24493 | For any metric there is an associated metric space. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| ⊢ 𝑀 = {〈(Base‘ndx), 𝑋〉, 〈(dist‘ndx), 𝐷〉} & ⊢ 𝐾 = (toMetSp‘𝐷) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐾 = (𝑀 sSet 〈(TopSet‘ndx), (MetOpen‘𝐷)〉)) | ||
| Theorem | tmslem 24494 | Lemma for tmsbas 24496, tmsds 24497, and tmstopn 24498. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| ⊢ 𝑀 = {〈(Base‘ndx), 𝑋〉, 〈(dist‘ndx), 𝐷〉} & ⊢ 𝐾 = (toMetSp‘𝐷) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑋 = (Base‘𝐾) ∧ 𝐷 = (dist‘𝐾) ∧ (MetOpen‘𝐷) = (TopOpen‘𝐾))) | ||
| Theorem | tmslemOLD 24495 | Obsolete version of tmslem 24494 as of 28-Oct-2024. Lemma for tmsbas 24496, tmsds 24497, and tmstopn 24498. (Contributed by Mario Carneiro, 2-Sep-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝑀 = {〈(Base‘ndx), 𝑋〉, 〈(dist‘ndx), 𝐷〉} & ⊢ 𝐾 = (toMetSp‘𝐷) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑋 = (Base‘𝐾) ∧ 𝐷 = (dist‘𝐾) ∧ (MetOpen‘𝐷) = (TopOpen‘𝐾))) | ||
| Theorem | tmsbas 24496 | The base set of a constructed metric space. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| ⊢ 𝐾 = (toMetSp‘𝐷) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = (Base‘𝐾)) | ||
| Theorem | tmsds 24497 | The metric of a constructed metric space. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| ⊢ 𝐾 = (toMetSp‘𝐷) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷 = (dist‘𝐾)) | ||
| Theorem | tmstopn 24498 | The topology of a constructed metric. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| ⊢ 𝐾 = (toMetSp‘𝐷) & ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 = (TopOpen‘𝐾)) | ||
| Theorem | tmsxms 24499 | The constructed metric space is an extended metric space. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| ⊢ 𝐾 = (toMetSp‘𝐷) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐾 ∈ ∞MetSp) | ||
| Theorem | tmsms 24500 | The constructed metric space is a metric space given a metric. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| ⊢ 𝐾 = (toMetSp‘𝐷) ⇒ ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐾 ∈ MetSp) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |