mapRange_def — Mathlib

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]

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