map_iInf

Mathlib.Order.OrdContinuous

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

English

For RightOrdContinuous f, f(iInf g) = iInf_i f(g(i)).

Русский

Для правой непрерывности f: f( iInf_i g(i) ) = iInf_i f(g(i)).

LaTeX

$$$ f\\left(\\iinf_{i} g(i)\\right) = \\iinf_{i} f(g(i)). $$$

Lean4

theorem map_iInf (hf : RightOrdContinuous f) (g : ι → α) : f (⨅ i, g i) = ⨅ i, f (g i) :=
  hf.orderDual.map_iSup g

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

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

Разделы

Аффилиация

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