mem_range_derivFamily — Mathlib

English

For Small ι and normal f, a belongs to the range of derivFamily f if and only if a is a common fixed point of all f_i.

Русский

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

LaTeX

$$$$ a \in \mathrm{range}(\derivFamily f) \iff \forall i, f_i a = a. $$$$

Lean4

theorem mem_range_derivFamily [Small.{u} ι] (H : ∀ i, IsNormal (f i)) {a} :
    a ∈ Set.range (derivFamily f) ↔ ∀ i, f i a = a :=
  (fp_iff_derivFamily H).symm

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