map_sSup — Mathlib

English

For complete lattices, left order continuity yields f(sSup s) = sup { f x : x ∈ s }. In particular f preserves all suprema.

Русский

Для полных решёток левый порядок непрерывности отображает сохранение верхних пределов: f(sSup s) = ⨆ x∈s, f(x).

LaTeX

$$$\text{LeftOrdContinuous}(f) \Rightarrow f(\mathrm{sSup}\,s) = \displaystyle \bigvee_{x\in s} f(x)$$$

Lean4

theorem map_sSup (hf : LeftOrdContinuous f) (s : Set α) : f (sSup s) = ⨆ x ∈ s, f x := by rw [hf.map_sSup', sSup_image]

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