sup'_eq_sup — Mathlib

English

Let s be a nonempty finite subset of β and f: β → α. Then the primed supremum equals the ordinary supremum: sup'_{s} f = sup_{s} f.

Русский

Пусть s — непустое конечное подмножество β и f: β → α. Тогда эквивалентно: sup'_{s} f = sup_{x ∈ s} f(x).

LaTeX

$$$s \neq \varnothing \Rightarrow \mathrm{sup}'_{s} f = \mathrm{sup}_{x \in s} f(x)$$$

Lean4

theorem sup'_eq_sup {s : Finset β} (H : s.Nonempty) (f : β → α) : s.sup' H f = s.sup f :=
  le_antisymm (sup'_le H f fun _ => le_sup) (Finset.sup_le fun _ => le_sup' f)

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