sup_eq_iSup — Mathlib

English

For a finite set s and a function f, the supremum over s of f equals the binary join over all elements of s with f evaluated at each element.

Русский

Для конечного множества s и функции f супремум над s равен попарному объединению по всем элементам s.

LaTeX

$$$s.sup f = \bigsqcup_{a \in s} f(a)$$$

Lean4

theorem sup_eq_iSup [CompleteLattice β] (s : Finset α) (f : α → β) : s.sup f = ⨆ a ∈ s, f a :=
  le_antisymm (Finset.sup_le (fun a ha => le_iSup_of_le a <| le_iSup (fun _ => f a) ha))
    (iSup_le fun _ => iSup_le fun ha => le_sup ha)

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