cast_finsetSup — Mathlib

English

Cast preserves Finset supremum when the codomain has order and addition structure.

Русский

Приведение сохраняет верхнюю грань по Finset, когда кодируемое множество обладает порядком и структурой сложения.

LaTeX

$$$(s.sup f)^{\\text{cast}} = s.sup (f\\mapsto f^{\\text{cast}})$$$

Lean4

@[simp, norm_cast]
theorem cast_finsetSup [OrderBot R] [CanonicallyOrderedAdd R] (s : Finset ι) (f : ι → ℕ) :
    (↑(s.sup f) : R) = s.sup fun i ↦ (f i : R) :=
  comp_sup_eq_sup_comp _ cast_max (by simp)

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