HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  df-cnfn Structured version   Visualization version   GIF version

Definition df-cnfn 27872
Description: Define the set of continuous functionals on Hilbert space. For every "epsilon" (𝑦) there is a "delta" (𝑧) such that... (Contributed by NM, 11-Feb-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-cnfn ConFn = {𝑡 ∈ (ℂ ↑𝑚 ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ ℋ ((norm‘(𝑤 𝑥)) < 𝑧 → (abs‘((𝑡𝑤) − (𝑡𝑥))) < 𝑦)}
Distinct variable group:   𝑤,𝑡,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-cnfn
StepHypRef Expression
1 ccnfn 26976 . 2 class ConFn
2 vw . . . . . . . . . . . 12 setvar 𝑤
32cv 1473 . . . . . . . . . . 11 class 𝑤
4 vx . . . . . . . . . . . 12 setvar 𝑥
54cv 1473 . . . . . . . . . . 11 class 𝑥
6 cmv 26948 . . . . . . . . . . 11 class
73, 5, 6co 6431 . . . . . . . . . 10 class (𝑤 𝑥)
8 cno 26946 . . . . . . . . . 10 class norm
97, 8cfv 5694 . . . . . . . . 9 class (norm‘(𝑤 𝑥))
10 vz . . . . . . . . . 10 setvar 𝑧
1110cv 1473 . . . . . . . . 9 class 𝑧
12 clt 9833 . . . . . . . . 9 class <
139, 11, 12wbr 4481 . . . . . . . 8 wff (norm‘(𝑤 𝑥)) < 𝑧
14 vt . . . . . . . . . . . . 13 setvar 𝑡
1514cv 1473 . . . . . . . . . . . 12 class 𝑡
163, 15cfv 5694 . . . . . . . . . . 11 class (𝑡𝑤)
175, 15cfv 5694 . . . . . . . . . . 11 class (𝑡𝑥)
18 cmin 10020 . . . . . . . . . . 11 class
1916, 17, 18co 6431 . . . . . . . . . 10 class ((𝑡𝑤) − (𝑡𝑥))
20 cabs 13684 . . . . . . . . . 10 class abs
2119, 20cfv 5694 . . . . . . . . 9 class (abs‘((𝑡𝑤) − (𝑡𝑥)))
22 vy . . . . . . . . . 10 setvar 𝑦
2322cv 1473 . . . . . . . . 9 class 𝑦
2421, 23, 12wbr 4481 . . . . . . . 8 wff (abs‘((𝑡𝑤) − (𝑡𝑥))) < 𝑦
2513, 24wi 4 . . . . . . 7 wff ((norm‘(𝑤 𝑥)) < 𝑧 → (abs‘((𝑡𝑤) − (𝑡𝑥))) < 𝑦)
26 chil 26942 . . . . . . 7 class
2725, 2, 26wral 2800 . . . . . 6 wff 𝑤 ∈ ℋ ((norm‘(𝑤 𝑥)) < 𝑧 → (abs‘((𝑡𝑤) − (𝑡𝑥))) < 𝑦)
28 crp 11577 . . . . . 6 class +
2927, 10, 28wrex 2801 . . . . 5 wff 𝑧 ∈ ℝ+𝑤 ∈ ℋ ((norm‘(𝑤 𝑥)) < 𝑧 → (abs‘((𝑡𝑤) − (𝑡𝑥))) < 𝑦)
3029, 22, 28wral 2800 . . . 4 wff 𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ ℋ ((norm‘(𝑤 𝑥)) < 𝑧 → (abs‘((𝑡𝑤) − (𝑡𝑥))) < 𝑦)
3130, 4, 26wral 2800 . . 3 wff 𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ ℋ ((norm‘(𝑤 𝑥)) < 𝑧 → (abs‘((𝑡𝑤) − (𝑡𝑥))) < 𝑦)
32 cc 9693 . . . 4 class
33 cmap 7624 . . . 4 class 𝑚
3432, 26, 33co 6431 . . 3 class (ℂ ↑𝑚 ℋ)
3531, 14, 34crab 2804 . 2 class {𝑡 ∈ (ℂ ↑𝑚 ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ ℋ ((norm‘(𝑤 𝑥)) < 𝑧 → (abs‘((𝑡𝑤) − (𝑡𝑥))) < 𝑦)}
361, 35wceq 1474 1 wff ConFn = {𝑡 ∈ (ℂ ↑𝑚 ℋ) ∣ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ ℋ ((norm‘(𝑤 𝑥)) < 𝑧 → (abs‘((𝑡𝑤) − (𝑡𝑥))) < 𝑦)}
Colors of variables: wff setvar class
This definition is referenced by:  elcnfn  27907  hhcnf  27930
  Copyright terms: Public domain W3C validator