coe_sup' — Mathlib

English

The coercion commutes with the finite sup' operation: the function (s.sup' H f) equals the supremum of the coerced functions.

Русский

Коэрция сохраняет операцию конечного суперпредела: (s.sup' H f) равен максимуму коэрцированных функций.

LaTeX

$$@[simp, norm_cast] (s.sup' H f) = s.sup' H (λ i, ⇑(f i))$$

Lean4

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

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