P. 244 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 24301-24400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	metdmdm 24301	Recover the base set from a metric. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ (𝐷 ∈ (Met‘𝑋) → 𝑋 = dom dom 𝐷)
Theorem	xmetunirn 24302	Two ways to express an extended metric on an unspecified base. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ (𝐷 ∈ ∪ ran ∞Met ↔ 𝐷 ∈ (∞Met‘dom dom 𝐷))
Theorem	xmeteq0 24303	The value of an extended metric is zero iff its arguments are equal. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝐷𝐵) = 0 ↔ 𝐴 = 𝐵))
Theorem	meteq0 24304	The value of a metric is zero iff its arguments are equal. Property M2 of [Kreyszig] p. 4. (Contributed by NM, 30-Aug-2006.)
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴𝐷𝐵) = 0 ↔ 𝐴 = 𝐵))
Theorem	xmettri2 24305	Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) +𝑒 (𝐶𝐷𝐵)))
Theorem	mettri2 24306	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 24307	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 24308	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 24309	The distance function of a metric space is nonnegative. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝐵))
Theorem	metge0 24310	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 24311	Real closure of an extended metric value that is upper bounded by a real. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ ℝ ∧ (𝐴𝐷𝐵) ≤ 𝐶)) → (𝐴𝐷𝐵) ∈ ℝ)
Theorem	xmetsym 24312	The distance function of an extended metric space is symmetric. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴))
Theorem	xmetpsmet 24313	An extended metric is a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷 ∈ (PsMet‘𝑋))
Theorem	xmettpos 24314	The distance function of an extended metric space is symmetric. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → tpos 𝐷 = 𝐷)
Theorem	metsym 24315	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 24316	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 24317	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 24318	Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) +𝑒 (𝐵𝐷𝐶)))
Theorem	mettri3 24319	Triangle inequality for the distance function of a metric space. (Contributed by NM, 13-Mar-2007.)
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) + (𝐵𝐷𝐶)))
Theorem	xmetrtri 24320	One half of the reverse triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 4-Sep-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐶) +𝑒 -𝑒(𝐵𝐷𝐶)) ≤ (𝐴𝐷𝐵))
Theorem	xmetrtri2 24321	The reverse triangle inequality for the distance function of an extended metric. In order to express the "extended absolute value function", we use the distance function xrsdsval 21391 defined on the extended real structure. (Contributed by Mario Carneiro, 4-Sep-2015.)
⊢ 𝐾 = (dist‘ℝ*𝑠)    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐷𝐶)𝐾(𝐵𝐷𝐶)) ≤ (𝐴𝐷𝐵))
Theorem	metrtri 24322	Reverse triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 5-May-2014.)
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (abs‘((𝐴𝐷𝐶) − (𝐵𝐷𝐶))) ≤ (𝐴𝐷𝐵))
Theorem	xmetgt0 24323	The distance function of an extended metric space is positive for unequal points. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ≠ 𝐵 ↔ 0 < (𝐴𝐷𝐵)))
Theorem	metgt0 24324	The distance function of a metric space is positive for unequal points. Definition 14-1.1(b) of [Gleason] p. 223 and its converse. (Contributed by NM, 27-Aug-2006.)
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 ≠ 𝐵 ↔ 0 < (𝐴𝐷𝐵)))
Theorem	metn0 24325	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 24326	Restriction of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑅 ⊆ 𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) ∈ (∞Met‘𝑅))
Theorem	metreslem 24327	Lemma for metres 24330. (Contributed by Mario Carneiro, 24-Aug-2015.)
⊢ (dom 𝐷 = (𝑋 × 𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) = (𝐷 ↾ ((𝑋 ∩ 𝑅) × (𝑋 ∩ 𝑅))))
Theorem	metres2 24328	Lemma for metres 24330. (Contributed by FL, 12-Oct-2006.) (Proof shortened by Mario Carneiro, 14-Aug-2015.)
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑅 ⊆ 𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) ∈ (Met‘𝑅))
Theorem	xmetres 24329	A restriction of an extended metric is an extended metric. (Contributed by Mario Carneiro, 24-Aug-2015.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) ∈ (∞Met‘(𝑋 ∩ 𝑅)))
Theorem	metres 24330	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 24331	The empty metric. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ ∅ ∈ (Met‘∅)
Theorem	prdsdsf 24332*	The product metric is a function into the nonnegative extended reals. In general this means that it is not a metric but rather an *extended* metric (even when all the factors are metrics), but it will be a metric when restricted to regions where it does not take infinite values. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅))    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝑉 = (Base‘𝑅)    &   ⊢ 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉))    &   ⊢ 𝐷 = (dist‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ 𝑍)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉))    ⇒   ⊢ (𝜑 → 𝐷:(𝐵 × 𝐵)⟶(0[,]+∞))
Theorem	prdsxmetlem 24333*	The product metric is an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅))    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝑉 = (Base‘𝑅)    &   ⊢ 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉))    &   ⊢ 𝐷 = (dist‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ 𝑍)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉))    ⇒   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝐵))
Theorem	prdsxmet 24334*	The product metric is an extended metric. Eliminate disjoint variable conditions from prdsxmetlem 24333. (Contributed by Mario Carneiro, 26-Sep-2015.)
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅))    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝑉 = (Base‘𝑅)    &   ⊢ 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉))    &   ⊢ 𝐷 = (dist‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ 𝑍)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉))    ⇒   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝐵))
Theorem	prdsmet 24335*	The product metric is a metric when the index set is finite. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅))    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝑉 = (Base‘𝑅)    &   ⊢ 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉))    &   ⊢ 𝐷 = (dist‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ 𝑍)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (Met‘𝑉))    ⇒   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝐵))
Theorem	ressprdsds 24336*	Restriction of a product metric. (Contributed by Mario Carneiro, 16-Sep-2015.)
⊢ (𝜑 → 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)))    &   ⊢ (𝜑 → 𝐻 = (𝑇Xs(𝑥 ∈ 𝐼 ↦ (𝑅 ↾s 𝐴))))    &   ⊢ 𝐵 = (Base‘𝐻)    &   ⊢ 𝐷 = (dist‘𝑌)    &   ⊢ 𝐸 = (dist‘𝐻)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑈)    &   ⊢ (𝜑 → 𝑇 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐴 ∈ 𝑍)    ⇒   ⊢ (𝜑 → 𝐸 = (𝐷 ↾ (𝐵 × 𝐵)))
Theorem	resspwsds 24337	Restriction of a power metric. (Contributed by Mario Carneiro, 16-Sep-2015.)
⊢ (𝜑 → 𝑌 = (𝑅 ↑s 𝐼))    &   ⊢ (𝜑 → 𝐻 = ((𝑅 ↾s 𝐴) ↑s 𝐼))    &   ⊢ 𝐵 = (Base‘𝐻)    &   ⊢ 𝐷 = (dist‘𝑌)    &   ⊢ 𝐸 = (dist‘𝐻)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    ⇒   ⊢ (𝜑 → 𝐸 = (𝐷 ↾ (𝐵 × 𝐵)))
Theorem	imasdsf1olem 24338*	Lemma for imasdsf1o 24339. (Contributed by Mario Carneiro, 21-Aug-2015.) (Proof shortened by AV, 6-Oct-2020.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉))    &   ⊢ 𝐷 = (dist‘𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ (∞Met‘𝑉))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ 𝑊 = (ℝ*𝑠 ↾s (ℝ* ∖ {-∞}))    &   ⊢ 𝑆 = {ℎ ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)) ∣ ((𝐹‘(1st ‘(ℎ‘1))) = (𝐹‘𝑋) ∧ (𝐹‘(2nd ‘(ℎ‘𝑛))) = (𝐹‘𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))))}    &   ⊢ 𝑇 = ∪ 𝑛 ∈ ℕ ran (𝑔 ∈ 𝑆 ↦ (ℝ*𝑠 Σg (𝐸 ∘ 𝑔)))    ⇒   ⊢ (𝜑 → ((𝐹‘𝑋)𝐷(𝐹‘𝑌)) = (𝑋𝐸𝑌))
Theorem	imasdsf1o 24339	The distance function is transferred across an image structure under a bijection. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉))    &   ⊢ 𝐷 = (dist‘𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ (∞Met‘𝑉))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝐹‘𝑋)𝐷(𝐹‘𝑌)) = (𝑋𝐸𝑌))
Theorem	imasf1oxmet 24340	The image of an extended metric is an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉))    &   ⊢ 𝐷 = (dist‘𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ (∞Met‘𝑉))    ⇒   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝐵))
Theorem	imasf1omet 24341	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 24342	Closure of the metric in a binary structure product. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ 𝑇 = (𝑅 ×s 𝑆)    &   ⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑌 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ 𝑃 = (dist‘𝑇)    ⇒   ⊢ (𝜑 → 𝑃 Fn ((𝑋 × 𝑌) × (𝑋 × 𝑌)))
Theorem	xpsdsfn2 24343	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 24344*	Lemma for xpsxmet 24345. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ 𝑇 = (𝑅 ×s 𝑆)    &   ⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑌 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ 𝑃 = (dist‘𝑇)    &   ⊢ 𝑀 = ((dist‘𝑅) ↾ (𝑋 × 𝑋))    &   ⊢ 𝑁 = ((dist‘𝑆) ↾ (𝑌 × 𝑌))    &   ⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌))    ⇒   ⊢ (𝜑 → (dist‘((Scalar‘𝑅)Xs{⟨∅, 𝑅⟩, ⟨1o, 𝑆⟩})) ∈ (∞Met‘ran (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩})))
Theorem	xpsxmet 24345	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 24346	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 24347	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‘(𝑋 × 𝑌)))
12.4.3  Metric space balls
Theorem	blfvalps 24348*	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 24349*	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 24350*	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 24351*	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 24352	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 24353	Membership in a ball. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝐴 ∈ 𝑋 ∧ (𝑃𝐷𝐴) < 𝑅)))
Theorem	elbl2ps 24354	Membership in a ball. (Contributed by NM, 9-Mar-2007.) (Revised by Thierry Arnoux, 11-Mar-2018.)
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝑃𝐷𝐴) < 𝑅))
Theorem	elbl2 24355	Membership in a ball. (Contributed by NM, 9-Mar-2007.)
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝑃𝐷𝐴) < 𝑅))
Theorem	elbl3ps 24356	Membership in a ball, with reversed distance function arguments. (Contributed by NM, 10-Nov-2007.)
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝐴𝐷𝑃) < 𝑅))
Theorem	elbl3 24357	Membership in a ball, with reversed distance function arguments. (Contributed by NM, 10-Nov-2007.)
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ (𝐴𝐷𝑃) < 𝑅))
Theorem	blcomps 24358	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 24359	Commute the arguments to the ball function. (Contributed by Mario Carneiro, 22-Jan-2014.)
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ*) ∧ (𝑃 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐴 ∈ (𝑃(ball‘𝐷)𝑅) ↔ 𝑃 ∈ (𝐴(ball‘𝐷)𝑅)))
Theorem	xblpnfps 24360	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 24361	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 24362	The infinity ball in a standard metric is just the whole space. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝑃(ball‘𝐷)+∞) = 𝑋)
Theorem	bldisj 24363	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 24364	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 24365	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 24366	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 24369 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 24367	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 24369 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 24368	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 24369	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 24370	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 24371	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 24372	Mapping of a ball. (Contributed by NM, 7-May-2007.) (Revised by Mario Carneiro, 23-Aug-2015.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → (ball‘𝐷):(𝑋 × ℝ*)⟶𝒫 𝑋)
Theorem	blrnps 24373*	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 24374*	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 24375	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 24376	A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ (𝑅 ∈ ℝ* ∧ 0 < 𝑅)) → 𝑃 ∈ (𝑃(ball‘𝐷)𝑅))
Theorem	blcntrps 24377	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 24378	A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → 𝑃 ∈ (𝑃(ball‘𝐷)𝑅))
Theorem	xbln0 24379	A ball is nonempty iff the radius is positive. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → ((𝑃(ball‘𝐷)𝑅) ≠ ∅ ↔ 0 < 𝑅))
Theorem	bln0 24380	A ball is not empty. (Contributed by NM, 6-Oct-2007.) (Revised by Mario Carneiro, 12-Nov-2013.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → (𝑃(ball‘𝐷)𝑅) ≠ ∅)
Theorem	blelrnps 24381	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 24382	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 24383	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 24384	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 24385	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 24386	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 24387	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 24388	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 24389*	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 24390*	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 24391*	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 24392*	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 24393*	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 24394*	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 24395	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 24396	A ball in a restricted metric space. (Contributed by Mario Carneiro, 5-Jan-2014.)
⊢ 𝐶 = (𝐷 ↾ (𝑌 × 𝑌))    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ (𝑋 ∩ 𝑌) ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐶)𝑅) = ((𝑃(ball‘𝐷)𝑅) ∩ 𝑌))
Theorem	xmeterval 24397	Value of the "finitely separated" relation. (Contributed by Mario Carneiro, 24-Aug-2015.)
⊢ ∼ = (◡𝐷 “ ℝ)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐴 ∼ 𝐵 ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (𝐴𝐷𝐵) ∈ ℝ)))
Theorem	xmeter 24398	The "finitely separated" relation is an equivalence relation. (Contributed by Mario Carneiro, 24-Aug-2015.)
⊢ ∼ = (◡𝐷 “ ℝ)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → ∼ Er 𝑋)
Theorem	xmetec 24399	The equivalence classes under the finite separation equivalence relation are infinity balls. Thus, by erdisj 8701, 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 24400	A ball centered at 𝑃 is contained in the set of points finitely separated from 𝑃. This is just an application of ssbl 24388 to the infinity ball. (Contributed by Mario Carneiro, 24-Aug-2015.)
⊢ ∼ = (◡𝐷 “ ℝ)    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑆) ⊆ [𝑃] ∼ )