ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-limced GIF version

Definition df-limced 12721
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.) (Revised by Jim Kingdon, 3-Jun-2023.)
Assertion
Ref Expression
df-limced lim = (𝑓 ∈ (ℂ ↑pm ℂ), 𝑥 ∈ ℂ ↦ {𝑦 ∈ ℂ ∣ ((𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ ℂ) ∧ (𝑥 ∈ ℂ ∧ ∀𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑧 ∈ dom 𝑓((𝑧 # 𝑥 ∧ (abs‘(𝑧𝑥)) < 𝑑) → (abs‘((𝑓𝑧) − 𝑦)) < 𝑒)))})
Distinct variable group:   𝑒,𝑑,𝑓,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-limced
StepHypRef Expression
1 climc 12719 . 2 class lim
2 vf . . 3 setvar 𝑓
3 vx . . 3 setvar 𝑥
4 cc 7586 . . . 4 class
5 cpm 6511 . . . 4 class pm
64, 4, 5co 5742 . . 3 class (ℂ ↑pm ℂ)
72cv 1315 . . . . . . . 8 class 𝑓
87cdm 4509 . . . . . . 7 class dom 𝑓
98, 4, 7wf 5089 . . . . . 6 wff 𝑓:dom 𝑓⟶ℂ
108, 4wss 3041 . . . . . 6 wff dom 𝑓 ⊆ ℂ
119, 10wa 103 . . . . 5 wff (𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ ℂ)
123cv 1315 . . . . . . 7 class 𝑥
1312, 4wcel 1465 . . . . . 6 wff 𝑥 ∈ ℂ
14 vz . . . . . . . . . . . . 13 setvar 𝑧
1514cv 1315 . . . . . . . . . . . 12 class 𝑧
16 cap 8311 . . . . . . . . . . . 12 class #
1715, 12, 16wbr 3899 . . . . . . . . . . 11 wff 𝑧 # 𝑥
18 cmin 7901 . . . . . . . . . . . . . 14 class
1915, 12, 18co 5742 . . . . . . . . . . . . 13 class (𝑧𝑥)
20 cabs 10737 . . . . . . . . . . . . 13 class abs
2119, 20cfv 5093 . . . . . . . . . . . 12 class (abs‘(𝑧𝑥))
22 vd . . . . . . . . . . . . 13 setvar 𝑑
2322cv 1315 . . . . . . . . . . . 12 class 𝑑
24 clt 7768 . . . . . . . . . . . 12 class <
2521, 23, 24wbr 3899 . . . . . . . . . . 11 wff (abs‘(𝑧𝑥)) < 𝑑
2617, 25wa 103 . . . . . . . . . 10 wff (𝑧 # 𝑥 ∧ (abs‘(𝑧𝑥)) < 𝑑)
2715, 7cfv 5093 . . . . . . . . . . . . 13 class (𝑓𝑧)
28 vy . . . . . . . . . . . . . 14 setvar 𝑦
2928cv 1315 . . . . . . . . . . . . 13 class 𝑦
3027, 29, 18co 5742 . . . . . . . . . . . 12 class ((𝑓𝑧) − 𝑦)
3130, 20cfv 5093 . . . . . . . . . . 11 class (abs‘((𝑓𝑧) − 𝑦))
32 ve . . . . . . . . . . . 12 setvar 𝑒
3332cv 1315 . . . . . . . . . . 11 class 𝑒
3431, 33, 24wbr 3899 . . . . . . . . . 10 wff (abs‘((𝑓𝑧) − 𝑦)) < 𝑒
3526, 34wi 4 . . . . . . . . 9 wff ((𝑧 # 𝑥 ∧ (abs‘(𝑧𝑥)) < 𝑑) → (abs‘((𝑓𝑧) − 𝑦)) < 𝑒)
3635, 14, 8wral 2393 . . . . . . . 8 wff 𝑧 ∈ dom 𝑓((𝑧 # 𝑥 ∧ (abs‘(𝑧𝑥)) < 𝑑) → (abs‘((𝑓𝑧) − 𝑦)) < 𝑒)
37 crp 9409 . . . . . . . 8 class +
3836, 22, 37wrex 2394 . . . . . . 7 wff 𝑑 ∈ ℝ+𝑧 ∈ dom 𝑓((𝑧 # 𝑥 ∧ (abs‘(𝑧𝑥)) < 𝑑) → (abs‘((𝑓𝑧) − 𝑦)) < 𝑒)
3938, 32, 37wral 2393 . . . . . 6 wff 𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑧 ∈ dom 𝑓((𝑧 # 𝑥 ∧ (abs‘(𝑧𝑥)) < 𝑑) → (abs‘((𝑓𝑧) − 𝑦)) < 𝑒)
4013, 39wa 103 . . . . 5 wff (𝑥 ∈ ℂ ∧ ∀𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑧 ∈ dom 𝑓((𝑧 # 𝑥 ∧ (abs‘(𝑧𝑥)) < 𝑑) → (abs‘((𝑓𝑧) − 𝑦)) < 𝑒))
4111, 40wa 103 . . . 4 wff ((𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ ℂ) ∧ (𝑥 ∈ ℂ ∧ ∀𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑧 ∈ dom 𝑓((𝑧 # 𝑥 ∧ (abs‘(𝑧𝑥)) < 𝑑) → (abs‘((𝑓𝑧) − 𝑦)) < 𝑒)))
4241, 28, 4crab 2397 . . 3 class {𝑦 ∈ ℂ ∣ ((𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ ℂ) ∧ (𝑥 ∈ ℂ ∧ ∀𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑧 ∈ dom 𝑓((𝑧 # 𝑥 ∧ (abs‘(𝑧𝑥)) < 𝑑) → (abs‘((𝑓𝑧) − 𝑦)) < 𝑒)))}
432, 3, 6, 4, 42cmpo 5744 . 2 class (𝑓 ∈ (ℂ ↑pm ℂ), 𝑥 ∈ ℂ ↦ {𝑦 ∈ ℂ ∣ ((𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ ℂ) ∧ (𝑥 ∈ ℂ ∧ ∀𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑧 ∈ dom 𝑓((𝑧 # 𝑥 ∧ (abs‘(𝑧𝑥)) < 𝑑) → (abs‘((𝑓𝑧) − 𝑦)) < 𝑒)))})
441, 43wceq 1316 1 wff lim = (𝑓 ∈ (ℂ ↑pm ℂ), 𝑥 ∈ ℂ ↦ {𝑦 ∈ ℂ ∣ ((𝑓:dom 𝑓⟶ℂ ∧ dom 𝑓 ⊆ ℂ) ∧ (𝑥 ∈ ℂ ∧ ∀𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑧 ∈ dom 𝑓((𝑧 # 𝑥 ∧ (abs‘(𝑧𝑥)) < 𝑑) → (abs‘((𝑓𝑧) − 𝑦)) < 𝑒)))})
Colors of variables: wff set class
This definition is referenced by:  limcrcl  12723  limccl  12724  ellimc3apf  12725
  Copyright terms: Public domain W3C validator