Theorems · Theorem · group theory

MulAction.IsBlock.compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl

∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s : Set α} [Finite α]
  [MulAction.IsMultiplyPretransitive M α (s.ncard + 1)] {G : Subgroup M},
  MulAction.stabilizer M s ≤ G → ∀ {B : Set α}, ¬B ⊆ s → ¬B ⊆ sᶜ → MulAction.IsBlock (↥G) B → sᶜ ⊆ B

Defined in

Mathlib.GroupTheory.Perm.MaximalSubgroups

Cited by

2 results in Mathlib

Foundations

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

Assumes

GroupMulActionFiniteMulAction.IsMultiplyPretransitive