English
If f is a normal function betweenconditionally complete linear orders, then for any nonempty bounded-below set s, f(sSup s) equals sSup of the image f'' s.
Русский
Если f — нормальная функция между частично совокупно завершёнными линейными порядками, то для любого ненулевого множества s ограниченного сверху выполняется f( sSup s ) = sSup( f'' s ).
LaTeX
$$$\\mathrm{IsNormal}(f) \\Rightarrow \\forall s, s \\neq \\emptyset \\wedge \\mathrm{BddAbove}(s) \\Rightarrow f(\\mathrm{sSup}\\ s) = \\mathrm{sSup}(f''\\,s).$$$
Lean4
theorem map_sSup (hf : IsNormal f) {s : Set α} (hs : s.Nonempty) (hs' : BddAbove s) : f (sSup s) = sSup (f '' s) :=
((hf.map_isLUB (isLUB_csSup hs hs') hs).csSup_eq (hs.image f)).symm
