iInf_mem_map_of_exists_le_sInf_empty

English

Let s be a finite multiset of indices and f: ι → α. If there exists x ∈ s with f(x) ≤ sInf ∅, then the infimum of f on s lies in the image of s.map f; i.e. there exists x ∈ s with f(x) = inf_{y∈s} f(y).

Русский

Пусть s — конечное мультимножество индексов и f: ι → α. Если существует x ∈ s такое, что f(x) ≤ sInf ∅, то инфimum значений f на s достигается образе s.map f; найдётся x ∈ s такое, что f(x) = inf_{y∈s} f(y).

LaTeX

$$$\exists x \in s, f(x) = \inf_{y\in s} f(y).$$$

Lean4

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

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