P. 128 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12701-12800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mettri2 12701	Triangle inequality for the distance function of a metric space. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) + (𝐶𝐷𝐵)))
Theorem	xmet0 12702	The distance function of a metric space is zero if its arguments are equal. Definition 14-1.1(a) of [Gleason] p. 223. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐴𝐷𝐴) = 0)
Theorem	met0 12703	The distance function of a metric space is zero if its arguments are equal. Definition 14-1.1(a) of [Gleason] p. 223. (Contributed by NM, 30-Aug-2006.)
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐴𝐷𝐴) = 0)
Theorem	xmetge0 12704	The distance function of a metric space is nonnegative. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝐵))
Theorem	metge0 12705	The distance function of a metric space is nonnegative. (Contributed by NM, 27-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝐵))
Theorem	xmetlecl 12706	Real closure of an extended metric value that is upper bounded by a real. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ ℝ ∧ (𝐴𝐷𝐵) ≤ 𝐶)) → (𝐴𝐷𝐵) ∈ ℝ)
Theorem	xmetsym 12707	The distance function of an extended metric space is symmetric. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴))
Theorem	xmetpsmet 12708	An extended metric is a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷 ∈ (PsMet‘𝑋))
Theorem	xmettpos 12709	The distance function of an extended metric space is symmetric. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → tpos 𝐷 = 𝐷)
Theorem	metsym 12710	The distance function of a metric space is symmetric. Definition 14-1.1(c) of [Gleason] p. 223. (Contributed by NM, 27-Aug-2006.) (Revised by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴))
Theorem	xmettri 12711	Triangle inequality for the distance function of a metric space. Definition 14-1.1(d) of [Gleason] p. 223. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) +𝑒 (𝐶𝐷𝐵)))
Theorem	mettri 12712	Triangle inequality for the distance function of a metric space. Definition 14-1.1(d) of [Gleason] p. 223. (Contributed by NM, 27-Aug-2006.)
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) + (𝐶𝐷𝐵)))
Theorem	xmettri3 12713	Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) +𝑒 (𝐵𝐷𝐶)))
Theorem	mettri3 12714	Triangle inequality for the distance function of a metric space. (Contributed by NM, 13-Mar-2007.)
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) + (𝐵𝐷𝐶)))
Theorem	xmetrtri 12715	One half of the reverse triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 4-Sep-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐶) +𝑒 -𝑒(𝐵𝐷𝐶)) ≤ (𝐴𝐷𝐵))
Theorem	metrtri 12716	Reverse triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Jim Kingdon, 21-Apr-2023.)
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (abs‘((𝐴𝐷𝐶) − (𝐵𝐷𝐶))) ≤ (𝐴𝐷𝐵))
Theorem	metn0 12717	A metric space is nonempty iff its base set is nonempty. (Contributed by NM, 4-Oct-2007.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ (𝐷 ∈ (Met‘𝑋) → (𝐷 ≠ ∅ ↔ 𝑋 ≠ ∅))
Theorem	xmetres2 12718	Restriction of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑅 ⊆ 𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) ∈ (∞Met‘𝑅))
Theorem	metreslem 12719	Lemma for metres 12722. (Contributed by Mario Carneiro, 24-Aug-2015.)
⊢ (dom 𝐷 = (𝑋 × 𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) = (𝐷 ↾ ((𝑋 ∩ 𝑅) × (𝑋 ∩ 𝑅))))
Theorem	metres2 12720	Lemma for metres 12722. (Contributed by FL, 12-Oct-2006.) (Proof shortened by Mario Carneiro, 14-Aug-2015.)
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑅 ⊆ 𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) ∈ (Met‘𝑅))
Theorem	xmetres 12721	A restriction of an extended metric is an extended metric. (Contributed by Mario Carneiro, 24-Aug-2015.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) ∈ (∞Met‘(𝑋 ∩ 𝑅)))
Theorem	metres 12722	A restriction of a metric is a metric. (Contributed by NM, 26-Aug-2007.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ (𝐷 ∈ (Met‘𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) ∈ (Met‘(𝑋 ∩ 𝑅)))
Theorem	0met 12723	The empty metric. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ ∅ ∈ (Met‘∅)
7.2.3  Metric space balls
Theorem	blfvalps 12724*	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 12725*	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	blex 12726	A ball is a set. (Contributed by Jim Kingdon, 4-May-2023.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → (ball‘𝐷) ∈ V)
Theorem	blvalps 12727*	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 12728*	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 12729	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 12730	Membership in a ball. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝐴 ∈ 𝑋 ∧ (𝑃𝐷𝐴) < 𝑅)))
Theorem	elbl2ps 12731	Membership in a ball. (Contributed by NM, 9-Mar-2007.) (Revised by Thierry Arnoux, 11-Mar-2018.)
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝑃𝐷𝐴) < 𝑅))
Theorem	elbl2 12732	Membership in a ball. (Contributed by NM, 9-Mar-2007.)
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝑃𝐷𝐴) < 𝑅))
Theorem	elbl3ps 12733	Membership in a ball, with reversed distance function arguments. (Contributed by NM, 10-Nov-2007.)
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝐴𝐷𝑃) < 𝑅))
Theorem	elbl3 12734	Membership in a ball, with reversed distance function arguments. (Contributed by NM, 10-Nov-2007.)
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝐴𝐷𝑃) < 𝑅))
Theorem	blcomps 12735	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 12736	Commute the arguments to the ball function. (Contributed by Mario Carneiro, 22-Jan-2014.)
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ 𝑃 ∈ (𝐴(ball‘𝐷)𝑅)))
Theorem	xblpnfps 12737	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 12738	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 12739	The infinity ball in a standard metric is just the whole space. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝑃(ball‘𝐷)+∞) = 𝑋)
Theorem	bldisj 12740	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 12741	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 12742	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 12743	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 12746 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 12744	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 12746 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 12745	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 12746	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 12747	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 12748	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 12749	Mapping of a ball. (Contributed by NM, 7-May-2007.) (Revised by Mario Carneiro, 23-Aug-2015.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → (ball‘𝐷):(𝑋 × ℝ*)⟶𝒫 𝑋)
Theorem	blrnps 12750*	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 12751*	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 12752	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 12753	A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ (𝑅 ∈ ℝ* ∧ 0 < 𝑅)) → 𝑃 ∈ (𝑃(ball‘𝐷)𝑅))
Theorem	blcntrps 12754	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 12755	A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → 𝑃 ∈ (𝑃(ball‘𝐷)𝑅))
Theorem	xblm 12756*	A ball is inhabited iff the radius is positive. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (∃𝑥 𝑥 ∈ (𝑃(ball‘𝐷)𝑅) ↔ 0 < 𝑅))
Theorem	bln0 12757	A ball is not empty. It is also inhabited, as seen at blcntr 12755. (Contributed by NM, 6-Oct-2007.) (Revised by Mario Carneiro, 12-Nov-2013.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → (𝑃(ball‘𝐷)𝑅) ≠ ∅)
Theorem	blelrnps 12758	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 12759	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 12760	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 12761	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 12762	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	blininf 12763	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‘𝐷)inf({𝑅, 𝑆}, ℝ*, < )))
Theorem	ssblps 12764	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 12765	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 12766*	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 12767*	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 12768*	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 12769*	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 12770*	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 12771*	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 12772	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 12773	A ball in a restricted metric space. (Contributed by Mario Carneiro, 5-Jan-2014.)
⊢ 𝐶 = (𝐷 ↾ (𝑌 × 𝑌))    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ (𝑋 ∩ 𝑌) ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐶)𝑅) = ((𝑃(ball‘𝐷)𝑅) ∩ 𝑌))
Theorem	xmeterval 12774	Value of the "finitely separated" relation. (Contributed by Mario Carneiro, 24-Aug-2015.)
⊢ ∼ = (◡𝐷 “ ℝ)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐴 ∼ 𝐵 ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (𝐴𝐷𝐵) ∈ ℝ)))
Theorem	xmeter 12775	The "finitely separated" relation is an equivalence relation. (Contributed by Mario Carneiro, 24-Aug-2015.)
⊢ ∼ = (◡𝐷 “ ℝ)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → ∼ Er 𝑋)
Theorem	xmetec 12776	The equivalence classes under the finite separation equivalence relation are infinity balls. (Contributed by Mario Carneiro, 24-Aug-2015.)
⊢ ∼ = (◡𝐷 “ ℝ)    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → [𝑃] ∼ = (𝑃(ball‘𝐷)+∞))
Theorem	blssec 12777	A ball centered at 𝑃 is contained in the set of points finitely separated from 𝑃. This is just an application of ssbl 12765 to the infinity ball. (Contributed by Mario Carneiro, 24-Aug-2015.)
⊢ ∼ = (◡𝐷 “ ℝ)    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑆) ⊆ [𝑃] ∼ )
Theorem	blpnfctr 12778	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 12779	An extended metric restricted to any ball (in particular the infinity ball) is a proper metric. Together with xmetec 12776, 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‘𝐵))
7.2.4  Open sets of a metric space
Theorem	mopnrel 12780	The class of open sets of a metric space is a relation. (Contributed by Jim Kingdon, 5-May-2023.)
⊢ Rel MetOpen
Theorem	mopnval 12781	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 12783, the open sets of a metric space form a topology 𝐽, whose base set is ∪ 𝐽 by mopnuni 12784. (Contributed by NM, 1-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 = (topGen‘ran (ball‘𝐷)))
Theorem	mopntopon 12782	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 12783	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 12784	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 12785*	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 12786	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 12787	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 12788*	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 12789	An open set of a metric space is a subspace of its base set. (Contributed by NM, 3-Sep-2006.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝑋)
Theorem	isxms 12790	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 12791	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 12792	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 12793	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 12794	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 12795	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 12796	An extended metric space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ (𝑀 ∈ ∞MetSp → 𝑀 ∈ TopSp)
Theorem	msxms 12797	A metric space is an extended metric space. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ (𝑀 ∈ MetSp → 𝑀 ∈ ∞MetSp)
Theorem	mstps 12798	A metric space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ (𝑀 ∈ MetSp → 𝑀 ∈ TopSp)
Theorem	xmsxmet 12799	The distance function, suitably truncated, is an extended metric on 𝑋. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝑋 = (Base‘𝑀)    &   ⊢ 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋))    ⇒   ⊢ (𝑀 ∈ ∞MetSp → 𝐷 ∈ (∞Met‘𝑋))
Theorem	msmet 12800	The distance function, suitably truncated, is a metric on 𝑋. (Contributed by Mario Carneiro, 12-Nov-2013.)
⊢ 𝑋 = (Base‘𝑀)    &   ⊢ 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋))    ⇒   ⊢ (𝑀 ∈ MetSp → 𝐷 ∈ (Met‘𝑋))