take_iterate — Mathlib

English

For any f, a, m, n, take m of iterate f a n equals iterate f a (min(m,n)).

Русский

Для любых f, a, m, n взятие первых m элементов iterate f a n равно iterate f a (min(m,n)).

LaTeX

$$$$ \\operatorname{take} m \\bigl( \\operatorname{iterate} f\\, a\\, n \\bigr) = \\operatorname{iterate} f\\, a\\, \\min(m,n). $$$$

Lean4

theorem take_iterate (f : α → α) (a : α) (m n : ℕ) : take m (iterate f a n) = iterate f a (min m n) := by
  rw [← range_map_iterate, ← range_map_iterate, ← map_take, take_range]

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