English
If a monotone function f sends bottom to bottom and is continuous at the supremum of a set, then it preserves the supremum of the image of the set.
Русский
Если монотонная функция f отправляет нижнюю границу в нижнюю границу и непрерывна в верхней границе множества, то она сохраняет верхнюю грань образа множества.
LaTeX
$$$\text{ContinuousAt}(f, \mathrm{sup}(s)) \land Monotone(f) \land f(\bot)=\bot \Rightarrow f(\mathrm{sup}(s)) = \mathrm{sup}(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_continuousAt {f : α → β} {s : Set α} (Cf : ContinuousAt f (sSup s)) (Mf : Monotone f)
(fbot : f ⊥ = ⊥) : f (sSup s) = sSup (f '' s) :=
MonotoneOn.map_sSup_of_continuousWithinAt Cf.continuousWithinAt (Mf.monotoneOn _) fbot
