English
The fixator of a finite subset s of cardinal d in an n-transitive action acts m-transitively on the complement provided d + m ≤ n.
Русский
Фиксатор конечного подмножества s кардинальности d в n-транзитивном действии действует транспитивно на дополнение при условии d + m ≤ n.
LaTeX
$$$IsMultiplyPretransitive\\ (fixingSubgroup\\ G\\ s)\\ (ofFixingSubgroup\\ G\\ s)\\ m$ при $s.ncard + m \\le n$$$
Lean4
/-- The fixator of a finite subset of cardinal d in an n-transitive action
acts m transitively on the complement if d + m ≤ n. -/
@[to_additive /-- The fixator of a finite subset of cardinal d in an n-transitive additive action
acts m transitively on the complement if d + m ≤ n. -/
]
theorem isMultiplyPretransitive' {m n : ℕ} [IsMultiplyPretransitive G α n] (s : Set α) [Finite s]
(hmn : s.ncard + m ≤ n) (hn : (n : ENat) ≤ ENat.card α) :
IsMultiplyPretransitive (fixingSubgroup G s) (SubMulAction.ofFixingSubgroup G s) m :=
letI : IsMultiplyPretransitive G α (s.ncard + m) := isMultiplyPretransitive_of_le' hmn hn
isMultiplyPretransitive G s rfl
