le_map_sSup — Mathlib

English

Let α, β be complete lattices and f: α → β be monotone. For any subset s ⊆ α, the supremum of f over s is at most f applied to the supremum of s: ⨆ a∈s, f(a) ≤ f(sSup s).

Русский

Пусть α, β — полные решетки, f: α → β монотонна. Тогда верхняя граница image f над подмножеством s не выше значения f на верхнем пределe s: ⨆_{a∈s} f(a) ≤ f(sSup s).

LaTeX

$$$\\\\sup_{a\\\\in s} f(a) \\\\le f(\\\\sup s) \\\\; (s \\\\subseteq α)$$$

Lean4

theorem le_map_sSup [CompleteLattice β] {s : Set α} {f : α → β} (hf : Monotone f) : ⨆ a ∈ s, f a ≤ f (sSup s) := by
  rw [sSup_eq_iSup]; exact hf.le_map_iSup₂ _

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