theorem MulAction.stabilizer_inf_stabilizer_le_stabilizer_union {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] {s t : Set α} : MulAction.stabilizer G s ⊓ MulAction.stabilizer G t ≤ MulAction.stabilizer G (s ∪ t)

theorem AddAction.stabilizer_inf_stabilizer_le_stabilizer_union {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] {s t : Set α} : AddAction.stabilizer G s ⊓ AddAction.stabilizer G t ≤ AddAction.stabilizer G (s ∪ t)

theorem MulAction.stabilizer_inf_stabilizer_le_stabilizer_inter {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] {s t : Set α} : MulAction.stabilizer G s ⊓ MulAction.stabilizer G t ≤ MulAction.stabilizer G (s ∩ t)

theorem AddAction.stabilizer_inf_stabilizer_le_stabilizer_inter {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] {s t : Set α} : AddAction.stabilizer G s ⊓ AddAction.stabilizer G t ≤ AddAction.stabilizer G (s ∩ t)

theorem MulAction.stabilizer_inf_stabilizer_le_stabilizer_sdiff {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] {s t : Set α} : MulAction.stabilizer G s ⊓ MulAction.stabilizer G t ≤ MulAction.stabilizer G (s \ t)

theorem AddAction.stabilizer_inf_stabilizer_le_stabilizer_sdiff {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] {s t : Set α} : AddAction.stabilizer G s ⊓ AddAction.stabilizer G t ≤ AddAction.stabilizer G (s \ t)

theorem MulAction.stabilizer_union_eq_left {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] {s t : Set α} (hdisj : Disjoint s t) (hstab : MulAction.stabilizer G s ≤ MulAction.stabilizer G t) (hstab_union : MulAction.stabilizer G (s ∪ t) ≤ MulAction.stabilizer G t) : MulAction.stabilizer G (s ∪ t) = MulAction.stabilizer G s

theorem AddAction.stabilizer_union_eq_left {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] {s t : Set α} (hdisj : Disjoint s t) (hstab : AddAction.stabilizer G s ≤ AddAction.stabilizer G t) (hstab_union : AddAction.stabilizer G (s ∪ t) ≤ AddAction.stabilizer G t) : AddAction.stabilizer G (s ∪ t) = AddAction.stabilizer G s

theorem MulAction.stabilizer_union_eq_right {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] {s t : Set α} (hdisj : Disjoint s t) (hstab : MulAction.stabilizer G t ≤ MulAction.stabilizer G s) (hstab_union : MulAction.stabilizer G (s ∪ t) ≤ MulAction.stabilizer G s) : MulAction.stabilizer G (s ∪ t) = MulAction.stabilizer G t

theorem AddAction.stabilizer_union_eq_right {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] {s t : Set α} (hdisj : Disjoint s t) (hstab : AddAction.stabilizer G t ≤ AddAction.stabilizer G s) (hstab_union : AddAction.stabilizer G (s ∪ t) ≤ AddAction.stabilizer G s) : AddAction.stabilizer G (s ∪ t) = AddAction.stabilizer G t

theorem MulAction.mem_stabilizer_iff_subset_smul_set {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] {s : Set α} {a : G} (hs : s.Finite) : a ∈ MulAction.stabilizer G s ↔ s ⊆ a • s

theorem AddAction.mem_stabilizer_iff_subset_vadd_set {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] {s : Set α} {a : G} (hs : s.Finite) : a ∈ AddAction.stabilizer G s ↔ s ⊆ a +ᵥ s

theorem MulAction.mem_stabilizer_iff_smul_set_subset {G : Type u_1} {α : Type u_3} [Group G] [MulAction G α] {s : Set α} {a : G} (hs : s.Finite) : a ∈ MulAction.stabilizer G s ↔ a • s ⊆ s

theorem AddAction.mem_stabilizer_iff_vadd_set_subset {G : Type u_1} {α : Type u_3} [AddGroup G] [AddAction G α] {s : Set α} {a : G} (hs : s.Finite) : a ∈ AddAction.stabilizer G s ↔ a +ᵥ s ⊆ s

theorem MulAction.op_smul_set_stabilizer_subset {G : Type u_1} [Group G] {a : G} {s : Set G} (ha : a ∈ s) : MulOpposite.op a • ↑(MulAction.stabilizer G s) ⊆ s

theorem AddAction.op_vadd_set_stabilizer_subset {G : Type u_1} [AddGroup G] {a : G} {s : Set G} (ha : a ∈ s) : AddOpposite.op a +ᵥ ↑(AddAction.stabilizer G s) ⊆ s

theorem MulAction.stabilizer_subset_div_right {G : Type u_1} [Group G] {a : G} {s : Set G} (ha : a ∈ s) : ↑(MulAction.stabilizer G s) ⊆ s / {a}

theorem AddAction.stabilizer_subset_sub_right {G : Type u_1} [AddGroup G] {a : G} {s : Set G} (ha : a ∈ s) : ↑(AddAction.stabilizer G s) ⊆ s - {a}

theorem MulAction.stabilizer_finite {G : Type u_1} [Group G] {s : Set G} (hs₀ : s.Nonempty) (hs : s.Finite) : (↑(MulAction.stabilizer G s)).Finite

theorem AddAction.stabilizer_finite {G : Type u_1} [AddGroup G] {s : Set G} (hs₀ : s.Nonempty) (hs : s.Finite) : (↑(AddAction.stabilizer G s)).Finite

theorem MulAction.smul_set_stabilizer_subset {G : Type u_1} [CommGroup G] {s : Set G} {a : G} (ha : a ∈ s) : a • ↑(MulAction.stabilizer G s) ⊆ s

theorem AddAction.vadd_set_stabilizer_subset {G : Type u_1} [AddCommGroup G] {s : Set G} {a : G} (ha : a ∈ s) : a +ᵥ ↑(AddAction.stabilizer G s) ⊆ s