HomeTheorem List (p. 157 of 172)
Unicode version.
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Intuitionistic Logic Explorer Theorem List (p. 157 of 172) | < Previous Next > |
| Browser slow? Try the
Unicode version. |
||
|
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | metss2 15601* |
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.)
|
           
 ![/\](wedge.gif "/\"){kind=small}
  | ||
| Theorem | comet 15602* | The composition of an extended metric with a monotonic subadditive function is an extended metric. (Contributed by Mario Carneiro, 21-Mar-2015.) |
    ![[,]](_icc.gif "[,]"){kind=small}   
 
 | ||
| Theorem | bdmetval 15603* | Value of the standard bounded metric. (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 9-May-2023.) |
 inf    
inf
| ||
| Theorem | bdxmet 15604* | 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 15605* | 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 15606* |
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 15607* |
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 15608* | 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 15609 | 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 15610* | The maximum metric (Chebyshev distance) on the product of two sets. (Contributed by Jim Kingdon, 11-Oct-2023.) |
      
| ||
| Theorem | xmetxpbl 15611* |
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 15612* | Lemma for xmettx 15613. (Contributed by Jim Kingdon, 15-Oct-2023.) |
  | ||
| Theorem | xmettx 15613* | The maximum metric (Chebyshev distance) on the product of two sets, expressed as a binary topological product. (Contributed by Jim Kingdon, 11-Oct-2023.) |
|
| ||
| Theorem | metcnp3 15614* |
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 15615* |
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 15616* |
Two ways to say a mapping from metric to metric is
continuous at point . The distance arguments are swapped compared
to metcnp 15615 (and Munkres' metcn 15617) for compatibility with df-lm 15293.
Definition 1.3-3 of [Kreyszig] p. 20.
(Contributed by NM, 4-Jun-2007.)
(Revised by Mario Carneiro, 13-Nov-2013.)
|
| | ||
| Theorem | metcn 15617* |
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 15618* | Epsilon-delta property of a continuous metric space function, with function arguments as in metcnp 15615. (Contributed by NM, 17-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
|
| ||
| Theorem | metcnpi2 15619* | Epsilon-delta property of a continuous metric space function, with swapped distance function arguments as in metcnp2 15616. (Contributed by NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
|
| ||
| Theorem | metcnpi3 15620* |
Epsilon-delta property of a metric space function continuous at .
A variation of metcnpi2 15619 with non-strict ordering. (Contributed by
NM,
16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|
|
| ||
| Theorem | txmetcnp 15621* | Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.) (Revised by Jim Kingdon, 22-Oct-2023.) |
 
 
| ||
| Theorem | txmetcn 15622* | Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.) |
|
| ||
| Theorem | metcnpd 15623* |
Two ways to say a mapping from metric to metric is
continuous at point . (Contributed by Jim Kingdon,
14-Jun-2023.)
|
|
| ||
| Theorem | qtopbasss 15624* | 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 15625 | The set of open intervals with rational endpoints forms a basis for a topology. (Contributed by NM, 8-Mar-2007.) |
 | ||
| Theorem | retopbas 15626 | 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 15627 | The standard topology on the reals. (Contributed by FL, 4-Jun-2007.) |
  | ||
| Theorem | uniretop 15628 | The underlying set of the standard topology on the reals is the reals. (Contributed by FL, 4-Jun-2007.) |
 
| ||
| Theorem | retopon 15629 | The standard topology on the reals is a topology on the reals. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| TopOn | ||
| Theorem | retps 15630 | The standard topological space on the reals. (Contributed by NM, 19-Oct-2012.) |
  TopSet
 | ||
| Theorem | iooretopg 15631 | 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 15632 | 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 15633 | 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 15634 | The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.) |
|
| ||
| Theorem | cntoptopon 15635 | The topology of the complex numbers is a topology. (Contributed by Jim Kingdon, 6-Jun-2023.) |
| TopOn | ||
| Theorem | cntoptop 15636 | The topology of the complex numbers is a topology. (Contributed by Jim Kingdon, 6-Jun-2023.) |
| | ||
| Theorem | cnbl0 15637 | Two ways to write the open ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.) |
  | ||
| Theorem | cnblcld 15638* | Two ways to write the closed ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.) |
 | ||
| Theorem | cnfldms 15639 | The complex number field is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
ℂfld  | ||
| Theorem | cnfldxms 15640 | The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| ℂfld | ||
| Theorem | cnfldtps 15641 | The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| ℂfld | ||
| Theorem | cnfldtopn 15642 | The topology of the complex numbers. (Contributed by Mario Carneiro, 28-Aug-2015.) |
 ℂfld | ||
| Theorem | cnfldtopon 15643 | The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| ℂfld TopOn | ||
| Theorem | cnfldtop 15644 | The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| ℂfld | ||
| Theorem | unicntopcntop 15645 | 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 | unicntop 15646 | The underlying set of the standard topology on the complex numbers is the set of complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ℂfld | ||
| Theorem | cnopncntop 15647 | 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 | cnopn 15648 | The set of complex numbers is open with respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
|
ℂfld | ||
| Theorem | reopnap 15649* | The real numbers apart from a given real number form an open set. (Contributed by Jim Kingdon, 13-Dec-2023.) |
| #
| ||
| Theorem | remetdval 15650 | Value of the distance function of the metric space of real numbers. (Contributed by NM, 16-May-2007.) |
|
| ||
| Theorem | remet 15651 | The absolute value metric determines a metric space on the reals. (Contributed by NM, 10-Feb-2007.) |
| | ||
| Theorem | rexmet 15652 | The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| | ||
| Theorem | bl2ioo 15653 | 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 15654 | 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 15655 | An open interval of reals in terms of a ball. (Contributed by Mario Carneiro, 14-Nov-2013.) |
| | ||
| Theorem | blssioo 15656 | 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 15657 | 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 15658 | 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 15659 | 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 15660 | 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 15661 | 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 | tgioo2 15662 | The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Mario Carneiro, 13-Aug-2014.) |
| ℂfld
↾t | ||
| Theorem | rerest 15663 | The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 13-Aug-2014.) |
| ℂfld ↾t
↾t | ||
| Theorem | addcncntoplem 15664* | Lemma for addcncntop 15665, subcncntop 15666, and mulcncntop 15667. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Jim Kingdon, 22-Oct-2023.) |
   
| ||
| Theorem | addcncntop 15665 | 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 15666 | 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 15667 | 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 15668* | 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 | mpomulcn 15669* | Complex number multiplication is a continuous function. (Contributed by GG, 16-Mar-2025.) |
| ℂfld
| ||
| Theorem | fsumcncntop 15670* |
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 
| ||
| Theorem | fsumcn 15671* |
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.)
|
| ℂfld TopOn
| ||
| Theorem | expcn 15672* |
The power function on complex numbers, for fixed exponent , is
continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by
Mario Carneiro, 23-Aug-2014.) Avoid ax-mulf 8302. (Revised by GG,
16-Mar-2025.)
|
ℂfld
 | ||
| Syntax | ccncf 15673 | Extend class notation to include the operation which returns a class of continuous complex functions. |
  | ||
| Definition | df-cncf 15674* | Define the operation whose value is a class of continuous complex functions. (Contributed by Paul Chapman, 11-Oct-2007.) |
  
 | ||
| Theorem | cncfval 15675* |
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 15676* |
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 15677* | Version of elcncf 15676 with arguments commuted. (Contributed by Mario Carneiro, 28-Apr-2014.) |
| | ||
| Theorem | cncfrss 15678 | Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.) |
| | ||
| Theorem | cncfrss2 15679 | Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.) |
| | ||
| Theorem | cncff 15680 | A continuous complex function's domain and codomain. (Contributed by Paul Chapman, 17-Jan-2008.) (Revised by Mario Carneiro, 25-Aug-2014.) |
| | ||
| Theorem | cncfi 15681* | Defining property of a continuous function. (Contributed by Mario Carneiro, 30-Apr-2014.) (Revised by Mario Carneiro, 25-Aug-2014.) |
|
| ||
| Theorem | elcncf1di 15682* |
Membership in the set of continuous complex functions from to
. (Contributed
by Paul Chapman, 26-Nov-2007.)
|
|
| ||
| Theorem | elcncf1ii 15683* |
Membership in the set of continuous complex functions from to
. (Contributed
by Paul Chapman, 26-Nov-2007.)
|
|
| ||
| Theorem | rescncf 15684 | 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 | cncfcdm 15685 | Change the codomain of a continuous complex function. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 1-May-2015.) |
| | ||
| Theorem | cncfss 15686 | The set of continuous functions is expanded when the codomain is expanded. (Contributed by Mario Carneiro, 30-Aug-2014.) |
| | ||
| Theorem | climcncf 15687 | Image of a limit under a continuous map. (Contributed by Mario Carneiro, 7-Apr-2015.) |
 
  | ||
| Theorem | abscncf 15688 | Absolute value is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
|
| ||
| Theorem | recncf 15689 | Real part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
 | ||
| Theorem | imcncf 15690 | Imaginary part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
 | ||
| Theorem | cjcncf 15691 | Complex conjugate is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
 | ||
| Theorem | mulc1cncf 15692* | Multiplication by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
|
| ||
| Theorem | divccncfap 15693* | Division by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Jim Kingdon, 9-Jan-2023.) |
| # | ||
| Theorem | cncfco 15694 | 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 15695 | Relate complex function continuity to metric space continuity. (Contributed by Paul Chapman, 26-Nov-2007.) (Revised by Mario Carneiro, 7-Sep-2015.) |
|
| ||
| Theorem | cncfcncntop 15696 | Relate complex function continuity to topological continuity. (Contributed by Mario Carneiro, 17-Feb-2015.) |
| ↾t ↾t
| ||
| Theorem | cncfcn1cntop 15697 | 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 | cncfcn1 15698 | Relate complex function continuity to topological continuity. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 7-Sep-2015.) |
| ℂfld | ||
| Theorem | cncfmptc 15699* |
A constant function is a continuous function on . (Contributed
by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro,
7-Sep-2015.)
|
| ||
| Theorem | cncfmptid 15700* |
The identity function is a continuous function on . (Contributed
by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro,
17-May-2016.)
|
| | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |