English
If an antitone function is continuous at the indexed supremum over a Sort, it sends this supremum to the indexed infimum of the composition.
Русский
Если антитонная функция непрерывна в индексном супремуме над набором, она переводит этот супремум в индексный инфимум композиции.
LaTeX
$$$Cf : ContinuousAt f (iSup g) \land Af : Antitone f \Rightarrow f(iSup g) = iInf (f \circ g)$$$
Lean4
/-- An antitone function `f` sending `bot` to `top` and continuous at the supremum of a set sends
this supremum to the infimum of the image of this set. -/
theorem map_sSup_of_continuousAt {f : α → β} {s : Set α} (Cf : ContinuousAt f (sSup s)) (Af : Antitone f)
(fbot : f ⊥ = ⊤) : f (sSup s) = sInf (f '' s) :=
Monotone.map_sSup_of_continuousAt (show ContinuousAt (OrderDual.toDual ∘ f) (sSup s) from Cf) Af fbot
