English
An antitone function on s that is continuous at the infimum of s maps this infimum to the supremum of the image.
Русский
Анти-монотонная функция на s, непрерывная в инфимума s, переводит этот инфимума в верхнюю грань образа.
LaTeX
$$$Cf : ContinuousWithinAt f s (sInf s) \land Af : AntitoneOn f s \Rightarrow f(sInf s) = sSup (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_continuousWithinAt {f : α → β} {s : Set α} (Cf : ContinuousWithinAt f s (sInf s))
(Af : AntitoneOn f s) (ftop : f ⊤ = ⊥) : f (sInf s) = sSup (f '' s) :=
MonotoneOn.map_sInf_of_continuousWithinAt (show ContinuousWithinAt (OrderDual.toDual ∘ f) s (sInf s) from Cf) Af ftop
