![]() |
Hilbert Space Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > HSE Home > Th. List > shssii | 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 |
---|---|
shssi.1 | ⊢ 𝐻 ∈ Sℋ |
Ref | Expression |
---|---|
shssii | ⊢ 𝐻 ⊆ ℋ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | shssi.1 | . 2 ⊢ 𝐻 ∈ Sℋ | |
2 | shss 28622 | . 2 ⊢ (𝐻 ∈ Sℋ → 𝐻 ⊆ ℋ) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐻 ⊆ ℋ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2166 ⊆ wss 3798 ℋchba 28331 Sℋ csh 28340 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2803 ax-sep 5005 ax-hilex 28411 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-rab 3126 df-v 3416 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-nul 4145 df-if 4307 df-pw 4380 df-sn 4398 df-pr 4400 df-op 4404 df-br 4874 df-opab 4936 df-xp 5348 df-cnv 5350 df-dm 5352 df-rn 5353 df-res 5354 df-ima 5355 df-sh 28619 |
This theorem is referenced by: sheli 28626 shelii 28627 chssii 28643 hhssabloilem 28673 hhssabloi 28674 hhssnv 28676 hhssba 28683 shunssji 28783 shsval3i 28802 shjshsi 28906 span0 28956 spanuni 28958 imaelshi 29472 nlelchi 29475 hmopidmchi 29565 pjimai 29590 shatomistici 29775 |
Copyright terms: Public domain | W3C validator |