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 24170
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 24166 . 2 class lim
2 vf . . 3 setvar 𝑓
3 vx . . 3 setvar 𝑥
4 cc 10335 . . . 4 class
5 cpm 8209 . . . 4 class pm
64, 4, 5co 6978 . . 3 class (ℂ ↑pm ℂ)
7 vz . . . . . . 7 setvar 𝑧
82cv 1506 . . . . . . . . 9 class 𝑓
98cdm 5408 . . . . . . . 8 class dom 𝑓
103cv 1506 . . . . . . . . 9 class 𝑥
1110csn 4442 . . . . . . . 8 class {𝑥}
129, 11cun 3829 . . . . . . 7 class (dom 𝑓 ∪ {𝑥})
137, 3weq 1922 . . . . . . . 8 wff 𝑧 = 𝑥
14 vy . . . . . . . . 9 setvar 𝑦
1514cv 1506 . . . . . . . 8 class 𝑦
167cv 1506 . . . . . . . . 9 class 𝑧
1716, 8cfv 6190 . . . . . . . 8 class (𝑓𝑧)
1813, 15, 17cif 4351 . . . . . . 7 class if(𝑧 = 𝑥, 𝑦, (𝑓𝑧))
197, 12, 18cmpt 5009 . . . . . 6 class (𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓𝑧)))
20 vj . . . . . . . . . 10 setvar 𝑗
2120cv 1506 . . . . . . . . 9 class 𝑗
22 crest 16553 . . . . . . . . 9 class t
2321, 12, 22co 6978 . . . . . . . 8 class (𝑗t (dom 𝑓 ∪ {𝑥}))
24 ccnp 21540 . . . . . . . 8 class CnP
2523, 21, 24co 6978 . . . . . . 7 class ((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)
2610, 25cfv 6190 . . . . . 6 class (((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)
2719, 26wcel 2050 . . . . 5 wff (𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓𝑧))) ∈ (((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)
28 ccnfld 20250 . . . . . 6 class fld
29 ctopn 16554 . . . . . 6 class TopOpen
3028, 29cfv 6190 . . . . 5 class (TopOpen‘ℂfld)
3127, 20, 30wsbc 3683 . . . 4 wff [(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓𝑧))) ∈ (((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)
3231, 14cab 2758 . . 3 class {𝑦[(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓𝑧))) ∈ (((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)}
332, 3, 6, 4, 32cmpo 6980 . 2 class (𝑓 ∈ (ℂ ↑pm ℂ), 𝑥 ∈ ℂ ↦ {𝑦[(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓𝑧))) ∈ (((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)})
341, 33wceq 1507 1 wff lim = (𝑓 ∈ (ℂ ↑pm ℂ), 𝑥 ∈ ℂ ↦ {𝑦[(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓𝑧))) ∈ (((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)})
Colors of variables: wff setvar class
This definition is referenced by:  limcfval  24176  limcrcl  24178
  Copyright terms: Public domain W3C validator