iInf_mem_map_of_exists_le_sInf_empty

English

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

Русский

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

LaTeX

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

Lean4

theorem iInf_mem_map_of_exists_le_sInf_empty {l : List ι} (f : ι → α) (h : ∃ x ∈ l, f x ≤ sInf ∅) :
    ⨅ x ∈ l, f x ∈ l.map f := by classical simpa using l.toFinset.ciInf_mem_image f (by simpa using h)

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