mem_iterate — Mathlib

English

For all f, a, n, b, b ∈ iterate f a n if and only if there exists m < n with b = f^[m] a.

Русский

Для всех f, a, n, b: b принадлежит iterate f a n тогда и только тогда, когда существует m < n такое, что b = f^[m] a.

LaTeX

$$$$ b \\in \\operatorname{iterate} f\\, a\\, n \\iff \\exists m < n,\\ b = f^{[m]} a. $$$$

Lean4

@[simp]
theorem mem_iterate {f : α → α} {a : α} {n : ℕ} {b : α} : b ∈ iterate f a n ↔ ∃ m < n, b = f^[m] a := by
  simp [List.mem_iff_get, Fin.exists_iff, eq_comm (b := b)]

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