sup_eq_sSup_image — Mathlib

English

If β is a complete lattice and s is a finite set, with f: α → β, then the supremum of f over s equals the supremum of the image f''s; equivalently, sup_{x∈s} f(x) = sup{ f(x) : x ∈ s }.

Русский

Пусть β — полная решетка, s — конечное множество, f: α → β. Тогда супремум значений f над s равен супремуму образа f''s; то есть sup_{x∈s} f(x) = sup{ f(x) : x ∈ s }.

LaTeX

$$$ \sup_{x \in s} f(x) = \sup \{ f(x) : x \in s \} $$$

Lean4

theorem sup_eq_sSup_image [CompleteLattice β] (s : Finset α) (f : α → β) : s.sup f = sSup (f '' s) := by
  classical rw [← Finset.coe_image, ← sup_id_eq_sSup, sup_image, Function.id_comp]

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