Type | Label | Description |
Statement |
|
Theorem | metss2 14401* |
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.)
|
β’ π½ = (MetOpenβπΆ)
& β’ πΎ = (MetOpenβπ·)
& β’ (π β πΆ β (Metβπ)) & β’ (π β π· β (Metβπ)) & β’ (π β π
β β+) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯πΆπ¦) β€ (π
Β· (π₯π·π¦))) β β’ (π β π½ β πΎ) |
|
Theorem | comet 14402* |
The composition of an extended metric with a monotonic subadditive
function is an extended metric. (Contributed by Mario Carneiro,
21-Mar-2015.)
|
β’ (π β π· β (βMetβπ)) & β’ (π β πΉ:(0[,]+β)βΆβ*) & β’ ((π β§ π₯ β (0[,]+β)) β ((πΉβπ₯) = 0 β π₯ = 0))
& β’ ((π
β§ (π₯ β (0[,]+β) β§
π¦ β (0[,]+β))) β
(π₯ β€ π¦ β (πΉβπ₯) β€ (πΉβπ¦)))
& β’ ((π
β§ (π₯ β (0[,]+β) β§
π¦ β (0[,]+β))) β
(πΉβ(π₯ +π π¦)) β€ ((πΉβπ₯) +π (πΉβπ¦))) β β’ (π
β (πΉ β π·) β (βMetβπ)) |
|
Theorem | bdmetval 14403* |
Value of the standard bounded metric. (Contributed by Mario Carneiro,
26-Aug-2015.) (Revised by Jim Kingdon, 9-May-2023.)
|
β’ π· = (π₯ β π, π¦ β π β¦ inf({(π₯πΆπ¦), π
}, β*, <
)) β β’ (((πΆ:(π Γ π)βΆβ* β§ π
β β*)
β§ (π΄ β π β§ π΅ β π)) β (π΄π·π΅) = inf({(π΄πΆπ΅), π
}, β*, <
)) |
|
Theorem | bdxmet 14404* |
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({(π₯πΆπ¦), π
}, β*, <
)) β β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β π· β (βMetβπ)) |
|
Theorem | bdmet 14405* |
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({(π₯πΆπ¦), π
}, β*, <
)) β β’ ((πΆ β (βMetβπ) β§ π
β β+) β π· β (Metβπ)) |
|
Theorem | bdbl 14406* |
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({(π₯πΆπ¦), π
}, β*, <
)) β β’ (((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β§ (π β π β§ π β β* β§ π β€ π
)) β (π(ballβπ·)π) = (π(ballβπΆ)π)) |
|
Theorem | bdmopn 14407* |
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({(π₯πΆπ¦), π
}, β*, < )) & β’ π½ = (MetOpenβπΆ)
β β’ ((πΆ β (βMetβπ) β§ π
β β* β§ 0 <
π
) β π½ = (MetOpenβπ·)) |
|
Theorem | mopnex 14408* |
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.)
|
β’ π½ = (MetOpenβπ·) β β’ (π· β (βMetβπ) β βπ β (Metβπ)π½ = (MetOpenβπ)) |
|
Theorem | metrest 14409 |
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.)
|
β’ π· = (πΆ βΎ (π Γ π)) & β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·)
β β’ ((πΆ β (βMetβπ) β§ π β π) β (π½ βΎt π) = πΎ) |
|
Theorem | xmetxp 14410* |
The maximum metric (Chebyshev distance) on the product of two sets.
(Contributed by Jim Kingdon, 11-Oct-2023.)
|
β’ π = (π’ β (π Γ π), π£ β (π Γ π) β¦ sup({((1st
βπ’)π(1st βπ£)), ((2nd βπ’)π(2nd βπ£))}, β*, <
))
& β’ (π β π β (βMetβπ)) & β’ (π β π β (βMetβπ)) β β’ (π β π β (βMetβ(π Γ π))) |
|
Theorem | xmetxpbl 14411* |
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.)
|
β’ π = (π’ β (π Γ π), π£ β (π Γ π) β¦ sup({((1st
βπ’)π(1st βπ£)), ((2nd βπ’)π(2nd βπ£))}, β*, <
))
& β’ (π β π β (βMetβπ)) & β’ (π β π β (βMetβπ)) & β’ (π β π
β β*) & β’ (π β πΆ β (π Γ π)) β β’ (π β (πΆ(ballβπ)π
) = (((1st βπΆ)(ballβπ)π
) Γ ((2nd βπΆ)(ballβπ)π
))) |
|
Theorem | xmettxlem 14412* |
Lemma for xmettx 14413. (Contributed by Jim Kingdon, 15-Oct-2023.)
|
β’ π = (π’ β (π Γ π), π£ β (π Γ π) β¦ sup({((1st
βπ’)π(1st βπ£)), ((2nd βπ’)π(2nd βπ£))}, β*, <
))
& β’ (π β π β (βMetβπ)) & β’ (π β π β (βMetβπ)) & β’ π½ = (MetOpenβπ) & β’ πΎ = (MetOpenβπ) & β’ πΏ = (MetOpenβπ)
β β’ (π β πΏ β (π½ Γt πΎ)) |
|
Theorem | xmettx 14413* |
The maximum metric (Chebyshev distance) on the product of two sets,
expressed as a binary topological product. (Contributed by Jim
Kingdon, 11-Oct-2023.)
|
β’ π = (π’ β (π Γ π), π£ β (π Γ π) β¦ sup({((1st
βπ’)π(1st βπ£)), ((2nd βπ’)π(2nd βπ£))}, β*, <
))
& β’ (π β π β (βMetβπ)) & β’ (π β π β (βMetβπ)) & β’ π½ = (MetOpenβπ) & β’ πΎ = (MetOpenβπ) & β’ πΏ = (MetOpenβπ)
β β’ (π β πΏ = (π½ Γt πΎ)) |
|
8.2.5 Continuity in metric spaces
|
|
Theorem | metcnp3 14414* |
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.)
|
β’ π½ = (MetOpenβπΆ)
& β’ πΎ = (MetOpenβπ·) β β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ¦ β β+ βπ§ β β+
(πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦)))) |
|
Theorem | metcnp 14415* |
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.)
|
β’ π½ = (MetOpenβπΆ)
& β’ πΎ = (MetOpenβπ·) β β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ¦ β β+ βπ§ β β+
βπ€ β π ((ππΆπ€) < π§ β ((πΉβπ)π·(πΉβπ€)) < π¦)))) |
|
Theorem | metcnp2 14416* |
Two ways to say a mapping from metric πΆ to metric π· is
continuous at point π. The distance arguments are swapped
compared
to metcnp 14415 (and Munkres' metcn 14417) for compatibility with df-lm 14093.
Definition 1.3-3 of [Kreyszig] p. 20.
(Contributed by NM, 4-Jun-2007.)
(Revised by Mario Carneiro, 13-Nov-2013.)
|
β’ π½ = (MetOpenβπΆ)
& β’ πΎ = (MetOpenβπ·) β β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ¦ β β+ βπ§ β β+
βπ€ β π ((π€πΆπ) < π§ β ((πΉβπ€)π·(πΉβπ)) < π¦)))) |
|
Theorem | metcn 14417* |
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.)
|
β’ π½ = (MetOpenβπΆ)
& β’ πΎ = (MetOpenβπ·) β β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆπ β§ βπ₯ β π βπ¦ β β+ βπ§ β β+
βπ€ β π ((π₯πΆπ€) < π§ β ((πΉβπ₯)π·(πΉβπ€)) < π¦)))) |
|
Theorem | metcnpi 14418* |
Epsilon-delta property of a continuous metric space function, with
function arguments as in metcnp 14415. (Contributed by NM, 17-Dec-2007.)
(Revised by Mario Carneiro, 13-Nov-2013.)
|
β’ π½ = (MetOpenβπΆ)
& β’ πΎ = (MetOpenβπ·) β β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β
βπ₯ β
β+ βπ¦ β π ((ππΆπ¦) < π₯ β ((πΉβπ)π·(πΉβπ¦)) < π΄)) |
|
Theorem | metcnpi2 14419* |
Epsilon-delta property of a continuous metric space function, with
swapped distance function arguments as in metcnp2 14416. (Contributed by
NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|
β’ π½ = (MetOpenβπΆ)
& β’ πΎ = (MetOpenβπ·) β β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β
βπ₯ β
β+ βπ¦ β π ((π¦πΆπ) < π₯ β ((πΉβπ¦)π·(πΉβπ)) < π΄)) |
|
Theorem | metcnpi3 14420* |
Epsilon-delta property of a metric space function continuous at π.
A variation of metcnpi2 14419 with non-strict ordering. (Contributed by
NM,
16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|
β’ π½ = (MetOpenβπΆ)
& β’ πΎ = (MetOpenβπ·) β β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β
βπ₯ β
β+ βπ¦ β π ((π¦πΆπ) β€ π₯ β ((πΉβπ¦)π·(πΉβπ)) β€ π΄)) |
|
Theorem | txmetcnp 14421* |
Continuity of a binary operation on metric spaces. (Contributed by
Mario Carneiro, 2-Sep-2015.) (Revised by Jim Kingdon, 22-Oct-2023.)
|
β’ π½ = (MetOpenβπΆ)
& β’ πΎ = (MetOpenβπ·)
& β’ πΏ = (MetOpenβπΈ) β β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ πΈ β (βMetβπ)) β§ (π΄ β π β§ π΅ β π)) β (πΉ β (((π½ Γt πΎ) CnP πΏ)ββ¨π΄, π΅β©) β (πΉ:(π Γ π)βΆπ β§ βπ§ β β+ βπ€ β β+
βπ’ β π βπ£ β π (((π΄πΆπ’) < π€ β§ (π΅π·π£) < π€) β ((π΄πΉπ΅)πΈ(π’πΉπ£)) < π§)))) |
|
Theorem | txmetcn 14422* |
Continuity of a binary operation on metric spaces. (Contributed by
Mario Carneiro, 2-Sep-2015.)
|
β’ π½ = (MetOpenβπΆ)
& β’ πΎ = (MetOpenβπ·)
& β’ πΏ = (MetOpenβπΈ) β β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ πΈ β (βMetβπ)) β (πΉ β ((π½ Γt πΎ) Cn πΏ) β (πΉ:(π Γ π)βΆπ β§ βπ₯ β π βπ¦ β π βπ§ β β+ βπ€ β β+
βπ’ β π βπ£ β π (((π₯πΆπ’) < π€ β§ (π¦π·π£) < π€) β ((π₯πΉπ¦)πΈ(π’πΉπ£)) < π§)))) |
|
Theorem | metcnpd 14423* |
Two ways to say a mapping from metric πΆ to metric π· is
continuous at point π. (Contributed by Jim Kingdon,
14-Jun-2023.)
|
β’ (π β π½ = (MetOpenβπΆ)) & β’ (π β πΎ = (MetOpenβπ·)) & β’ (π β πΆ β (βMetβπ)) & β’ (π β π· β (βMetβπ)) & β’ (π β π β π) β β’ (π β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ¦ β β+ βπ§ β β+
βπ€ β π ((ππΆπ€) < π§ β ((πΉβπ)π·(πΉβπ€)) < π¦)))) |
|
8.2.6 Topology on the reals
|
|
Theorem | qtopbasss 14424* |
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.)
|
β’ π β β* & β’ ((π₯ β π β§ π¦ β π) β sup({π₯, π¦}, β*, < ) β π) & β’ ((π₯ β π β§ π¦ β π) β inf({π₯, π¦}, β*, < ) β π)
β β’ ((,) β (π Γ π)) β TopBases |
|
Theorem | qtopbas 14425 |
The set of open intervals with rational endpoints forms a basis for a
topology. (Contributed by NM, 8-Mar-2007.)
|
β’ ((,) β (β Γ β))
β TopBases |
|
Theorem | retopbas 14426 |
A basis for the standard topology on the reals. (Contributed by NM,
6-Feb-2007.) (Proof shortened by Mario Carneiro, 17-Jun-2014.)
|
β’ ran (,) β TopBases |
|
Theorem | retop 14427 |
The standard topology on the reals. (Contributed by FL, 4-Jun-2007.)
|
β’ (topGenβran (,)) β
Top |
|
Theorem | uniretop 14428 |
The underlying set of the standard topology on the reals is the reals.
(Contributed by FL, 4-Jun-2007.)
|
β’ β = βͺ
(topGenβran (,)) |
|
Theorem | retopon 14429 |
The standard topology on the reals is a topology on the reals.
(Contributed by Mario Carneiro, 28-Aug-2015.)
|
β’ (topGenβran (,)) β
(TopOnββ) |
|
Theorem | retps 14430 |
The standard topological space on the reals. (Contributed by NM,
19-Oct-2012.)
|
β’ πΎ = {β¨(Baseβndx), ββ©,
β¨(TopSetβndx), (topGenβran
(,))β©} β β’ πΎ β TopSp |
|
Theorem | iooretopg 14431 |
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.)
|
β’ ((π΄ β β* β§ π΅ β β*)
β (π΄(,)π΅) β (topGenβran
(,))) |
|
Theorem | cnmetdval 14432 |
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.)
|
β’ π· = (abs β β
) β β’ ((π΄ β β β§ π΅ β β) β (π΄π·π΅) = (absβ(π΄ β π΅))) |
|
Theorem | cnmet 14433 |
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.)
|
β’ (abs β β ) β
(Metββ) |
|
Theorem | cnxmet 14434 |
The absolute value metric is an extended metric. (Contributed by Mario
Carneiro, 28-Aug-2015.)
|
β’ (abs β β ) β
(βMetββ) |
|
Theorem | cntoptopon 14435 |
The topology of the complex numbers is a topology. (Contributed by Jim
Kingdon, 6-Jun-2023.)
|
β’ π½ = (MetOpenβ(abs β β
)) β β’ π½ β
(TopOnββ) |
|
Theorem | cntoptop 14436 |
The topology of the complex numbers is a topology. (Contributed by Jim
Kingdon, 6-Jun-2023.)
|
β’ π½ = (MetOpenβ(abs β β
)) β β’ π½ β Top |
|
Theorem | cnbl0 14437 |
Two ways to write the open ball centered at zero. (Contributed by Mario
Carneiro, 8-Sep-2015.)
|
β’ π· = (abs β β
) β β’ (π
β β* β (β‘abs β (0[,)π
)) = (0(ballβπ·)π
)) |
|
Theorem | cnblcld 14438* |
Two ways to write the closed ball centered at zero. (Contributed by
Mario Carneiro, 8-Sep-2015.)
|
β’ π· = (abs β β
) β β’ (π
β β* β (β‘abs β (0[,]π
)) = {π₯ β β β£ (0π·π₯) β€ π
}) |
|
Theorem | unicntopcntop 14439 |
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.)
|
β’ β = βͺ
(MetOpenβ(abs β β )) |
|
Theorem | cnopncntop 14440 |
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.)
|
β’ β β (MetOpenβ(abs β
β )) |
|
Theorem | reopnap 14441* |
The real numbers apart from a given real number form an open set.
(Contributed by Jim Kingdon, 13-Dec-2023.)
|
β’ (π΄ β β β {π€ β β β£ π€ # π΄} β (topGenβran
(,))) |
|
Theorem | remetdval 14442 |
Value of the distance function of the metric space of real numbers.
(Contributed by NM, 16-May-2007.)
|
β’ π· = ((abs β β ) βΎ (β
Γ β)) β β’ ((π΄ β β β§ π΅ β β) β (π΄π·π΅) = (absβ(π΄ β π΅))) |
|
Theorem | remet 14443 |
The absolute value metric determines a metric space on the reals.
(Contributed by NM, 10-Feb-2007.)
|
β’ π· = ((abs β β ) βΎ (β
Γ β)) β β’ π· β
(Metββ) |
|
Theorem | rexmet 14444 |
The absolute value metric is an extended metric. (Contributed by Mario
Carneiro, 28-Aug-2015.)
|
β’ π· = ((abs β β ) βΎ (β
Γ β)) β β’ π· β
(βMetββ) |
|
Theorem | bl2ioo 14445 |
A ball in terms of an open interval of reals. (Contributed by NM,
18-May-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|
β’ π· = ((abs β β ) βΎ (β
Γ β)) β β’ ((π΄ β β β§ π΅ β β) β (π΄(ballβπ·)π΅) = ((π΄ β π΅)(,)(π΄ + π΅))) |
|
Theorem | ioo2bl 14446 |
An open interval of reals in terms of a ball. (Contributed by NM,
18-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)
|
β’ π· = ((abs β β ) βΎ (β
Γ β)) β β’ ((π΄ β β β§ π΅ β β) β (π΄(,)π΅) = (((π΄ + π΅) / 2)(ballβπ·)((π΅ β π΄) / 2))) |
|
Theorem | ioo2blex 14447 |
An open interval of reals in terms of a ball. (Contributed by Mario
Carneiro, 14-Nov-2013.)
|
β’ π· = ((abs β β ) βΎ (β
Γ β)) β β’ ((π΄ β β β§ π΅ β β) β (π΄(,)π΅) β ran (ballβπ·)) |
|
Theorem | blssioo 14448 |
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.)
|
β’ π· = ((abs β β ) βΎ (β
Γ β)) β β’ ran (ballβπ·) β ran
(,) |
|
Theorem | tgioo 14449 |
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.)
|
β’ π· = ((abs β β ) βΎ (β
Γ β))
& β’ π½ = (MetOpenβπ·) β β’ (topGenβran (,)) = π½ |
|
Theorem | tgqioo 14450 |
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.)
|
β’ π = (topGenβ((,) β (β
Γ β))) β β’ (topGenβran (,)) = π |
|
Theorem | resubmet 14451 |
The subspace topology induced by a subset of the reals. (Contributed by
Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Aug-2014.)
|
β’ π
= (topGenβran (,)) & β’ π½ = (MetOpenβ((abs β
β ) βΎ (π΄
Γ π΄))) β β’ (π΄ β β β π½ = (π
βΎt π΄)) |
|
Theorem | tgioo2cntop 14452 |
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.)
|
β’ π½ = (MetOpenβ(abs β β
)) β β’ (topGenβran (,)) = (π½ βΎt
β) |
|
Theorem | rerestcntop 14453 |
The subspace topology induced by a subset of the reals. (Contributed by
Mario Carneiro, 13-Aug-2014.) (Revised by Jim Kingdon, 6-Aug-2023.)
|
β’ π½ = (MetOpenβ(abs β β
))
& β’ π
= (topGenβran
(,)) β β’ (π΄ β β β (π½ βΎt π΄) = (π
βΎt π΄)) |
|
Theorem | addcncntoplem 14454* |
Lemma for addcncntop 14455, subcncntop 14456, and mulcncntop 14457.
(Contributed by Mario Carneiro, 5-May-2014.) (Revised by Jim Kingdon,
22-Oct-2023.)
|
β’ π½ = (MetOpenβ(abs β β
))
& β’ + :(β Γ
β)βΆβ
& β’ ((π β β+ β§ π β β β§ π β β) β
βπ¦ β
β+ βπ§ β β+ βπ’ β β βπ£ β β
(((absβ(π’ β
π)) < π¦ β§ (absβ(π£ β π)) < π§) β (absβ((π’ + π£) β (π + π))) < π)) β β’ + β ((π½ Γt π½) Cn π½) |
|
Theorem | addcncntop 14455 |
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.)
|
β’ π½ = (MetOpenβ(abs β β
)) β β’ + β ((π½ Γt π½) Cn π½) |
|
Theorem | subcncntop 14456 |
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.)
|
β’ π½ = (MetOpenβ(abs β β
)) β β’ β β ((π½ Γt π½) Cn π½) |
|
Theorem | mulcncntop 14457 |
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.)
|
β’ π½ = (MetOpenβ(abs β β
)) β β’ Β· β ((π½ Γt π½) Cn π½) |
|
Theorem | divcnap 14458* |
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.)
|
β’ π½ = (MetOpenβ(abs β β
))
& β’ πΎ = (π½ βΎt {π₯ β β β£ π₯ # 0}) β β’ (π¦ β β, π§ β {π₯ β β β£ π₯ # 0} β¦ (π¦ / π§)) β ((π½ Γt πΎ) Cn π½) |
|
Theorem | fsumcncntop 14459* |
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.)
|
β’ πΎ = (MetOpenβ(abs β β
))
& β’ (π β π½ β (TopOnβπ)) & β’ (π β π΄ β Fin) & β’ ((π β§ π β π΄) β (π₯ β π β¦ π΅) β (π½ Cn πΎ)) β β’ (π β (π₯ β π β¦ Ξ£π β π΄ π΅) β (π½ Cn πΎ)) |
|
8.2.7 Topological definitions using the
reals
|
|
Syntax | ccncf 14460 |
Extend class notation to include the operation which returns a class of
continuous complex functions.
|
class βcnβ |
|
Definition | df-cncf 14461* |
Define the operation whose value is a class of continuous complex
functions. (Contributed by Paul Chapman, 11-Oct-2007.)
|
β’ βcnβ = (π β π« β, π β π« β
β¦ {π β (π βπ
π) β£ βπ₯ β π βπ β β+ βπ β β+
βπ¦ β π ((absβ(π₯ β π¦)) < π β (absβ((πβπ₯) β (πβπ¦))) < π)}) |
|
Theorem | cncfval 14462* |
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.)
|
β’ ((π΄ β β β§ π΅ β β) β (π΄βcnβπ΅) = {π β (π΅ βπ π΄) β£ βπ₯ β π΄ βπ¦ β β+ βπ§ β β+
βπ€ β π΄ ((absβ(π₯ β π€)) < π§ β (absβ((πβπ₯) β (πβπ€))) < π¦)}) |
|
Theorem | elcncf 14463* |
Membership in the set of continuous complex functions from π΄ to
π΅. (Contributed by Paul Chapman,
11-Oct-2007.) (Revised by Mario
Carneiro, 9-Nov-2013.)
|
β’ ((π΄ β β β§ π΅ β β) β (πΉ β (π΄βcnβπ΅) β (πΉ:π΄βΆπ΅ β§ βπ₯ β π΄ βπ¦ β β+ βπ§ β β+
βπ€ β π΄ ((absβ(π₯ β π€)) < π§ β (absβ((πΉβπ₯) β (πΉβπ€))) < π¦)))) |
|
Theorem | elcncf2 14464* |
Version of elcncf 14463 with arguments commuted. (Contributed by
Mario
Carneiro, 28-Apr-2014.)
|
β’ ((π΄ β β β§ π΅ β β) β (πΉ β (π΄βcnβπ΅) β (πΉ:π΄βΆπ΅ β§ βπ₯ β π΄ βπ¦ β β+ βπ§ β β+
βπ€ β π΄ ((absβ(π€ β π₯)) < π§ β (absβ((πΉβπ€) β (πΉβπ₯))) < π¦)))) |
|
Theorem | cncfrss 14465 |
Reverse closure of the continuous function predicate. (Contributed by
Mario Carneiro, 25-Aug-2014.)
|
β’ (πΉ β (π΄βcnβπ΅) β π΄ β β) |
|
Theorem | cncfrss2 14466 |
Reverse closure of the continuous function predicate. (Contributed by
Mario Carneiro, 25-Aug-2014.)
|
β’ (πΉ β (π΄βcnβπ΅) β π΅ β β) |
|
Theorem | cncff 14467 |
A continuous complex function's domain and codomain. (Contributed by
Paul Chapman, 17-Jan-2008.) (Revised by Mario Carneiro,
25-Aug-2014.)
|
β’ (πΉ β (π΄βcnβπ΅) β πΉ:π΄βΆπ΅) |
|
Theorem | cncfi 14468* |
Defining property of a continuous function. (Contributed by Mario
Carneiro, 30-Apr-2014.) (Revised by Mario Carneiro, 25-Aug-2014.)
|
β’ ((πΉ β (π΄βcnβπ΅) β§ πΆ β π΄ β§ π
β β+) β
βπ§ β
β+ βπ€ β π΄ ((absβ(π€ β πΆ)) < π§ β (absβ((πΉβπ€) β (πΉβπΆ))) < π
)) |
|
Theorem | elcncf1di 14469* |
Membership in the set of continuous complex functions from π΄ to
π΅. (Contributed by Paul Chapman,
26-Nov-2007.)
|
β’ (π β πΉ:π΄βΆπ΅)
& β’ (π β ((π₯ β π΄ β§ π¦ β β+) β π β
β+))
& β’ (π β (((π₯ β π΄ β§ π€ β π΄) β§ π¦ β β+) β
((absβ(π₯ β
π€)) < π β (absβ((πΉβπ₯) β (πΉβπ€))) < π¦))) β β’ (π β ((π΄ β β β§ π΅ β β) β πΉ β (π΄βcnβπ΅))) |
|
Theorem | elcncf1ii 14470* |
Membership in the set of continuous complex functions from π΄ to
π΅. (Contributed by Paul Chapman,
26-Nov-2007.)
|
β’ πΉ:π΄βΆπ΅
& β’ ((π₯ β π΄ β§ π¦ β β+) β π β
β+)
& β’ (((π₯ β π΄ β§ π€ β π΄) β§ π¦ β β+) β
((absβ(π₯ β
π€)) < π β (absβ((πΉβπ₯) β (πΉβπ€))) < π¦)) β β’ ((π΄ β β β§ π΅ β β) β πΉ β (π΄βcnβπ΅)) |
|
Theorem | rescncf 14471 |
A continuous complex function restricted to a subset is continuous.
(Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro,
25-Aug-2014.)
|
β’ (πΆ β π΄ β (πΉ β (π΄βcnβπ΅) β (πΉ βΎ πΆ) β (πΆβcnβπ΅))) |
|
Theorem | cncfcdm 14472 |
Change the codomain of a continuous complex function. (Contributed by
Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 1-May-2015.)
|
β’ ((πΆ β β β§ πΉ β (π΄βcnβπ΅)) β (πΉ β (π΄βcnβπΆ) β πΉ:π΄βΆπΆ)) |
|
Theorem | cncfss 14473 |
The set of continuous functions is expanded when the codomain is
expanded. (Contributed by Mario Carneiro, 30-Aug-2014.)
|
β’ ((π΅ β πΆ β§ πΆ β β) β (π΄βcnβπ΅) β (π΄βcnβπΆ)) |
|
Theorem | climcncf 14474 |
Image of a limit under a continuous map. (Contributed by Mario
Carneiro, 7-Apr-2015.)
|
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β πΉ β (π΄βcnβπ΅)) & β’ (π β πΊ:πβΆπ΄)
& β’ (π β πΊ β π·)
& β’ (π β π· β π΄) β β’ (π β (πΉ β πΊ) β (πΉβπ·)) |
|
Theorem | abscncf 14475 |
Absolute value is continuous. (Contributed by Paul Chapman,
21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
|
β’ abs β (ββcnββ) |
|
Theorem | recncf 14476 |
Real part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.)
(Revised by Mario Carneiro, 28-Apr-2014.)
|
β’ β β (ββcnββ) |
|
Theorem | imcncf 14477 |
Imaginary part is continuous. (Contributed by Paul Chapman,
21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
|
β’ β β (ββcnββ) |
|
Theorem | cjcncf 14478 |
Complex conjugate is continuous. (Contributed by Paul Chapman,
21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.)
|
β’ β β (ββcnββ) |
|
Theorem | mulc1cncf 14479* |
Multiplication by a constant is continuous. (Contributed by Paul
Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 30-Apr-2014.)
|
β’ πΉ = (π₯ β β β¦ (π΄ Β· π₯)) β β’ (π΄ β β β πΉ β (ββcnββ)) |
|
Theorem | divccncfap 14480* |
Division by a constant is continuous. (Contributed by Paul Chapman,
28-Nov-2007.) (Revised by Jim Kingdon, 9-Jan-2023.)
|
β’ πΉ = (π₯ β β β¦ (π₯ / π΄)) β β’ ((π΄ β β β§ π΄ # 0) β πΉ β (ββcnββ)) |
|
Theorem | cncfco 14481 |
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.)
|
β’ (π β πΉ β (π΄βcnβπ΅)) & β’ (π β πΊ β (π΅βcnβπΆ)) β β’ (π β (πΊ β πΉ) β (π΄βcnβπΆ)) |
|
Theorem | cncfmet 14482 |
Relate complex function continuity to metric space continuity.
(Contributed by Paul Chapman, 26-Nov-2007.) (Revised by Mario Carneiro,
7-Sep-2015.)
|
β’ πΆ = ((abs β β ) βΎ (π΄ Γ π΄)) & β’ π· = ((abs β β )
βΎ (π΅ Γ π΅)) & β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·)
β β’ ((π΄ β β β§ π΅ β β) β (π΄βcnβπ΅) = (π½ Cn πΎ)) |
|
Theorem | cncfcncntop 14483 |
Relate complex function continuity to topological continuity.
(Contributed by Mario Carneiro, 17-Feb-2015.)
|
β’ π½ = (MetOpenβ(abs β β
))
& β’ πΎ = (π½ βΎt π΄)
& β’ πΏ = (π½ βΎt π΅) β β’ ((π΄ β β β§ π΅ β β) β (π΄βcnβπ΅) = (πΎ Cn πΏ)) |
|
Theorem | cncfcn1cntop 14484 |
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.)
|
β’ π½ = (MetOpenβ(abs β β
)) β β’ (ββcnββ) = (π½ Cn π½) |
|
Theorem | cncfmptc 14485* |
A constant function is a continuous function on β. (Contributed
by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro,
7-Sep-2015.)
|
β’ ((π΄ β π β§ π β β β§ π β β) β (π₯ β π β¦ π΄) β (πβcnβπ)) |
|
Theorem | cncfmptid 14486* |
The identity function is a continuous function on β. (Contributed
by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro,
17-May-2016.)
|
β’ ((π β π β§ π β β) β (π₯ β π β¦ π₯) β (πβcnβπ)) |
|
Theorem | cncfmpt1f 14487* |
Composition of continuous functions. βcnβ analogue of cnmpt11f 14187.
(Contributed by Mario Carneiro, 3-Sep-2014.)
|
β’ (π β πΉ β (ββcnββ)) & β’ (π β (π₯ β π β¦ π΄) β (πβcnββ)) β β’ (π β (π₯ β π β¦ (πΉβπ΄)) β (πβcnββ)) |
|
Theorem | cncfmpt2fcntop 14488* |
Composition of continuous functions. βcnβ analogue of cnmpt12f 14189.
(Contributed by Mario Carneiro, 3-Sep-2014.)
|
β’ π½ = (MetOpenβ(abs β β
))
& β’ (π β πΉ β ((π½ Γt π½) Cn π½)) & β’ (π β (π₯ β π β¦ π΄) β (πβcnββ)) & β’ (π β (π₯ β π β¦ π΅) β (πβcnββ)) β β’ (π β (π₯ β π β¦ (π΄πΉπ΅)) β (πβcnββ)) |
|
Theorem | addccncf 14489* |
Adding a constant is a continuous function. (Contributed by Jeff
Madsen, 2-Sep-2009.)
|
β’ πΉ = (π₯ β β β¦ (π₯ + π΄)) β β’ (π΄ β β β πΉ β (ββcnββ)) |
|
Theorem | cdivcncfap 14490* |
Division with a constant numerator is continuous. (Contributed by Mario
Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 26-May-2023.)
|
β’ πΉ = (π₯ β {π¦ β β β£ π¦ # 0} β¦ (π΄ / π₯)) β β’ (π΄ β β β πΉ β ({π¦ β β β£ π¦ # 0}βcnββ)) |
|
Theorem | negcncf 14491* |
The negative function is continuous. (Contributed by Mario Carneiro,
30-Dec-2016.)
|
β’ πΉ = (π₯ β π΄ β¦ -π₯) β β’ (π΄ β β β πΉ β (π΄βcnββ)) |
|
Theorem | negfcncf 14492* |
The negative of a continuous complex function is continuous.
(Contributed by Paul Chapman, 21-Jan-2008.) (Revised by Mario Carneiro,
25-Aug-2014.)
|
β’ πΊ = (π₯ β π΄ β¦ -(πΉβπ₯)) β β’ (πΉ β (π΄βcnββ) β πΊ β (π΄βcnββ)) |
|
Theorem | mulcncflem 14493* |
Lemma for mulcncf 14494. (Contributed by Jim Kingdon, 29-May-2023.)
|
β’ (π β (π₯ β π β¦ π΄) β (πβcnββ)) & β’ (π β (π₯ β π β¦ π΅) β (πβcnββ)) & β’ (π β π β π)
& β’ (π β πΈ β β+) & β’ (π β πΉ β β+) & β’ (π β πΊ β β+) & β’ (π β π β β+) & β’ (π β π β β+) & β’ (π β βπ’ β π ((absβ(π’ β π)) < π β (absβ(((π₯ β π β¦ π΄)βπ’) β ((π₯ β π β¦ π΄)βπ))) < πΉ)) & β’ (π β βπ’ β π ((absβ(π’ β π)) < π β (absβ(((π₯ β π β¦ π΅)βπ’) β ((π₯ β π β¦ π΅)βπ))) < πΊ)) & β’ (π β βπ’ β π (((absβ(β¦π’ / π₯β¦π΄ β β¦π / π₯β¦π΄)) < πΉ β§ (absβ(β¦π’ / π₯β¦π΅ β β¦π / π₯β¦π΅)) < πΊ) β (absβ((β¦π’ / π₯β¦π΄ Β· β¦π’ / π₯β¦π΅) β (β¦π / π₯β¦π΄ Β· β¦π / π₯β¦π΅))) < πΈ)) β β’ (π β βπ β β+ βπ’ β π ((absβ(π’ β π)) < π β (absβ(((π₯ β π β¦ (π΄ Β· π΅))βπ’) β ((π₯ β π β¦ (π΄ Β· π΅))βπ))) < πΈ)) |
|
Theorem | mulcncf 14494* |
The multiplication of two continuous complex functions is continuous.
(Contributed by Glauco Siliprandi, 29-Jun-2017.)
|
β’ (π β (π₯ β π β¦ π΄) β (πβcnββ)) & β’ (π β (π₯ β π β¦ π΅) β (πβcnββ)) β β’ (π β (π₯ β π β¦ (π΄ Β· π΅)) β (πβcnββ)) |
|
Theorem | expcncf 14495* |
The power function on complex numbers, for fixed exponent N, is
continuous. (Contributed by Glauco Siliprandi, 29-Jun-2017.)
|
β’ (π β β0 β (π₯ β β β¦ (π₯βπ)) β (ββcnββ)) |
|
Theorem | cnrehmeocntop 14496* |
The canonical bijection from (β Γ β)
to β described in
cnref1o 9669 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.)
|
β’ πΉ = (π₯ β β, π¦ β β β¦ (π₯ + (i Β· π¦))) & β’ π½ = (topGenβran
(,))
& β’ πΎ = (MetOpenβ(abs β β
)) β β’ πΉ β ((π½ Γt π½)HomeoπΎ) |
|
Theorem | cnopnap 14497* |
The complex numbers apart from a given complex number form an open set.
(Contributed by Jim Kingdon, 14-Dec-2023.)
|
β’ (π΄ β β β {π€ β β β£ π€ # π΄} β (MetOpenβ(abs β
β ))) |
|
PART 9 BASIC REAL AND COMPLEX
ANALYSIS
|
|
9.0.1 Dedekind cuts
|
|
Theorem | dedekindeulemuub 14498* |
Lemma for dedekindeu 14504. Any element of the upper cut is an upper
bound for the lower cut. (Contributed by Jim Kingdon, 2-Feb-2024.)
|
β’ (π β πΏ β β) & β’ (π β π β β) & β’ (π β βπ β β π β πΏ)
& β’ (π β βπ β β π β π)
& β’ (π β βπ β β (π β πΏ β βπ β πΏ π < π))
& β’ (π β βπ β β (π β π β βπ β π π < π))
& β’ (π β (πΏ β© π) = β
) & β’ (π β βπ β β βπ β β (π < π β (π β πΏ β¨ π β π))) & β’ (π β π΄ β π) β β’ (π β βπ§ β πΏ π§ < π΄) |
|
Theorem | dedekindeulemub 14499* |
Lemma for dedekindeu 14504. The lower cut has an upper bound.
(Contributed by Jim Kingdon, 31-Jan-2024.)
|
β’ (π β πΏ β β) & β’ (π β π β β) & β’ (π β βπ β β π β πΏ)
& β’ (π β βπ β β π β π)
& β’ (π β βπ β β (π β πΏ β βπ β πΏ π < π))
& β’ (π β βπ β β (π β π β βπ β π π < π))
& β’ (π β (πΏ β© π) = β
) & β’ (π β βπ β β βπ β β (π < π β (π β πΏ β¨ π β π))) β β’ (π β βπ₯ β β βπ¦ β πΏ π¦ < π₯) |
|
Theorem | dedekindeulemloc 14500* |
Lemma for dedekindeu 14504. The set L is located. (Contributed by Jim
Kingdon, 31-Jan-2024.)
|
β’ (π β πΏ β β) & β’ (π β π β β) & β’ (π β βπ β β π β πΏ)
& β’ (π β βπ β β π β π)
& β’ (π β βπ β β (π β πΏ β βπ β πΏ π < π))
& β’ (π β βπ β β (π β π β βπ β π π < π))
& β’ (π β (πΏ β© π) = β
) & β’ (π β βπ β β βπ β β (π < π β (π β πΏ β¨ π β π))) β β’ (π β βπ₯ β β βπ¦ β β (π₯ < π¦ β (βπ§ β πΏ π₯ < π§ β¨ βπ§ β πΏ π§ < π¦))) |