Type | Label | Description |
Statement |
|
Theorem | psmettri 14101 |
Triangle inequality for the distance function of a pseudometric space.
(Contributed by Thierry Arnoux, 11-Feb-2018.)
|
β’ ((π· β (PsMetβπ) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π·π΅) β€ ((π΄π·πΆ) +π (πΆπ·π΅))) |
|
Theorem | psmetge0 14102 |
The distance function of a pseudometric space is nonnegative.
(Contributed by Thierry Arnoux, 7-Feb-2018.) (Revised by Jim Kingdon,
19-Apr-2023.)
|
β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β 0 β€ (π΄π·π΅)) |
|
Theorem | psmetxrge0 14103 |
The distance function of a pseudometric space is a function into the
nonnegative extended real numbers. (Contributed by Thierry Arnoux,
24-Feb-2018.)
|
β’ (π· β (PsMetβπ) β π·:(π Γ π)βΆ(0[,]+β)) |
|
Theorem | psmetres2 14104 |
Restriction of a pseudometric. (Contributed by Thierry Arnoux,
11-Feb-2018.)
|
β’ ((π· β (PsMetβπ) β§ π
β π) β (π· βΎ (π
Γ π
)) β (PsMetβπ
)) |
|
Theorem | psmetlecl 14105 |
Real closure of an extended metric value that is upper bounded by a
real. (Contributed by Thierry Arnoux, 11-Mar-2018.)
|
β’ ((π· β (PsMetβπ) β§ (π΄ β π β§ π΅ β π) β§ (πΆ β β β§ (π΄π·π΅) β€ πΆ)) β (π΄π·π΅) β β) |
|
Theorem | distspace 14106 |
A set π together with a (distance) function
π·
which is a
pseudometric is a distance space (according to E. Deza, M.M. Deza:
"Dictionary of Distances", Elsevier, 2006), i.e. a (base) set
π
equipped with a distance π·, which is a mapping of two elements
of
the base set to the (extended) reals and which is nonnegative, symmetric
and equal to 0 if the two elements are equal. (Contributed by AV,
15-Oct-2021.) (Revised by AV, 5-Jul-2022.)
|
β’ ((π· β (PsMetβπ) β§ π΄ β π β§ π΅ β π) β ((π·:(π Γ π)βΆβ* β§ (π΄π·π΄) = 0) β§ (0 β€ (π΄π·π΅) β§ (π΄π·π΅) = (π΅π·π΄)))) |
|
8.2.2 Basic metric space
properties
|
|
Syntax | cxms 14107 |
Extend class notation with the class of extended metric spaces.
|
class βMetSp |
|
Syntax | cms 14108 |
Extend class notation with the class of metric spaces.
|
class MetSp |
|
Syntax | ctms 14109 |
Extend class notation with the function mapping a metric to the metric
space it defines.
|
class toMetSp |
|
Definition | df-xms 14110 |
Define the (proper) class of extended metric spaces. (Contributed by
Mario Carneiro, 2-Sep-2015.)
|
β’ βMetSp = {π β TopSp β£ (TopOpenβπ) =
(MetOpenβ((distβπ) βΎ ((Baseβπ) Γ (Baseβπ))))} |
|
Definition | df-ms 14111 |
Define the (proper) class of metric spaces. (Contributed by NM,
27-Aug-2006.)
|
β’ MetSp = {π β βMetSp β£
((distβπ) βΎ
((Baseβπ) Γ
(Baseβπ))) β
(Metβ(Baseβπ))} |
|
Definition | df-tms 14112 |
Define the function mapping a metric to the metric space which it defines.
(Contributed by Mario Carneiro, 2-Sep-2015.)
|
β’ toMetSp = (π β βͺ ran
βMet β¦ ({β¨(Baseβndx), dom dom πβ©, β¨(distβndx), πβ©} sSet
β¨(TopSetβndx), (MetOpenβπ)β©)) |
|
Theorem | metrel 14113 |
The class of metrics is a relation. (Contributed by Jim Kingdon,
20-Apr-2023.)
|
β’ Rel Met |
|
Theorem | xmetrel 14114 |
The class of extended metrics is a relation. (Contributed by Jim
Kingdon, 20-Apr-2023.)
|
β’ Rel βMet |
|
Theorem | ismet 14115* |
Express the predicate "π· is a metric". (Contributed by
NM,
25-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
|
β’ (π β π΄ β (π· β (Metβπ) β (π·:(π Γ π)βΆβ β§ βπ₯ β π βπ¦ β π (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) + (π§π·π¦)))))) |
|
Theorem | isxmet 14116* |
Express the predicate "π· is an extended metric".
(Contributed by
Mario Carneiro, 20-Aug-2015.)
|
β’ (π β π΄ β (π· β (βMetβπ) β (π·:(π Γ π)βΆβ* β§
βπ₯ β π βπ¦ β π (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦)))))) |
|
Theorem | ismeti 14117* |
Properties that determine a metric. (Contributed by NM, 17-Nov-2006.)
(Revised by Mario Carneiro, 14-Aug-2015.)
|
β’ π β V & β’ π·:(π Γ π)βΆβ & β’ ((π₯ β π β§ π¦ β π) β ((π₯π·π¦) = 0 β π₯ = π¦))
& β’ ((π₯ β π β§ π¦ β π β§ π§ β π) β (π₯π·π¦) β€ ((π§π·π₯) + (π§π·π¦))) β β’ π· β (Metβπ) |
|
Theorem | isxmetd 14118* |
Properties that determine an extended metric. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
β’ (π β π β V) & β’ (π β π·:(π Γ π)βΆβ*) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β ((π₯π·π¦) = 0 β π₯ = π¦))
& β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π₯π·π¦) β€ ((π§π·π₯) +π (π§π·π¦))) β β’ (π β π· β (βMetβπ)) |
|
Theorem | isxmet2d 14119* |
It is safe to only require the triangle inequality when the values are
real (so that we can use the standard addition over the reals), but in
this case the nonnegativity constraint cannot be deduced and must be
provided separately. (Counterexample:
π·(π₯, π¦) = if(π₯ = π¦, 0, -β) satisfies all
hypotheses
except nonnegativity.) (Contributed by Mario Carneiro,
20-Aug-2015.)
|
β’ (π β π β V) & β’ (π β π·:(π Γ π)βΆβ*) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β 0 β€ (π₯π·π¦))
& β’ ((π β§ (π₯ β π β§ π¦ β π)) β ((π₯π·π¦) β€ 0 β π₯ = π¦))
& β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π) β§ ((π§π·π₯) β β β§ (π§π·π¦) β β)) β (π₯π·π¦) β€ ((π§π·π₯) + (π§π·π¦))) β β’ (π β π· β (βMetβπ)) |
|
Theorem | metflem 14120* |
Lemma for metf 14122 and others. (Contributed by NM,
30-Aug-2006.)
(Revised by Mario Carneiro, 14-Aug-2015.)
|
β’ (π· β (Metβπ) β (π·:(π Γ π)βΆβ β§ βπ₯ β π βπ¦ β π (((π₯π·π¦) = 0 β π₯ = π¦) β§ βπ§ β π (π₯π·π¦) β€ ((π§π·π₯) + (π§π·π¦))))) |
|
Theorem | xmetf 14121 |
Mapping of the distance function of an extended metric. (Contributed by
Mario Carneiro, 20-Aug-2015.)
|
β’ (π· β (βMetβπ) β π·:(π Γ π)βΆβ*) |
|
Theorem | metf 14122 |
Mapping of the distance function of a metric space. (Contributed by NM,
30-Aug-2006.)
|
β’ (π· β (Metβπ) β π·:(π Γ π)βΆβ) |
|
Theorem | xmetcl 14123 |
Closure of the distance function of a metric space. Part of Property M1
of [Kreyszig] p. 3. (Contributed by
NM, 30-Aug-2006.)
|
β’ ((π· β (βMetβπ) β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) β
β*) |
|
Theorem | metcl 14124 |
Closure of the distance function of a metric space. Part of Property M1
of [Kreyszig] p. 3. (Contributed by
NM, 30-Aug-2006.)
|
β’ ((π· β (Metβπ) β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) β β) |
|
Theorem | ismet2 14125 |
An extended metric is a metric exactly when it takes real values for all
values of the arguments. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
β’ (π· β (Metβπ) β (π· β (βMetβπ) β§ π·:(π Γ π)βΆβ)) |
|
Theorem | metxmet 14126 |
A metric is an extended metric. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
β’ (π· β (Metβπ) β π· β (βMetβπ)) |
|
Theorem | xmetdmdm 14127 |
Recover the base set from an extended metric. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
β’ (π· β (βMetβπ) β π = dom dom π·) |
|
Theorem | metdmdm 14128 |
Recover the base set from a metric. (Contributed by Mario Carneiro,
23-Aug-2015.)
|
β’ (π· β (Metβπ) β π = dom dom π·) |
|
Theorem | xmetunirn 14129 |
Two ways to express an extended metric on an unspecified base.
(Contributed by Mario Carneiro, 13-Oct-2015.)
|
β’ (π· β βͺ ran
βMet β π· β
(βMetβdom dom π·)) |
|
Theorem | xmeteq0 14130 |
The value of an extended metric is zero iff its arguments are equal.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
β’ ((π· β (βMetβπ) β§ π΄ β π β§ π΅ β π) β ((π΄π·π΅) = 0 β π΄ = π΅)) |
|
Theorem | meteq0 14131 |
The value of a metric is zero iff its arguments are equal. Property M2
of [Kreyszig] p. 4. (Contributed by
NM, 30-Aug-2006.)
|
β’ ((π· β (Metβπ) β§ π΄ β π β§ π΅ β π) β ((π΄π·π΅) = 0 β π΄ = π΅)) |
|
Theorem | xmettri2 14132 |
Triangle inequality for the distance function of an extended metric.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
β’ ((π· β (βMetβπ) β§ (πΆ β π β§ π΄ β π β§ π΅ β π)) β (π΄π·π΅) β€ ((πΆπ·π΄) +π (πΆπ·π΅))) |
|
Theorem | mettri2 14133 |
Triangle inequality for the distance function of a metric space.
(Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro,
20-Aug-2015.)
|
β’ ((π· β (Metβπ) β§ (πΆ β π β§ π΄ β π β§ π΅ β π)) β (π΄π·π΅) β€ ((πΆπ·π΄) + (πΆπ·π΅))) |
|
Theorem | xmet0 14134 |
The distance function of a metric space is zero if its arguments are
equal. Definition 14-1.1(a) of [Gleason] p. 223. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
β’ ((π· β (βMetβπ) β§ π΄ β π) β (π΄π·π΄) = 0) |
|
Theorem | met0 14135 |
The distance function of a metric space is zero if its arguments are
equal. Definition 14-1.1(a) of [Gleason] p. 223. (Contributed by NM,
30-Aug-2006.)
|
β’ ((π· β (Metβπ) β§ π΄ β π) β (π΄π·π΄) = 0) |
|
Theorem | xmetge0 14136 |
The distance function of a metric space is nonnegative. (Contributed by
Mario Carneiro, 20-Aug-2015.)
|
β’ ((π· β (βMetβπ) β§ π΄ β π β§ π΅ β π) β 0 β€ (π΄π·π΅)) |
|
Theorem | metge0 14137 |
The distance function of a metric space is nonnegative. (Contributed by
NM, 27-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
|
β’ ((π· β (Metβπ) β§ π΄ β π β§ π΅ β π) β 0 β€ (π΄π·π΅)) |
|
Theorem | xmetlecl 14138 |
Real closure of an extended metric value that is upper bounded by a
real. (Contributed by Mario Carneiro, 20-Aug-2015.)
|
β’ ((π· β (βMetβπ) β§ (π΄ β π β§ π΅ β π) β§ (πΆ β β β§ (π΄π·π΅) β€ πΆ)) β (π΄π·π΅) β β) |
|
Theorem | xmetsym 14139 |
The distance function of an extended metric space is symmetric.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
β’ ((π· β (βMetβπ) β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) = (π΅π·π΄)) |
|
Theorem | xmetpsmet 14140 |
An extended metric is a pseudometric. (Contributed by Thierry Arnoux,
7-Feb-2018.)
|
β’ (π· β (βMetβπ) β π· β (PsMetβπ)) |
|
Theorem | xmettpos 14141 |
The distance function of an extended metric space is symmetric.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
β’ (π· β (βMetβπ) β tpos π· = π·) |
|
Theorem | metsym 14142 |
The distance function of a metric space is symmetric. Definition
14-1.1(c) of [Gleason] p. 223.
(Contributed by NM, 27-Aug-2006.)
(Revised by Mario Carneiro, 20-Aug-2015.)
|
β’ ((π· β (Metβπ) β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) = (π΅π·π΄)) |
|
Theorem | xmettri 14143 |
Triangle inequality for the distance function of a metric space.
Definition 14-1.1(d) of [Gleason] p.
223. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
β’ ((π· β (βMetβπ) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π·π΅) β€ ((π΄π·πΆ) +π (πΆπ·π΅))) |
|
Theorem | mettri 14144 |
Triangle inequality for the distance function of a metric space.
Definition 14-1.1(d) of [Gleason] p.
223. (Contributed by NM,
27-Aug-2006.)
|
β’ ((π· β (Metβπ) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π·π΅) β€ ((π΄π·πΆ) + (πΆπ·π΅))) |
|
Theorem | xmettri3 14145 |
Triangle inequality for the distance function of an extended metric.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
β’ ((π· β (βMetβπ) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π·π΅) β€ ((π΄π·πΆ) +π (π΅π·πΆ))) |
|
Theorem | mettri3 14146 |
Triangle inequality for the distance function of a metric space.
(Contributed by NM, 13-Mar-2007.)
|
β’ ((π· β (Metβπ) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π·π΅) β€ ((π΄π·πΆ) + (π΅π·πΆ))) |
|
Theorem | xmetrtri 14147 |
One half of the reverse triangle inequality for the distance function of
an extended metric. (Contributed by Mario Carneiro, 4-Sep-2015.)
|
β’ ((π· β (βMetβπ) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄π·πΆ) +π
-π(π΅π·πΆ)) β€ (π΄π·π΅)) |
|
Theorem | metrtri 14148 |
Reverse triangle inequality for the distance function of a metric space.
(Contributed by Mario Carneiro, 5-May-2014.) (Revised by Jim Kingdon,
21-Apr-2023.)
|
β’ ((π· β (Metβπ) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (absβ((π΄π·πΆ) β (π΅π·πΆ))) β€ (π΄π·π΅)) |
|
Theorem | metn0 14149 |
A metric space is nonempty iff its base set is nonempty. (Contributed
by NM, 4-Oct-2007.) (Revised by Mario Carneiro, 14-Aug-2015.)
|
β’ (π· β (Metβπ) β (π· β β
β π β β
)) |
|
Theorem | xmetres2 14150 |
Restriction of an extended metric. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
β’ ((π· β (βMetβπ) β§ π
β π) β (π· βΎ (π
Γ π
)) β (βMetβπ
)) |
|
Theorem | metreslem 14151 |
Lemma for metres 14154. (Contributed by Mario Carneiro,
24-Aug-2015.)
|
β’ (dom π· = (π Γ π) β (π· βΎ (π
Γ π
)) = (π· βΎ ((π β© π
) Γ (π β© π
)))) |
|
Theorem | metres2 14152 |
Lemma for metres 14154. (Contributed by FL, 12-Oct-2006.) (Proof
shortened by Mario Carneiro, 14-Aug-2015.)
|
β’ ((π· β (Metβπ) β§ π
β π) β (π· βΎ (π
Γ π
)) β (Metβπ
)) |
|
Theorem | xmetres 14153 |
A restriction of an extended metric is an extended metric. (Contributed
by Mario Carneiro, 24-Aug-2015.)
|
β’ (π· β (βMetβπ) β (π· βΎ (π
Γ π
)) β (βMetβ(π β© π
))) |
|
Theorem | metres 14154 |
A restriction of a metric is a metric. (Contributed by NM, 26-Aug-2007.)
(Revised by Mario Carneiro, 14-Aug-2015.)
|
β’ (π· β (Metβπ) β (π· βΎ (π
Γ π
)) β (Metβ(π β© π
))) |
|
Theorem | 0met 14155 |
The empty metric. (Contributed by NM, 30-Aug-2006.) (Revised by Mario
Carneiro, 14-Aug-2015.)
|
β’ β
β
(Metββ
) |
|
8.2.3 Metric space balls
|
|
Theorem | blfvalps 14156* |
The value of the ball function. (Contributed by NM, 30-Aug-2006.)
(Revised by Mario Carneiro, 11-Nov-2013.) (Revised by Thierry Arnoux,
11-Feb-2018.)
|
β’ (π· β (PsMetβπ) β (ballβπ·) = (π₯ β π, π β β* β¦ {π¦ β π β£ (π₯π·π¦) < π})) |
|
Theorem | blfval 14157* |
The value of the ball function. (Contributed by NM, 30-Aug-2006.)
(Revised by Mario Carneiro, 11-Nov-2013.) (Proof shortened by Thierry
Arnoux, 11-Feb-2018.)
|
β’ (π· β (βMetβπ) β (ballβπ·) = (π₯ β π, π β β* β¦ {π¦ β π β£ (π₯π·π¦) < π})) |
|
Theorem | blex 14158 |
A ball is a set. (Contributed by Jim Kingdon, 4-May-2023.)
|
β’ (π· β (βMetβπ) β (ballβπ·) β V) |
|
Theorem | blvalps 14159* |
The ball around a point π is the set of all points whose
distance
from π is less than the ball's radius π
.
(Contributed by NM,
31-Aug-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) (Revised by
Thierry Arnoux, 11-Mar-2018.)
|
β’ ((π· β (PsMetβπ) β§ π β π β§ π
β β*) β (π(ballβπ·)π
) = {π₯ β π β£ (ππ·π₯) < π
}) |
|
Theorem | blval 14160* |
The ball around a point π is the set of all points whose
distance
from π is less than the ball's radius π
.
(Contributed by NM,
31-Aug-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
|
β’ ((π· β (βMetβπ) β§ π β π β§ π
β β*) β (π(ballβπ·)π
) = {π₯ β π β£ (ππ·π₯) < π
}) |
|
Theorem | elblps 14161 |
Membership in a ball. (Contributed by NM, 2-Sep-2006.) (Revised by
Mario Carneiro, 11-Nov-2013.) (Revised by Thierry Arnoux,
11-Mar-2018.)
|
β’ ((π· β (PsMetβπ) β§ π β π β§ π
β β*) β (π΄ β (π(ballβπ·)π
) β (π΄ β π β§ (ππ·π΄) < π
))) |
|
Theorem | elbl 14162 |
Membership in a ball. (Contributed by NM, 2-Sep-2006.) (Revised by
Mario Carneiro, 11-Nov-2013.)
|
β’ ((π· β (βMetβπ) β§ π β π β§ π
β β*) β (π΄ β (π(ballβπ·)π
) β (π΄ β π β§ (ππ·π΄) < π
))) |
|
Theorem | elbl2ps 14163 |
Membership in a ball. (Contributed by NM, 9-Mar-2007.) (Revised by
Thierry Arnoux, 11-Mar-2018.)
|
β’ (((π· β (PsMetβπ) β§ π
β β*) β§ (π β π β§ π΄ β π)) β (π΄ β (π(ballβπ·)π
) β (ππ·π΄) < π
)) |
|
Theorem | elbl2 14164 |
Membership in a ball. (Contributed by NM, 9-Mar-2007.)
|
β’ (((π· β (βMetβπ) β§ π
β β*) β§ (π β π β§ π΄ β π)) β (π΄ β (π(ballβπ·)π
) β (ππ·π΄) < π
)) |
|
Theorem | elbl3ps 14165 |
Membership in a ball, with reversed distance function arguments.
(Contributed by NM, 10-Nov-2007.)
|
β’ (((π· β (PsMetβπ) β§ π
β β*) β§ (π β π β§ π΄ β π)) β (π΄ β (π(ballβπ·)π
) β (π΄π·π) < π
)) |
|
Theorem | elbl3 14166 |
Membership in a ball, with reversed distance function arguments.
(Contributed by NM, 10-Nov-2007.)
|
β’ (((π· β (βMetβπ) β§ π
β β*) β§ (π β π β§ π΄ β π)) β (π΄ β (π(ballβπ·)π
) β (π΄π·π) < π
)) |
|
Theorem | blcomps 14167 |
Commute the arguments to the ball function. (Contributed by Mario
Carneiro, 22-Jan-2014.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|
β’ (((π· β (PsMetβπ) β§ π
β β*) β§ (π β π β§ π΄ β π)) β (π΄ β (π(ballβπ·)π
) β π β (π΄(ballβπ·)π
))) |
|
Theorem | blcom 14168 |
Commute the arguments to the ball function. (Contributed by Mario
Carneiro, 22-Jan-2014.)
|
β’ (((π· β (βMetβπ) β§ π
β β*) β§ (π β π β§ π΄ β π)) β (π΄ β (π(ballβπ·)π
) β π β (π΄(ballβπ·)π
))) |
|
Theorem | xblpnfps 14169 |
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 14170 |
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 14171 |
The infinity ball in a standard metric is just the whole space.
(Contributed by Mario Carneiro, 23-Aug-2015.)
|
β’ ((π· β (Metβπ) β§ π β π) β (π(ballβπ·)+β) = π) |
|
Theorem | bldisj 14172 |
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 14173 |
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 14174 |
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 14175 |
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 14178 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 14176 |
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 14178 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 14177 |
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 14178 |
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 14179 |
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 14180 |
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 14181 |
Mapping of a ball. (Contributed by NM, 7-May-2007.) (Revised by Mario
Carneiro, 23-Aug-2015.)
|
β’ (π· β (βMetβπ) β (ballβπ·):(π Γ
β*)βΆπ« π) |
|
Theorem | blrnps 14182* |
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 14183* |
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 14184 |
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 14185 |
A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised
by Mario Carneiro, 12-Nov-2013.)
|
β’ ((π· β (βMetβπ) β§ π β π β§ (π
β β* β§ 0 <
π
)) β π β (π(ballβπ·)π
)) |
|
Theorem | blcntrps 14186 |
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 14187 |
A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised
by Mario Carneiro, 12-Nov-2013.)
|
β’ ((π· β (βMetβπ) β§ π β π β§ π
β β+) β π β (π(ballβπ·)π
)) |
|
Theorem | xblm 14188* |
A ball is inhabited iff the radius is positive. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
β’ ((π· β (βMetβπ) β§ π β π β§ π
β β*) β
(βπ₯ π₯ β (π(ballβπ·)π
) β 0 < π
)) |
|
Theorem | bln0 14189 |
A ball is not empty. It is also inhabited, as seen at blcntr 14187.
(Contributed by NM, 6-Oct-2007.) (Revised by Mario Carneiro,
12-Nov-2013.)
|
β’ ((π· β (βMetβπ) β§ π β π β§ π
β β+) β (π(ballβπ·)π
) β β
) |
|
Theorem | blelrnps 14190 |
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 14191 |
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 14192 |
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 14193 |
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 14194 |
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 14195 |
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 14196 |
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 14197 |
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 14198* |
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 14199* |
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 14200* |
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βπ·)π) β π΄)) |