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 23842
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 23838 . 2 class lim
2 vf . . 3 setvar 𝑓
3 vx . . 3 setvar 𝑥
4 cc 10217 . . . 4 class
5 cpm 8091 . . . 4 class pm
64, 4, 5co 6872 . . 3 class (ℂ ↑pm ℂ)
7 vz . . . . . . 7 setvar 𝑧
82cv 1636 . . . . . . . . 9 class 𝑓
98cdm 5309 . . . . . . . 8 class dom 𝑓
103cv 1636 . . . . . . . . 9 class 𝑥
1110csn 4368 . . . . . . . 8 class {𝑥}
129, 11cun 3765 . . . . . . 7 class (dom 𝑓 ∪ {𝑥})
137, 3weq 2054 . . . . . . . 8 wff 𝑧 = 𝑥
14 vy . . . . . . . . 9 setvar 𝑦
1514cv 1636 . . . . . . . 8 class 𝑦
167cv 1636 . . . . . . . . 9 class 𝑧
1716, 8cfv 6099 . . . . . . . 8 class (𝑓𝑧)
1813, 15, 17cif 4277 . . . . . . 7 class if(𝑧 = 𝑥, 𝑦, (𝑓𝑧))
197, 12, 18cmpt 4921 . . . . . 6 class (𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓𝑧)))
20 vj . . . . . . . . . 10 setvar 𝑗
2120cv 1636 . . . . . . . . 9 class 𝑗
22 crest 16284 . . . . . . . . 9 class t
2321, 12, 22co 6872 . . . . . . . 8 class (𝑗t (dom 𝑓 ∪ {𝑥}))
24 ccnp 21241 . . . . . . . 8 class CnP
2523, 21, 24co 6872 . . . . . . 7 class ((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)
2610, 25cfv 6099 . . . . . 6 class (((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)
2719, 26wcel 2156 . . . . 5 wff (𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓𝑧))) ∈ (((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)
28 ccnfld 19952 . . . . . 6 class fld
29 ctopn 16285 . . . . . 6 class TopOpen
3028, 29cfv 6099 . . . . 5 class (TopOpen‘ℂfld)
3127, 20, 30wsbc 3631 . . . 4 wff [(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓𝑧))) ∈ (((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)
3231, 14cab 2790 . . 3 class {𝑦[(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓𝑧))) ∈ (((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)}
332, 3, 6, 4, 32cmpt2 6874 . 2 class (𝑓 ∈ (ℂ ↑pm ℂ), 𝑥 ∈ ℂ ↦ {𝑦[(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓𝑧))) ∈ (((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)})
341, 33wceq 1637 1 wff lim = (𝑓 ∈ (ℂ ↑pm ℂ), 𝑥 ∈ ℂ ↦ {𝑦[(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓𝑧))) ∈ (((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)})
Colors of variables: wff setvar class
This definition is referenced by:  limcfval  23848  limcrcl  23850
  Copyright terms: Public domain W3C validator