English
In a finite direct sum indexed by a finite set s, the value at a point n inside s is exactly the component f at n; i.e., the canonical projection to the n-th coordinate picks out the corresponding entry.
Русский
В конечной прямой сумме, индексируемой по конечному множеству s, значение в точке n внутри s равно компоненте на n; то есть проекция на n-ю координату выбирает соответствующий член.
LaTeX
$$$ mk\, \beta\, s\, f\, n = f \langle n, \text{hn} \rangle \quad (\text{для } \text{hn} : n \in s). $$$
Lean4
theorem mk_apply_of_mem {s : Finset ι} {f : ∀ i : (↑s : Set ι), β i.val} {n : ι} (hn : n ∈ s) :
mk β s f n = f ⟨n, hn⟩ :=
by
dsimp only [Finset.coe_sort_coe, mk, AddMonoidHom.coe_mk, ZeroHom.coe_mk, DFinsupp.mk_apply]
rw [dif_pos hn]
