Theorems · Theorem · group theory

MulAction.IsPretransitive.of_partition

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

Defined in

Mathlib.GroupTheory.Perm.MaximalSubgroups

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupMulAction