map_ciSup — Mathlib

English

Let α and β be ConditionallyComplete Lattices and f: α → β be left-continuous. If (g_i) is a family in α whose range is bounded above, then f preserves the supremum: f( sup_i g_i ) = sup_i f(g_i).

Русский

Пусть α, β — условно полноупорядоченные решетки, а отображение f: α → β — левая непрерывность. Если семейство (g_i) из α ограничено сверху, то f сохраняет супремум: f( sup_i g_i ) = sup_i f(g_i).

LaTeX

$$$ f\\left(\\sup_{i} g_i\\right) = \\sup_{i} f(g_i) $$$

Lean4

theorem map_ciSup (hf : LeftOrdContinuous f) {g : ι → α} (hg : BddAbove (range g)) : f (⨆ i, g i) = ⨆ i, f (g i) :=
  by
  simp only [iSup, hf.map_csSup (range_nonempty _) hg, ← range_comp]
  rfl

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