finsetSup'_apply — Mathlib

English

For a nonempty finite set s and a family f: ι → C_c(α,β), the evaluation of the finite supremum over s at a equals the supremum over i in s of f(i) evaluated at a.

Русский

Для непустого конечного множества s и семейства f: ι → C_c(α,β) значение определённого верхнего предела в точке равно верхнему пределу значений на элементах множества.

LaTeX

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

Lean4

theorem finsetSup'_apply {ι : Type*} {s : Finset ι} (H : s.Nonempty) (f : ι → C_c(α, β)) (a : α) :
    s.sup' H f a = s.sup' H fun i ↦ f i a :=
  Finset.comp_sup'_eq_sup'_comp H (fun g : C_c(α, β) ↦ g a) fun _ _ ↦ rfl

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