finsetSup_apply — Mathlib

English

For a nonempty finite set s of indices Y, the coefficient of the supremum at x,y equals the finite supremum over i ∈ s of f(i)(x,y).

Русский

Для непустого конечного множества индексов s, значение $ (s.sup f)(x,y) $ равно максимуму по i∈s от $ f(i)(x,y) $.

LaTeX

$$$\bigl( s.sup f \bigr)(x,y) = \max_{i \in s} f(i)(x,y).$$$

Lean4

theorem finsetSup_apply [IsOrderedAddMonoid R] {Y : Type*} {f : Y → PseudoMetric X R} {s : Finset Y} (hs : s.Nonempty)
    (x y : X) : s.sup f x y = s.sup' hs fun i ↦ f i x y := by
  induction hs using Finset.Nonempty.cons_induction with
  | singleton i => simp
  | cons a s ha hs ih => simp [hs, ih]

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