coe_finsetSup' — Mathlib

English

The function equality for finset sup' holds after applying the coe map: the function underlying s.sup' H f equals s.sup' H of the mapped f(i).

Русский

Преобразование через приведение к функциям сохраняет равенство для верхнего предела по Finset: коe(...)= ...

LaTeX

$$coe((s.sup' H f)) = s.sup' H (λ i, coe(f(i)))$$

Lean4

@[simp, norm_cast]
theorem coe_finsetSup' {ι : Type*} {s : Finset ι} (H : s.Nonempty) (f : ι → C_c(α, β)) :
    ⇑(s.sup' H f) = s.sup' H fun i ↦ ⇑(f i) := by ext; simp [finsetSup'_apply]

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