def IsMulOrderPropWith {G : Type u_1} [Group G] (n : ℕ) (A : Set G) : Prop

Equations

• IsMulOrderPropWith n A = IsOrderPropRelWith n fun (x1 x2 : G) => x1 * x2 ∈ A

def IsAddOrderPropWith {G : Type u_1} [AddGroup G] (n : ℕ) (A : Set G) : Prop

Equations

• IsAddOrderPropWith n A = IsOrderPropRelWith n fun (x1 x2 : G) => x1 + x2 ∈ A

def IsMulOrderProp {G : Type u_1} [Group G] (A : Set G) : Prop

Equations

• IsMulOrderProp A = IsOrderPropRel fun (x1 x2 : G) => x1 * x2 ∈ A

def IsAddOrderProp {G : Type u_1} [AddGroup G] (A : Set G) : Prop

Equations

• IsAddOrderProp A = IsOrderPropRel fun (x1 x2 : G) => x1 + x2 ∈ A

def IsMulStableWith {G : Type u_1} [Group G] (n : ℕ) (A : Set G) : Prop

Equations

• IsMulStableWith n A = IsStableRelWith n fun (x1 x2 : G) => x1 * x2 ∈ A

def IsAddStableWith {G : Type u_1} [AddGroup G] (n : ℕ) (A : Set G) : Prop

Equations

• IsAddStableWith n A = IsStableRelWith n fun (x1 x2 : G) => x1 + x2 ∈ A

def IsMulStable {G : Type u_1} [Group G] (A : Set G) : Prop

Equations

• IsMulStable A = IsStableRel fun (x1 x2 : G) => x1 * x2 ∈ A

def IsAddStable {G : Type u_1} [AddGroup G] (A : Set G) : Prop

Equations

• IsAddStable A = IsStableRel fun (x1 x2 : G) => x1 + x2 ∈ A

def IsMulTreeBoundedWith {G : Type u_1} [Group G] (n : ℕ) (A : Set G) : Prop

Equations

• IsMulTreeBoundedWith n A = IsTreeBoundedRelWith n fun (x1 x2 : G) => x1 * x2 ∈ A

def IsAddTreeBoundedWith {G : Type u_1} [AddGroup G] (n : ℕ) (A : Set G) : Prop

Equations

• IsAddTreeBoundedWith n A = IsTreeBoundedRelWith n fun (x1 x2 : G) => x1 + x2 ∈ A

@[simp]

theorem not_isMulStableWith {G : Type u_1} [Group G] {n : ℕ} {A : Set G} : ¬IsMulStableWith n A ↔ IsMulOrderPropWith n A

@[simp]

theorem not_isAddStableWith {G : Type u_1} [AddGroup G] {n : ℕ} {A : Set G} : ¬IsAddStableWith n A ↔ IsAddOrderPropWith n A

@[simp]

theorem not_isMulOrderPropWith {G : Type u_1} [Group G] {n : ℕ} {A : Set G} : ¬IsMulOrderPropWith n A ↔ IsMulStableWith n A

@[simp]

theorem not_isAddOrderPropWith {G : Type u_1} [AddGroup G] {n : ℕ} {A : Set G} : ¬IsAddOrderPropWith n A ↔ IsAddStableWith n A

@[simp]

theorem not_isMulStable {G : Type u_1} [Group G] {A : Set G} : ¬IsMulStable A ↔ IsMulOrderProp A

@[simp]

theorem not_isAddStable {G : Type u_1} [AddGroup G] {A : Set G} : ¬IsAddStable A ↔ IsAddOrderProp A

@[simp]

theorem not_isMulOrderProp {G : Type u_1} [Group G] {A : Set G} : ¬IsMulOrderProp A ↔ IsMulStable A

@[simp]

theorem not_isAddOrderProp {G : Type u_1} [AddGroup G] {A : Set G} : ¬IsAddOrderProp A ↔ IsAddStable A

theorem IsMulStableWith.isMulTreeBoundedWith {G : Type u_1} [Group G] {n : ℕ} {A : Set G} (hr : IsMulStableWith n A) : IsMulTreeBoundedWith (2 ^ n + 1) A

theorem IsAddStableWith.isAddTreeBoundedWith {G : Type u_1} [AddGroup G] {n : ℕ} {A : Set G} (hr : IsAddStableWith n A) : IsAddTreeBoundedWith (2 ^ n + 1) A

theorem IsMulTreeBoundedWith.isMulStableWith {G : Type u_1} [Group G] {n : ℕ} {A : Set G} (hr : IsMulTreeBoundedWith n A) : IsMulStableWith (2 ^ n) A

theorem IsAddTreeBoundedWith.isAddStableWith {G : Type u_1} [AddGroup G] {n : ℕ} {A : Set G} (hr : IsAddTreeBoundedWith n A) : IsAddStableWith (2 ^ n) A