mem_range_deriv

Mathlib.SetTheory.Ordinal.FixedPoint

URI: https://scilib.ai/kg/mathlib#Ordinal.IsNormal.mem_range_deriv

English

For a normal f, a is in the range of deriv f iff f a = a.

Русский

Для нормальной f элемент a принадлежит диапазону deriv f тогда и только тогда, когда f a = a.

LaTeX

$$$$ a \in \mathrm{range}(\operatorname{deriv} f) \iff f a = a $$$$

Lean4

theorem mem_range_deriv (H : IsNormal f) {a} : a ∈ Set.range (deriv f) ↔ f a = a :=
  H.fp_iff_deriv.symm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru