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

Definition df-limc 24479
 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 24475 . 2 class lim
2 vf . . 3 setvar 𝑓
3 vx . . 3 setvar 𝑥
4 cc 10527 . . . 4 class
5 cpm 8393 . . . 4 class pm
64, 4, 5co 7136 . . 3 class (ℂ ↑pm ℂ)
7 vz . . . . . . 7 setvar 𝑧
82cv 1537 . . . . . . . . 9 class 𝑓
98cdm 5520 . . . . . . . 8 class dom 𝑓
103cv 1537 . . . . . . . . 9 class 𝑥
1110csn 4525 . . . . . . . 8 class {𝑥}
129, 11cun 3879 . . . . . . 7 class (dom 𝑓 ∪ {𝑥})
137, 3weq 1964 . . . . . . . 8 wff 𝑧 = 𝑥
14 vy . . . . . . . . 9 setvar 𝑦
1514cv 1537 . . . . . . . 8 class 𝑦
167cv 1537 . . . . . . . . 9 class 𝑧
1716, 8cfv 6325 . . . . . . . 8 class (𝑓𝑧)
1813, 15, 17cif 4425 . . . . . . 7 class if(𝑧 = 𝑥, 𝑦, (𝑓𝑧))
197, 12, 18cmpt 5111 . . . . . 6 class (𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓𝑧)))
20 vj . . . . . . . . . 10 setvar 𝑗
2120cv 1537 . . . . . . . . 9 class 𝑗
22 crest 16689 . . . . . . . . 9 class t
2321, 12, 22co 7136 . . . . . . . 8 class (𝑗t (dom 𝑓 ∪ {𝑥}))
24 ccnp 21840 . . . . . . . 8 class CnP
2523, 21, 24co 7136 . . . . . . 7 class ((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)
2610, 25cfv 6325 . . . . . 6 class (((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)
2719, 26wcel 2111 . . . . 5 wff (𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓𝑧))) ∈ (((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)
28 ccnfld 20095 . . . . . 6 class fld
29 ctopn 16690 . . . . . 6 class TopOpen
3028, 29cfv 6325 . . . . 5 class (TopOpen‘ℂfld)
3127, 20, 30wsbc 3720 . . . 4 wff [(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓𝑧))) ∈ (((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)
3231, 14cab 2776 . . 3 class {𝑦[(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓𝑧))) ∈ (((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)}
332, 3, 6, 4, 32cmpo 7138 . 2 class (𝑓 ∈ (ℂ ↑pm ℂ), 𝑥 ∈ ℂ ↦ {𝑦[(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓𝑧))) ∈ (((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)})
341, 33wceq 1538 1 wff lim = (𝑓 ∈ (ℂ ↑pm ℂ), 𝑥 ∈ ℂ ↦ {𝑦[(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓𝑧))) ∈ (((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)})
 Colors of variables: wff setvar class This definition is referenced by:  limcfval  24485  limcrcl  24487
 Copyright terms: Public domain W3C validator