Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HSE Home > Th. List > df-ch | Structured version Visualization version GIF version |
Description: Define the set of closed subspaces of a Hilbert space. A closed subspace is one in which the limit of every convergent sequence in the subspace belongs to the subspace. For its membership relation, see isch 29157. From Definition of [Beran] p. 107. Alternate definitions are given by isch2 29158 and isch3 29176. (Contributed by NM, 17-Aug-1999.) (New usage is discouraged.) |
Ref | Expression |
---|---|
df-ch | ⊢ Cℋ = {ℎ ∈ Sℋ ∣ ( ⇝𝑣 “ (ℎ ↑m ℕ)) ⊆ ℎ} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cch 28864 | . 2 class Cℋ | |
2 | chli 28862 | . . . . 5 class ⇝𝑣 | |
3 | vh | . . . . . . 7 setvar ℎ | |
4 | 3 | cv 1541 | . . . . . 6 class ℎ |
5 | cn 11716 | . . . . . 6 class ℕ | |
6 | cmap 8437 | . . . . . 6 class ↑m | |
7 | 4, 5, 6 | co 7170 | . . . . 5 class (ℎ ↑m ℕ) |
8 | 2, 7 | cima 5528 | . . . 4 class ( ⇝𝑣 “ (ℎ ↑m ℕ)) |
9 | 8, 4 | wss 3843 | . . 3 wff ( ⇝𝑣 “ (ℎ ↑m ℕ)) ⊆ ℎ |
10 | csh 28863 | . . 3 class Sℋ | |
11 | 9, 3, 10 | crab 3057 | . 2 class {ℎ ∈ Sℋ ∣ ( ⇝𝑣 “ (ℎ ↑m ℕ)) ⊆ ℎ} |
12 | 1, 11 | wceq 1542 | 1 wff Cℋ = {ℎ ∈ Sℋ ∣ ( ⇝𝑣 “ (ℎ ↑m ℕ)) ⊆ ℎ} |
Colors of variables: wff setvar class |
This definition is referenced by: isch 29157 |
Copyright terms: Public domain | W3C validator |