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

Definition df-cncf 12741
 Description: Define the operation whose value is a class of continuous complex functions. (Contributed by Paul Chapman, 11-Oct-2007.)
Assertion
Ref Expression
df-cncf cn→ = (𝑎 ∈ 𝒫 ℂ, 𝑏 ∈ 𝒫 ℂ ↦ {𝑓 ∈ (𝑏𝑚 𝑎) ∣ ∀𝑥𝑎𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑦𝑎 ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)})
Distinct variable group:   𝑎,𝑏,𝑑,𝑒,𝑓,𝑥,𝑦

Detailed syntax breakdown of Definition df-cncf
StepHypRef Expression
1 ccncf 12740 . 2 class cn
2 va . . 3 setvar 𝑎
3 vb . . 3 setvar 𝑏
4 cc 7630 . . . 4 class
54cpw 3510 . . 3 class 𝒫 ℂ
6 vx . . . . . . . . . . . . 13 setvar 𝑥
76cv 1330 . . . . . . . . . . . 12 class 𝑥
8 vy . . . . . . . . . . . . 13 setvar 𝑦
98cv 1330 . . . . . . . . . . . 12 class 𝑦
10 cmin 7945 . . . . . . . . . . . 12 class
117, 9, 10co 5774 . . . . . . . . . . 11 class (𝑥𝑦)
12 cabs 10781 . . . . . . . . . . 11 class abs
1311, 12cfv 5123 . . . . . . . . . 10 class (abs‘(𝑥𝑦))
14 vd . . . . . . . . . . 11 setvar 𝑑
1514cv 1330 . . . . . . . . . 10 class 𝑑
16 clt 7812 . . . . . . . . . 10 class <
1713, 15, 16wbr 3929 . . . . . . . . 9 wff (abs‘(𝑥𝑦)) < 𝑑
18 vf . . . . . . . . . . . . . 14 setvar 𝑓
1918cv 1330 . . . . . . . . . . . . 13 class 𝑓
207, 19cfv 5123 . . . . . . . . . . . 12 class (𝑓𝑥)
219, 19cfv 5123 . . . . . . . . . . . 12 class (𝑓𝑦)
2220, 21, 10co 5774 . . . . . . . . . . 11 class ((𝑓𝑥) − (𝑓𝑦))
2322, 12cfv 5123 . . . . . . . . . 10 class (abs‘((𝑓𝑥) − (𝑓𝑦)))
24 ve . . . . . . . . . . 11 setvar 𝑒
2524cv 1330 . . . . . . . . . 10 class 𝑒
2623, 25, 16wbr 3929 . . . . . . . . 9 wff (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒
2717, 26wi 4 . . . . . . . 8 wff ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)
282cv 1330 . . . . . . . 8 class 𝑎
2927, 8, 28wral 2416 . . . . . . 7 wff 𝑦𝑎 ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)
30 crp 9453 . . . . . . 7 class +
3129, 14, 30wrex 2417 . . . . . 6 wff 𝑑 ∈ ℝ+𝑦𝑎 ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)
3231, 24, 30wral 2416 . . . . 5 wff 𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑦𝑎 ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)
3332, 6, 28wral 2416 . . . 4 wff 𝑥𝑎𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑦𝑎 ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)
343cv 1330 . . . . 5 class 𝑏
35 cmap 6542 . . . . 5 class 𝑚
3634, 28, 35co 5774 . . . 4 class (𝑏𝑚 𝑎)
3733, 18, 36crab 2420 . . 3 class {𝑓 ∈ (𝑏𝑚 𝑎) ∣ ∀𝑥𝑎𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑦𝑎 ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)}
382, 3, 5, 5, 37cmpo 5776 . 2 class (𝑎 ∈ 𝒫 ℂ, 𝑏 ∈ 𝒫 ℂ ↦ {𝑓 ∈ (𝑏𝑚 𝑎) ∣ ∀𝑥𝑎𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑦𝑎 ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)})
391, 38wceq 1331 1 wff cn→ = (𝑎 ∈ 𝒫 ℂ, 𝑏 ∈ 𝒫 ℂ ↦ {𝑓 ∈ (𝑏𝑚 𝑎) ∣ ∀𝑥𝑎𝑒 ∈ ℝ+𝑑 ∈ ℝ+𝑦𝑎 ((abs‘(𝑥𝑦)) < 𝑑 → (abs‘((𝑓𝑥) − (𝑓𝑦))) < 𝑒)})
 Colors of variables: wff set class This definition is referenced by:  cncfval  12742  cncfrss  12745  cncfrss2  12746
 Copyright terms: Public domain W3C validator