iSup_mem_map_of_ne_zero — Mathlib

English

For a nonzero multiset s of indices and a function f: ι → α, the supremum of f(i) over i ∈ s is attained by some i ∈ s (i.e. it lies in the image of s.map f).

Русский

Для мультимножества s невырожденного индексов и функции f: ι → α, верхняя грань f по i∈s достигается в образе s.map f.

LaTeX

$$$\exists i \in s, f(i) = \sup_{x\in s} f(x).$$$

Lean4

theorem iSup_mem_map_of_ne_zero {s : Multiset ι} (f : ι → α) (h : s ≠ 0) : ⨆ x ∈ s, f x ∈ s.map f :=
  s.iSup_mem_map_of_exists_sSup_empty_le _ (by simpa using exists_mem_of_ne_zero h)

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