Database
COMPLEX HILBERT SPACE EXPLORER (DEPRECATED)
Subspaces and projections
Subspace sum, span, lattice join, lattice supremum
df-span
Metamath Proof Explorer
Description: Define the linear span of a subset of Hilbert space. Definition of span
in Schechter p. 276. See spanval for its value. (Contributed by NM , 2-Jun-2004) (New usage is discouraged.)
Ref
Expression
Assertion
df-span
⊢ span = x ∈ 𝒫 ℋ ⟼ ⋂ y ∈ S ℋ | x ⊆ y
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
cspn
class span
1
vx
setvar x
2
chba
class ℋ
3
2
cpw
class 𝒫 ℋ
4
vy
setvar y
5
csh
class S ℋ
6
1
cv
setvar x
7
4
cv
setvar y
8
6 7
wss
wff x ⊆ y
9
8 4 5
crab
class y ∈ S ℋ | x ⊆ y
10
9
cint
class ⋂ y ∈ S ℋ | x ⊆ y
11
1 3 10
cmpt
class x ∈ 𝒫 ℋ ⟼ ⋂ y ∈ S ℋ | x ⊆ y
12
0 11
wceq
wff span = x ∈ 𝒫 ℋ ⟼ ⋂ y ∈ S ℋ | x ⊆ y