iterate — Mathlib

English

Iterates of an injOn function remain injOn, provided MapsTo holds at each step.

Русский

Итерации функции, инъективной на s, сохраняют инъективность на s на каждом шаге, если выполняется соответствующее отображение.

LaTeX

$$$ \\text{For } f:\\alpha\\to\\alpha, s:\\mathrm{Set}\\alpha, (h: \\operatorname{InjOn} f s) (hf: \\operatorname{MapsTo} f s s) : \\forall n, \\operatorname{InjOn} f^{[n]} s$$$

Lean4

theorem iterate {f : α → α} {s : Set α} (h : InjOn f s) (hf : MapsTo f s s) : ∀ n, InjOn f^[n] s
  | 0 => injOn_id _
  | (n + 1) => (h.iterate hf n).comp h hf

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