map_sInf_of_continuousWithinAt — Mathlib

English

If a monotone function on s is continuous at the sup of s, then it maps the sup to the sup of the image of s in a suitable order-theoretic setting.

Русский

Если монотонная функция на s непрерывна в верхнем пределе s, то она отображает верхний предел в верхний предел образа s в соответствующей порядковой обстановке.

LaTeX

$$$\forall Cf Mf ftop,\; f(sSup(s)) = sSup(f''s)$$$

Lean4

/-- A monotone function `f` sending `top` to `top` and continuous at the infimum of a set sends
this infimum to the infimum of the image of this set. -/
theorem map_sInf_of_continuousWithinAt {f : α → β} {s : Set α} (Cf : ContinuousWithinAt f s (sInf s))
    (Mf : MonotoneOn f s) (ftop : f ⊤ = ⊤) : f (sInf s) = sInf (f '' s) :=
  MonotoneOn.map_sSup_of_continuousWithinAt (α := αᵒᵈ) (β := βᵒᵈ) Cf Mf.dual ftop

Похожие утверждения