inductive KTypeBoundedness' : Type

• boundedBoth : KTypeBoundedness'
• unboundedBoth : KTypeBoundedness'
• boundedBelow : KTypeBoundedness'
• boundedAbove : KTypeBoundedness'

@[implicit_reducible]

instance instDecidableEqKTypeBoundedness' : DecidableEq KTypeBoundedness'

def instReprKTypeBoundedness'.repr : KTypeBoundedness' → ℕ → Std.Format

@[implicit_reducible]

instance instReprKTypeBoundedness' : Repr KTypeBoundedness'

noncomputable def SL2GKModule.ktypeBoundedness {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} {V : Type u_3} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : SL2GKModule 𝔤 K 𝔨 Ad V) : KTypeBoundedness'

theorem SL2GKModule.ktypeBoundedness_eq_boundedBoth_iff {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} {V : Type u_3} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : SL2GKModule 𝔤 K 𝔨 Ad V) : M.ktypeBoundedness = KTypeBoundedness'.boundedBoth ↔ BddAbove M.ktypeSet ∧ BddBelow M.ktypeSet

theorem SL2GKModule.ktypeBoundedness_eq_boundedAbove_iff {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} {V : Type u_3} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : SL2GKModule 𝔤 K 𝔨 Ad V) : M.ktypeBoundedness = KTypeBoundedness'.boundedAbove ↔ BddAbove M.ktypeSet ∧ ¬BddBelow M.ktypeSet

theorem SL2GKModule.ktypeBoundedness_eq_boundedBelow_iff {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} {V : Type u_3} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : SL2GKModule 𝔤 K 𝔨 Ad V) : M.ktypeBoundedness = KTypeBoundedness'.boundedBelow ↔ ¬BddAbove M.ktypeSet ∧ BddBelow M.ktypeSet

theorem SL2GKModule.ktypeBoundedness_eq_unboundedBoth_iff {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] {K : Type u_2} [Group K] {𝔨 : LieSubalgebra ℂ 𝔤} {Ad : K →* 𝔤 →ₗ[ℂ] 𝔤} {V : Type u_3} [AddCommGroup V] [Module ℂ V] [LieRingModule 𝔤 V] [LieModule ℂ 𝔤 V] (M : SL2GKModule 𝔤 K 𝔨 Ad V) : M.ktypeBoundedness = KTypeBoundedness'.unboundedBoth ↔ ¬BddAbove M.ktypeSet ∧ ¬BddBelow M.ktypeSet