ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-limced Unicode version

Definition df-limced 13121
Description: Define the set of limits of a complex function at a point. Under normal circumstances, this will be a singleton or empty, depending on whether the limit exists. (Contributed by Mario Carneiro, 24-Dec-2016.) (Revised by Jim Kingdon, 3-Jun-2023.)
Assertion
Ref Expression
df-limced  |- lim CC  =  ( f  e.  ( CC  ^pm  CC ) ,  x  e.  CC  |->  { y  e.  CC  |  ( ( f : dom  f --> CC 
/\  dom  f  C_  CC )  /\  (
x  e.  CC  /\  A. e  e.  RR+  E. d  e.  RR+  A. z  e. 
dom  f ( ( z #  x  /\  ( abs `  ( z  -  x ) )  < 
d )  ->  ( abs `  ( ( f `
 z )  -  y ) )  < 
e ) ) ) } )
Distinct variable group:    e, d, f, x, y, z

Detailed syntax breakdown of Definition df-limced
StepHypRef Expression
1 climc 13119 . 2  class lim CC
2 vf . . 3  setvar  f
3 vx . . 3  setvar  x
4 cc 7733 . . . 4  class  CC
5 cpm 6597 . . . 4  class  ^pm
64, 4, 5co 5827 . . 3  class  ( CC 
^pm  CC )
72cv 1334 . . . . . . . 8  class  f
87cdm 4589 . . . . . . 7  class  dom  f
98, 4, 7wf 5169 . . . . . 6  wff  f : dom  f --> CC
108, 4wss 3102 . . . . . 6  wff  dom  f  C_  CC
119, 10wa 103 . . . . 5  wff  ( f : dom  f --> CC 
/\  dom  f  C_  CC )
123cv 1334 . . . . . . 7  class  x
1312, 4wcel 2128 . . . . . 6  wff  x  e.  CC
14 vz . . . . . . . . . . . . 13  setvar  z
1514cv 1334 . . . . . . . . . . . 12  class  z
16 cap 8461 . . . . . . . . . . . 12  class #
1715, 12, 16wbr 3967 . . . . . . . . . . 11  wff  z #  x
18 cmin 8051 . . . . . . . . . . . . . 14  class  -
1915, 12, 18co 5827 . . . . . . . . . . . . 13  class  ( z  -  x )
20 cabs 10909 . . . . . . . . . . . . 13  class  abs
2119, 20cfv 5173 . . . . . . . . . . . 12  class  ( abs `  ( z  -  x
) )
22 vd . . . . . . . . . . . . 13  setvar  d
2322cv 1334 . . . . . . . . . . . 12  class  d
24 clt 7915 . . . . . . . . . . . 12  class  <
2521, 23, 24wbr 3967 . . . . . . . . . . 11  wff  ( abs `  ( z  -  x
) )  <  d
2617, 25wa 103 . . . . . . . . . 10  wff  ( z #  x  /\  ( abs `  ( z  -  x
) )  <  d
)
2715, 7cfv 5173 . . . . . . . . . . . . 13  class  ( f `
 z )
28 vy . . . . . . . . . . . . . 14  setvar  y
2928cv 1334 . . . . . . . . . . . . 13  class  y
3027, 29, 18co 5827 . . . . . . . . . . . 12  class  ( ( f `  z )  -  y )
3130, 20cfv 5173 . . . . . . . . . . 11  class  ( abs `  ( ( f `  z )  -  y
) )
32 ve . . . . . . . . . . . 12  setvar  e
3332cv 1334 . . . . . . . . . . 11  class  e
3431, 33, 24wbr 3967 . . . . . . . . . 10  wff  ( abs `  ( ( f `  z )  -  y
) )  <  e
3526, 34wi 4 . . . . . . . . 9  wff  ( ( z #  x  /\  ( abs `  ( z  -  x ) )  < 
d )  ->  ( abs `  ( ( f `
 z )  -  y ) )  < 
e )
3635, 14, 8wral 2435 . . . . . . . 8  wff  A. z  e.  dom  f ( ( z #  x  /\  ( abs `  ( z  -  x ) )  < 
d )  ->  ( abs `  ( ( f `
 z )  -  y ) )  < 
e )
37 crp 9567 . . . . . . . 8  class  RR+
3836, 22, 37wrex 2436 . . . . . . 7  wff  E. d  e.  RR+  A. z  e. 
dom  f ( ( z #  x  /\  ( abs `  ( z  -  x ) )  < 
d )  ->  ( abs `  ( ( f `
 z )  -  y ) )  < 
e )
3938, 32, 37wral 2435 . . . . . 6  wff  A. e  e.  RR+  E. d  e.  RR+  A. z  e.  dom  f ( ( z #  x  /\  ( abs `  ( z  -  x
) )  <  d
)  ->  ( abs `  ( ( f `  z )  -  y
) )  <  e
)
4013, 39wa 103 . . . . 5  wff  ( x  e.  CC  /\  A. e  e.  RR+  E. d  e.  RR+  A. z  e. 
dom  f ( ( z #  x  /\  ( abs `  ( z  -  x ) )  < 
d )  ->  ( abs `  ( ( f `
 z )  -  y ) )  < 
e ) )
4111, 40wa 103 . . . 4  wff  ( ( f : dom  f --> CC  /\  dom  f  C_  CC )  /\  (
x  e.  CC  /\  A. e  e.  RR+  E. d  e.  RR+  A. z  e. 
dom  f ( ( z #  x  /\  ( abs `  ( z  -  x ) )  < 
d )  ->  ( abs `  ( ( f `
 z )  -  y ) )  < 
e ) ) )
4241, 28, 4crab 2439 . . 3  class  { y  e.  CC  |  ( ( f : dom  f
--> CC  /\  dom  f  C_  CC )  /\  (
x  e.  CC  /\  A. e  e.  RR+  E. d  e.  RR+  A. z  e. 
dom  f ( ( z #  x  /\  ( abs `  ( z  -  x ) )  < 
d )  ->  ( abs `  ( ( f `
 z )  -  y ) )  < 
e ) ) ) }
432, 3, 6, 4, 42cmpo 5829 . 2  class  ( f  e.  ( CC  ^pm  CC ) ,  x  e.  CC  |->  { y  e.  CC  |  ( ( f : dom  f --> CC  /\  dom  f  C_  CC )  /\  (
x  e.  CC  /\  A. e  e.  RR+  E. d  e.  RR+  A. z  e. 
dom  f ( ( z #  x  /\  ( abs `  ( z  -  x ) )  < 
d )  ->  ( abs `  ( ( f `
 z )  -  y ) )  < 
e ) ) ) } )
441, 43wceq 1335 1  wff lim CC  =  ( f  e.  ( CC  ^pm  CC ) ,  x  e.  CC  |->  { y  e.  CC  |  ( ( f : dom  f --> CC 
/\  dom  f  C_  CC )  /\  (
x  e.  CC  /\  A. e  e.  RR+  E. d  e.  RR+  A. z  e. 
dom  f ( ( z #  x  /\  ( abs `  ( z  -  x ) )  < 
d )  ->  ( abs `  ( ( f `
 z )  -  y ) )  < 
e ) ) ) } )
Colors of variables: wff set class
This definition is referenced by:  limcrcl  13123  limccl  13124  ellimc3apf  13125
  Copyright terms: Public domain W3C validator