English
For a family of maps f_i and a DFinsupp g, mapRange f hf g equals the DFinsupp with the same support as g and coordinates given by f i (g i).
Русский
Для семейства отображений f_i и DFinsupp g функция mapRange f hf g равна DFinsupp с тем же опорным множеством и координатами f i (g i).
LaTeX
$$$\\mathrm{mapRange}\,f\,hf\,g = \\mathrm{mk}\\; g.{\\mathrm{support}}\\; (\\lambda i, f i.1 (g i.1))$$$
Lean4
theorem mapRange_def [∀ (i) (x : β₁ i), Decidable (x ≠ 0)] {f : ∀ i, β₁ i → β₂ i} {hf : ∀ i, f i 0 = 0}
{g : Π₀ i, β₁ i} : mapRange f hf g = mk g.support fun i => f i.1 (g i.1) :=
by
ext i
by_cases h : g i ≠ 0 <;> simp at h <;> simp [h, hf]