gfp_const_inf_le

Mathlib.Order.FixedPoints

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

English

GFP interacts with GFP through fixed-point mechanics under higher-order operators.

Русский

GFP взаимодействует с GFP в контексте операторов высших порядков.

LaTeX

$$$(\mathrm{gfp} \circ \mathrm{gfp})(f) = \mathrm{gfp}(f)$ under suitable conditions.$$

Lean4

theorem gfp_const_inf_le (x : α) : (const α x ⊓ f).gfp ≤ x :=
  (gfp_le _) fun _ hb => hb.trans inf_le_left

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

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

Разделы

Аффилиация

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