Theorems · Theorem · group theory

Subgroup.isPretransitive_of_stabilizer_lt

∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s : Set α} {G : Subgroup M},
  MulAction.stabilizer M s < G →
    (∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ g ∈ MulAction.stabilizer M s, g • a = b) → MulAction.IsPretransitive (↥G) α

Defined in

Mathlib.GroupTheory.Perm.MaximalSubgroups

Cited by

2 results in Mathlib

Foundations

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

Assumes

GroupMulAction