Theorems · Theorem · group theory

AddAction.le_stabilizer_iff_vadd_le

∀ {G : Type u_1} [inst : AddGroup G] {α : Type u_2} [inst_1 : AddAction G α] (s : Set α) (H : AddSubgroup G),
  H ≤ AddAction.stabilizer G s ↔ ∀ g ∈ H, g +ᵥ s ⊆ s

To prove inclusion of a subgroup in a stabilizer, it is enough to prove inclusions.

Defined in

Mathlib.GroupTheory.GroupAction.Basic

Cited by

0 results in Mathlib

Foundations

Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddGroupAddAction