`BookProof.ChapterWeylSl2.Sl2Rep.IsInv.inf` {R : Sl2Rep V} {U W : Submodule ℂ V} (hU : R.IsInv U) (hW : R.IsInv W) : R.IsInv (U ⊓ W)

-- Generated from ChapterWeylSl2.lean — theorem BookProof.ChapterWeylSl2.Sl2Rep.IsInv.inf
import Mathlib
import Definitions.Def_ChapterWeylSl2
import Definitions.Def_ChapterDoubleSlit
import Definitions.Def_ChapterGleasonPureMixed
open BookProof.ChapterDoubleSlit
open BookProof.ChapterGleasonPureMixed
open BookProof.ChapterWeylSl2



universe u

variable {V : Type u} [AddCommGroup V] [Module ℂ V]

variable (R : Sl2Rep V)
variable {R}
variable {R : Sl2Rep V}

theorem BookProof.ChapterWeylSl2.Sl2Rep.IsInv.inf {R : Sl2Rep V} {U W : Submodule ℂ V} (hU : R.IsInv U) (hW : R.IsInv W) :
    R.IsInv (U ⊓ W) := by sorry