![]() |
Metamath
Proof Explorer Theorem List (p. 245 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | imasf1omet 24401 | The image of a metric is a metric. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝐵) & ⊢ (𝜑 → 𝑅 ∈ 𝑍) & ⊢ 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉)) & ⊢ 𝐷 = (dist‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ (Met‘𝑉)) ⇒ ⊢ (𝜑 → 𝐷 ∈ (Met‘𝐵)) | ||
Theorem | xpsdsfn 24402 | Closure of the metric in a binary structure product. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ 𝑃 = (dist‘𝑇) ⇒ ⊢ (𝜑 → 𝑃 Fn ((𝑋 × 𝑌) × (𝑋 × 𝑌))) | ||
Theorem | xpsdsfn2 24403 | Closure of the metric in a binary structure product. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ 𝑃 = (dist‘𝑇) ⇒ ⊢ (𝜑 → 𝑃 Fn ((Base‘𝑇) × (Base‘𝑇))) | ||
Theorem | xpsxmetlem 24404* | Lemma for xpsxmet 24405. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ 𝑃 = (dist‘𝑇) & ⊢ 𝑀 = ((dist‘𝑅) ↾ (𝑋 × 𝑋)) & ⊢ 𝑁 = ((dist‘𝑆) ↾ (𝑌 × 𝑌)) & ⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌)) ⇒ ⊢ (𝜑 → (dist‘((Scalar‘𝑅)Xs{〈∅, 𝑅〉, 〈1o, 𝑆〉})) ∈ (∞Met‘ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}))) | ||
Theorem | xpsxmet 24405 | A product metric of extended metrics is an extended metric. (Contributed by Mario Carneiro, 21-Aug-2015.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ 𝑃 = (dist‘𝑇) & ⊢ 𝑀 = ((dist‘𝑅) ↾ (𝑋 × 𝑋)) & ⊢ 𝑁 = ((dist‘𝑆) ↾ (𝑌 × 𝑌)) & ⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌)) ⇒ ⊢ (𝜑 → 𝑃 ∈ (∞Met‘(𝑋 × 𝑌))) | ||
Theorem | xpsdsval 24406 | Value of the metric in a binary structure product. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ 𝑃 = (dist‘𝑇) & ⊢ 𝑀 = ((dist‘𝑅) ↾ (𝑋 × 𝑋)) & ⊢ 𝑁 = ((dist‘𝑆) ↾ (𝑌 × 𝑌)) & ⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌)) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑌) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑌) ⇒ ⊢ (𝜑 → (〈𝐴, 𝐵〉𝑃〈𝐶, 𝐷〉) = sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < )) | ||
Theorem | xpsmet 24407 | The direct product of two metric spaces. Definition 14-1.5 of [Gleason] p. 225. (Contributed by NM, 20-Jun-2007.) (Revised by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ 𝑃 = (dist‘𝑇) & ⊢ 𝑀 = ((dist‘𝑅) ↾ (𝑋 × 𝑋)) & ⊢ 𝑁 = ((dist‘𝑆) ↾ (𝑌 × 𝑌)) & ⊢ (𝜑 → 𝑀 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝑁 ∈ (Met‘𝑌)) ⇒ ⊢ (𝜑 → 𝑃 ∈ (Met‘(𝑋 × 𝑌))) | ||
Theorem | blfvalps 24408* | The value of the ball function. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
⊢ (𝐷 ∈ (PsMet‘𝑋) → (ball‘𝐷) = (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟})) | ||
Theorem | blfval 24409* | The value of the ball function. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) (Proof shortened by Thierry Arnoux, 11-Feb-2018.) |
⊢ (𝐷 ∈ (∞Met‘𝑋) → (ball‘𝐷) = (𝑥 ∈ 𝑋, 𝑟 ∈ ℝ* ↦ {𝑦 ∈ 𝑋 ∣ (𝑥𝐷𝑦) < 𝑟})) | ||
Theorem | blvalps 24410* | The ball around a point 𝑃 is the set of all points whose distance from 𝑃 is less than the ball's radius 𝑅. (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) = {𝑥 ∈ 𝑋 ∣ (𝑃𝐷𝑥) < 𝑅}) | ||
Theorem | blval 24411* | The ball around a point 𝑃 is the set of all points whose distance from 𝑃 is less than the ball's radius 𝑅. (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) = {𝑥 ∈ 𝑋 ∣ (𝑃𝐷𝑥) < 𝑅}) | ||
Theorem | elblps 24412 | Membership in a ball. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝐴 ∈ 𝑋 ∧ (𝑃𝐷𝐴) < 𝑅))) | ||
Theorem | elbl 24413 | Membership in a ball. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝐴 ∈ 𝑋 ∧ (𝑃𝐷𝐴) < 𝑅))) | ||
Theorem | elbl2ps 24414 | Membership in a ball. (Contributed by NM, 9-Mar-2007.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝑃𝐷𝐴) < 𝑅)) | ||
Theorem | elbl2 24415 | Membership in a ball. (Contributed by NM, 9-Mar-2007.) |
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝑃𝐷𝐴) < 𝑅)) | ||
Theorem | elbl3ps 24416 | Membership in a ball, with reversed distance function arguments. (Contributed by NM, 10-Nov-2007.) |
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝐴𝐷𝑃) < 𝑅)) | ||
Theorem | elbl3 24417 | Membership in a ball, with reversed distance function arguments. (Contributed by NM, 10-Nov-2007.) |
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝐴𝐷𝑃) < 𝑅)) | ||
Theorem | blcomps 24418 | 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 24419 | Commute the arguments to the ball function. (Contributed by Mario Carneiro, 22-Jan-2014.) |
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ 𝑃 ∈ (𝐴(ball‘𝐷)𝑅))) | ||
Theorem | xblpnfps 24420 | 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 24421 | 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 24422 | The infinity ball in a standard metric is just the whole space. (Contributed by Mario Carneiro, 23-Aug-2015.) |
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝑃(ball‘𝐷)+∞) = 𝑋) | ||
Theorem | bldisj 24423 | 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 24424 | 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 24425 | 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 24426 | 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 24429 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 24427 | 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 24429 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 24428 | 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 24429 | 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 24430 | 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 24431 | 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 24432 | Mapping of a ball. (Contributed by NM, 7-May-2007.) (Revised by Mario Carneiro, 23-Aug-2015.) |
⊢ (𝐷 ∈ (∞Met‘𝑋) → (ball‘𝐷):(𝑋 × ℝ*)⟶𝒫 𝑋) | ||
Theorem | blrnps 24433* | 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 24434* | 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 24435 | 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 24436 | A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ (𝑅 ∈ ℝ* ∧ 0 < 𝑅)) → 𝑃 ∈ (𝑃(ball‘𝐷)𝑅)) | ||
Theorem | blcntrps 24437 | 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 24438 | A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → 𝑃 ∈ (𝑃(ball‘𝐷)𝑅)) | ||
Theorem | xbln0 24439 | A ball is nonempty iff the radius is positive. (Contributed by Mario Carneiro, 23-Aug-2015.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → ((𝑃(ball‘𝐷)𝑅) ≠ ∅ ↔ 0 < 𝑅)) | ||
Theorem | bln0 24440 | A ball is not empty. (Contributed by NM, 6-Oct-2007.) (Revised by Mario Carneiro, 12-Nov-2013.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → (𝑃(ball‘𝐷)𝑅) ≠ ∅) | ||
Theorem | blelrnps 24441 | 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 24442 | 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 24443 | 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 24444 | 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 24445 | 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 24446 | 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 24447 | 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 24448 | 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 24449* | 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 24450* | 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 24451* | 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 24452* | 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 24453* | 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 24454* | 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 24455 | 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 24456 | A ball in a restricted metric space. (Contributed by Mario Carneiro, 5-Jan-2014.) |
⊢ 𝐶 = (𝐷 ↾ (𝑌 × 𝑌)) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ (𝑋 ∩ 𝑌) ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐶)𝑅) = ((𝑃(ball‘𝐷)𝑅) ∩ 𝑌)) | ||
Theorem | xmeterval 24457 | Value of the "finitely separated" relation. (Contributed by Mario Carneiro, 24-Aug-2015.) |
⊢ ∼ = (◡𝐷 “ ℝ) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐴 ∼ 𝐵 ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (𝐴𝐷𝐵) ∈ ℝ))) | ||
Theorem | xmeter 24458 | The "finitely separated" relation is an equivalence relation. (Contributed by Mario Carneiro, 24-Aug-2015.) |
⊢ ∼ = (◡𝐷 “ ℝ) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → ∼ Er 𝑋) | ||
Theorem | xmetec 24459 | The equivalence classes under the finite separation equivalence relation are infinity balls. Thus, by erdisj 8797, 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 24460 | A ball centered at 𝑃 is contained in the set of points finitely separated from 𝑃. This is just an application of ssbl 24448 to the infinity ball. (Contributed by Mario Carneiro, 24-Aug-2015.) |
⊢ ∼ = (◡𝐷 “ ℝ) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑆) ⊆ [𝑃] ∼ ) | ||
Theorem | blpnfctr 24461 | 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 24462 | An extended metric restricted to any ball (in particular the infinity ball) is a proper metric. Together with xmetec 24459, 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 24463 | 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 24465, the open sets of a metric space form a topology 𝐽, whose base set is ∪ 𝐽 by mopnuni 24466. (Contributed by NM, 1-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 = (topGen‘ran (ball‘𝐷))) | ||
Theorem | mopntopon 24464 | 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 24465 | 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 24466 | 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 24467* | 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 24468 | 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 24469 | 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 24470* | 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 24471 | An open set of a metric space is a subspace of its base set. (Contributed by NM, 3-Sep-2006.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝑋) | ||
Theorem | isxms 24472 | 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 24473 | 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 24474 | 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 24475 | 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 24476 | 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 24477 | 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 24478 | An extended metric space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ (𝑀 ∈ ∞MetSp → 𝑀 ∈ TopSp) | ||
Theorem | msxms 24479 | A metric space is an extended metric space. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ (𝑀 ∈ MetSp → 𝑀 ∈ ∞MetSp) | ||
Theorem | mstps 24480 | A metric space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ (𝑀 ∈ MetSp → 𝑀 ∈ TopSp) | ||
Theorem | xmsxmet 24481 | The distance function, suitably truncated, is an extended metric on 𝑋. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ 𝑋 = (Base‘𝑀) & ⊢ 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝑀 ∈ ∞MetSp → 𝐷 ∈ (∞Met‘𝑋)) | ||
Theorem | msmet 24482 | The distance function, suitably truncated, is a metric on 𝑋. (Contributed by Mario Carneiro, 12-Nov-2013.) |
⊢ 𝑋 = (Base‘𝑀) & ⊢ 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝑀 ∈ MetSp → 𝐷 ∈ (Met‘𝑋)) | ||
Theorem | msf 24483 | 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 24484 | The distance function, suitably truncated, is an extended metric on 𝑋. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑋 = (Base‘𝑀) & ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ (𝑀 ∈ ∞MetSp → (𝐷 ↾ (𝑋 × 𝑋)) ∈ (∞Met‘𝑋)) | ||
Theorem | msmet2 24485 | The distance function, suitably truncated, is a metric on 𝑋. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑋 = (Base‘𝑀) & ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ (𝑀 ∈ MetSp → (𝐷 ↾ (𝑋 × 𝑋)) ∈ (Met‘𝑋)) | ||
Theorem | mscl 24486 | 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 24487 | Closure of the distance function of an extended metric space. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑋 = (Base‘𝑀) & ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ ℝ*) | ||
Theorem | xmsge0 24488 | The distance function in an extended metric space is nonnegative. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝑋 = (Base‘𝑀) & ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝐵)) | ||
Theorem | xmseq0 24489 | 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 24490 | The distance function in an extended metric space is symmetric. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑋 = (Base‘𝑀) & ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴)) | ||
Theorem | xmstri2 24491 | Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑋 = (Base‘𝑀) & ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ ∞MetSp ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) +𝑒 (𝐶𝐷𝐵))) | ||
Theorem | mstri2 24492 | Triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑋 = (Base‘𝑀) & ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ MetSp ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) + (𝐶𝐷𝐵))) | ||
Theorem | xmstri 24493 | 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 24494 | 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 24495 | Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑋 = (Base‘𝑀) & ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ ∞MetSp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) +𝑒 (𝐵𝐷𝐶))) | ||
Theorem | mstri3 24496 | Triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.) |
⊢ 𝑋 = (Base‘𝑀) & ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ MetSp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) + (𝐵𝐷𝐶))) | ||
Theorem | msrtri 24497 | Reverse triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ 𝑋 = (Base‘𝑀) & ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ MetSp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (abs‘((𝐴𝐷𝐶) − (𝐵𝐷𝐶))) ≤ (𝐴𝐷𝐵)) | ||
Theorem | xmspropd 24498 | Property deduction for an extended metric space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵))) & ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿)) ⇒ ⊢ (𝜑 → (𝐾 ∈ ∞MetSp ↔ 𝐿 ∈ ∞MetSp)) | ||
Theorem | mspropd 24499 | Property deduction for a metric space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵))) & ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿)) ⇒ ⊢ (𝜑 → (𝐾 ∈ MetSp ↔ 𝐿 ∈ MetSp)) | ||
Theorem | setsmsbas 24500 | 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‘𝐾)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |