map_ciInf — Mathlib

English

For RightOrdContinuous f, for any g: ι → α with BddBelow (range g), f( iInf g ) = iInf (f ∘ g).

Русский

Для правой непрерывности f, при g: ι → α с ограниченностью снизу множества образов, f( iInf g ) = iInf (f ∘ g).

LaTeX

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

Lean4

theorem map_ciInf (hf : RightOrdContinuous f) {g : ι → α} (hg : BddBelow (range g)) : f (⨅ i, g i) = ⨅ i, f (g i) :=
  hf.orderDual.map_ciSup hg

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