![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > HSE Home > Th. List > df-hcau | Structured version Unicode version |
Description: Define the set of Cauchy
sequences on a Hilbert space. See hcau 24739 for
its membership relation. Note that ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
df-hcau |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ccau 24481 |
. 2
![]() ![]() | |
2 | vy |
. . . . . . . . . . 11
![]() ![]() | |
3 | 2 | cv 1369 |
. . . . . . . . . 10
![]() ![]() |
4 | vf |
. . . . . . . . . . 11
![]() ![]() | |
5 | 4 | cv 1369 |
. . . . . . . . . 10
![]() ![]() |
6 | 3, 5 | cfv 5527 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() |
7 | vz |
. . . . . . . . . . 11
![]() ![]() | |
8 | 7 | cv 1369 |
. . . . . . . . . 10
![]() ![]() |
9 | 8, 5 | cfv 5527 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() |
10 | cmv 24480 |
. . . . . . . . 9
![]() ![]() | |
11 | 6, 9, 10 | co 6201 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | cno 24478 |
. . . . . . . 8
![]() ![]() | |
13 | 11, 12 | cfv 5527 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | vx |
. . . . . . . 8
![]() ![]() | |
15 | 14 | cv 1369 |
. . . . . . 7
![]() ![]() |
16 | clt 9530 |
. . . . . . 7
![]() ![]() | |
17 | 13, 15, 16 | wbr 4401 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
18 | cuz 10973 |
. . . . . . 7
![]() ![]() | |
19 | 3, 18 | cfv 5527 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() |
20 | 17, 7, 19 | wral 2799 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
21 | cn 10434 |
. . . . 5
![]() ![]() | |
22 | 20, 2, 21 | wrex 2800 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
23 | crp 11103 |
. . . 4
![]() ![]() | |
24 | 22, 14, 23 | wral 2799 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
25 | chil 24474 |
. . . 4
![]() ![]() | |
26 | cmap 7325 |
. . . 4
![]() ![]() | |
27 | 25, 21, 26 | co 6201 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
28 | 24, 4, 27 | crab 2803 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
29 | 1, 28 | wceq 1370 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
This definition is referenced by: h2hcau 24534 hcau 24739 |
Copyright terms: Public domain | W3C validator |