instIsMultiplyPretransitiveOfIsMultiplyPreprimitive

English

An action is n-pretransitive iff the action on Fin n ↪ α is pretransitive; relation between pretransitive and preprimitive.

Русский

Действие является n-предтранзитивным тогда и только тогда, когда действие на Fin n ↪ α является предтранситивным; связь между предтранситивностью и предпримитивностью.

LaTeX

$$IsMultiplyPretransitive M α n ↔ IsPretransitive G α n$$

Lean4

@[to_additive]
instance (n : ℕ) [IsMultiplyPreprimitive M α n] : IsMultiplyPretransitive M α n :=
  IsMultiplyPreprimitive.isMultiplyPretransitive M α n

Похожие утверждения