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 24763
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 24759 . 2 class lim
2 vf . . 3 setvar 𝑓
3 vx . . 3 setvar 𝑥
4 cc 10727 . . . 4 class
5 cpm 8509 . . . 4 class pm
64, 4, 5co 7213 . . 3 class (ℂ ↑pm ℂ)
7 vz . . . . . . 7 setvar 𝑧
82cv 1542 . . . . . . . . 9 class 𝑓
98cdm 5551 . . . . . . . 8 class dom 𝑓
103cv 1542 . . . . . . . . 9 class 𝑥
1110csn 4541 . . . . . . . 8 class {𝑥}
129, 11cun 3864 . . . . . . 7 class (dom 𝑓 ∪ {𝑥})
137, 3weq 1971 . . . . . . . 8 wff 𝑧 = 𝑥
14 vy . . . . . . . . 9 setvar 𝑦
1514cv 1542 . . . . . . . 8 class 𝑦
167cv 1542 . . . . . . . . 9 class 𝑧
1716, 8cfv 6380 . . . . . . . 8 class (𝑓𝑧)
1813, 15, 17cif 4439 . . . . . . 7 class if(𝑧 = 𝑥, 𝑦, (𝑓𝑧))
197, 12, 18cmpt 5135 . . . . . 6 class (𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓𝑧)))
20 vj . . . . . . . . . 10 setvar 𝑗
2120cv 1542 . . . . . . . . 9 class 𝑗
22 crest 16925 . . . . . . . . 9 class t
2321, 12, 22co 7213 . . . . . . . 8 class (𝑗t (dom 𝑓 ∪ {𝑥}))
24 ccnp 22122 . . . . . . . 8 class CnP
2523, 21, 24co 7213 . . . . . . 7 class ((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)
2610, 25cfv 6380 . . . . . 6 class (((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)
2719, 26wcel 2110 . . . . 5 wff (𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓𝑧))) ∈ (((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)
28 ccnfld 20363 . . . . . 6 class fld
29 ctopn 16926 . . . . . 6 class TopOpen
3028, 29cfv 6380 . . . . 5 class (TopOpen‘ℂfld)
3127, 20, 30wsbc 3694 . . . 4 wff [(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓𝑧))) ∈ (((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)
3231, 14cab 2714 . . 3 class {𝑦[(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓𝑧))) ∈ (((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)}
332, 3, 6, 4, 32cmpo 7215 . 2 class (𝑓 ∈ (ℂ ↑pm ℂ), 𝑥 ∈ ℂ ↦ {𝑦[(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓𝑧))) ∈ (((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)})
341, 33wceq 1543 1 wff lim = (𝑓 ∈ (ℂ ↑pm ℂ), 𝑥 ∈ ℂ ↦ {𝑦[(TopOpen‘ℂfld) / 𝑗](𝑧 ∈ (dom 𝑓 ∪ {𝑥}) ↦ if(𝑧 = 𝑥, 𝑦, (𝑓𝑧))) ∈ (((𝑗t (dom 𝑓 ∪ {𝑥})) CnP 𝑗)‘𝑥)})
Colors of variables: wff setvar class
This definition is referenced by:  limcfval  24769  limcrcl  24771
  Copyright terms: Public domain W3C validator