Theorems · Theorem · group theory

MulAction.IsBlock.subsingleton_of_stabilizer_lt_of_subset

∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s B : Set α} {G : Subgroup M}
  [MulAction.IsPreprimitive ↥(MulAction.stabilizer (↥G) s) ↑s],
  MulAction.IsBlock (↥G) B →
    (∀ (B : Set α), MulAction.IsBlock (↥G) B → B ⊆ sᶜ → B.Subsingleton) →
      MulAction.stabilizer M s < G → B ⊆ s → B.Subsingleton

Defined in

Mathlib.GroupTheory.Perm.MaximalSubgroups

Cited by

2 results in Mathlib

Foundations

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

Assumes

GroupMulActionMulAction.IsPreprimitive