map_csSup — Mathlib

English

A variant of map_csSup for ConditionallyCompleteLattice with nonempty set and bounding condition.

Русский

Вариант map_csSup для условно полностью упорядоченной множество с непустостью и ограничением сверху.

LaTeX

$$$\text{LeftOrdContinuous}(f) \rightarrow \forall s, s.Nonempty \rightarrow BddAbove s \rightarrow f(\mathrm{sSup}\,s) = \mathrm{csSup}\, (f''s)$$$

Lean4

theorem map_csSup (hf : LeftOrdContinuous f) {s : Set α} (sne : s.Nonempty) (sbdd : BddAbove s) :
    f (sSup s) = sSup (f '' s) :=
  ((hf <| isLUB_csSup sne sbdd).csSup_eq <| sne.image f).symm

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