iSup_mem_map_of_exists_sSup_empty_le

English

For a finite list l and a function f: ι → α, if there exists x ∈ l with sSup ∅ ≤ f(x), then the supremum of f(x) over x ∈ l lies in the list map f, i.e. there exists i ∈ l with f(i) = sup_{x∈l} f(x).

Русский

Для конечного списка l и функции f: ι → α, если существует x ∈ l такое, что sSup ∅ ≤ f(x), то верхняя грань значений f на l достигается в образе списка: найдётся i∈l такое, что f(i) = sup_{x∈l} f(x).

LaTeX

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

Lean4

theorem iSup_mem_map_of_exists_sSup_empty_le {l : List ι} (f : ι → α) (h : ∃ x ∈ l, sSup ∅ ≤ f x) :
    ⨆ x ∈ l, f x ∈ l.map f := by classical simpa using l.toFinset.ciSup_mem_image f (by simpa using h)

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