iterate_commute — Mathlib

English

For all f, m, n ∈ ℕ, the two maps sending f to f^{[m]} and to f^{[n]} commute: the induced commutativity holds.

Русский

Для всех f, m, n ∈ ℕ соответствующие отображения «итерация» commute между собой.

LaTeX

$$$$\forall f:\alpha\to\alpha,\forall m,n:\mathbb{N},\ \mathrm{Commute}(\lambda x. x^{[m]}, \lambda x. x^{[n]}). $$$$

Lean4

theorem iterate_commute (m n : ℕ) : Commute (fun f : α → α ↦ f^[m]) fun f ↦ f^[n] := fun f ↦ iterate_comm f m n

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