English
A monotone function on a set s that is continuous at the supremum of s maps that supremum to the supremum of the image of s.
Русский
Монотонная функция на множестве s, непрерывная в s.sup, переводит верхнюю грань в верхнюю грань образа.
LaTeX
$$$\forall f\ s, (Cf : ContinuousWithinAt f s (sSup s)) \to (MonotoneOn f s) \to f(sSup s) = sSup(f''s)$$$
Lean4
/-- If a monotone function sending `bot` to `bot` 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)) (Mf : Monotone f)
(fbot : f ⊥ = ⊥) : f (⨆ i, g i) = ⨆ i, f (g i) := by
rw [iSup, Mf.map_sSup_of_continuousAt Cf fbot, ← range_comp, iSup, comp_def]
