iSup_mem_map_of_ne_nil — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem iSup_mem_map_of_ne_nil {l : List ι} (f : ι → α) (h : l ≠ []) : ⨆ x ∈ l, f x ∈ l.map f :=
  l.iSup_mem_map_of_exists_sSup_empty_le _ (by simpa using exists_mem_of_ne_nil _ h)

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