map_sInf

Mathlib.Order.OrdContinuous

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

English

For RightOrdContinuous f, for any set s, f(sInf s) = ⨅ x ∈ s, f(x).

Русский

Для правой непрерывности f, для любого множества s выполняется f(sInf s) = ⨅_{x ∈ s} f(x).

LaTeX

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

Lean4

theorem map_sInf (hf : RightOrdContinuous f) (s : Set α) : f (sInf s) = ⨅ x ∈ s, f x :=
  hf.orderDual.map_sSup s

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

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

Разделы

Аффилиация

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