ciSup_mem_image — Mathlib

English

Let s be a finite subset of ι and f: ι → α. Then the supremum of the values f(i) for i ∈ s is attained by some i ∈ s, i.e. ⨆ i∈s f(i) ∈ { f(j) : j ∈ s }. Equivalently, there exists i ∈ s with f(i) = ⨆ j∈s f(j).

Русский

Пусть s—конечное подмножество индексов ι и пусть f: ι → α. Тогда супремум значений f(i) по i ∈ s достигается некоторым i ∈ s, то есть ⨆ i∈s f(i) ∈ { f(j) : j ∈ s }. Эквивалентно существует i ∈ s такое, что f(i) = ⨆ j∈s f(j).

LaTeX

$$$\exists i \in s, f(i) = \sup_{j\in s} f(j).$$$

Lean4

theorem ciSup_mem_image {s : Set ι} (hs : s.Finite) (h : ∃ x ∈ s, sSup ∅ ≤ f x) : ⨆ i ∈ s, f i ∈ f '' s :=
  by
  lift s to Finset ι using hs
  simp only [Finset.mem_coe] at h
  simpa using Finset.ciSup_mem_image f h

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