English
In a suitable setting, a monotone function respects infima when continuous at the infimum of the domain set.
Русский
В соответствующей обстановке монотонная функция сохраняет инфимуми при условии непрерывности в инфимума области определения.
LaTeX
$$$Cf : ContinuousWithinAt f s (sInf s) \land Mf : MonotoneOn f s \Rightarrow f(sInf s) = sInf (f''s)$$$
Lean4
/-- If an antitone function sending `top` to `bot` is continuous at the indexed infimum over
a `Sort`, then it sends this indexed infimum to the indexed supremum of the composition. -/
theorem map_iInf_of_continuousAt {ι : Sort*} {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iInf g)) (Af : Antitone f)
(ftop : f ⊤ = ⊥) : f (iInf g) = iSup (f ∘ g) :=
Monotone.map_iInf_of_continuousAt (show ContinuousAt (OrderDual.toDual ∘ f) (iInf g) from Cf) Af ftop
