Definition df-span

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	$$⊢\mathrm{span}=\left(x\in 𝒫\mathscr{H}⟼\bigcap \left\{y\in {\mathbf{S}}_{\mathscr{H}}|x\subseteq y\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cspn	$$class\mathrm{span}$$
1		vx	$$setvarx$$
2		chba	$$class\mathscr{H}$$
3	2	cpw	$$class𝒫\mathscr{H}$$
4		vy	$$setvary$$
5		csh	$$class{\mathbf{S}}_{\mathscr{H}}$$
6	1	cv	$$setvarx$$
7	4	cv	$$setvary$$
8	6 7	wss	$$wffx\subseteq y$$
9	8 4 5	crab	$$class\left\{y\in {\mathbf{S}}_{\mathscr{H}}|x\subseteq y\right\}$$
10	9	cint	$$class\bigcap \left\{y\in {\mathbf{S}}_{\mathscr{H}}|x\subseteq y\right\}$$
11	1 3 10	cmpt	$$class\left(x\in 𝒫\mathscr{H}⟼\bigcap \left\{y\in {\mathbf{S}}_{\mathscr{H}}|x\subseteq y\right\}\right)$$
12	0 11	wceq	$$wff\mathrm{span}=\left(x\in 𝒫\mathscr{H}⟼\bigcap \left\{y\in {\mathbf{S}}_{\mathscr{H}}|x\subseteq y\right\}\right)$$