English
For a nonempty finite set s of indices Y and a family f: Y → PseudoMetric X R, the pointwise coe of the finite supremum equals the finite supremum of the coe of f across indices.
Русский
Для непустого конечного множества индексов s и семейства f: Y → PseudoMetric X R, равенство предела по точке выполняется: верхняя грань по s равна по точке верхней грани по каждому индексу.
LaTeX
$$$\bigl( s. sup\; f \bigr) = s. sup'\; hs\; (f \cdot) \;\text{in pointwise coe}.$$$
Lean4
@[simp, push_cast]
theorem coe_finsetSup [IsOrderedAddMonoid R] {Y : Type*} {f : Y → PseudoMetric X R} {s : Finset Y} (hs : s.Nonempty) :
⇑(s.sup f) = s.sup' hs (f ·) := by
induction hs using Finset.Nonempty.cons_induction with
| singleton i => simp
| cons a s ha hs ih => simp [hs, ih]
