sup'_eq_csSup_image — Mathlib

English

For a finite set s and function f, the supremum of f over s equals the supremum of the image f''s.

Русский

Для конечного множества s и функции f супремум значений f на s равен супремуму образа f''s.

LaTeX

$$$\sup_{i∈s} f(i) = \sup (f''s)$$$

Lean4

theorem sup'_eq_csSup_image (s : Finset ι) (H : s.Nonempty) (f : ι → α) : s.sup' H f = sSup (f '' s) :=
  eq_of_forall_ge_iff fun a => by simp [csSup_le_iff (s.finite_toSet.image f).bddAbove (H.to_set.image f)]

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