exists_eq_ciSup_of_finite — Mathlib

English

If the index set ι is nonempty and finite, then there exists i ∈ ι such that f(i) equals the supremum of all f(j) over j ∈ ι.

Русский

Если множество индексов ι непусто и конечно, то существует i ∈ ι такое, что f(i) равно супремуму всех значений f(j) по j∈ι.

LaTeX

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

Lean4

theorem exists_eq_ciSup_of_finite [Nonempty ι] [Finite ι] {f : ι → α} : ∃ i, f i = ⨆ i, f i :=
  Nonempty.csSup_mem (range_nonempty f) (finite_range f)

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