HomeTheorem List (p. 158 of 174)
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. 158 of 174) | < 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 | xmettxlem 15701* | Lemma for xmettx 15702. (Contributed by Jim Kingdon, 15-Oct-2023.) |
                      
            | ||
| Theorem | xmettx 15702* | 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 15703* |
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.)
|
  ![/\](wedge.gif "/\"){kind=small}            | ||
| Theorem | metcnp 15704* |
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 15705* |
Two ways to say a mapping from metric to metric is
continuous at point . The distance arguments are swapped compared
to metcnp 15704 (and Munkres' metcn 15706) for compatibility with df-lm 15382.
Definition 1.3-3 of [Kreyszig] p. 20.
(Contributed by NM, 4-Jun-2007.)
(Revised by Mario Carneiro, 13-Nov-2013.)
|
| | ||
| Theorem | metcn 15706* |
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 15707* | Epsilon-delta property of a continuous metric space function, with function arguments as in metcnp 15704. (Contributed by NM, 17-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
| ||
| Theorem | metcnpi2 15708* | Epsilon-delta property of a continuous metric space function, with swapped distance function arguments as in metcnp2 15705. (Contributed by NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
|
| ||
| Theorem | metcnpi3 15709* |
Epsilon-delta property of a metric space function continuous at .
A variation of metcnpi2 15708 with non-strict ordering. (Contributed by
NM,
16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|
| ||
| Theorem | txmetcnp 15710* | Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.) (Revised by Jim Kingdon, 22-Oct-2023.) |
  
 
| ||
| Theorem | txmetcn 15711* | Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.) |
|
| ||
| Theorem | metcnpd 15712* |
Two ways to say a mapping from metric to metric is
continuous at point . (Contributed by Jim Kingdon,
14-Jun-2023.)
|
|
| ||
| Theorem | qtopbasss 15713* | 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 15714 | The set of open intervals with rational endpoints forms a basis for a topology. (Contributed by NM, 8-Mar-2007.) |
 | ||
| Theorem | retopbas 15715 | 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 15716 | The standard topology on the reals. (Contributed by FL, 4-Jun-2007.) |
  | ||
| Theorem | uniretop 15717 | The underlying set of the standard topology on the reals is the reals. (Contributed by FL, 4-Jun-2007.) |
 
| ||
| Theorem | retopon 15718 | The standard topology on the reals is a topology on the reals. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| TopOn | ||
| Theorem | retps 15719 | The standard topological space on the reals. (Contributed by NM, 19-Oct-2012.) |
  TopSet
 | ||
| Theorem | iooretopg 15720 | 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 15721 | 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 15722 | 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 15723 | The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.) |
|
| ||
| Theorem | cntoptopon 15724 | The topology of the complex numbers is a topology. (Contributed by Jim Kingdon, 6-Jun-2023.) |
| TopOn | ||
| Theorem | cntoptop 15725 | The topology of the complex numbers is a topology. (Contributed by Jim Kingdon, 6-Jun-2023.) |
| | ||
| Theorem | cnbl0 15726 | Two ways to write the open ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.) |
    | ||
| Theorem | cnblcld 15727* | Two ways to write the closed ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.) |
![[,]](_icc.gif "[,]"){kind=small}  | ||
| Theorem | cnfldms 15728 | The complex number field is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
ℂfld  | ||
| Theorem | cnfldxms 15729 | The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| ℂfld | ||
| Theorem | cnfldtps 15730 | The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| ℂfld | ||
| Theorem | cnfldtopn 15731 | The topology of the complex numbers. (Contributed by Mario Carneiro, 28-Aug-2015.) |
 ℂfld | ||
| Theorem | cnfldtopon 15732 | The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| ℂfld TopOn | ||
| Theorem | cnfldtop 15733 | The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| ℂfld | ||
| Theorem | unicntopcntop 15734 | 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 15735 | 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 15736 | 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 15737 | 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 15738* | The real numbers apart from a given real number form an open set. (Contributed by Jim Kingdon, 13-Dec-2023.) |
| #
| ||
| Theorem | remetdval 15739 | Value of the distance function of the metric space of real numbers. (Contributed by NM, 16-May-2007.) |
| ||
| Theorem | remet 15740 | The absolute value metric determines a metric space on the reals. (Contributed by NM, 10-Feb-2007.) |
| | ||
| Theorem | rexmet 15741 | The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| | ||
| Theorem | bl2ioo 15742 | 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 15743 | 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 15744 | An open interval of reals in terms of a ball. (Contributed by Mario Carneiro, 14-Nov-2013.) |
| | ||
| Theorem | blssioo 15745 | 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 15746 | 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 15747 | 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 15748 | 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 15749 | 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 15750 | 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 15751 | 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 15752 | The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 13-Aug-2014.) |
| ℂfld ↾t
↾t | ||
| Theorem | addcncntoplem 15753* | Lemma for addcncntop 15754, subcncntop 15755, and mulcncntop 15756. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Jim Kingdon, 22-Oct-2023.) |
   
| ||
| Theorem | addcncntop 15754 | 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 15755 | 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 15756 | 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 15757* | 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 15758* | Complex number multiplication is a continuous function. (Contributed by GG, 16-Mar-2025.) |
| ℂfld
| ||
| Theorem | fsumcncntop 15759* |
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 15760* |
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 15761* |
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 8303. (Revised by GG,
16-Mar-2025.)
|
ℂfld
 | ||
| Syntax | ccncf 15762 | Extend class notation to include the operation which returns a class of continuous complex functions. |
  | ||
| Definition | df-cncf 15763* | Define the operation whose value is a class of continuous complex functions. (Contributed by Paul Chapman, 11-Oct-2007.) |
  
  | ||
| Theorem | cncfval 15764* |
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 15765* |
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 15766* | Version of elcncf 15765 with arguments commuted. (Contributed by Mario Carneiro, 28-Apr-2014.) |
| | ||
| Theorem | cncfrss 15767 | Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.) |
| | ||
| Theorem | cncfrss2 15768 | Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.) |
| | ||
| Theorem | cncff 15769 | A continuous complex function's domain and codomain. (Contributed by Paul Chapman, 17-Jan-2008.) (Revised by Mario Carneiro, 25-Aug-2014.) |
| | ||
| Theorem | cncfi 15770* | Defining property of a continuous function. (Contributed by Mario Carneiro, 30-Apr-2014.) (Revised by Mario Carneiro, 25-Aug-2014.) |
|
| ||
| Theorem | elcncf1di 15771* |
Membership in the set of continuous complex functions from to
. (Contributed
by Paul Chapman, 26-Nov-2007.)
|
|
| ||
| Theorem | elcncf1ii 15772* |
Membership in the set of continuous complex functions from to
. (Contributed
by Paul Chapman, 26-Nov-2007.)
|
|
| ||
| Theorem | rescncf 15773 | 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 15774 | Change the codomain of a continuous complex function. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 1-May-2015.) |
| | ||
| Theorem | cncfss 15775 | The set of continuous functions is expanded when the codomain is expanded. (Contributed by Mario Carneiro, 30-Aug-2014.) |
| | ||
| Theorem | climcncf 15776 | Image of a limit under a continuous map. (Contributed by Mario Carneiro, 7-Apr-2015.) |
 
  | ||
| Theorem | abscncf 15777 | Absolute value is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
|
| ||
| Theorem | recncf 15778 | Real part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
 | ||
| Theorem | imcncf 15779 | Imaginary part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
 | ||
| Theorem | cjcncf 15780 | Complex conjugate is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
 | ||
| Theorem | mulc1cncf 15781* | Multiplication by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
|
| ||
| Theorem | divccncfap 15782* | Division by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Jim Kingdon, 9-Jan-2023.) |
| # | ||
| Theorem | cncfco 15783 | 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 15784 | Relate complex function continuity to metric space continuity. (Contributed by Paul Chapman, 26-Nov-2007.) (Revised by Mario Carneiro, 7-Sep-2015.) |
|
| ||
| Theorem | cncfcncntop 15785 | Relate complex function continuity to topological continuity. (Contributed by Mario Carneiro, 17-Feb-2015.) |
| ↾t ↾t
| ||
| Theorem | cncfcn1cntop 15786 | 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 15787 | Relate complex function continuity to topological continuity. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 7-Sep-2015.) |
| ℂfld | ||
| Theorem | cncfmptc 15788* |
A constant function is a continuous function on . (Contributed
by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro,
7-Sep-2015.)
|
| ||
| Theorem | cncfmptid 15789* |
The identity function is a continuous function on . (Contributed
by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro,
17-May-2016.)
|
| | ||
| Theorem | cncfmpt1f 15790* |
Composition of continuous functions. analogue of cnmpt11f 15476.
(Contributed by Mario Carneiro, 3-Sep-2014.)
|
|
| ||
| Theorem | cncfmpt2fcntop 15791* |
Composition of continuous functions. analogue of cnmpt12f 15478.
(Contributed by Mario Carneiro, 3-Sep-2014.)
|
|
| ||
| Theorem | addccncf 15792* | Adding a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009.) |
|
| ||
| Theorem | idcncf 15793 |
The identity function is a continuous function on . (Contributed
by Jeff Madsen, 11-Jun-2010.) (Moved into main set.mm as cncfmptid 15789
and may be deleted by mathbox owner, JM. --MC 12-Sep-2015.) (Revised by
Mario Carneiro, 12-Sep-2015.)
|
|
| ||
| Theorem | sub1cncf 15794* | Subtracting a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
|
| ||
| Theorem | sub2cncf 15795* | Subtraction from a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
|
| ||
| Theorem | cdivcncfap 15796* | Division with a constant numerator is continuous. (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 26-May-2023.) |
| #
#
| ||
| Theorem | negcncf 15797* | The negative function is continuous. (Contributed by Mario Carneiro, 30-Dec-2016.) |
 | ||
| Theorem | negfcncf 15798* | 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 15799* | Lemma for mulcncf 15800. (Contributed by Jim Kingdon, 29-May-2023.) |
 
![]_](_urbrack.gif "]_"){kind=small}
| ||
| Theorem | mulcncf 15800* | The multiplication of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
|
| ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |