Theorems · Theorem · group theory

MulAction.isMultiplyPretransitive_of_le

∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {m n : ℕ}
  [MulAction.IsMultiplyPretransitive G α n],
  m ≤ n → n ≤ Nat.card α → ∀ [Finite α], MulAction.IsMultiplyPretransitive G α m

If α has at least n elements, then an n-pretransitive action is m-pretransitive for any m ≤ n. For an infinite α, use MulAction.isMultiplyPretransitive_of_le'.

Defined in

Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Cited by

6 results in Mathlib

Foundations

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

Assumes

GroupMulActionMulAction.IsMultiplyPretransitiveFinite