finset_sup_apply — Mathlib

English

For a finite set s of indices, the value at a of the pointwise supremum of a family fc is the supremum over c in s of the values at a: (s.sup f) a = s.sup (λ c, f c a).

Русский

Для конечного множества индексов s значение на точке a верхней суммы по семейству функций fc равно верхней границе значений fc(a) по c в s.

LaTeX

$$$\\left( s \\text{.sup } f \\right) a = s \\;\\text{sup}_{c \\in s} \\; (f c) a.$$$

Lean4

theorem finset_sup_apply [SemilatticeSup β] [OrderBot β] {f : γ → α →ₛ β} (s : Finset γ) (a : α) :
    s.sup f a = s.sup fun c => f c a := by
  classical
  refine Finset.induction_on s rfl ?_
  intro a s _ ih
  rw [Finset.sup_insert, Finset.sup_insert, sup_apply, ih]

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