English
Let f be a normal function between ConditionallyCompleteLinearOrders. Then f of the supremum of a nonempty bounded above range is the supremum of the image, i.e., f(⨆ i, g i) = ⨆ i, f(g i).
Русский
Пусть f — нормальная функция между операторами ConditionallyCompleteLinearOrder. Тогда f(⨆ i, g(i)) = ⨆ i, f(g(i)).
LaTeX
$$$\\mathrm{IsNormal}(f) \\Rightarrow \\forall \\{g : ι \\to α\\}, (s.Nonempty) \\to (\\mathrm{BddAbove}(\\{ g i \\mid i \\in ι\\})) \\Rightarrow f(\\bigvee_i g(i)) = \\bigvee_i f(g(i)).$$$
Lean4
theorem map_iSup {ι} [Nonempty ι] {g : ι → α} (hf : IsNormal f) (hg : BddAbove (range g)) :
f (⨆ i, g i) = ⨆ i, f (g i) := by
unfold iSup
convert map_sSup hf (range_nonempty g) hg
ext
simp
