`BookProof.QgOuterFockFL.mem_dsDom` {x : lp G 2} : x ∈ dsDom C ↔ (∀ i, (x : ∀ i, G i) i ∈ (C i).dom) ∧ Memℓp (fun i => opTot (C i).op ((x : ∀ i, G i) i)) 2

Initializing...

`BookProof.QgOuterFockFL.mem_dsDom` {x : lp G 2} : x ∈ dsDom C ↔ (∀ i, (x : ∀ i, G i) i ∈ (C i).dom) ∧ Memℓp (fun i => opTot (C i).op ((x : ∀ i, G i) i)) 2 · Prove2Me