Theorems · Theorem · group theory

MulAction.le_stabilizer_iff_smul_le

∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] (s : Set α) (H : Subgroup G),
  H ≤ MulAction.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

1 results in Mathlib

Foundations

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

Assumes

GroupMulAction