Theorem List for Intuitionistic Logic Explorer - 12601-12700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | blin2 12601* |
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.)
|
|
|
Theorem | blbas 12602 |
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.)
|
|
|
Theorem | blres 12603 |
A ball in a restricted metric space. (Contributed by Mario Carneiro,
5-Jan-2014.)
|
|
|
Theorem | xmeterval 12604 |
Value of the "finitely separated" relation. (Contributed by Mario
Carneiro, 24-Aug-2015.)
|
|
|
Theorem | xmeter 12605 |
The "finitely separated" relation is an equivalence relation.
(Contributed by Mario Carneiro, 24-Aug-2015.)
|
|
|
Theorem | xmetec 12606 |
The equivalence classes under the finite separation equivalence relation
are infinity balls. (Contributed by Mario Carneiro, 24-Aug-2015.)
|
|
|
Theorem | blssec 12607 |
A ball centered at is
contained in the set of points finitely
separated from . This is just an application of ssbl 12595
to the
infinity ball. (Contributed by Mario Carneiro, 24-Aug-2015.)
|
|
|
Theorem | blpnfctr 12608 |
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.)
|
|
|
Theorem | xmetresbl 12609 |
An extended metric restricted to any ball (in particular the infinity
ball) is a proper metric. Together with xmetec 12606, 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.)
|
|
|
7.2.4 Open sets of a metric space
|
|
Theorem | mopnrel 12610 |
The class of open sets of a metric space is a relation. (Contributed by
Jim Kingdon, 5-May-2023.)
|
|
|
Theorem | mopnval 12611 |
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
is the family of all open sets in the metric space
determined by the metric . By mopntop 12613, the open sets of a
metric space form a topology , whose base set is by
mopnuni 12614. (Contributed by NM, 1-Sep-2006.) (Revised
by Mario
Carneiro, 12-Nov-2013.)
|
|
|
Theorem | mopntopon 12612 |
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.)
|
TopOn |
|
Theorem | mopntop 12613 |
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.)
|
|
|
Theorem | mopnuni 12614 |
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.)
|
|
|
Theorem | elmopn 12615* |
The defining property of an open set of a metric space. (Contributed by
NM, 1-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)
|
|
|
Theorem | mopnfss 12616 |
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.)
|
|
|
Theorem | mopnm 12617 |
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.)
|
|
|
Theorem | elmopn2 12618* |
A defining property of an open set of a metric space. (Contributed by
NM, 5-May-2007.) (Revised by Mario Carneiro, 12-Nov-2013.)
|
|
|
Theorem | mopnss 12619 |
An open set of a metric space is a subspace of its base set.
(Contributed by NM, 3-Sep-2006.)
|
|
|
Theorem | isxms 12620 |
Express the predicate " is an extended metric space"
with underlying set and distance function . (Contributed by
Mario Carneiro, 2-Sep-2015.)
|
|
|
Theorem | isxms2 12621 |
Express the predicate " is an extended metric space"
with underlying set and distance function . (Contributed by
Mario Carneiro, 2-Sep-2015.)
|
|
|
Theorem | isms 12622 |
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.)
|
|
|
Theorem | isms2 12623 |
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.)
|
|
|
Theorem | xmstopn 12624 |
The topology component of an extended metric space coincides with the
topology generated by the metric component. (Contributed by Mario
Carneiro, 26-Aug-2015.)
|
|
|
Theorem | mstopn 12625 |
The topology component of a metric space coincides with the topology
generated by the metric component. (Contributed by Mario Carneiro,
26-Aug-2015.)
|
|
|
Theorem | xmstps 12626 |
An extended metric space is a topological space. (Contributed by Mario
Carneiro, 26-Aug-2015.)
|
|
|
Theorem | msxms 12627 |
A metric space is an extended metric space. (Contributed by Mario
Carneiro, 26-Aug-2015.)
|
|
|
Theorem | mstps 12628 |
A metric space is a topological space. (Contributed by Mario Carneiro,
26-Aug-2015.)
|
|
|
Theorem | xmsxmet 12629 |
The distance function, suitably truncated, is an extended metric on
. (Contributed
by Mario Carneiro, 2-Sep-2015.)
|
|
|
Theorem | msmet 12630 |
The distance function, suitably truncated, is a metric on .
(Contributed by Mario Carneiro, 12-Nov-2013.)
|
|
|
Theorem | msf 12631 |
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.)
|
|
|
Theorem | xmsxmet2 12632 |
The distance function, suitably truncated, is an extended metric on
. (Contributed
by Mario Carneiro, 2-Oct-2015.)
|
|
|
Theorem | msmet2 12633 |
The distance function, suitably truncated, is a metric on .
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
|
|
Theorem | mscl 12634 |
Closure of the distance function of a metric space. (Contributed by NM,
30-Aug-2006.) (Revised by Mario Carneiro, 2-Oct-2015.)
|
|
|
Theorem | xmscl 12635 |
Closure of the distance function of an extended metric space.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
|
|
Theorem | xmsge0 12636 |
The distance function in an extended metric space is nonnegative.
(Contributed by Mario Carneiro, 4-Oct-2015.)
|
|
|
Theorem | xmseq0 12637 |
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.)
|
|
|
Theorem | xmssym 12638 |
The distance function in an extended metric space is symmetric.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
|
|
Theorem | xmstri2 12639 |
Triangle inequality for the distance function of an extended metric.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
|
|
Theorem | mstri2 12640 |
Triangle inequality for the distance function of a metric space.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
|
|
Theorem | xmstri 12641 |
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.)
|
|
|
Theorem | mstri 12642 |
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.)
|
|
|
Theorem | xmstri3 12643 |
Triangle inequality for the distance function of an extended metric.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
|
|
Theorem | mstri3 12644 |
Triangle inequality for the distance function of a metric space.
(Contributed by Mario Carneiro, 2-Oct-2015.)
|
|
|
Theorem | msrtri 12645 |
Reverse triangle inequality for the distance function of a metric space.
(Contributed by Mario Carneiro, 4-Oct-2015.)
|
|
|
Theorem | xmspropd 12646 |
Property deduction for an extended metric space. (Contributed by Mario
Carneiro, 4-Oct-2015.)
|
|
|
Theorem | mspropd 12647 |
Property deduction for a metric space. (Contributed by Mario Carneiro,
4-Oct-2015.)
|
|
|
Theorem | setsmsbasg 12648 |
The base set of a constructed metric space. (Contributed by Mario
Carneiro, 28-Aug-2015.)
|
sSet TopSet
|
|
Theorem | setsmsdsg 12649 |
The distance function of a constructed metric space. (Contributed by
Mario Carneiro, 28-Aug-2015.)
|
sSet TopSet
|
|
Theorem | setsmstsetg 12650 |
The topology of a constructed metric space. (Contributed by Mario
Carneiro, 28-Aug-2015.) (Revised by Jim Kingdon, 7-May-2023.)
|
sSet TopSet
TopSet |
|
Theorem | mopni 12651* |
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.)
|
|
|
Theorem | mopni2 12652* |
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.)
|
|
|
Theorem | mopni3 12653* |
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.)
|
|
|
Theorem | blssopn 12654 |
The balls of a metric space are open sets. (Contributed by NM,
12-Sep-2006.) (Revised by Mario Carneiro, 23-Dec-2013.)
|
|
|
Theorem | unimopn 12655 |
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.)
|
|
|
Theorem | mopnin 12656 |
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.)
|
|
|
Theorem | mopn0 12657 |
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.)
|
|
|
Theorem | rnblopn 12658 |
A ball of a metric space is an open set. (Contributed by NM,
12-Sep-2006.)
|
|
|
Theorem | blopn 12659 |
A ball of a metric space is an open set. (Contributed by NM,
9-Mar-2007.) (Revised by Mario Carneiro, 12-Nov-2013.)
|
|
|
Theorem | neibl 12660* |
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.)
|
|
|
Theorem | blnei 12661 |
A ball around a point is a neighborhood of the point. (Contributed by
NM, 8-Nov-2007.) (Revised by Mario Carneiro, 24-Aug-2015.)
|
|
|
Theorem | blsscls2 12662* |
A smaller closed ball is contained in a larger open ball. (Contributed
by Mario Carneiro, 10-Jan-2014.)
|
|
|
Theorem | metss 12663* |
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.)
|
|
|
Theorem | metequiv 12664* |
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.)
|
|
|
Theorem | metequiv2 12665* |
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.)
|
|
|
Theorem | metss2lem 12666* |
Lemma for metss2 12667. (Contributed by Mario Carneiro,
14-Sep-2015.)
|
|
|
Theorem | metss2 12667* |
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.)
|
|
|
Theorem | comet 12668* |
The composition of an extended metric with a monotonic subadditive
function is an extended metric. (Contributed by Mario Carneiro,
21-Mar-2015.)
|
|
|
Theorem | bdmetval 12669* |
Value of the standard bounded metric. (Contributed by Mario Carneiro,
26-Aug-2015.) (Revised by Jim Kingdon, 9-May-2023.)
|
inf
inf
|
|
Theorem | bdxmet 12670* |
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
|
|
Theorem | bdmet 12671* |
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 |
|
Theorem | bdbl 12672* |
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
|
|
Theorem | bdmopn 12673* |
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 |
|
Theorem | mopnex 12674* |
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.)
|
|
|
Theorem | metrest 12675 |
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.)
|
↾t |
|
Theorem | xmetxp 12676* |
The maximum metric (Chebyshev distance) on the product of two sets.
(Contributed by Jim Kingdon, 11-Oct-2023.)
|
|
|
Theorem | xmetxpbl 12677* |
The maximum metric (Chebyshev distance) on the product of two sets,
expressed in terms of balls centered on a point with radius
.
(Contributed by Jim Kingdon, 22-Oct-2023.)
|
|
|
Theorem | xmettxlem 12678* |
Lemma for xmettx 12679. (Contributed by Jim Kingdon, 15-Oct-2023.)
|
|
|
Theorem | xmettx 12679* |
The maximum metric (Chebyshev distance) on the product of two sets,
expressed as a binary topological product. (Contributed by Jim
Kingdon, 11-Oct-2023.)
|
|
|
7.2.5 Continuity in metric spaces
|
|
Theorem | metcnp3 12680* |
Two ways to express that is continuous at for metric spaces.
Proposition 14-4.2 of [Gleason] p. 240.
(Contributed by NM,
17-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
|
|
|
Theorem | metcnp 12681* |
Two ways to say a mapping from metric to metric is
continuous at point . (Contributed by NM, 11-May-2007.) (Revised
by Mario Carneiro, 28-Aug-2015.)
|
|
|
Theorem | metcnp2 12682* |
Two ways to say a mapping from metric to metric is
continuous at point . The distance arguments are swapped compared
to metcnp 12681 (and Munkres' metcn 12683) for compatibility with df-lm 12359.
Definition 1.3-3 of [Kreyszig] p. 20.
(Contributed by NM, 4-Jun-2007.)
(Revised by Mario Carneiro, 13-Nov-2013.)
|
|
|
Theorem | metcn 12683* |
Two ways to say a mapping from metric to metric is
continuous. Theorem 10.1 of [Munkres]
p. 127. The second biconditional
argument says that for every positive "epsilon" there is a
positive "delta" such that a distance less than delta in
maps to a distance less than epsilon in . (Contributed by NM,
15-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
|
|
|
Theorem | metcnpi 12684* |
Epsilon-delta property of a continuous metric space function, with
function arguments as in metcnp 12681. (Contributed by NM, 17-Dec-2007.)
(Revised by Mario Carneiro, 13-Nov-2013.)
|
|
|
Theorem | metcnpi2 12685* |
Epsilon-delta property of a continuous metric space function, with
swapped distance function arguments as in metcnp2 12682. (Contributed by
NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|
|
|
Theorem | metcnpi3 12686* |
Epsilon-delta property of a metric space function continuous at .
A variation of metcnpi2 12685 with non-strict ordering. (Contributed by
NM,
16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|
|
|
Theorem | txmetcnp 12687* |
Continuity of a binary operation on metric spaces. (Contributed by
Mario Carneiro, 2-Sep-2015.) (Revised by Jim Kingdon, 22-Oct-2023.)
|
|
|
Theorem | txmetcn 12688* |
Continuity of a binary operation on metric spaces. (Contributed by
Mario Carneiro, 2-Sep-2015.)
|
|
|
Theorem | metcnpd 12689* |
Two ways to say a mapping from metric to metric is
continuous at point . (Contributed by Jim Kingdon,
14-Jun-2023.)
|
|
|
7.2.6 Topology on the reals
|
|
Theorem | qtopbasss 12690* |
The set of open intervals with endpoints in a subset forms a basis for a
topology. (Contributed by Mario Carneiro, 17-Jun-2014.) (Revised by
Jim Kingdon, 22-May-2023.)
|
inf
|
|
Theorem | qtopbas 12691 |
The set of open intervals with rational endpoints forms a basis for a
topology. (Contributed by NM, 8-Mar-2007.)
|
|
|
Theorem | retopbas 12692 |
A basis for the standard topology on the reals. (Contributed by NM,
6-Feb-2007.) (Proof shortened by Mario Carneiro, 17-Jun-2014.)
|
|
|
Theorem | retop 12693 |
The standard topology on the reals. (Contributed by FL, 4-Jun-2007.)
|
|
|
Theorem | uniretop 12694 |
The underlying set of the standard topology on the reals is the reals.
(Contributed by FL, 4-Jun-2007.)
|
|
|
Theorem | retopon 12695 |
The standard topology on the reals is a topology on the reals.
(Contributed by Mario Carneiro, 28-Aug-2015.)
|
TopOn |
|
Theorem | retps 12696 |
The standard topological space on the reals. (Contributed by NM,
19-Oct-2012.)
|
TopSet
|
|
Theorem | iooretopg 12697 |
Open intervals are open sets of the standard topology on the reals .
(Contributed by FL, 18-Jun-2007.) (Revised by Jim Kingdon,
23-May-2023.)
|
|
|
Theorem | cnmetdval 12698 |
Value of the distance function of the metric space of complex numbers.
(Contributed by NM, 9-Dec-2006.) (Revised by Mario Carneiro,
27-Dec-2014.)
|
|
|
Theorem | cnmet 12699 |
The absolute value metric determines a metric space on the complex
numbers. This theorem provides a link between complex numbers and
metrics spaces, making metric space theorems available for use with
complex numbers. (Contributed by FL, 9-Oct-2006.)
|
|
|
Theorem | cnxmet 12700 |
The absolute value metric is an extended metric. (Contributed by Mario
Carneiro, 28-Aug-2015.)
|
|