English
A monotone function on s that is continuous at the infimum of s sends this infimum to the infimum of the image of s.
Русский
Монотонная функция на s, непрерывная в инфимума s, отправляет инфимума в инфимума образа s.
LaTeX
$$$Cf : ContinuousWithinAt f s (sInf s) \land Mf : MonotoneOn f s \Rightarrow f(sInf s) = sInf (f''s)$$$
Lean4
/-- An antitone function `f` sending `top` to `bot` and continuous at the infimum of a set sends
this infimum to the supremum of the image of this set. -/
theorem map_sInf_of_continuousAt {f : α → β} {s : Set α} (Cf : ContinuousAt f (sInf s)) (Af : Antitone f)
(ftop : f ⊤ = ⊥) : f (sInf s) = sSup (f '' s) :=
Monotone.map_sInf_of_continuousAt (show ContinuousAt (OrderDual.toDual ∘ f) (sInf s) from Cf) Af ftop
