map_sSup' — Mathlib

English

If f is left order continuous and s is a nonempty set bounded above, then f(sSup s) = sSup (f''s).

Русский

Если f слева непрерывна и s непусто и сверху ограничено, то f( sSup s ) = sSup (f''s).

LaTeX

$$$\text{LeftOrdContinuous}(f) \Rightarrow f(\mathrm{sSup}\,s) = \mathrm{sSup}(f''s)$ under nonempty sbdd$$

Lean4

theorem map_sSup' (hf : LeftOrdContinuous f) (s : Set α) : f (sSup s) = sSup (f '' s) :=
  (hf <| isLUB_sSup s).sSup_eq.symm

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