Theorem List for Intuitionistic Logic Explorer - 12601-12700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | mopnex 12601* |
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 12602 |
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 12603* |
The maximum metric (Chebyshev distance) on the product of two sets.
(Contributed by Jim Kingdon, 11-Oct-2023.)
|
|
|
Theorem | xmetxpbl 12604* |
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 12605* |
Lemma for xmettx 12606. (Contributed by Jim Kingdon, 15-Oct-2023.)
|
|
|
Theorem | xmettx 12606* |
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 12607* |
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 12608* |
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 12609* |
Two ways to say a mapping from metric to metric is
continuous at point . The distance arguments are swapped compared
to metcnp 12608 (and Munkres' metcn 12610) for compatibility with df-lm 12286.
Definition 1.3-3 of [Kreyszig] p. 20.
(Contributed by NM, 4-Jun-2007.)
(Revised by Mario Carneiro, 13-Nov-2013.)
|
|
|
Theorem | metcn 12610* |
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 12611* |
Epsilon-delta property of a continuous metric space function, with
function arguments as in metcnp 12608. (Contributed by NM, 17-Dec-2007.)
(Revised by Mario Carneiro, 13-Nov-2013.)
|
|
|
Theorem | metcnpi2 12612* |
Epsilon-delta property of a continuous metric space function, with
swapped distance function arguments as in metcnp2 12609. (Contributed by
NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|
|
|
Theorem | metcnpi3 12613* |
Epsilon-delta property of a metric space function continuous at .
A variation of metcnpi2 12612 with non-strict ordering. (Contributed by
NM,
16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|
|
|
Theorem | txmetcnp 12614* |
Continuity of a binary operation on metric spaces. (Contributed by
Mario Carneiro, 2-Sep-2015.) (Revised by Jim Kingdon, 22-Oct-2023.)
|
|
|
Theorem | txmetcn 12615* |
Continuity of a binary operation on metric spaces. (Contributed by
Mario Carneiro, 2-Sep-2015.)
|
|
|
Theorem | metcnpd 12616* |
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 12617* |
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 12618 |
The set of open intervals with rational endpoints forms a basis for a
topology. (Contributed by NM, 8-Mar-2007.)
|
|
|
Theorem | retopbas 12619 |
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 12620 |
The standard topology on the reals. (Contributed by FL, 4-Jun-2007.)
|
|
|
Theorem | uniretop 12621 |
The underlying set of the standard topology on the reals is the reals.
(Contributed by FL, 4-Jun-2007.)
|
|
|
Theorem | retopon 12622 |
The standard topology on the reals is a topology on the reals.
(Contributed by Mario Carneiro, 28-Aug-2015.)
|
TopOn |
|
Theorem | retps 12623 |
The standard topological space on the reals. (Contributed by NM,
19-Oct-2012.)
|
TopSet
|
|
Theorem | iooretopg 12624 |
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 12625 |
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 12626 |
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 12627 |
The absolute value metric is an extended metric. (Contributed by Mario
Carneiro, 28-Aug-2015.)
|
|
|
Theorem | cntoptopon 12628 |
The topology of the complex numbers is a topology. (Contributed by Jim
Kingdon, 6-Jun-2023.)
|
TopOn |
|
Theorem | cntoptop 12629 |
The topology of the complex numbers is a topology. (Contributed by Jim
Kingdon, 6-Jun-2023.)
|
|
|
Theorem | cnbl0 12630 |
Two ways to write the open ball centered at zero. (Contributed by Mario
Carneiro, 8-Sep-2015.)
|
|
|
Theorem | cnblcld 12631* |
Two ways to write the closed ball centered at zero. (Contributed by
Mario Carneiro, 8-Sep-2015.)
|
|
|
Theorem | unicntopcntop 12632 |
The underlying set of the standard topology on the complex numbers is the
set of complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(Revised by Jim Kingdon, 12-Dec-2023.)
|
|
|
Theorem | cnopncntop 12633 |
The set of complex numbers is open with respect to the standard topology
on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(Revised by Jim Kingdon, 12-Dec-2023.)
|
|
|
Theorem | reopnap 12634* |
The real numbers apart from a given real number form an open set.
(Contributed by Jim Kingdon, 13-Dec-2023.)
|
#
|
|
Theorem | remetdval 12635 |
Value of the distance function of the metric space of real numbers.
(Contributed by NM, 16-May-2007.)
|
|
|
Theorem | remet 12636 |
The absolute value metric determines a metric space on the reals.
(Contributed by NM, 10-Feb-2007.)
|
|
|
Theorem | rexmet 12637 |
The absolute value metric is an extended metric. (Contributed by Mario
Carneiro, 28-Aug-2015.)
|
|
|
Theorem | bl2ioo 12638 |
A ball in terms of an open interval of reals. (Contributed by NM,
18-May-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|
|
|
Theorem | ioo2bl 12639 |
An open interval of reals in terms of a ball. (Contributed by NM,
18-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
|
|
|
Theorem | ioo2blex 12640 |
An open interval of reals in terms of a ball. (Contributed by Mario
Carneiro, 14-Nov-2013.)
|
|
|
Theorem | blssioo 12641 |
The balls of the standard real metric space are included in the open
real intervals. (Contributed by NM, 8-May-2007.) (Revised by Mario
Carneiro, 13-Nov-2013.)
|
|
|
Theorem | tgioo 12642 |
The topology generated by open intervals of reals is the same as the
open sets of the standard metric space on the reals. (Contributed by
NM, 7-May-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|
|
|
Theorem | tgqioo 12643 |
The topology generated by open intervals of reals with rational
endpoints is the same as the open sets of the standard metric space on
the reals. In particular, this proves that the standard topology on the
reals is second-countable. (Contributed by Mario Carneiro,
17-Jun-2014.)
|
|
|
Theorem | resubmet 12644 |
The subspace topology induced by a subset of the reals. (Contributed by
Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Aug-2014.)
|
↾t |
|
Theorem | tgioo2cntop 12645 |
The standard topology on the reals is a subspace of the complex metric
topology. (Contributed by Mario Carneiro, 13-Aug-2014.) (Revised by
Jim Kingdon, 6-Aug-2023.)
|
↾t |
|
Theorem | rerestcntop 12646 |
The subspace topology induced by a subset of the reals. (Contributed by
Mario Carneiro, 13-Aug-2014.) (Revised by Jim Kingdon, 6-Aug-2023.)
|
↾t ↾t |
|
Theorem | addcncntoplem 12647* |
Lemma for addcncntop 12648, subcncntop 12649, and mulcncntop 12650.
(Contributed by Mario Carneiro, 5-May-2014.) (Revised by Jim Kingdon,
22-Oct-2023.)
|
|
|
Theorem | addcncntop 12648 |
Complex number addition is a continuous function. Part of Proposition
14-4.16 of [Gleason] p. 243.
(Contributed by NM, 30-Jul-2007.) (Proof
shortened by Mario Carneiro, 5-May-2014.)
|
|
|
Theorem | subcncntop 12649 |
Complex number subtraction is a continuous function. Part of
Proposition 14-4.16 of [Gleason] p. 243.
(Contributed by NM,
4-Aug-2007.) (Proof shortened by Mario Carneiro, 5-May-2014.)
|
|
|
Theorem | mulcncntop 12650 |
Complex number multiplication is a continuous function. Part of
Proposition 14-4.16 of [Gleason] p. 243.
(Contributed by NM,
30-Jul-2007.) (Proof shortened by Mario Carneiro, 5-May-2014.)
|
|
|
Theorem | divcnap 12651* |
Complex number division is a continuous function, when the second
argument is apart from zero. (Contributed by Mario Carneiro,
12-Aug-2014.) (Revised by Jim Kingdon, 25-Oct-2023.)
|
↾t
#
#
|
|
Theorem | fsumcncntop 12652* |
A finite sum of functions to complex numbers from a common topological
space is continuous. The class expression for normally contains
free variables
and to index it.
(Contributed by NM,
8-Aug-2007.) (Revised by Mario Carneiro, 23-Aug-2014.)
|
TopOn
|
|
7.2.7 Topological definitions using the
reals
|
|
Syntax | ccncf 12653 |
Extend class notation to include the operation which returns a class of
continuous complex functions.
|
|
|
Definition | df-cncf 12654* |
Define the operation whose value is a class of continuous complex
functions. (Contributed by Paul Chapman, 11-Oct-2007.)
|
|
|
Theorem | cncfval 12655* |
The value of the continuous complex function operation is the set of
continuous functions from to .
(Contributed by Paul
Chapman, 11-Oct-2007.) (Revised by Mario Carneiro, 9-Nov-2013.)
|
|
|
Theorem | elcncf 12656* |
Membership in the set of continuous complex functions from to
. (Contributed
by Paul Chapman, 11-Oct-2007.) (Revised by Mario
Carneiro, 9-Nov-2013.)
|
|
|
Theorem | elcncf2 12657* |
Version of elcncf 12656 with arguments commuted. (Contributed by
Mario
Carneiro, 28-Apr-2014.)
|
|
|
Theorem | cncfrss 12658 |
Reverse closure of the continuous function predicate. (Contributed by
Mario Carneiro, 25-Aug-2014.)
|
|
|
Theorem | cncfrss2 12659 |
Reverse closure of the continuous function predicate. (Contributed by
Mario Carneiro, 25-Aug-2014.)
|
|
|
Theorem | cncff 12660 |
A continuous complex function's domain and codomain. (Contributed by
Paul Chapman, 17-Jan-2008.) (Revised by Mario Carneiro,
25-Aug-2014.)
|
|
|
Theorem | cncfi 12661* |
Defining property of a continuous function. (Contributed by Mario
Carneiro, 30-Apr-2014.) (Revised by Mario Carneiro, 25-Aug-2014.)
|
|
|
Theorem | elcncf1di 12662* |
Membership in the set of continuous complex functions from to
. (Contributed
by Paul Chapman, 26-Nov-2007.)
|
|
|
Theorem | elcncf1ii 12663* |
Membership in the set of continuous complex functions from to
. (Contributed
by Paul Chapman, 26-Nov-2007.)
|
|
|
Theorem | rescncf 12664 |
A continuous complex function restricted to a subset is continuous.
(Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro,
25-Aug-2014.)
|
|
|
Theorem | cncffvrn 12665 |
Change the codomain of a continuous complex function. (Contributed by
Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 1-May-2015.)
|
|
|
Theorem | cncfss 12666 |
The set of continuous functions is expanded when the range is expanded.
(Contributed by Mario Carneiro, 30-Aug-2014.)
|
|
|
Theorem | climcncf 12667 |
Image of a limit under a continuous map. (Contributed by Mario
Carneiro, 7-Apr-2015.)
|
|
|
Theorem | abscncf 12668 |
Absolute value is continuous. (Contributed by Paul Chapman,
21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
|
|
|
Theorem | recncf 12669 |
Real part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.)
(Revised by Mario Carneiro, 28-Apr-2014.)
|
|
|
Theorem | imcncf 12670 |
Imaginary part is continuous. (Contributed by Paul Chapman,
21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
|
|
|
Theorem | cjcncf 12671 |
Complex conjugate is continuous. (Contributed by Paul Chapman,
21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
|
|
|
Theorem | mulc1cncf 12672* |
Multiplication by a constant is continuous. (Contributed by Paul
Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
|
|
|
Theorem | divccncfap 12673* |
Division by a constant is continuous. (Contributed by Paul Chapman,
28-Nov-2007.) (Revised by Jim Kingdon, 9-Jan-2023.)
|
# |
|
Theorem | cncfco 12674 |
The composition of two continuous maps on complex numbers is also
continuous. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by
Mario Carneiro, 25-Aug-2014.)
|
|
|
Theorem | cncfmet 12675 |
Relate complex function continuity to metric space continuity.
(Contributed by Paul Chapman, 26-Nov-2007.) (Revised by Mario Carneiro,
7-Sep-2015.)
|
|
|
Theorem | cncfcncntop 12676 |
Relate complex function continuity to topological continuity.
(Contributed by Mario Carneiro, 17-Feb-2015.)
|
↾t ↾t
|
|
Theorem | cncfcn1cntop 12677 |
Relate complex function continuity to topological continuity.
(Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro,
7-Sep-2015.) (Revised by Jim Kingdon, 16-Jun-2023.)
|
|
|
Theorem | cncfmptc 12678* |
A constant function is a continuous function on . (Contributed
by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro,
7-Sep-2015.)
|
|
|
Theorem | cncfmptid 12679* |
The identity function is a continuous function on . (Contributed
by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro,
17-May-2016.)
|
|
|
Theorem | cncfmpt1f 12680* |
Composition of continuous functions. analogue of cnmpt11f 12380.
(Contributed by Mario Carneiro, 3-Sep-2014.)
|
|
|
Theorem | cncfmpt2fcntop 12681* |
Composition of continuous functions. analogue of cnmpt12f 12382.
(Contributed by Mario Carneiro, 3-Sep-2014.)
|
|
|
Theorem | addccncf 12682* |
Adding a constant is a continuous function. (Contributed by Jeff
Madsen, 2-Sep-2009.)
|
|
|
Theorem | cdivcncfap 12683* |
Division with a constant numerator is continuous. (Contributed by Mario
Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 26-May-2023.)
|
#
#
|
|
Theorem | negcncf 12684* |
The negative function is continuous. (Contributed by Mario Carneiro,
30-Dec-2016.)
|
|
|
Theorem | negfcncf 12685* |
The negative of a continuous complex function is continuous.
(Contributed by Paul Chapman, 21-Jan-2008.) (Revised by Mario Carneiro,
25-Aug-2014.)
|
|
|
Theorem | mulcncflem 12686* |
Lemma for mulcncf 12687. (Contributed by Jim Kingdon, 29-May-2023.)
|
|
|
Theorem | mulcncf 12687* |
The multiplication of two continuous complex functions is continuous.
(Contributed by Glauco Siliprandi, 29-Jun-2017.)
|
|
|
Theorem | expcncf 12688* |
The power function on complex numbers, for fixed exponent N, is
continuous. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|
|
|
Theorem | cnrehmeocntop 12689* |
The canonical bijection from to described in
cnref1o 9408 is in fact a homeomorphism of the usual
topologies on these
sets. (It is also an isometry, if
is metrized with the
l<SUP>2</SUP> norm.) (Contributed by Mario Carneiro,
25-Aug-2014.)
|
|
|
Theorem | cnopnap 12690* |
The complex numbers apart from a given complex number form an open set.
(Contributed by Jim Kingdon, 14-Dec-2023.)
|
#
|
|
PART 8 BASIC REAL AND COMPLEX
ANALYSIS
|
|
8.0.1 Dedekind cuts
|
|
Theorem | dedekindeulemuub 12691* |
Lemma for dedekindeu 12697. Any element of the upper cut is an upper
bound for the lower cut. (Contributed by Jim Kingdon, 2-Feb-2024.)
|
|
|
Theorem | dedekindeulemub 12692* |
Lemma for dedekindeu 12697. The lower cut has an upper bound.
(Contributed by Jim Kingdon, 31-Jan-2024.)
|
|
|
Theorem | dedekindeulemloc 12693* |
Lemma for dedekindeu 12697. The set L is located. (Contributed by Jim
Kingdon, 31-Jan-2024.)
|
|
|
Theorem | dedekindeulemlub 12694* |
Lemma for dedekindeu 12697. The set L has a least upper bound.
(Contributed by Jim Kingdon, 31-Jan-2024.)
|
|
|
Theorem | dedekindeulemlu 12695* |
Lemma for dedekindeu 12697. There is a number which separates the
lower
and upper cuts. (Contributed by Jim Kingdon, 31-Jan-2024.)
|
|
|
Theorem | dedekindeulemeu 12696* |
Lemma for dedekindeu 12697. Part of proving uniqueness. (Contributed
by
Jim Kingdon, 31-Jan-2024.)
|
|
|
Theorem | dedekindeu 12697* |
A Dedekind cut identifies a unique real number. Similar to df-inp 7242
except that the the Dedekind cut is formed by sets of reals (rather than
positive rationals). But in both cases the defining property of a
Dedekind cut is that it is inhabited (bounded), rounded, disjoint, and
located. (Contributed by Jim Kingdon, 5-Jan-2024.)
|
|
|
Theorem | suplociccreex 12698* |
An inhabited, bounded-above, located set of reals in a closed interval
has a supremum. A similar theorem is axsuploc 7805 but that one is for
the entire real line rather than a closed interval. (Contributed by
Jim Kingdon, 14-Feb-2024.)
|
|
|
Theorem | suplociccex 12699* |
An inhabited, bounded-above, located set of reals in a closed interval
has a supremum. A similar theorem is axsuploc 7805 but that one is for the
entire real line rather than a closed interval. (Contributed by Jim
Kingdon, 14-Feb-2024.)
|
|
|
Theorem | dedekindicclemuub 12700* |
Lemma for dedekindicc 12707. Any element of the upper cut is an upper
bound for the lower cut. (Contributed by Jim Kingdon,
15-Feb-2024.)
|
|