Type | Label | Description |
Statement |
|
Theorem | xblpnfps 14301 |
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 14302 |
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 14303 |
The infinity ball in a standard metric is just the whole space.
(Contributed by Mario Carneiro, 23-Aug-2015.)
|
β’ ((π· β (Metβπ) β§ π β π) β (π(ballβπ·)+β) = π) |
|
Theorem | bldisj 14304 |
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 14305 |
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 14306 |
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 14307 |
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 14310 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 14308 |
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 14310 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 14309 |
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 14310 |
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 14311 |
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 14312 |
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 14313 |
Mapping of a ball. (Contributed by NM, 7-May-2007.) (Revised by Mario
Carneiro, 23-Aug-2015.)
|
β’ (π· β (βMetβπ) β (ballβπ·):(π Γ
β*)βΆπ« π) |
|
Theorem | blrnps 14314* |
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 14315* |
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 14316 |
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 14317 |
A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised
by Mario Carneiro, 12-Nov-2013.)
|
β’ ((π· β (βMetβπ) β§ π β π β§ (π
β β* β§ 0 <
π
)) β π β (π(ballβπ·)π
)) |
|
Theorem | blcntrps 14318 |
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 14319 |
A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised
by Mario Carneiro, 12-Nov-2013.)
|
β’ ((π· β (βMetβπ) β§ π β π β§ π
β β+) β π β (π(ballβπ·)π
)) |
|
Theorem | xblm 14320* |
A ball is inhabited iff the radius is positive. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
β’ ((π· β (βMetβπ) β§ π β π β§ π
β β*) β
(βπ₯ π₯ β (π(ballβπ·)π
) β 0 < π
)) |
|
Theorem | bln0 14321 |
A ball is not empty. It is also inhabited, as seen at blcntr 14319.
(Contributed by NM, 6-Oct-2007.) (Revised by Mario Carneiro,
12-Nov-2013.)
|
β’ ((π· β (βMetβπ) β§ π β π β§ π
β β+) β (π(ballβπ·)π
) β β
) |
|
Theorem | blelrnps 14322 |
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 14323 |
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 14324 |
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 14325 |
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 14326 |
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 14327 |
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 14328 |
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 14329 |
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 14330* |
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 14331* |
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 14332* |
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 14333* |
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 14334* |
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 14335* |
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 14336 |
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 14337 |
A ball in a restricted metric space. (Contributed by Mario Carneiro,
5-Jan-2014.)
|
β’ πΆ = (π· βΎ (π Γ π)) β β’ ((π· β (βMetβπ) β§ π β (π β© π) β§ π
β β*) β (π(ballβπΆ)π
) = ((π(ballβπ·)π
) β© π)) |
|
Theorem | xmeterval 14338 |
Value of the "finitely separated" relation. (Contributed by Mario
Carneiro, 24-Aug-2015.)
|
β’ βΌ = (β‘π· β β)
β β’ (π· β (βMetβπ) β (π΄ βΌ π΅ β (π΄ β π β§ π΅ β π β§ (π΄π·π΅) β β))) |
|
Theorem | xmeter 14339 |
The "finitely separated" relation is an equivalence relation.
(Contributed by Mario Carneiro, 24-Aug-2015.)
|
β’ βΌ = (β‘π· β β)
β β’ (π· β (βMetβπ) β βΌ Er π) |
|
Theorem | xmetec 14340 |
The equivalence classes under the finite separation equivalence relation
are infinity balls. (Contributed by Mario Carneiro, 24-Aug-2015.)
|
β’ βΌ = (β‘π· β β)
β β’ ((π· β (βMetβπ) β§ π β π) β [π] βΌ = (π(ballβπ·)+β)) |
|
Theorem | blssec 14341 |
A ball centered at π is contained in the set of points
finitely
separated from π. This is just an application of ssbl 14329
to the
infinity ball. (Contributed by Mario Carneiro, 24-Aug-2015.)
|
β’ βΌ = (β‘π· β β)
β β’ ((π· β (βMetβπ) β§ π β π β§ π β β*) β (π(ballβπ·)π) β [π] βΌ ) |
|
Theorem | blpnfctr 14342 |
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 14343 |
An extended metric restricted to any ball (in particular the infinity
ball) is a proper metric. Together with xmetec 14340, 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 14344 |
The class of open sets of a metric space is a relation. (Contributed by
Jim Kingdon, 5-May-2023.)
|
β’ Rel MetOpen |
|
Theorem | mopnval 14345 |
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 14347, the open sets of a
metric space form a topology π½, whose base set is βͺ π½ by
mopnuni 14348. (Contributed by NM, 1-Sep-2006.) (Revised
by Mario
Carneiro, 12-Nov-2013.)
|
β’ π½ = (MetOpenβπ·) β β’ (π· β (βMetβπ) β π½ = (topGenβran (ballβπ·))) |
|
Theorem | mopntopon 14346 |
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 14347 |
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 14348 |
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 14349* |
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 14350 |
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 14351 |
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 14352* |
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 14353 |
An open set of a metric space is a subspace of its base set.
(Contributed by NM, 3-Sep-2006.)
|
β’ π½ = (MetOpenβπ·) β β’ ((π· β (βMetβπ) β§ π΄ β π½) β π΄ β π) |
|
Theorem | isxms 14354 |
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 14355 |
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 14356 |
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 14357 |
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 14358 |
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 14359 |
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 14360 |
An extended metric space is a topological space. (Contributed by Mario
Carneiro, 26-Aug-2015.)
|
β’ (π β βMetSp β π β TopSp) |
|
Theorem | msxms 14361 |
A metric space is an extended metric space. (Contributed by Mario
Carneiro, 26-Aug-2015.)
|
β’ (π β MetSp β π β βMetSp) |
|
Theorem | mstps 14362 |
A metric space is a topological space. (Contributed by Mario Carneiro,
26-Aug-2015.)
|
β’ (π β MetSp β π β TopSp) |
|
Theorem | xmsxmet 14363 |
The distance function, suitably truncated, is an extended metric on
π. (Contributed by Mario Carneiro,
2-Sep-2015.)
|
β’ π = (Baseβπ)
& β’ π· = ((distβπ) βΎ (π Γ π)) β β’ (π β βMetSp β π· β (βMetβπ)) |
|
Theorem | msmet 14364 |
The distance function, suitably truncated, is a metric on π.
(Contributed by Mario Carneiro, 12-Nov-2013.)
|
β’ π = (Baseβπ)
& β’ π· = ((distβπ) βΎ (π Γ π)) β β’ (π β MetSp β π· β (Metβπ)) |
|
Theorem | msf 14365 |
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 14366 |
The distance function, suitably truncated, is an extended metric on
π. (Contributed by Mario Carneiro,
2-Oct-2015.)
|
β’ π = (Baseβπ)
& β’ π· = (distβπ) β β’ (π β βMetSp β (π· βΎ (π Γ π)) β (βMetβπ)) |
|
Theorem | msmet2 14367 |
The distance function, suitably truncated, is a metric on π.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
β’ π = (Baseβπ)
& β’ π· = (distβπ) β β’ (π β MetSp β (π· βΎ (π Γ π)) β (Metβπ)) |
|
Theorem | mscl 14368 |
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 14369 |
Closure of the distance function of an extended metric space.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
β’ π = (Baseβπ)
& β’ π· = (distβπ) β β’ ((π β βMetSp β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) β
β*) |
|
Theorem | xmsge0 14370 |
The distance function in an extended metric space is nonnegative.
(Contributed by Mario Carneiro, 4-Oct-2015.)
|
β’ π = (Baseβπ)
& β’ π· = (distβπ) β β’ ((π β βMetSp β§ π΄ β π β§ π΅ β π) β 0 β€ (π΄π·π΅)) |
|
Theorem | xmseq0 14371 |
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 14372 |
The distance function in an extended metric space is symmetric.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
β’ π = (Baseβπ)
& β’ π· = (distβπ) β β’ ((π β βMetSp β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) = (π΅π·π΄)) |
|
Theorem | xmstri2 14373 |
Triangle inequality for the distance function of an extended metric.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
β’ π = (Baseβπ)
& β’ π· = (distβπ) β β’ ((π β βMetSp β§ (πΆ β π β§ π΄ β π β§ π΅ β π)) β (π΄π·π΅) β€ ((πΆπ·π΄) +π (πΆπ·π΅))) |
|
Theorem | mstri2 14374 |
Triangle inequality for the distance function of a metric space.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
β’ π = (Baseβπ)
& β’ π· = (distβπ) β β’ ((π β MetSp β§ (πΆ β π β§ π΄ β π β§ π΅ β π)) β (π΄π·π΅) β€ ((πΆπ·π΄) + (πΆπ·π΅))) |
|
Theorem | xmstri 14375 |
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 14376 |
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 14377 |
Triangle inequality for the distance function of an extended metric.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
β’ π = (Baseβπ)
& β’ π· = (distβπ) β β’ ((π β βMetSp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π·π΅) β€ ((π΄π·πΆ) +π (π΅π·πΆ))) |
|
Theorem | mstri3 14378 |
Triangle inequality for the distance function of a metric space.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
β’ π = (Baseβπ)
& β’ π· = (distβπ) β β’ ((π β MetSp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π·π΅) β€ ((π΄π·πΆ) + (π΅π·πΆ))) |
|
Theorem | msrtri 14379 |
Reverse triangle inequality for the distance function of a metric space.
(Contributed by Mario Carneiro, 4-Oct-2015.)
|
β’ π = (Baseβπ)
& β’ π· = (distβπ) β β’ ((π β MetSp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (absβ((π΄π·πΆ) β (π΅π·πΆ))) β€ (π΄π·π΅)) |
|
Theorem | xmspropd 14380 |
Property deduction for an extended metric space. (Contributed by Mario
Carneiro, 4-Oct-2015.)
|
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ (π β ((distβπΎ) βΎ (π΅ Γ π΅)) = ((distβπΏ) βΎ (π΅ Γ π΅))) & β’ (π β (TopOpenβπΎ) = (TopOpenβπΏ))
β β’ (π β (πΎ β βMetSp β πΏ β
βMetSp)) |
|
Theorem | mspropd 14381 |
Property deduction for a metric space. (Contributed by Mario Carneiro,
4-Oct-2015.)
|
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ (π β ((distβπΎ) βΎ (π΅ Γ π΅)) = ((distβπΏ) βΎ (π΅ Γ π΅))) & β’ (π β (TopOpenβπΎ) = (TopOpenβπΏ))
β β’ (π β (πΎ β MetSp β πΏ β MetSp)) |
|
Theorem | setsmsbasg 14382 |
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 14383 |
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 14384 |
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 14385* |
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 14386* |
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 14387* |
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 14388 |
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 14389 |
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 14390 |
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 14391 |
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 14392 |
A ball of a metric space is an open set. (Contributed by NM,
12-Sep-2006.)
|
β’ π½ = (MetOpenβπ·) β β’ ((π· β (βMetβπ) β§ π΅ β ran (ballβπ·)) β π΅ β π½) |
|
Theorem | blopn 14393 |
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 14394* |
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 14395 |
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 14396* |
A smaller closed ball is contained in a larger open ball. (Contributed
by Mario Carneiro, 10-Jan-2014.)
|
β’ π½ = (MetOpenβπ·)
& β’ π = {π§ β π β£ (ππ·π§) β€ π
} β β’ (((π· β (βMetβπ) β§ π β π) β§ (π
β β* β§ π β β*
β§ π
< π)) β π β (π(ballβπ·)π)) |
|
Theorem | metss 14397* |
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 14398* |
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 14399* |
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 14400* |
Lemma for metss2 14401. (Contributed by Mario Carneiro,
14-Sep-2015.)
|
β’ π½ = (MetOpenβπΆ)
& β’ πΎ = (MetOpenβπ·)
& β’ (π β πΆ β (Metβπ)) & β’ (π β π· β (Metβπ)) & β’ (π β π
β β+) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯πΆπ¦) β€ (π
Β· (π₯π·π¦))) β β’ ((π β§ (π₯ β π β§ π β β+)) β (π₯(ballβπ·)(π / π
)) β (π₯(ballβπΆ)π)) |