Description: Closure of complement of Hilbert subspace. Part of Remark 3.12 of Beran p. 107. (Contributed by NM, 13-Oct-1999) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | shoccl | ⊢ ( 𝐴 ∈ Sℋ → ( ⊥ ‘ 𝐴 ) ∈ Cℋ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | shss | ⊢ ( 𝐴 ∈ Sℋ → 𝐴 ⊆ ℋ ) | |
2 | occl | ⊢ ( 𝐴 ⊆ ℋ → ( ⊥ ‘ 𝐴 ) ∈ Cℋ ) | |
3 | 1 2 | syl | ⊢ ( 𝐴 ∈ Sℋ → ( ⊥ ‘ 𝐴 ) ∈ Cℋ ) |