![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > HSE Home > Th. List > chssii | Structured version Visualization version GIF version |
Description: A closed subspace of a Hilbert space is a subset of Hilbert space. (Contributed by NM, 6-Oct-1999.) (New usage is discouraged.) |
Ref | Expression |
---|---|
chssi.1 | ⊢ 𝐻 ∈ Cℋ |
Ref | Expression |
---|---|
chssii | ⊢ 𝐻 ⊆ ℋ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | chssi.1 | . . 3 ⊢ 𝐻 ∈ Cℋ | |
2 | 1 | chshii 28798 | . 2 ⊢ 𝐻 ∈ Sℋ |
3 | 2 | shssii 28784 | 1 ⊢ 𝐻 ⊆ ℋ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2051 ⊆ wss 3822 ℋchba 28490 Cℋ cch 28500 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-ext 2743 ax-sep 5056 ax-hilex 28570 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-clab 2752 df-cleq 2764 df-clel 2839 df-nfc 2911 df-rex 3087 df-rab 3090 df-v 3410 df-dif 3825 df-un 3827 df-in 3829 df-ss 3836 df-nul 4173 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-op 4442 df-uni 4709 df-br 4926 df-opab 4988 df-xp 5409 df-cnv 5411 df-dm 5413 df-rn 5414 df-res 5415 df-ima 5416 df-iota 6149 df-fv 6193 df-ov 6977 df-sh 28778 df-ch 28792 |
This theorem is referenced by: cheli 28803 chelii 28804 hhsscms 28850 chocvali 28872 chm1i 29029 chsscon3i 29034 chsscon2i 29036 chjoi 29061 chj1i 29062 shjshsi 29065 sshhococi 29119 h1dei 29123 spansnpji 29151 spanunsni 29152 h1datomi 29154 spansnji 29219 pjfi 29277 riesz3i 29635 hmopidmpji 29725 pjoccoi 29751 pjinvari 29764 stcltr2i 29848 mdsymi 29984 mdcompli 30002 dmdcompli 30003 |
Copyright terms: Public domain | W3C validator |