fp_iff_derivFamily — Mathlib

English

For normal f, a is a fixed point of all f_i if and only if a lies in the range of derivFamily f.

Русский

Для нормальной системы f верно: a является фиксированной точкой всех f_i тогда и только тогда, когда a лежит в образе derivFamily f.

LaTeX

$$$$ (\forall i, f_i a = a) \iff \exists o, derivFamily f o = a. $$$$

Lean4

theorem fp_iff_derivFamily [Small.{u} ι] (H : ∀ i, IsNormal (f i)) {a} : (∀ i, f i a = a) ↔ ∃ o, derivFamily f o = a :=
  Iff.trans ⟨fun h i => le_of_eq (h i), fun h i => (H i).le_iff_eq.1 (h i)⟩ (le_iff_derivFamily H)

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