iSup_mem_map_of_exists_sSup_empty_le

English

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

Русский

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

LaTeX

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

Lean4

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

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