P. 247 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 24601-24700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	blf 24601	Mapping of a ball. (Contributed by NM, 7-May-2007.) (Revised by Mario Carneiro, 23-Aug-2015.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → (ball‘𝐷):(𝑋 × ℝ*)⟶𝒫 𝑋)
Theorem	blrnps 24602*	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 24603*	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 24604	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 24605	A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ (𝑅 ∈ ℝ* ∧ 0 < 𝑅)) → 𝑃 ∈ (𝑃(ball‘𝐷)𝑅))
Theorem	blcntrps 24606	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 24607	A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → 𝑃 ∈ (𝑃(ball‘𝐷)𝑅))
Theorem	xbln0 24608	A ball is nonempty iff the radius is positive. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → ((𝑃(ball‘𝐷)𝑅) ≠ ∅ ↔ 0 < 𝑅))
Theorem	bln0 24609	A ball is not empty. (Contributed by NM, 6-Oct-2007.) (Revised by Mario Carneiro, 12-Nov-2013.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → (𝑃(ball‘𝐷)𝑅) ≠ ∅)
Theorem	blelrnps 24610	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 24611	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 24612	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 24613	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 24614	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 24615	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 24616	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 24617	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 24618*	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 24619*	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 24620*	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 24621*	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 24622*	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 24623*	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 24624	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 24625	A ball in a restricted metric space. (Contributed by Mario Carneiro, 5-Jan-2014.)
⊢ 𝐶 = (𝐷 ↾ (𝑌 × 𝑌))    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ (𝑋 ∩ 𝑌) ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐶)𝑅) = ((𝑃(ball‘𝐷)𝑅) ∩ 𝑌))
Theorem	xmeterval 24626	Value of the "finitely separated" relation. (Contributed by Mario Carneiro, 24-Aug-2015.)
⊢ ∼ = (◡𝐷 “ ℝ)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐴 ∼ 𝐵 ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (𝐴𝐷𝐵) ∈ ℝ)))
Theorem	xmeter 24627	The "finitely separated" relation is an equivalence relation. (Contributed by Mario Carneiro, 24-Aug-2015.)
⊢ ∼ = (◡𝐷 “ ℝ)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → ∼ Er 𝑋)
Theorem	xmetec 24628	The equivalence classes under the finite separation equivalence relation are infinity balls. Thus, by erdisj 8761, 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 24629	A ball centered at 𝑃 is contained in the set of points finitely separated from 𝑃. This is just an application of ssbl 24617 to the infinity ball. (Contributed by Mario Carneiro, 24-Aug-2015.)
⊢ ∼ = (◡𝐷 “ ℝ)    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑆) ⊆ [𝑃] ∼ )
Theorem	blpnfctr 24630	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 24631	An extended metric restricted to any ball (in particular the infinity ball) is a proper metric. Together with xmetec 24628, 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‘𝐵))
12.4.4  Open sets of a metric space
Theorem	mopnval 24632	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 24634, the open sets of a metric space form a topology 𝐽, whose base set is ∪ 𝐽 by mopnuni 24635. (Contributed by NM, 1-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 = (topGen‘ran (ball‘𝐷)))
Theorem	mopntopon 24633	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 24634	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 24635	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 24636*	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 24637	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 24638	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 24639*	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 24640	An open set of a metric space is a subspace of its base set. (Contributed by NM, 3-Sep-2006.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝑋)
Theorem	isxms 24641	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 24642	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 24643	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 24644	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 24645	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 24646	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 24647	An extended metric space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ (𝑀 ∈ ∞MetSp → 𝑀 ∈ TopSp)
Theorem	msxms 24648	A metric space is an extended metric space. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ (𝑀 ∈ MetSp → 𝑀 ∈ ∞MetSp)
Theorem	mstps 24649	A metric space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ (𝑀 ∈ MetSp → 𝑀 ∈ TopSp)
Theorem	xmsxmet 24650	The distance function, suitably truncated, is an extended metric on 𝑋. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝑋 = (Base‘𝑀)    &   ⊢ 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋))    ⇒   ⊢ (𝑀 ∈ ∞MetSp → 𝐷 ∈ (∞Met‘𝑋))
Theorem	msmet 24651	The distance function, suitably truncated, is a metric on 𝑋. (Contributed by Mario Carneiro, 12-Nov-2013.)
⊢ 𝑋 = (Base‘𝑀)    &   ⊢ 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋))    ⇒   ⊢ (𝑀 ∈ MetSp → 𝐷 ∈ (Met‘𝑋))
Theorem	msf 24652	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 24653	The distance function, suitably truncated, is an extended metric on 𝑋. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑋 = (Base‘𝑀)    &   ⊢ 𝐷 = (dist‘𝑀)    ⇒   ⊢ (𝑀 ∈ ∞MetSp → (𝐷 ↾ (𝑋 × 𝑋)) ∈ (∞Met‘𝑋))
Theorem	msmet2 24654	The distance function, suitably truncated, is a metric on 𝑋. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑋 = (Base‘𝑀)    &   ⊢ 𝐷 = (dist‘𝑀)    ⇒   ⊢ (𝑀 ∈ MetSp → (𝐷 ↾ (𝑋 × 𝑋)) ∈ (Met‘𝑋))
Theorem	mscl 24655	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 24656	Closure of the distance function of an extended metric space. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑋 = (Base‘𝑀)    &   ⊢ 𝐷 = (dist‘𝑀)    ⇒   ⊢ ((𝑀 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ ℝ*)
Theorem	xmsge0 24657	The distance function in an extended metric space is nonnegative. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑋 = (Base‘𝑀)    &   ⊢ 𝐷 = (dist‘𝑀)    ⇒   ⊢ ((𝑀 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝐵))
Theorem	xmseq0 24658	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 24659	The distance function in an extended metric space is symmetric. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑋 = (Base‘𝑀)    &   ⊢ 𝐷 = (dist‘𝑀)    ⇒   ⊢ ((𝑀 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴))
Theorem	xmstri2 24660	Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑋 = (Base‘𝑀)    &   ⊢ 𝐷 = (dist‘𝑀)    ⇒   ⊢ ((𝑀 ∈ ∞MetSp ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) +𝑒 (𝐶𝐷𝐵)))
Theorem	mstri2 24661	Triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑋 = (Base‘𝑀)    &   ⊢ 𝐷 = (dist‘𝑀)    ⇒   ⊢ ((𝑀 ∈ MetSp ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) + (𝐶𝐷𝐵)))
Theorem	xmstri 24662	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 24663	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 24664	Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑋 = (Base‘𝑀)    &   ⊢ 𝐷 = (dist‘𝑀)    ⇒   ⊢ ((𝑀 ∈ ∞MetSp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) +𝑒 (𝐵𝐷𝐶)))
Theorem	mstri3 24665	Triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑋 = (Base‘𝑀)    &   ⊢ 𝐷 = (dist‘𝑀)    ⇒   ⊢ ((𝑀 ∈ MetSp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) + (𝐵𝐷𝐶)))
Theorem	msrtri 24666	Reverse triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑋 = (Base‘𝑀)    &   ⊢ 𝐷 = (dist‘𝑀)    ⇒   ⊢ ((𝑀 ∈ MetSp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (abs‘((𝐴𝐷𝐶) − (𝐵𝐷𝐶))) ≤ (𝐴𝐷𝐵))
Theorem	xmspropd 24667	Property deduction for an extended metric space. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵)))    &   ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿))    ⇒   ⊢ (𝜑 → (𝐾 ∈ ∞MetSp ↔ 𝐿 ∈ ∞MetSp))
Theorem	mspropd 24668	Property deduction for a metric space. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵)))    &   ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿))    ⇒   ⊢ (𝜑 → (𝐾 ∈ MetSp ↔ 𝐿 ∈ MetSp))
Theorem	setsmsbas 24669	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	setsmsds 24670	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	setsmstset 24671	The topology of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ (𝜑 → 𝑋 = (Base‘𝑀))    &   ⊢ (𝜑 → 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋)))    &   ⊢ (𝜑 → 𝐾 = (𝑀 sSet ⟨(TopSet‘ndx), (MetOpen‘𝐷)⟩))    &   ⊢ (𝜑 → 𝑀 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (MetOpen‘𝐷) = (TopSet‘𝐾))
Theorem	setsmstopn 24672	The topology of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ (𝜑 → 𝑋 = (Base‘𝑀))    &   ⊢ (𝜑 → 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋)))    &   ⊢ (𝜑 → 𝐾 = (𝑀 sSet ⟨(TopSet‘ndx), (MetOpen‘𝐷)⟩))    &   ⊢ (𝜑 → 𝑀 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (MetOpen‘𝐷) = (TopOpen‘𝐾))
Theorem	setsxms 24673	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 24674	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 24675	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 24676	Lemma for tmsbas 24677, tmsds 24678, and tmstopn 24679. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝑀 = {⟨(Base‘ndx), 𝑋⟩, ⟨(dist‘ndx), 𝐷⟩}    &   ⊢ 𝐾 = (toMetSp‘𝐷)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑋 = (Base‘𝐾) ∧ 𝐷 = (dist‘𝐾) ∧ (MetOpen‘𝐷) = (TopOpen‘𝐾)))
Theorem	tmsbas 24677	The base set of a constructed metric space. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝐾 = (toMetSp‘𝐷)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = (Base‘𝐾))
Theorem	tmsds 24678	The metric of a constructed metric space. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝐾 = (toMetSp‘𝐷)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷 = (dist‘𝐾))
Theorem	tmstopn 24679	The topology of a constructed metric. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝐾 = (toMetSp‘𝐷)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 = (TopOpen‘𝐾))
Theorem	tmsxms 24680	The constructed metric space is an extended metric space. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝐾 = (toMetSp‘𝐷)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐾 ∈ ∞MetSp)
Theorem	tmsms 24681	The constructed metric space is a metric space given a metric. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝐾 = (toMetSp‘𝐷)    ⇒   ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐾 ∈ MetSp)
Theorem	imasf1obl 24682	The image of a metric space ball. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑍)    &   ⊢ 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉))    &   ⊢ 𝐷 = (dist‘𝑈)    &   ⊢ (𝜑 → 𝐸 ∈ (∞Met‘𝑉))    &   ⊢ (𝜑 → 𝑃 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ ℝ*)    ⇒   ⊢ (𝜑 → ((𝐹‘𝑃)(ball‘𝐷)𝑆) = (𝐹 “ (𝑃(ball‘𝐸)𝑆)))
Theorem	imasf1oxms 24683	The image of a metric space is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ ∞MetSp)    ⇒   ⊢ (𝜑 → 𝑈 ∈ ∞MetSp)
Theorem	imasf1oms 24684	The image of a metric space is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–1-1-onto→𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ MetSp)    ⇒   ⊢ (𝜑 → 𝑈 ∈ MetSp)
Theorem	prdsbl 24685*	A ball in the product metric for finite index set is the Cartesian product of balls in all coordinates. For infinite index set this is no longer true; instead the correct statement is that a *closed ball* is the product of closed balls in each coordinate (where closed ball means a set of the form in blcld 24699) - for a counterexample the point 𝑝 in ℝ↑ℕ whose 𝑛-th coordinate is 1 − 1 / 𝑛 is in X𝑛 ∈ ℕball(0, 1) but is not in the 1-ball of the product (since 𝑑(0, 𝑝) = 1). The last assumption, 0 < 𝐴, is needed only in the case 𝐼 = ∅, when the right side evaluates to {∅} and the left evaluates to ∅ if 𝐴 ≤ 0 and {∅} if 0 < 𝐴. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅))    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝑉 = (Base‘𝑅)    &   ⊢ 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉))    &   ⊢ 𝐷 = (dist‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ 𝑍)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐸 ∈ (∞Met‘𝑉))    &   ⊢ (𝜑 → 𝑃 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 0 < 𝐴)    ⇒   ⊢ (𝜑 → (𝑃(ball‘𝐷)𝐴) = X𝑥 ∈ 𝐼 ((𝑃‘𝑥)(ball‘𝐸)𝐴))
Theorem	mopni 24686*	An open set of a metric space includes a ball around each of its points. (Contributed by NM, 3-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝐽 ∧ 𝑃 ∈ 𝐴) → ∃𝑥 ∈ ran (ball‘𝐷)(𝑃 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴))
Theorem	mopni2 24687*	An open set of a metric space includes a ball around each of its points. (Contributed by NM, 2-May-2007.) (Revised by Mario Carneiro, 12-Nov-2013.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝐽 ∧ 𝑃 ∈ 𝐴) → ∃𝑥 ∈ ℝ+ (𝑃(ball‘𝐷)𝑥) ⊆ 𝐴)
Theorem	mopni3 24688*	An open set of a metric space includes an arbitrarily small ball around each of its points. (Contributed by NM, 20-Sep-2007.) (Revised by Mario Carneiro, 12-Nov-2013.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝐽 ∧ 𝑃 ∈ 𝐴) ∧ 𝑅 ∈ ℝ+) → ∃𝑥 ∈ ℝ+ (𝑥 < 𝑅 ∧ (𝑃(ball‘𝐷)𝑥) ⊆ 𝐴))
Theorem	blssopn 24689	The balls of a metric space are open sets. (Contributed by NM, 12-Sep-2006.) (Revised by Mario Carneiro, 23-Dec-2013.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → ran (ball‘𝐷) ⊆ 𝐽)
Theorem	unimopn 24690	The union of a collection of open sets of a metric space is open. Theorem T2 of [Kreyszig] p. 19. (Contributed by NM, 4-Sep-2006.) (Revised by Mario Carneiro, 23-Dec-2013.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ⊆ 𝐽) → ∪ 𝐴 ∈ 𝐽)
Theorem	mopnin 24691	The intersection of two open sets of a metric space is open. (Contributed by NM, 4-Sep-2006.) (Revised by Mario Carneiro, 23-Dec-2013.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽) → (𝐴 ∩ 𝐵) ∈ 𝐽)
Theorem	mopn0 24692	The empty set is an open set of a metric space. Part of Theorem T1 of [Kreyszig] p. 19. (Contributed by NM, 4-Sep-2006.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → ∅ ∈ 𝐽)
Theorem	rnblopn 24693	A ball of a metric space is an open set. (Contributed by NM, 12-Sep-2006.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ ran (ball‘𝐷)) → 𝐵 ∈ 𝐽)
Theorem	blopn 24694	A ball of a metric space is an open set. (Contributed by NM, 9-Mar-2007.) (Revised by Mario Carneiro, 12-Nov-2013.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) ∈ 𝐽)
Theorem	neibl 24695*	The neighborhoods around a point 𝑃 of a metric space are those subsets containing a ball around 𝑃. Definition of neighborhood in [Kreyszig] p. 19. (Contributed by NM, 8-Nov-2007.) (Revised by Mario Carneiro, 23-Dec-2013.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) ↔ (𝑁 ⊆ 𝑋 ∧ ∃𝑟 ∈ ℝ+ (𝑃(ball‘𝐷)𝑟) ⊆ 𝑁)))
Theorem	blnei 24696	A ball around a point is a neighborhood of the point. (Contributed by NM, 8-Nov-2007.) (Revised by Mario Carneiro, 24-Aug-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → (𝑃(ball‘𝐷)𝑅) ∈ ((nei‘𝐽)‘{𝑃}))
Theorem	lpbl 24697*	Every ball around a limit point 𝑃 of a subset 𝑆 includes a member of 𝑆 (even if 𝑃 ∉ 𝑆). (Contributed by NM, 9-Nov-2007.) (Revised by Mario Carneiro, 23-Dec-2013.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ((limPt‘𝐽)‘𝑆)) ∧ 𝑅 ∈ ℝ+) → ∃𝑥 ∈ 𝑆 𝑥 ∈ (𝑃(ball‘𝐷)𝑅))
Theorem	blsscls2 24698*	A smaller closed ball is contained in a larger open ball. (Contributed by Mario Carneiro, 10-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝑆 = {𝑧 ∈ 𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅}    ⇒   ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑇 ∈ ℝ* ∧ 𝑅 < 𝑇)) → 𝑆 ⊆ (𝑃(ball‘𝐷)𝑇))
Theorem	blcld 24699*	A "closed ball" in a metric space is actually closed. (Contributed by Mario Carneiro, 31-Dec-2013.) (Revised by Mario Carneiro, 24-Aug-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝑆 = {𝑧 ∈ 𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅}    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → 𝑆 ∈ (Clsd‘𝐽))
Theorem	blcls 24700*	The closure of an open ball in a metric space is contained in the corresponding closed ball. (Equality need not hold; for example, with the discrete metric, the closed ball of radius 1 is the whole space, but the open ball of radius 1 is just a point, whose closure is also a point.) (Contributed by Mario Carneiro, 31-Dec-2013.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝑆 = {𝑧 ∈ 𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅}    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) → ((cls‘𝐽)‘(𝑃(ball‘𝐷)𝑅)) ⊆ 𝑆)