preimage_iterate_eq — Mathlib

English

For a function f: α → α and a natural number n, the n-fold preimage by f equals the n-fold preimage operator applied to f: preimage f^[n] = (preimage f)^[n].

Русский

Для функции f: α → α и натурального числа n верно, что n-кратный предобраз f равен n-кратному композиционному применению предобраза: preimage f^[n] = (preimage f)^[n].

LaTeX

$$$ \\operatorname{preimage} f^{[n]} = (\\operatorname{preimage} f)^{[n]}.$$$

Lean4

theorem preimage_iterate_eq {f : α → α} {n : ℕ} : Set.preimage f^[n] = (Set.preimage f)^[n] := by
  induction n with
  | zero => simp
  | succ n ih => rw [iterate_succ, iterate_succ', preimage_comp_eq, ih]

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