English
If a monotone function on s is continuous at the supremum of s, then it preserves suprema on s, i.e., f(sSup s) = sSup(f''s).
Русский
Если монотонная функция на s непрерывна в точке верхнего предела s, то она сохраняет верхнюю грань образа: f(sSup s) = sSup(f''s).
LaTeX
$$$\text{ContinuousWithinAt}(f,s,\,sSup(s)) \land MonotoneOn(f,s) \land f(\bot)=\bot \Rightarrow f(sSup(s)) = sSup(f''s)$$$
Lean4
/-- A monotone function `f` sending `bot` to `bot` and continuous at the supremum of a set sends
this supremum to the supremum of the image of this set. -/
theorem map_sSup_of_continuousWithinAt {f : α → β} {s : Set α} (Cf : ContinuousWithinAt f s (sSup s))
(Mf : MonotoneOn f s) (fbot : f ⊥ = ⊥) : f (sSup s) = sSup (f '' s) :=
by
rcases s.eq_empty_or_nonempty with h | h
· simp [h, fbot]
· exact Mf.map_csSup_of_continuousWithinAt Cf h
