nfp_zero_left — Mathlib

English

For a normal f, f a = a iff there exists o with deriv f o = a.

Русский

Для нормальной f, f a = a тогда и только если существует o с deriv f o = a.

LaTeX

$$$$ f a = a \iff \exists o, \operatorname{deriv} f o = a $$$$

Lean4

theorem nfp_zero_left (a) : nfp 0 a = a := by
  rw [← iSup_iterate_eq_nfp]
  apply (Ordinal.iSup_le ?_).antisymm (Ordinal.le_iSup _ 0)
  intro n
  cases n
  · rfl
  · rw [Function.iterate_succ']
    simp

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