map_sInf'

Mathlib.Order.OrdContinuous

URI: https://scilib.ai/kg/mathlib#RightOrdContinuous.map_sInf'

English

For RightOrdContinuous f, for any s, f(sInf s) = sInf (f '' s).

Русский

Для правой непрерывности f: f( sInf s ) = sInf( f'' s ).

LaTeX

$$$ f\\left(\\mathrm{sInf}(s)\\right) = \\mathrm{sInf}\\left(\\{ f(x) : x \\in s\\} \\right). $$$

Lean4

theorem map_sInf' (hf : RightOrdContinuous f) (s : Set α) : f (sInf s) = sInf (f '' s) :=
  hf.orderDual.map_sSup' s

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

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

Разделы

Аффилиация

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