English
From a finite set s and a family x defined on s, one builds a finitely supported function mk s x in which the i-th coordinate is x(i) if i ∈ s, and 0 otherwise.
Русский
Из конечного множества s и семейства x, определенного на s, строится конечно-поддерживаемая функция mk s x, у которой i-й компонент равен x(i) при i ∈ s, и 0 иначе.
LaTeX
$$$(\mathrm{mk}\ s\ x)_i = \begin{cases} x(i), & i \in s \\ 0, & i \notin s \end{cases}$$$
Lean4
/-- Create an element of `Π₀ i, β i` from a finset `s` and a function `x`
defined on this `Finset`. -/
def mk (s : Finset ι) (x : ∀ i : (↑s : Set ι), β (i : ι)) : Π₀ i, β i :=
⟨fun i => if H : i ∈ s then x ⟨i, H⟩ else 0,
Trunc.mk ⟨s.1, fun i => if H : i ∈ s then Or.inl H else Or.inr <| dif_neg H⟩⟩
