map_lfp

Mathlib.Order.FixedPoints

URI: https://scilib.ai/kg/mathlib#OrderHom.map_lfp

English

The mapping from lfp to its image under f is compatible with f and lfp; the lfp maps through f consistently.

Русский

Отображение lfp через f согласовано с f и lfp; lfp сохраняется под действием f.

LaTeX

$$$f\,\mathrm{lfp}(f) = \mathrm{lfp}(f)$$$

Lean4

@[simp]
theorem map_lfp : f f.lfp = f.lfp :=
  have h : f f.lfp ≤ f.lfp := f.map_le_lfp le_rfl
  h.antisymm <| f.lfp_le <| f.mono h

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

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

Разделы

Аффилиация

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