Theorem List for Intuitionistic Logic Explorer - 12501-12600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | psmetxrge0 12501 |
The distance function of a pseudometric space is a function into the
nonnegative extended real numbers. (Contributed by Thierry Arnoux,
24-Feb-2018.)
|
PsMet |
|
Theorem | psmetres2 12502 |
Restriction of a pseudometric. (Contributed by Thierry Arnoux,
11-Feb-2018.)
|
PsMet
PsMet |
|
Theorem | psmetlecl 12503 |
Real closure of an extended metric value that is upper bounded by a
real. (Contributed by Thierry Arnoux, 11-Mar-2018.)
|
PsMet
|
|
Theorem | distspace 12504 |
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
|
|
7.2.2 Basic metric space
properties
|
|
Syntax | cxms 12505 |
Extend class notation with the class of extended metric spaces.
|
|
|
Syntax | cms 12506 |
Extend class notation with the class of metric spaces.
|
|
|
Syntax | ctms 12507 |
Extend class notation with the function mapping a metric to the metric
space it defines.
|
toMetSp |
|
Definition | df-xms 12508 |
Define the (proper) class of extended metric spaces. (Contributed by
Mario Carneiro, 2-Sep-2015.)
|
|
|
Definition | df-ms 12509 |
Define the (proper) class of metric spaces. (Contributed by NM,
27-Aug-2006.)
|
|
|
Definition | df-tms 12510 |
Define the function mapping a metric to the metric space which it defines.
(Contributed by Mario Carneiro, 2-Sep-2015.)
|
toMetSp sSet
TopSet
|
|
Theorem | metrel 12511 |
The class of metrics is a relation. (Contributed by Jim Kingdon,
20-Apr-2023.)
|
|
|
Theorem | xmetrel 12512 |
The class of extended metrics is a relation. (Contributed by Jim
Kingdon, 20-Apr-2023.)
|
|
|
Theorem | ismet 12513* |
Express the predicate " is a metric." (Contributed by NM,
25-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
|
|
|
Theorem | isxmet 12514* |
Express the predicate " is an extended metric." (Contributed by
Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | ismeti 12515* |
Properties that determine a metric. (Contributed by NM, 17-Nov-2006.)
(Revised by Mario Carneiro, 14-Aug-2015.)
|
|
|
Theorem | isxmetd 12516* |
Properties that determine an extended metric. (Contributed by Mario
Carneiro, 20-Aug-2015.)
|
|
|
Theorem | isxmet2d 12517* |
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:
satisfies all hypotheses
except nonnegativity.) (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | metflem 12518* |
Lemma for metf 12520 and others. (Contributed by NM,
30-Aug-2006.)
(Revised by Mario Carneiro, 14-Aug-2015.)
|
|
|
Theorem | xmetf 12519 |
Mapping of the distance function of an extended metric. (Contributed by
Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | metf 12520 |
Mapping of the distance function of a metric space. (Contributed by NM,
30-Aug-2006.)
|
|
|
Theorem | xmetcl 12521 |
Closure of the distance function of a metric space. Part of Property M1
of [Kreyszig] p. 3. (Contributed by
NM, 30-Aug-2006.)
|
|
|
Theorem | metcl 12522 |
Closure of the distance function of a metric space. Part of Property M1
of [Kreyszig] p. 3. (Contributed by
NM, 30-Aug-2006.)
|
|
|
Theorem | ismet2 12523 |
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.)
|
|
|
Theorem | metxmet 12524 |
A metric is an extended metric. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xmetdmdm 12525 |
Recover the base set from an extended metric. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
|
|
Theorem | metdmdm 12526 |
Recover the base set from a metric. (Contributed by Mario Carneiro,
23-Aug-2015.)
|
|
|
Theorem | xmetunirn 12527 |
Two ways to express an extended metric on an unspecified base.
(Contributed by Mario Carneiro, 13-Oct-2015.)
|
|
|
Theorem | xmeteq0 12528 |
The value of an extended metric is zero iff its arguments are equal.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | meteq0 12529 |
The value of a metric is zero iff its arguments are equal. Property M2
of [Kreyszig] p. 4. (Contributed by
NM, 30-Aug-2006.)
|
|
|
Theorem | xmettri2 12530 |
Triangle inequality for the distance function of an extended metric.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | mettri2 12531 |
Triangle inequality for the distance function of a metric space.
(Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | xmet0 12532 |
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.)
|
|
|
Theorem | met0 12533 |
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.)
|
|
|
Theorem | xmetge0 12534 |
The distance function of a metric space is nonnegative. (Contributed by
Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | metge0 12535 |
The distance function of a metric space is nonnegative. (Contributed by
NM, 27-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
|
|
|
Theorem | xmetlecl 12536 |
Real closure of an extended metric value that is upper bounded by a
real. (Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xmetsym 12537 |
The distance function of an extended metric space is symmetric.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | xmetpsmet 12538 |
An extended metric is a pseudometric. (Contributed by Thierry Arnoux,
7-Feb-2018.)
|
PsMet |
|
Theorem | xmettpos 12539 |
The distance function of an extended metric space is symmetric.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
tpos |
|
Theorem | metsym 12540 |
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.)
|
|
|
Theorem | xmettri 12541 |
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.)
|
|
|
Theorem | mettri 12542 |
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.)
|
|
|
Theorem | xmettri3 12543 |
Triangle inequality for the distance function of an extended metric.
(Contributed by Mario Carneiro, 20-Aug-2015.)
|
|
|
Theorem | mettri3 12544 |
Triangle inequality for the distance function of a metric space.
(Contributed by NM, 13-Mar-2007.)
|
|
|
Theorem | xmetrtri 12545 |
One half of the reverse triangle inequality for the distance function of
an extended metric. (Contributed by Mario Carneiro, 4-Sep-2015.)
|
|
|
Theorem | metrtri 12546 |
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.)
|
|
|
Theorem | metn0 12547 |
A metric space is nonempty iff its base set is nonempty. (Contributed
by NM, 4-Oct-2007.) (Revised by Mario Carneiro, 14-Aug-2015.)
|
|
|
Theorem | xmetres2 12548 |
Restriction of an extended metric. (Contributed by Mario Carneiro,
20-Aug-2015.)
|
|
|
Theorem | metreslem 12549 |
Lemma for metres 12552. (Contributed by Mario Carneiro,
24-Aug-2015.)
|
|
|
Theorem | metres2 12550 |
Lemma for metres 12552. (Contributed by FL, 12-Oct-2006.) (Proof
shortened by Mario Carneiro, 14-Aug-2015.)
|
|
|
Theorem | xmetres 12551 |
A restriction of an extended metric is an extended metric. (Contributed
by Mario Carneiro, 24-Aug-2015.)
|
|
|
Theorem | metres 12552 |
A restriction of a metric is a metric. (Contributed by NM, 26-Aug-2007.)
(Revised by Mario Carneiro, 14-Aug-2015.)
|
|
|
Theorem | 0met 12553 |
The empty metric. (Contributed by NM, 30-Aug-2006.) (Revised by Mario
Carneiro, 14-Aug-2015.)
|
|
|
7.2.3 Metric space balls
|
|
Theorem | blfvalps 12554* |
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
|
|
Theorem | blfval 12555* |
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.)
|
|
|
Theorem | blex 12556 |
A ball is a set. (Contributed by Jim Kingdon, 4-May-2023.)
|
|
|
Theorem | blvalps 12557* |
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
|
|
Theorem | blval 12558* |
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.)
|
|
|
Theorem | elblps 12559 |
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
|
|
Theorem | elbl 12560 |
Membership in a ball. (Contributed by NM, 2-Sep-2006.) (Revised by
Mario Carneiro, 11-Nov-2013.)
|
|
|
Theorem | elbl2ps 12561 |
Membership in a ball. (Contributed by NM, 9-Mar-2007.) (Revised by
Thierry Arnoux, 11-Mar-2018.)
|
PsMet
|
|
Theorem | elbl2 12562 |
Membership in a ball. (Contributed by NM, 9-Mar-2007.)
|
|
|
Theorem | elbl3ps 12563 |
Membership in a ball, with reversed distance function arguments.
(Contributed by NM, 10-Nov-2007.)
|
PsMet
|
|
Theorem | elbl3 12564 |
Membership in a ball, with reversed distance function arguments.
(Contributed by NM, 10-Nov-2007.)
|
|
|
Theorem | blcomps 12565 |
Commute the arguments to the ball function. (Contributed by Mario
Carneiro, 22-Jan-2014.) (Revised by Thierry Arnoux, 11-Mar-2018.)
|
PsMet
|
|
Theorem | blcom 12566 |
Commute the arguments to the ball function. (Contributed by Mario
Carneiro, 22-Jan-2014.)
|
|
|
Theorem | xblpnfps 12567 |
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
|
|
Theorem | xblpnf 12568 |
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.)
|
|
|
Theorem | blpnf 12569 |
The infinity ball in a standard metric is just the whole space.
(Contributed by Mario Carneiro, 23-Aug-2015.)
|
|
|
Theorem | bldisj 12570 |
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.)
|
|
|
Theorem | blgt0 12571 |
A nonempty ball implies that the radius is positive. (Contributed by
NM, 11-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.)
|
|
|
Theorem | bl2in 12572 |
Two balls are disjoint if they don't overlap. (Contributed by NM,
11-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.)
|
|
|
Theorem | xblss2ps 12573 |
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 12576 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
|
|
Theorem | xblss2 12574 |
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 12576 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.)
|
|
|
Theorem | blss2ps 12575 |
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 |
|
Theorem | blss2 12576 |
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.)
|
|
|
Theorem | blhalf 12577 |
A ball of radius 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.)
|
|
|
Theorem | blfps 12578 |
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 |
|
Theorem | blf 12579 |
Mapping of a ball. (Contributed by NM, 7-May-2007.) (Revised by Mario
Carneiro, 23-Aug-2015.)
|
|
|
Theorem | blrnps 12580* |
Membership in the range of the ball function. Note that
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
|
|
Theorem | blrn 12581* |
Membership in the range of the ball function. Note that
is the
collection of all balls for metric .
(Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro,
12-Nov-2013.)
|
|
|
Theorem | xblcntrps 12582 |
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
|
|
Theorem | xblcntr 12583 |
A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised
by Mario Carneiro, 12-Nov-2013.)
|
|
|
Theorem | blcntrps 12584 |
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
|
|
Theorem | blcntr 12585 |
A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised
by Mario Carneiro, 12-Nov-2013.)
|
|
|
Theorem | xblm 12586* |
A ball is inhabited iff the radius is positive. (Contributed by Mario
Carneiro, 23-Aug-2015.)
|
|
|
Theorem | bln0 12587 |
A ball is not empty. It is also inhabited, as seen at blcntr 12585.
(Contributed by NM, 6-Oct-2007.) (Revised by Mario Carneiro,
12-Nov-2013.)
|
|
|
Theorem | blelrnps 12588 |
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
|
|
Theorem | blelrn 12589 |
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.)
|
|
|
Theorem | blssm 12590 |
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.)
|
|
|
Theorem | unirnblps 12591 |
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 |
|
Theorem | unirnbl 12592 |
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.)
|
|
|
Theorem | blininf 12593 |
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.)
|
inf
|
|
Theorem | ssblps 12594 |
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
|
|
Theorem | ssbl 12595 |
The size of a ball increases monotonically with its radius.
(Contributed by NM, 20-Sep-2007.) (Revised by Mario Carneiro,
24-Aug-2015.)
|
|
|
Theorem | blssps 12596* |
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
|
|
Theorem | blss 12597* |
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.)
|
|
|
Theorem | blssexps 12598* |
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
|
|
Theorem | blssex 12599* |
Two ways to express the existence of a ball subset. (Contributed by NM,
5-May-2007.) (Revised by Mario Carneiro, 12-Nov-2013.)
|
|
|
Theorem | ssblex 12600* |
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.)
|
|