MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-limc Unicode version

Definition df-limc 19232
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.)
Assertion
Ref Expression
df-limc  |- lim CC  =  ( f  e.  ( CC  ^pm  CC ) ,  x  e.  CC  |->  { y  |  [. ( TopOpen ` fld )  /  j ]. ( z  e.  ( dom  f  u.  {
x } )  |->  if ( z  =  x ,  y ,  ( f `  z ) ) )  e.  ( ( ( jt  ( dom  f  u.  { x } ) )  CnP  j ) `  x
) } )
Distinct variable group:    f, j, x, y, z

Detailed syntax breakdown of Definition df-limc
StepHypRef Expression
1 climc 19228 . 2  class lim CC
2 vf . . 3  set  f
3 vx . . 3  set  x
4 cc 8751 . . . 4  class  CC
5 cpm 6789 . . . 4  class  ^pm
64, 4, 5co 5874 . . 3  class  ( CC 
^pm  CC )
7 vz . . . . . . 7  set  z
82cv 1631 . . . . . . . . 9  class  f
98cdm 4705 . . . . . . . 8  class  dom  f
103cv 1631 . . . . . . . . 9  class  x
1110csn 3653 . . . . . . . 8  class  { x }
129, 11cun 3163 . . . . . . 7  class  ( dom  f  u.  { x } )
137, 3weq 1633 . . . . . . . 8  wff  z  =  x
14 vy . . . . . . . . 9  set  y
1514cv 1631 . . . . . . . 8  class  y
167cv 1631 . . . . . . . . 9  class  z
1716, 8cfv 5271 . . . . . . . 8  class  ( f `
 z )
1813, 15, 17cif 3578 . . . . . . 7  class  if ( z  =  x ,  y ,  ( f `
 z ) )
197, 12, 18cmpt 4093 . . . . . 6  class  ( z  e.  ( dom  f  u.  { x } ) 
|->  if ( z  =  x ,  y ,  ( f `  z
) ) )
20 vj . . . . . . . . . 10  set  j
2120cv 1631 . . . . . . . . 9  class  j
22 crest 13341 . . . . . . . . 9  classt
2321, 12, 22co 5874 . . . . . . . 8  class  ( jt  ( dom  f  u.  {
x } ) )
24 ccnp 16971 . . . . . . . 8  class  CnP
2523, 21, 24co 5874 . . . . . . 7  class  ( ( jt  ( dom  f  u. 
{ x } ) )  CnP  j )
2610, 25cfv 5271 . . . . . 6  class  ( ( ( jt  ( dom  f  u.  { x } ) )  CnP  j ) `
 x )
2719, 26wcel 1696 . . . . 5  wff  ( z  e.  ( dom  f  u.  { x } ) 
|->  if ( z  =  x ,  y ,  ( f `  z
) ) )  e.  ( ( ( jt  ( dom  f  u.  {
x } ) )  CnP  j ) `  x )
28 ccnfld 16393 . . . . . 6  classfld
29 ctopn 13342 . . . . . 6  class  TopOpen
3028, 29cfv 5271 . . . . 5  class  ( TopOpen ` fld )
3127, 20, 30wsbc 3004 . . . 4  wff  [. ( TopOpen
` fld
)  /  j ]. ( z  e.  ( dom  f  u.  {
x } )  |->  if ( z  =  x ,  y ,  ( f `  z ) ) )  e.  ( ( ( jt  ( dom  f  u.  { x } ) )  CnP  j ) `  x
)
3231, 14cab 2282 . . 3  class  { y  |  [. ( TopOpen ` fld )  /  j ]. (
z  e.  ( dom  f  u.  { x } )  |->  if ( z  =  x ,  y ,  ( f `
 z ) ) )  e.  ( ( ( jt  ( dom  f  u.  { x } ) )  CnP  j ) `
 x ) }
332, 3, 6, 4, 32cmpt2 5876 . 2  class  ( f  e.  ( CC  ^pm  CC ) ,  x  e.  CC  |->  { y  | 
[. ( TopOpen ` fld )  /  j ]. ( z  e.  ( dom  f  u.  {
x } )  |->  if ( z  =  x ,  y ,  ( f `  z ) ) )  e.  ( ( ( jt  ( dom  f  u.  { x } ) )  CnP  j ) `  x
) } )
341, 33wceq 1632 1  wff lim CC  =  ( f  e.  ( CC  ^pm  CC ) ,  x  e.  CC  |->  { y  |  [. ( TopOpen ` fld )  /  j ]. ( z  e.  ( dom  f  u.  {
x } )  |->  if ( z  =  x ,  y ,  ( f `  z ) ) )  e.  ( ( ( jt  ( dom  f  u.  { x } ) )  CnP  j ) `  x
) } )
Colors of variables: wff set class
This definition is referenced by:  limcfval  19238  limcrcl  19240
  Copyright terms: Public domain W3C validator