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

Definition df-limc 23353
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 = (𝑓 ∈ (ℂ ↑pm ℂ), 𝑥 ∈ ℂ ↦ {𝑦[(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓𝑧))) ∈ (((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)})
Distinct variable group:   𝑓,𝑗,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-limc
StepHypRef Expression
1 climc 23349 . 2 class lim
2 vf . . 3 setvar 𝑓
3 vx . . 3 setvar 𝑥
4 cc 9790 . . . 4 class
5 cpm 7722 . . . 4 class pm
64, 4, 5co 6527 . . 3 class (ℂ ↑pm ℂ)
7 vz . . . . . . 7 setvar 𝑧
82cv 1473 . . . . . . . . 9 class 𝑓
98cdm 5028 . . . . . . . 8 class dom 𝑓
103cv 1473 . . . . . . . . 9 class 𝑥
1110csn 4124 . . . . . . . 8 class {𝑥}
129, 11cun 3537 . . . . . . 7 class (dom 𝑓 ∪ {𝑥})
137, 3weq 1860 . . . . . . . 8 wff 𝑧 = 𝑥
14 vy . . . . . . . . 9 setvar 𝑦
1514cv 1473 . . . . . . . 8 class 𝑦
167cv 1473 . . . . . . . . 9 class 𝑧
1716, 8cfv 5790 . . . . . . . 8 class (𝑓𝑧)
1813, 15, 17cif 4035 . . . . . . 7 class if(𝑧 = 𝑥, 𝑦, (𝑓𝑧))
197, 12, 18cmpt 4637 . . . . . 6 class (𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓𝑧)))
20 vj . . . . . . . . . 10 setvar 𝑗
2120cv 1473 . . . . . . . . 9 class 𝑗
22 crest 15850 . . . . . . . . 9 class t
2321, 12, 22co 6527 . . . . . . . 8 class (𝑗t (dom 𝑓 ∪ {𝑥}))
24 ccnp 20781 . . . . . . . 8 class CnP
2523, 21, 24co 6527 . . . . . . 7 class ((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)
2610, 25cfv 5790 . . . . . 6 class (((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)
2719, 26wcel 1976 . . . . 5 wff (𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓𝑧))) ∈ (((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)
28 ccnfld 19513 . . . . . 6 class fld
29 ctopn 15851 . . . . . 6 class TopOpen
3028, 29cfv 5790 . . . . 5 class (TopOpen‘ℂfld)
3127, 20, 30wsbc 3401 . . . 4 wff [(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓𝑧))) ∈ (((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)
3231, 14cab 2595 . . 3 class {𝑦[(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓𝑧))) ∈ (((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)}
332, 3, 6, 4, 32cmpt2 6529 . 2 class (𝑓 ∈ (ℂ ↑pm ℂ), 𝑥 ∈ ℂ ↦ {𝑦[(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓𝑧))) ∈ (((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)})
341, 33wceq 1474 1 wff lim = (𝑓 ∈ (ℂ ↑pm ℂ), 𝑥 ∈ ℂ ↦ {𝑦[(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓𝑧))) ∈ (((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)})
Colors of variables: wff setvar class
This definition is referenced by:  limcfval  23359  limcrcl  23361
  Copyright terms: Public domain W3C validator