sup_univ_eq_ciSup — Mathlib

English

Let s be a nonempty finite Finset of indices and f: ι → α. Then the supremum of f over i ∈ s lies in the image f''s.

Русский

Пусть s — непустая конечная конечнотоповая часть индексов и f: ι → α. Тогда верхняя граница по i∈s лежит в образе f, т.е. существует i ∈ s с f(i) = sup_{i∈s} f(i).

LaTeX

$$$\exists i \in s, f(i) = \big\lceil\!\!\!\!\!\!\!\!\!\; \sup_{i∈s} f(i) \;\rceil$$$

Lean4

theorem sup_univ_eq_ciSup [Fintype ι] (f : ι → α) : univ.sup f = ⨆ i, f i :=
  le_antisymm (Finset.sup_le fun _ _ => le_ciSup (finite_range _).bddAbove _)
    (ciSup_le' fun _ => Finset.le_sup (mem_univ _))

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