Description: A subset of Hilbert space is included in its span. (Contributed by NM, 2-Jun-2004) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | spanss2 | |- ( A C_ ~H -> A C_ ( span ` A ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssintub | |- A C_ |^| { x e. SH | A C_ x } |
|
2 | spanval | |- ( A C_ ~H -> ( span ` A ) = |^| { x e. SH | A C_ x } ) |
|
3 | 1 2 | sseqtrrid | |- ( A C_ ~H -> A C_ ( span ` A ) ) |