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

Definition df-limc 22900
 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 fld t
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-limc
StepHypRef Expression
1 climc 22896 . 2 lim
2 vf . . 3
3 vx . . 3
4 cc 9555 . . . 4
5 cpm 7491 . . . 4
64, 4, 5co 6308 . . 3
7 vz . . . . . . 7
82cv 1451 . . . . . . . . 9
98cdm 4839 . . . . . . . 8
103cv 1451 . . . . . . . . 9
1110csn 3959 . . . . . . . 8
129, 11cun 3388 . . . . . . 7
137, 3weq 1799 . . . . . . . 8
14 vy . . . . . . . . 9
1514cv 1451 . . . . . . . 8
167cv 1451 . . . . . . . . 9
1716, 8cfv 5589 . . . . . . . 8
1813, 15, 17cif 3872 . . . . . . 7
197, 12, 18cmpt 4454 . . . . . 6
20 vj . . . . . . . . . 10
2120cv 1451 . . . . . . . . 9
22 crest 15397 . . . . . . . . 9 t
2321, 12, 22co 6308 . . . . . . . 8 t
24 ccnp 20318 . . . . . . . 8
2523, 21, 24co 6308 . . . . . . 7 t
2610, 25cfv 5589 . . . . . 6 t
2719, 26wcel 1904 . . . . 5 t
28 ccnfld 19047 . . . . . 6 fld
29 ctopn 15398 . . . . . 6
3028, 29cfv 5589 . . . . 5 fld
3127, 20, 30wsbc 3255 . . . 4 fld t
3231, 14cab 2457 . . 3 fld t
332, 3, 6, 4, 32cmpt2 6310 . 2 fld t
341, 33wceq 1452 1 lim fld t
 Colors of variables: wff setvar class This definition is referenced by:  limcfval  22906  limcrcl  22908
 Copyright terms: Public domain W3C validator