Theorem List for Intuitionistic Logic Explorer - 13201-13300 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | blss2 13201 |
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 13202 |
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 13203 |
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 13204 |
Mapping of a ball. (Contributed by NM, 7-May-2007.) (Revised by Mario
Carneiro, 23-Aug-2015.)
|
⊢ (𝐷 ∈ (∞Met‘𝑋) → (ball‘𝐷):(𝑋 ×
ℝ*)⟶𝒫 𝑋) |
|
Theorem | blrnps 13205* |
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 13206* |
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 13207 |
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 13208 |
A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised
by Mario Carneiro, 12-Nov-2013.)
|
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ (𝑅 ∈ ℝ* ∧ 0 <
𝑅)) → 𝑃 ∈ (𝑃(ball‘𝐷)𝑅)) |
|
Theorem | blcntrps 13209 |
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 13210 |
A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised
by Mario Carneiro, 12-Nov-2013.)
|
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → 𝑃 ∈ (𝑃(ball‘𝐷)𝑅)) |
|
Theorem | xblm 13211* |
A ball is inhabited iff the radius is positive. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ*) →
(∃𝑥 𝑥 ∈ (𝑃(ball‘𝐷)𝑅) ↔ 0 < 𝑅)) |
|
Theorem | bln0 13212 |
A ball is not empty. It is also inhabited, as seen at blcntr 13210.
(Contributed by NM, 6-Oct-2007.) (Revised by Mario Carneiro,
12-Nov-2013.)
|
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+) → (𝑃(ball‘𝐷)𝑅) ≠ ∅) |
|
Theorem | blelrnps 13213 |
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 13214 |
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 13215 |
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 13216 |
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 13217 |
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 13218 |
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 13219 |
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 13220 |
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 13221* |
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 13222* |
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 13223* |
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 13224* |
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 13225* |
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 13226* |
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 13227 |
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 13228 |
A ball in a restricted metric space. (Contributed by Mario Carneiro,
5-Jan-2014.)
|
⊢ 𝐶 = (𝐷 ↾ (𝑌 × 𝑌)) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ (𝑋 ∩ 𝑌) ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐶)𝑅) = ((𝑃(ball‘𝐷)𝑅) ∩ 𝑌)) |
|
Theorem | xmeterval 13229 |
Value of the "finitely separated" relation. (Contributed by Mario
Carneiro, 24-Aug-2015.)
|
⊢ ∼ = (◡𝐷 “ ℝ)
⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐴 ∼ 𝐵 ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (𝐴𝐷𝐵) ∈ ℝ))) |
|
Theorem | xmeter 13230 |
The "finitely separated" relation is an equivalence relation.
(Contributed by Mario Carneiro, 24-Aug-2015.)
|
⊢ ∼ = (◡𝐷 “ ℝ)
⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → ∼ Er 𝑋) |
|
Theorem | xmetec 13231 |
The equivalence classes under the finite separation equivalence relation
are infinity balls. (Contributed by Mario Carneiro, 24-Aug-2015.)
|
⊢ ∼ = (◡𝐷 “ ℝ)
⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) → [𝑃] ∼ = (𝑃(ball‘𝐷)+∞)) |
|
Theorem | blssec 13232 |
A ball centered at 𝑃 is contained in the set of points
finitely
separated from 𝑃. This is just an application of ssbl 13220
to the
infinity ball. (Contributed by Mario Carneiro, 24-Aug-2015.)
|
⊢ ∼ = (◡𝐷 “ ℝ)
⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑆) ⊆ [𝑃] ∼ ) |
|
Theorem | blpnfctr 13233 |
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 13234 |
An extended metric restricted to any ball (in particular the infinity
ball) is a proper metric. Together with xmetec 13231, 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‘𝐵)) |
|
8.2.4 Open sets of a metric space
|
|
Theorem | mopnrel 13235 |
The class of open sets of a metric space is a relation. (Contributed by
Jim Kingdon, 5-May-2023.)
|
⊢ Rel MetOpen |
|
Theorem | mopnval 13236 |
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 13238, the open sets of a
metric space form a topology 𝐽, whose base set is ∪ 𝐽 by
mopnuni 13239. (Contributed by NM, 1-Sep-2006.) (Revised
by Mario
Carneiro, 12-Nov-2013.)
|
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 = (topGen‘ran (ball‘𝐷))) |
|
Theorem | mopntopon 13237 |
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 13238 |
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 13239 |
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 13240* |
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 13241 |
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 13242 |
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 13243* |
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 13244 |
An open set of a metric space is a subspace of its base set.
(Contributed by NM, 3-Sep-2006.)
|
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝑋) |
|
Theorem | isxms 13245 |
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 13246 |
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 13247 |
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 13248 |
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 13249 |
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 13250 |
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 13251 |
An extended metric space is a topological space. (Contributed by Mario
Carneiro, 26-Aug-2015.)
|
⊢ (𝑀 ∈ ∞MetSp → 𝑀 ∈ TopSp) |
|
Theorem | msxms 13252 |
A metric space is an extended metric space. (Contributed by Mario
Carneiro, 26-Aug-2015.)
|
⊢ (𝑀 ∈ MetSp → 𝑀 ∈ ∞MetSp) |
|
Theorem | mstps 13253 |
A metric space is a topological space. (Contributed by Mario Carneiro,
26-Aug-2015.)
|
⊢ (𝑀 ∈ MetSp → 𝑀 ∈ TopSp) |
|
Theorem | xmsxmet 13254 |
The distance function, suitably truncated, is an extended metric on
𝑋. (Contributed by Mario Carneiro,
2-Sep-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝑀 ∈ ∞MetSp → 𝐷 ∈ (∞Met‘𝑋)) |
|
Theorem | msmet 13255 |
The distance function, suitably truncated, is a metric on 𝑋.
(Contributed by Mario Carneiro, 12-Nov-2013.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝑀 ∈ MetSp → 𝐷 ∈ (Met‘𝑋)) |
|
Theorem | msf 13256 |
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 13257 |
The distance function, suitably truncated, is an extended metric on
𝑋. (Contributed by Mario Carneiro,
2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ (𝑀 ∈ ∞MetSp → (𝐷 ↾ (𝑋 × 𝑋)) ∈ (∞Met‘𝑋)) |
|
Theorem | msmet2 13258 |
The distance function, suitably truncated, is a metric on 𝑋.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ (𝑀 ∈ MetSp → (𝐷 ↾ (𝑋 × 𝑋)) ∈ (Met‘𝑋)) |
|
Theorem | mscl 13259 |
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 13260 |
Closure of the distance function of an extended metric space.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈
ℝ*) |
|
Theorem | xmsge0 13261 |
The distance function in an extended metric space is nonnegative.
(Contributed by Mario Carneiro, 4-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 0 ≤ (𝐴𝐷𝐵)) |
|
Theorem | xmseq0 13262 |
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 13263 |
The distance function in an extended metric space is symmetric.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ ∞MetSp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴)) |
|
Theorem | xmstri2 13264 |
Triangle inequality for the distance function of an extended metric.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ ∞MetSp ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) +𝑒 (𝐶𝐷𝐵))) |
|
Theorem | mstri2 13265 |
Triangle inequality for the distance function of a metric space.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ MetSp ∧ (𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐶𝐷𝐴) + (𝐶𝐷𝐵))) |
|
Theorem | xmstri 13266 |
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 13267 |
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 13268 |
Triangle inequality for the distance function of an extended metric.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ ∞MetSp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) +𝑒 (𝐵𝐷𝐶))) |
|
Theorem | mstri3 13269 |
Triangle inequality for the distance function of a metric space.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ MetSp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐷𝐵) ≤ ((𝐴𝐷𝐶) + (𝐵𝐷𝐶))) |
|
Theorem | msrtri 13270 |
Reverse triangle inequality for the distance function of a metric space.
(Contributed by Mario Carneiro, 4-Oct-2015.)
|
⊢ 𝑋 = (Base‘𝑀)
& ⊢ 𝐷 = (dist‘𝑀) ⇒ ⊢ ((𝑀 ∈ MetSp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (abs‘((𝐴𝐷𝐶) − (𝐵𝐷𝐶))) ≤ (𝐴𝐷𝐵)) |
|
Theorem | xmspropd 13271 |
Property deduction for an extended metric space. (Contributed by Mario
Carneiro, 4-Oct-2015.)
|
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵))) & ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿))
⇒ ⊢ (𝜑 → (𝐾 ∈ ∞MetSp ↔ 𝐿 ∈
∞MetSp)) |
|
Theorem | mspropd 13272 |
Property deduction for a metric space. (Contributed by Mario Carneiro,
4-Oct-2015.)
|
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵))) & ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿))
⇒ ⊢ (𝜑 → (𝐾 ∈ MetSp ↔ 𝐿 ∈ MetSp)) |
|
Theorem | setsmsbasg 13273 |
The base set of a constructed metric space. (Contributed by Mario
Carneiro, 28-Aug-2015.)
|
⊢ (𝜑 → 𝑋 = (Base‘𝑀)) & ⊢ (𝜑 → 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋))) & ⊢ (𝜑 → 𝐾 = (𝑀 sSet 〈(TopSet‘ndx),
(MetOpen‘𝐷)〉)) & ⊢ (𝜑 → 𝑀 ∈ 𝑉)
& ⊢ (𝜑 → (MetOpen‘𝐷) ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝑋 = (Base‘𝐾)) |
|
Theorem | setsmsdsg 13274 |
The distance function of a constructed metric space. (Contributed by
Mario Carneiro, 28-Aug-2015.)
|
⊢ (𝜑 → 𝑋 = (Base‘𝑀)) & ⊢ (𝜑 → 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋))) & ⊢ (𝜑 → 𝐾 = (𝑀 sSet 〈(TopSet‘ndx),
(MetOpen‘𝐷)〉)) & ⊢ (𝜑 → 𝑀 ∈ 𝑉)
& ⊢ (𝜑 → (MetOpen‘𝐷) ∈ 𝑊) ⇒ ⊢ (𝜑 → (dist‘𝑀) = (dist‘𝐾)) |
|
Theorem | setsmstsetg 13275 |
The topology of a constructed metric space. (Contributed by Mario
Carneiro, 28-Aug-2015.) (Revised by Jim Kingdon, 7-May-2023.)
|
⊢ (𝜑 → 𝑋 = (Base‘𝑀)) & ⊢ (𝜑 → 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋))) & ⊢ (𝜑 → 𝐾 = (𝑀 sSet 〈(TopSet‘ndx),
(MetOpen‘𝐷)〉)) & ⊢ (𝜑 → 𝑀 ∈ 𝑉)
& ⊢ (𝜑 → (MetOpen‘𝐷) ∈ 𝑊) ⇒ ⊢ (𝜑 → (MetOpen‘𝐷) = (TopSet‘𝐾)) |
|
Theorem | mopni 13276* |
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 13277* |
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 13278* |
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 13279 |
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 13280 |
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 13281 |
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 13282 |
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 13283 |
A ball of a metric space is an open set. (Contributed by NM,
12-Sep-2006.)
|
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ ran (ball‘𝐷)) → 𝐵 ∈ 𝐽) |
|
Theorem | blopn 13284 |
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 13285* |
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 13286 |
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 | blsscls2 13287* |
A smaller closed ball is contained in a larger open ball. (Contributed
by Mario Carneiro, 10-Jan-2014.)
|
⊢ 𝐽 = (MetOpen‘𝐷)
& ⊢ 𝑆 = {𝑧 ∈ 𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅} ⇒ ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ (𝑅 ∈ ℝ* ∧ 𝑇 ∈ ℝ*
∧ 𝑅 < 𝑇)) → 𝑆 ⊆ (𝑃(ball‘𝐷)𝑇)) |
|
Theorem | metss 13288* |
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 13289* |
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 13290* |
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 13291* |
Lemma for metss2 13292. (Contributed by Mario Carneiro,
14-Sep-2015.)
|
⊢ 𝐽 = (MetOpen‘𝐶)
& ⊢ 𝐾 = (MetOpen‘𝐷)
& ⊢ (𝜑 → 𝐶 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐶𝑦) ≤ (𝑅 · (𝑥𝐷𝑦))) ⇒ ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑆 ∈ ℝ+)) → (𝑥(ball‘𝐷)(𝑆 / 𝑅)) ⊆ (𝑥(ball‘𝐶)𝑆)) |
|
Theorem | metss2 13292* |
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 13293* |
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 | bdmetval 13294* |
Value of the standard bounded metric. (Contributed by Mario Carneiro,
26-Aug-2015.) (Revised by Jim Kingdon, 9-May-2023.)
|
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ inf({(𝑥𝐶𝑦), 𝑅}, ℝ*, <
)) ⇒ ⊢ (((𝐶:(𝑋 × 𝑋)⟶ℝ* ∧ 𝑅 ∈ ℝ*)
∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐷𝐵) = inf({(𝐴𝐶𝐵), 𝑅}, ℝ*, <
)) |
|
Theorem | bdxmet 13295* |
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.) (Revised by Jim Kingdon, 9-May-2023.)
|
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ inf({(𝑥𝐶𝑦), 𝑅}, ℝ*, <
)) ⇒ ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 𝐷 ∈ (∞Met‘𝑋)) |
|
Theorem | bdmet 13296* |
The standard bounded metric is a proper metric given an extended metric
and a positive real cutoff. (Contributed by Mario Carneiro,
26-Aug-2015.) (Revised by Jim Kingdon, 19-May-2023.)
|
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ inf({(𝑥𝐶𝑦), 𝑅}, ℝ*, <
)) ⇒ ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ+) → 𝐷 ∈ (Met‘𝑋)) |
|
Theorem | bdbl 13297* |
The standard bounded metric corresponding to 𝐶 generates the same
balls as 𝐶 for radii less than 𝑅.
(Contributed by Mario
Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 19-May-2023.)
|
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ inf({(𝑥𝐶𝑦), 𝑅}, ℝ*, <
)) ⇒ ⊢ (((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) ∧ (𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ* ∧ 𝑆 ≤ 𝑅)) → (𝑃(ball‘𝐷)𝑆) = (𝑃(ball‘𝐶)𝑆)) |
|
Theorem | bdmopn 13298* |
The standard bounded metric corresponding to 𝐶 generates the same
topology as 𝐶. (Contributed by Mario Carneiro,
26-Aug-2015.)
(Revised by Jim Kingdon, 19-May-2023.)
|
⊢ 𝐷 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ inf({(𝑥𝐶𝑦), 𝑅}, ℝ*, < )) & ⊢ 𝐽 = (MetOpen‘𝐶)
⇒ ⊢ ((𝐶 ∈ (∞Met‘𝑋) ∧ 𝑅 ∈ ℝ* ∧ 0 <
𝑅) → 𝐽 = (MetOpen‘𝐷)) |
|
Theorem | mopnex 13299* |
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 | metrest 13300 |
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 𝑌) = 𝐾) |