support_mapRange — Mathlib

English

MapRange distributes over the entries of a DFinsupp with respect to each index.

Русский

MapRange распределяется по записям DFinsupp по каждому индексу.

LaTeX

$$$\\mathrm{mapRange}\,f\,hf\,g = \\mathrm{mk}\\; g.{\\mathrm{support}}\\; (\\lambda i, f i.1 (g i.1))$$$

Lean4

theorem support_mapRange {f : ∀ i, β₁ i → β₂ i} {hf : ∀ i, f i 0 = 0} {g : Π₀ i, β₁ i} :
    (mapRange f hf g).support ⊆ g.support := by simp [mapRange_def]

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