P. 246 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 24501-24600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	xmstri3 24501	Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑋 = (Base‘𝑀)    &   ⊢ 𝐷 = (dist‘𝑀)    ⇒   ⊢ ((𝑀 ∈ ∞MetSp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) +𝑒 (𝐵𝐷𝐶)))
Theorem	mstri3 24502	Triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑋 = (Base‘𝑀)    &   ⊢ 𝐷 = (dist‘𝑀)    ⇒   ⊢ ((𝑀 ∈ MetSp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) + (𝐵𝐷𝐶)))
Theorem	msrtri 24503	Reverse triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝑋 = (Base‘𝑀)    &   ⊢ 𝐷 = (dist‘𝑀)    ⇒   ⊢ ((𝑀 ∈ MetSp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (abs‘((𝐴𝐷𝐶) − (𝐵𝐷𝐶))) ≤ (𝐴𝐷𝐵))
Theorem	xmspropd 24504	Property deduction for an extended metric space. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵)))    &   ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿))    ⇒   ⊢ (𝜑 → (𝐾 ∈ ∞MetSp ↔ 𝐿 ∈ ∞MetSp))
Theorem	mspropd 24505	Property deduction for a metric space. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵)))    &   ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿))    ⇒   ⊢ (𝜑 → (𝐾 ∈ MetSp ↔ 𝐿 ∈ MetSp))
Theorem	setsmsbas 24506	The base set of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) (Proof shortened by AV, 12-Nov-2024.)
⊢ (𝜑 → 𝑋 = (Base‘𝑀))    &   ⊢ (𝜑 → 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋)))    &   ⊢ (𝜑 → 𝐾 = (𝑀 sSet ⟨(TopSet‘ndx), (MetOpen‘𝐷)⟩))    ⇒   ⊢ (𝜑 → 𝑋 = (Base‘𝐾))
Theorem	setsmsbasOLD 24507	Obsolete proof of setsmsbas 24506 as of 12-Nov-2024. The base set of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝑋 = (Base‘𝑀))    &   ⊢ (𝜑 → 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋)))    &   ⊢ (𝜑 → 𝐾 = (𝑀 sSet ⟨(TopSet‘ndx), (MetOpen‘𝐷)⟩))    ⇒   ⊢ (𝜑 → 𝑋 = (Base‘𝐾))
Theorem	setsmsds 24508	The distance function of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) (Proof shortened by AV, 11-Nov-2024.)
⊢ (𝜑 → 𝑋 = (Base‘𝑀))    &   ⊢ (𝜑 → 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋)))    &   ⊢ (𝜑 → 𝐾 = (𝑀 sSet ⟨(TopSet‘ndx), (MetOpen‘𝐷)⟩))    ⇒   ⊢ (𝜑 → (dist‘𝑀) = (dist‘𝐾))
Theorem	setsmsdsOLD 24509	Obsolete proof of setsmsds 24508 as of 11-Nov-2024. The distance function of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝑋 = (Base‘𝑀))    &   ⊢ (𝜑 → 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋)))    &   ⊢ (𝜑 → 𝐾 = (𝑀 sSet ⟨(TopSet‘ndx), (MetOpen‘𝐷)⟩))    ⇒   ⊢ (𝜑 → (dist‘𝑀) = (dist‘𝐾))
Theorem	setsmstset 24510	The topology of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ (𝜑 → 𝑋 = (Base‘𝑀))    &   ⊢ (𝜑 → 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋)))    &   ⊢ (𝜑 → 𝐾 = (𝑀 sSet ⟨(TopSet‘ndx), (MetOpen‘𝐷)⟩))    &   ⊢ (𝜑 → 𝑀 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (MetOpen‘𝐷) = (TopSet‘𝐾))
Theorem	setsmstopn 24511	The topology of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ (𝜑 → 𝑋 = (Base‘𝑀))    &   ⊢ (𝜑 → 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋)))    &   ⊢ (𝜑 → 𝐾 = (𝑀 sSet ⟨(TopSet‘ndx), (MetOpen‘𝐷)⟩))    &   ⊢ (𝜑 → 𝑀 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (MetOpen‘𝐷) = (TopOpen‘𝐾))
Theorem	setsxms 24512	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 24513	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 24514	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 24515	Lemma for tmsbas 24517, tmsds 24518, and tmstopn 24519. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝑀 = {⟨(Base‘ndx), 𝑋⟩, ⟨(dist‘ndx), 𝐷⟩}    &   ⊢ 𝐾 = (toMetSp‘𝐷)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑋 = (Base‘𝐾) ∧ 𝐷 = (dist‘𝐾) ∧ (MetOpen‘𝐷) = (TopOpen‘𝐾)))
Theorem	tmslemOLD 24516	Obsolete version of tmslem 24515 as of 28-Oct-2024. Lemma for tmsbas 24517, tmsds 24518, and tmstopn 24519. (Contributed by Mario Carneiro, 2-Sep-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑀 = {⟨(Base‘ndx), 𝑋⟩, ⟨(dist‘ndx), 𝐷⟩}    &   ⊢ 𝐾 = (toMetSp‘𝐷)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝑋 = (Base‘𝐾) ∧ 𝐷 = (dist‘𝐾) ∧ (MetOpen‘𝐷) = (TopOpen‘𝐾)))
Theorem	tmsbas 24517	The base set of a constructed metric space. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝐾 = (toMetSp‘𝐷)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = (Base‘𝐾))
Theorem	tmsds 24518	The metric of a constructed metric space. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝐾 = (toMetSp‘𝐷)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷 = (dist‘𝐾))
Theorem	tmstopn 24519	The topology of a constructed metric. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝐾 = (toMetSp‘𝐷)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 = (TopOpen‘𝐾))
Theorem	tmsxms 24520	The constructed metric space is an extended metric space. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝐾 = (toMetSp‘𝐷)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐾 ∈ ∞MetSp)
Theorem	tmsms 24521	The constructed metric space is a metric space given a metric. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝐾 = (toMetSp‘𝐷)    ⇒   ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐾 ∈ MetSp)
Theorem	imasf1obl 24522	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 24523	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 24524	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 24525*	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 24539) - 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 24526*	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 24527*	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 24528*	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 24529	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 24530	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 24531	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 24532	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 24533	A ball of a metric space is an open set. (Contributed by NM, 12-Sep-2006.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ ran (ball‘𝐷)) → 𝐵 ∈ 𝐽)
Theorem	blopn 24534	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 24535*	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 24536	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 24537*	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 24538*	A smaller closed ball is contained in a larger open ball. (Contributed by Mario Carneiro, 10-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝑆 = {𝑧 ∈ 𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅}    ⇒   ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑇 ∈ ℝ* ∧ 𝑅 < 𝑇)) → 𝑆 ⊆ (𝑃(ball‘𝐷)𝑇))
Theorem	blcld 24539*	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 24540*	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‘𝐷)𝑅)) ⊆ 𝑆)
Theorem	blsscls 24541	If two concentric balls have different radii, the closure of the smaller one is contained in the larger one. (Contributed by Mario Carneiro, 5-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ 𝑅 < 𝑆)) → ((cls‘𝐽)‘(𝑃(ball‘𝐷)𝑅)) ⊆ (𝑃(ball‘𝐷)𝑆))
Theorem	metss 24542*	Two ways of saying that metric 𝐷 generates a finer topology than metric 𝐶. (Contributed by Mario Carneiro, 12-Nov-2013.) (Revised by Mario Carneiro, 24-Aug-2015.)
⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) → (𝐽 ⊆ 𝐾 ↔ ∀𝑥 ∈ 𝑋 ∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟)))
Theorem	metequiv 24543*	Two ways of saying that two metrics generate the same topology. Two metrics satisfying the right-hand side are said to be (topologically) equivalent. (Contributed by Jeff Hankins, 21-Jun-2009.) (Revised by Mario Carneiro, 12-Nov-2013.)
⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) → (𝐽 = 𝐾 ↔ ∀𝑥 ∈ 𝑋 (∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+ (𝑥(ball‘𝐷)𝑠) ⊆ (𝑥(ball‘𝐶)𝑟) ∧ ∀𝑎 ∈ ℝ+ ∃𝑏 ∈ ℝ+ (𝑥(ball‘𝐶)𝑏) ⊆ (𝑥(ball‘𝐷)𝑎))))
Theorem	metequiv2 24544*	If there is a sequence of radii approaching zero for which the balls of both metrics coincide, then the generated topologies are equivalent. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑋)) → (∀𝑥 ∈ 𝑋 ∀𝑟 ∈ ℝ+ ∃𝑠 ∈ ℝ+ (𝑠 ≤ 𝑟 ∧ (𝑥(ball‘𝐶)𝑠) = (𝑥(ball‘𝐷)𝑠)) → 𝐽 = 𝐾))
Theorem	metss2lem 24545*	Lemma for metss2 24546. (Contributed by Mario Carneiro, 14-Sep-2015.)
⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐶𝑦) ≤ (𝑅 · (𝑥𝐷𝑦)))    ⇒   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) → (𝑥(ball‘𝐷)(𝑆 / 𝑅)) ⊆ (𝑥(ball‘𝐶)𝑆))
Theorem	metss2 24546*	If the metric 𝐷 is "strongly finer" than 𝐶 (meaning that there is a positive real constant 𝑅 such that 𝐶(𝑥, 𝑦) ≤ 𝑅 · 𝐷(𝑥, 𝑦)), then 𝐷 generates a finer topology. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then they generate the same topology.) (Contributed by Mario Carneiro, 14-Sep-2015.)
⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐶𝑦) ≤ (𝑅 · (𝑥𝐷𝑦)))    ⇒   ⊢ (𝜑 → 𝐽 ⊆ 𝐾)
Theorem	comet 24547*	The composition of an extended metric with a monotonic subadditive function is an extended metric. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝐹:(0[,]+∞)⟶ℝ*)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞)) → ((𝐹‘𝑥) = 0 ↔ 𝑥 = 0))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞))) → (𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦)))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞))) → (𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦)))    ⇒   ⊢ (𝜑 → (𝐹 ∘ 𝐷) ∈ (∞Met‘𝑋))
Theorem	stdbdmetval 24548*	Value of the standard bounded metric. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ if((𝑥𝐶𝑦) ≤ 𝑅, (𝑥𝐶𝑦), 𝑅))    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = if((𝐴𝐶𝐵) ≤ 𝑅, (𝐴𝐶𝐵), 𝑅))
Theorem	stdbdxmet 24549*	The standard bounded metric is an extended metric given an extended metric and a positive extended real cutoff. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ if((𝑥𝐶𝑦) ≤ 𝑅, (𝑥𝐶𝑦), 𝑅))    ⇒   ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) → 𝐷 ∈ (∞Met‘𝑋))
Theorem	stdbdmet 24550*	The standard bounded metric is a proper metric given an extended metric and a positive real cutoff. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ if((𝑥𝐶𝑦) ≤ 𝑅, (𝑥𝐶𝑦), 𝑅))    ⇒   ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ+) → 𝐷 ∈ (Met‘𝑋))
Theorem	stdbdbl 24551*	The standard bounded metric corresponding to 𝐶 generates the same balls as 𝐶 for radii less than 𝑅. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ if((𝑥𝐶𝑦) ≤ 𝑅, (𝑥𝐶𝑦), 𝑅))    ⇒   ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) ∧ (𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ* ∧ 𝑆 ≤ 𝑅)) → (𝑃(ball‘𝐷)𝑆) = (𝑃(ball‘𝐶)𝑆))
Theorem	stdbdmopn 24552*	The standard bounded metric corresponding to 𝐶 generates the same topology as 𝐶. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ if((𝑥𝐶𝑦) ≤ 𝑅, (𝑥𝐶𝑦), 𝑅))    &   ⊢ 𝐽 = (MetOpen‘𝐶)    ⇒   ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 < 𝑅) → 𝐽 = (MetOpen‘𝐷))
Theorem	mopnex 24553*	The topology generated by an extended metric can also be generated by a true metric. Thus, "metrizable topologies" can equivalently be defined in terms of metrics or extended metrics. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → ∃𝑑 ∈ (Met‘𝑋)𝐽 = (MetOpen‘𝑑))
Theorem	methaus 24554	The topology generated by a metric space is Hausdorff. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 26-Aug-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Haus)
Theorem	met1stc 24555	The topology generated by a metric space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ 1stω)
Theorem	met2ndci 24556	A separable metric space (a metric space with a countable dense subset) is second-countable. (Contributed by Mario Carneiro, 13-Apr-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐴 ≼ ω ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → 𝐽 ∈ 2ndω)
Theorem	met2ndc 24557*	A metric space is second-countable iff it is separable (has a countable dense subset). (Contributed by Mario Carneiro, 13-Apr-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐽 ∈ 2ndω ↔ ∃𝑥 ∈ 𝒫 𝑋(𝑥 ≼ ω ∧ ((cls‘𝐽)‘𝑥) = 𝑋)))
Theorem	metrest 24558	Two alternate formulations of a subspace topology of a metric space topology. (Contributed by Jeff Hankins, 19-Aug-2009.) (Proof shortened by Mario Carneiro, 5-Jan-2014.)
⊢ 𝐷 = (𝐶 ↾ (𝑌 × 𝑌))    &   ⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑌 ⊆ 𝑋) → (𝐽 ↾t 𝑌) = 𝐾)
Theorem	ressxms 24559	The restriction of a metric space is a metric space. (Contributed by Mario Carneiro, 24-Aug-2015.)
⊢ ((𝐾 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑉) → (𝐾 ↾s 𝐴) ∈ ∞MetSp)
Theorem	ressms 24560	The restriction of a metric space is a metric space. (Contributed by Mario Carneiro, 24-Aug-2015.)
⊢ ((𝐾 ∈ MetSp ∧ 𝐴 ∈ 𝑉) → (𝐾 ↾s 𝐴) ∈ MetSp)
Theorem	prdsmslem1 24561	Lemma for prdsms 24565. The distance function of a product structure is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ 𝐷 = (dist‘𝑌)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑅:𝐼⟶MetSp)    ⇒   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝐵))
Theorem	prdsxmslem1 24562	Lemma for prdsms 24565. The distance function of a product structure is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ 𝐷 = (dist‘𝑌)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑅:𝐼⟶∞MetSp)    ⇒   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝐵))
Theorem	prdsxmslem2 24563*	Lemma for prdsxms 24564. The topology generated by the supremum metric is the same as the product topology, when the index set is finite. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ 𝐷 = (dist‘𝑌)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝑅:𝐼⟶∞MetSp)    &   ⊢ 𝐽 = (TopOpen‘𝑌)    &   ⊢ 𝑉 = (Base‘(𝑅‘𝑘))    &   ⊢ 𝐸 = ((dist‘(𝑅‘𝑘)) ↾ (𝑉 × 𝑉))    &   ⊢ 𝐾 = (TopOpen‘(𝑅‘𝑘))    &   ⊢ 𝐶 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑘 ∈ 𝐼 (𝑔‘𝑘) ∈ ((TopOpen ∘ 𝑅)‘𝑘) ∧ ∃𝑧 ∈ Fin ∀𝑘 ∈ (𝐼 ∖ 𝑧)(𝑔‘𝑘) = ∪ ((TopOpen ∘ 𝑅)‘𝑘)) ∧ 𝑥 = X𝑘 ∈ 𝐼 (𝑔‘𝑘))}    ⇒   ⊢ (𝜑 → 𝐽 = (MetOpen‘𝐷))
Theorem	prdsxms 24564	The indexed product structure is an extended metric space when the index set is finite. (Although the extended metric is still valid when the index set is infinite, it no longer agrees with the product topology, which is not metrizable in any case.) (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    ⇒   ⊢ ((𝑆 ∈ 𝑊 ∧ 𝐼 ∈ Fin ∧ 𝑅:𝐼⟶∞MetSp) → 𝑌 ∈ ∞MetSp)
Theorem	prdsms 24565	The indexed product structure is a metric space when the index set is finite. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    ⇒   ⊢ ((𝑆 ∈ 𝑊 ∧ 𝐼 ∈ Fin ∧ 𝑅:𝐼⟶MetSp) → 𝑌 ∈ MetSp)
Theorem	pwsxms 24566	A power of an extended metric space is an extended metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    ⇒   ⊢ ((𝑅 ∈ ∞MetSp ∧ 𝐼 ∈ Fin) → 𝑌 ∈ ∞MetSp)
Theorem	pwsms 24567	A power of a metric space is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    ⇒   ⊢ ((𝑅 ∈ MetSp ∧ 𝐼 ∈ Fin) → 𝑌 ∈ MetSp)
Theorem	xpsxms 24568	A binary product of metric spaces is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ 𝑇 = (𝑅 ×s 𝑆)    ⇒   ⊢ ((𝑅 ∈ ∞MetSp ∧ 𝑆 ∈ ∞MetSp) → 𝑇 ∈ ∞MetSp)
Theorem	xpsms 24569	A binary product of metric spaces is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ 𝑇 = (𝑅 ×s 𝑆)    ⇒   ⊢ ((𝑅 ∈ MetSp ∧ 𝑆 ∈ MetSp) → 𝑇 ∈ MetSp)
Theorem	tmsxps 24570	Express the product of two metrics as another metric. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝑃 = (dist‘((toMetSp‘𝑀) ×s (toMetSp‘𝑁)))    &   ⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌))    ⇒   ⊢ (𝜑 → 𝑃 ∈ (∞Met‘(𝑋 × 𝑌)))
Theorem	tmsxpsmopn 24571	Express the product of two metrics as another metric. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝑃 = (dist‘((toMetSp‘𝑀) ×s (toMetSp‘𝑁)))    &   ⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌))    &   ⊢ 𝐽 = (MetOpen‘𝑀)    &   ⊢ 𝐾 = (MetOpen‘𝑁)    &   ⊢ 𝐿 = (MetOpen‘𝑃)    ⇒   ⊢ (𝜑 → 𝐿 = (𝐽 ×t 𝐾))
Theorem	tmsxpsval 24572	Value of the product of two metrics. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝑃 = (dist‘((toMetSp‘𝑀) ×s (toMetSp‘𝑁)))    &   ⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑌)    ⇒   ⊢ (𝜑 → (⟨𝐴, 𝐵⟩𝑃⟨𝐶, 𝐷⟩) = sup({(𝐴𝑀𝐶), (𝐵𝑁𝐷)}, ℝ*, < ))
Theorem	tmsxpsval2 24573	Value of the product of two metrics. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝑃 = (dist‘((toMetSp‘𝑀) ×s (toMetSp‘𝑁)))    &   ⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑌)    ⇒   ⊢ (𝜑 → (⟨𝐴, 𝐵⟩𝑃⟨𝐶, 𝐷⟩) = if((𝐴𝑀𝐶) ≤ (𝐵𝑁𝐷), (𝐵𝑁𝐷), (𝐴𝑀𝐶)))
12.4.5  Continuity in metric spaces
Theorem	metcnp3 24574*	Two ways to express that 𝐹 is continuous at 𝑃 for metric spaces. Proposition 14-4.2 of [Gleason] p. 240. (Contributed by NM, 17-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌) ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ (𝐹 “ (𝑃(ball‘𝐶)𝑧)) ⊆ ((𝐹‘𝑃)(ball‘𝐷)𝑦))))
Theorem	metcnp 24575*	Two ways to say a mapping from metric 𝐶 to metric 𝐷 is continuous at point 𝑃. (Contributed by NM, 11-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌) ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝑋 ((𝑃𝐶𝑤) < 𝑧 → ((𝐹‘𝑃)𝐷(𝐹‘𝑤)) < 𝑦))))
Theorem	metcnp2 24576*	Two ways to say a mapping from metric 𝐶 to metric 𝐷 is continuous at point 𝑃. The distance arguments are swapped compared to metcnp 24575 (and Munkres' metcn 24577) for compatibility with df-lm 23258. Definition 1.3-3 of [Kreyszig] p. 20. (Contributed by NM, 4-Jun-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌) ∧ 𝑃 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝑋 ((𝑤𝐶𝑃) < 𝑧 → ((𝐹‘𝑤)𝐷(𝐹‘𝑃)) < 𝑦))))
Theorem	metcn 24577*	Two ways to say a mapping from metric 𝐶 to metric 𝐷 is continuous. Theorem 10.1 of [Munkres] p. 127. The second biconditional argument says that for every positive "epsilon" 𝑦 there is a positive "delta" 𝑧 such that a distance less than delta in 𝐶 maps to a distance less than epsilon in 𝐷. (Contributed by NM, 15-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝑋 ((𝑥𝐶𝑤) < 𝑧 → ((𝐹‘𝑥)𝐷(𝐹‘𝑤)) < 𝑦))))
Theorem	metcnpi 24578*	Epsilon-delta property of a continuous metric space function, with function arguments as in metcnp 24575. (Contributed by NM, 17-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    ⇒   ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌)) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐴 ∈ ℝ+)) → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝑋 ((𝑃𝐶𝑦) < 𝑥 → ((𝐹‘𝑃)𝐷(𝐹‘𝑦)) < 𝐴))
Theorem	metcnpi2 24579*	Epsilon-delta property of a continuous metric space function, with swapped distance function arguments as in metcnp2 24576. (Contributed by NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    ⇒   ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌)) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐴 ∈ ℝ+)) → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝑋 ((𝑦𝐶𝑃) < 𝑥 → ((𝐹‘𝑦)𝐷(𝐹‘𝑃)) < 𝐴))
Theorem	metcnpi3 24580*	Epsilon-delta property of a metric space function continuous at 𝑃. A variation of metcnpi2 24579 with non-strict ordering. (Contributed by NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    ⇒   ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌)) ∧ (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ∧ 𝐴 ∈ ℝ+)) → ∃𝑥 ∈ ℝ+ ∀𝑦 ∈ 𝑋 ((𝑦𝐶𝑃) ≤ 𝑥 → ((𝐹‘𝑦)𝐷(𝐹‘𝑃)) ≤ 𝐴))
Theorem	txmetcnp 24581*	Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    &   ⊢ 𝐿 = (MetOpen‘𝐸)    ⇒   ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌) ∧ 𝐸 ∈ (∞Met‘𝑍)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌)) → (𝐹 ∈ (((𝐽 ×t 𝐾) CnP 𝐿)‘⟨𝐴, 𝐵⟩) ↔ (𝐹:(𝑋 × 𝑌)⟶𝑍 ∧ ∀𝑧 ∈ ℝ+ ∃𝑤 ∈ ℝ+ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑌 (((𝐴𝐶𝑢) < 𝑤 ∧ (𝐵𝐷𝑣) < 𝑤) → ((𝐴𝐹𝐵)𝐸(𝑢𝐹𝑣)) < 𝑧))))
Theorem	txmetcn 24582*	Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    &   ⊢ 𝐿 = (MetOpen‘𝐸)    ⇒   ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝐷 ∈ (∞Met‘𝑌) ∧ 𝐸 ∈ (∞Met‘𝑍)) → (𝐹 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ↔ (𝐹:(𝑋 × 𝑌)⟶𝑍 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ∀𝑧 ∈ ℝ+ ∃𝑤 ∈ ℝ+ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑌 (((𝑥𝐶𝑢) < 𝑤 ∧ (𝑦𝐷𝑣) < 𝑤) → ((𝑥𝐹𝑦)𝐸(𝑢𝐹𝑣)) < 𝑧))))
12.4.6  The uniform structure generated by a metric
Theorem	metuval 24583*	Value of the uniform structure generated by metric 𝐷. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ (𝐷 ∈ (PsMet‘𝑋) → (metUnif‘𝐷) = ((𝑋 × 𝑋)filGenran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))))
Theorem	metustel 24584*	Define a filter base 𝐹 generated by a metric 𝐷. (Contributed by Thierry Arnoux, 22-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))    ⇒   ⊢ (𝐷 ∈ (PsMet‘𝑋) → (𝐵 ∈ 𝐹 ↔ ∃𝑎 ∈ ℝ+ 𝐵 = (◡𝐷 “ (0[,)𝑎))))
Theorem	metustss 24585*	Range of the elements of the filter base generated by the metric 𝐷. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))    ⇒   ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) → 𝐴 ⊆ (𝑋 × 𝑋))
Theorem	metustrel 24586*	Elements of the filter base generated by the metric 𝐷 are relations. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))    ⇒   ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) → Rel 𝐴)
Theorem	metustto 24587*	Any two elements of the filter base generated by the metric 𝐷 can be compared, like for RR+ (i.e. it's totally ordered). (Contributed by Thierry Arnoux, 22-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))    ⇒   ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐹) → (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴))
Theorem	metustid 24588*	The identity diagonal is included in all elements of the filter base generated by the metric 𝐷. (Contributed by Thierry Arnoux, 22-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))    ⇒   ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) → ( I ↾ 𝑋) ⊆ 𝐴)
Theorem	metustsym 24589*	Elements of the filter base generated by the metric 𝐷 are symmetric. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))    ⇒   ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝐹) → ◡𝐴 = 𝐴)
Theorem	metustexhalf 24590*	For any element 𝐴 of the filter base generated by the metric 𝐷, the half element (corresponding to half the distance) is also in this base. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))    ⇒   ⊢ (((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) ∧ 𝐴 ∈ 𝐹) → ∃𝑣 ∈ 𝐹 (𝑣 ∘ 𝑣) ⊆ 𝐴)
Theorem	metustfbas 24591*	The filter base generated by a metric 𝐷. (Contributed by Thierry Arnoux, 26-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) (Proof shortened by Peter Mazsa, 2-Oct-2022.)
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))    ⇒   ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → 𝐹 ∈ (fBas‘(𝑋 × 𝑋)))
Theorem	metust 24592*	The uniform structure generated by a metric 𝐷. (Contributed by Thierry Arnoux, 26-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))    ⇒   ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → ((𝑋 × 𝑋)filGen𝐹) ∈ (UnifOn‘𝑋))
Theorem	cfilucfil 24593*	Given a metric 𝐷 and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the filter bases which contain balls of any pre-chosen size. See iscfil 25318. (Contributed by Thierry Arnoux, 29-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ 𝐹 = ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))    ⇒   ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐶 ∈ (CauFilu‘((𝑋 × 𝑋)filGen𝐹)) ↔ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))))
Theorem	metuust 24594	The uniform structure generated by metric 𝐷 is a uniform structure. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (metUnif‘𝐷) ∈ (UnifOn‘𝑋))
Theorem	cfilucfil2 24595*	Given a metric 𝐷 and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the filter bases which contain balls of any pre-chosen size. See iscfil 25318. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝐶 ∈ (CauFilu‘(metUnif‘𝐷)) ↔ (𝐶 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐶 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))))
Theorem	blval2 24596	The ball around a point 𝑃, alternative definition. (Contributed by Thierry Arnoux, 7-Dec-2017.) (Revised by Thierry Arnoux, 11-Mar-2018.)
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → (𝑃(ball‘𝐷)𝑅) = ((◡𝐷 “ (0[,)𝑅)) “ {𝑃}))
Theorem	elbl4 24597	Membership in a ball, alternative definition. (Contributed by Thierry Arnoux, 26-Jan-2018.) (Revised by Thierry Arnoux, 11-Mar-2018.)
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ∈ ℝ+) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐵 ∈ (𝐴(ball‘𝐷)𝑅) ↔ 𝐵(◡𝐷 “ (0[,)𝑅))𝐴))
Theorem	metuel 24598*	Elementhood in the uniform structure generated by a metric 𝐷 (Contributed by Thierry Arnoux, 8-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝑉 ∈ (metUnif‘𝐷) ↔ (𝑉 ⊆ (𝑋 × 𝑋) ∧ ∃𝑤 ∈ ran (𝑎 ∈ ℝ+ ↦ (◡𝐷 “ (0[,)𝑎)))𝑤 ⊆ 𝑉)))
Theorem	metuel2 24599*	Elementhood in the uniform structure generated by a metric 𝐷 (Contributed by Thierry Arnoux, 24-Jan-2018.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ 𝑈 = (metUnif‘𝐷)    ⇒   ⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (PsMet‘𝑋)) → (𝑉 ∈ 𝑈 ↔ (𝑉 ⊆ (𝑋 × 𝑋) ∧ ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥𝐷𝑦) < 𝑑 → 𝑥𝑉𝑦))))
Theorem	metustbl 24600*	The "section" image of an entourage at a point 𝑃 always contains a ball (centered on this point). (Contributed by Thierry Arnoux, 8-Dec-2017.)
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑉 ∈ (metUnif‘𝐷) ∧ 𝑃 ∈ 𝑋) → ∃𝑎 ∈ ran (ball‘𝐷)(𝑃 ∈ 𝑎 ∧ 𝑎 ⊆ (𝑉 “ {𝑃})))