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

Definition df-limc 19211
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 19207 . 2  class lim CC
2 vf . . 3  set  f
3 vx . . 3  set  x
4 cc 8731 . . . 4  class  CC
5 cpm 6769 . . . 4  class  ^pm
64, 4, 5co 5820 . . 3  class  ( CC 
^pm  CC )
7 vz . . . . . . 7  set  z
82cv 1623 . . . . . . . . 9  class  f
98cdm 4689 . . . . . . . 8  class  dom  f
103cv 1623 . . . . . . . . 9  class  x
1110csn 3642 . . . . . . . 8  class  { x }
129, 11cun 3152 . . . . . . 7  class  ( dom  f  u.  { x } )
137, 3weq 1625 . . . . . . . 8  wff  z  =  x
14 vy . . . . . . . . 9  set  y
1514cv 1623 . . . . . . . 8  class  y
167cv 1623 . . . . . . . . 9  class  z
1716, 8cfv 5222 . . . . . . . 8  class  ( f `
 z )
1813, 15, 17cif 3567 . . . . . . 7  class  if ( z  =  x ,  y ,  ( f `
 z ) )
197, 12, 18cmpt 4079 . . . . . 6  class  ( z  e.  ( dom  f  u.  { x } ) 
|->  if ( z  =  x ,  y ,  ( f `  z
) ) )
20 vj . . . . . . . . . 10  set  j
2120cv 1623 . . . . . . . . 9  class  j
22 crest 13320 . . . . . . . . 9  classt
2321, 12, 22co 5820 . . . . . . . 8  class  ( jt  ( dom  f  u.  {
x } ) )
24 ccnp 16950 . . . . . . . 8  class  CnP
2523, 21, 24co 5820 . . . . . . 7  class  ( ( jt  ( dom  f  u. 
{ x } ) )  CnP  j )
2610, 25cfv 5222 . . . . . 6  class  ( ( ( jt  ( dom  f  u.  { x } ) )  CnP  j ) `
 x )
2719, 26wcel 1685 . . . . 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 16372 . . . . . 6  classfld
29 ctopn 13321 . . . . . 6  class  TopOpen
3028, 29cfv 5222 . . . . 5  class  ( TopOpen ` fld )
3127, 20, 30wsbc 2993 . . . 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 2271 . . 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 5822 . 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 1624 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  19217  limcrcl  19219
  Copyright terms: Public domain W3C validator