coe_finset_sup — Mathlib

English

For a finite set s and f : s → NNReal, the embedding commutes with finite suprema: ofNNReal(s.sup f) = s.sup (λ x, ENNReal.ofNNReal(f x)).

Русский

Для конечного множества s и функции f : s → NNReal встраивание сохраняет конечный верхний предел: ofNNReal(s.sup f) = s.sup (λ x, ENNReal.ofNNReal(f x)).

LaTeX

$$$\operatorname{ofNNReal}\bigl(s.sup f\bigr) = s.sup\bigl(\lambda x.\operatorname{ofNNReal}(f x)\bigr)$$$

Lean4

@[simp, norm_cast]
theorem coe_finset_sup {s : Finset α} {f : α → ℝ≥0} : ↑(s.sup f) = s.sup fun x => (f x : ℝ≥0∞) :=
  Finset.comp_sup_eq_sup_comp_of_is_total _ coe_mono rfl

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