# Metamath Proof Explorer

## Definition df-cnfn

Description: Define the set of continuous functionals on Hilbert space. For every "epsilon" ( y ) there is a "delta" ( z ) such that... (Contributed by NM, 11-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion df-cnfn ${⊢}\mathrm{ContFn}=\left\{{t}\in \left({ℂ}^{ℋ}\right)|\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}\to \left|{t}\left({w}\right)-{t}\left({x}\right)\right|<{y}\right)\right\}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 ccnfn ${class}\mathrm{ContFn}$
1 vt ${setvar}{t}$
2 cc ${class}ℂ$
3 cmap ${class}{↑}_{𝑚}$
4 chba ${class}ℋ$
5 2 4 3 co ${class}\left({ℂ}^{ℋ}\right)$
6 vx ${setvar}{x}$
7 vy ${setvar}{y}$
8 crp ${class}{ℝ}^{+}$
9 vz ${setvar}{z}$
10 vw ${setvar}{w}$
11 cno ${class}{norm}_{ℎ}$
12 10 cv ${setvar}{w}$
13 cmv ${class}{-}_{ℎ}$
14 6 cv ${setvar}{x}$
15 12 14 13 co ${class}\left({w}{-}_{ℎ}{x}\right)$
16 15 11 cfv ${class}{norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)$
17 clt ${class}<$
18 9 cv ${setvar}{z}$
19 16 18 17 wbr ${wff}{norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}$
20 cabs ${class}\mathrm{abs}$
21 1 cv ${setvar}{t}$
22 12 21 cfv ${class}{t}\left({w}\right)$
23 cmin ${class}-$
24 14 21 cfv ${class}{t}\left({x}\right)$
25 22 24 23 co ${class}\left({t}\left({w}\right)-{t}\left({x}\right)\right)$
26 25 20 cfv ${class}\left|{t}\left({w}\right)-{t}\left({x}\right)\right|$
27 7 cv ${setvar}{y}$
28 26 27 17 wbr ${wff}\left|{t}\left({w}\right)-{t}\left({x}\right)\right|<{y}$
29 19 28 wi ${wff}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}\to \left|{t}\left({w}\right)-{t}\left({x}\right)\right|<{y}\right)$
30 29 10 4 wral ${wff}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}\to \left|{t}\left({w}\right)-{t}\left({x}\right)\right|<{y}\right)$
31 30 9 8 wrex ${wff}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}\to \left|{t}\left({w}\right)-{t}\left({x}\right)\right|<{y}\right)$
32 31 7 8 wral ${wff}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}\to \left|{t}\left({w}\right)-{t}\left({x}\right)\right|<{y}\right)$
33 32 6 4 wral ${wff}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}\to \left|{t}\left({w}\right)-{t}\left({x}\right)\right|<{y}\right)$
34 33 1 5 crab ${class}\left\{{t}\in \left({ℂ}^{ℋ}\right)|\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}\to \left|{t}\left({w}\right)-{t}\left({x}\right)\right|<{y}\right)\right\}$
35 0 34 wceq ${wff}\mathrm{ContFn}=\left\{{t}\in \left({ℂ}^{ℋ}\right)|\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\forall {y}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {z}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\forall {w}\in ℋ\phantom{\rule{.4em}{0ex}}\left({norm}_{ℎ}\left({w}{-}_{ℎ}{x}\right)<{z}\to \left|{t}\left({w}\right)-{t}\left({x}\right)\right|<{y}\right)\right\}$