English
An antitone function sending top to top is continuous at the indexed supremum over a Sort, then it preserves the top of the image supremum to the top.
Русский
Анти-монотонная функция, сохраняющая верхнюю границу, непрерывна в индексном супремуме; верхняя точка образа сохраняется.
LaTeX
$$$Cf : ContinuousAt f (iSup g) \land Af : Antitone f \land f(\top)=\top \Rightarrow f(iSup g) = iSup (f \circ g)$$$
Lean4
/-- An antitone function sending `bot` to `top` is continuous at the indexed supremum over
a `Sort`, then it sends this indexed supremum to the indexed supremum of the composition. -/
theorem map_iSup_of_continuousAt {ι : Sort*} {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iSup g)) (Af : Antitone f)
(fbot : f ⊥ = ⊤) : f (⨆ i, g i) = ⨅ i, f (g i) :=
Monotone.map_iSup_of_continuousAt (show ContinuousAt (OrderDual.toDual ∘ f) (iSup g) from Cf) Af fbot
