English
Composition commutes with mapRange: mapping a composition f ∘ f2 along with hp and hf2 equals mapping f then mapRange f2 along with hf.
Русский
Композиция сохраняется при отображении через mapRange: применение mapRange к композиции f ∘ f2 эквивалентно последовательному применению mapRange к f и затем mapRange к f2.
LaTeX
$$$ \mathrm{DFinsupp.mapRange} (\lambda i. f i \circ f_2 i)\, h\, g = \mathrm{DFinsupp.mapRange} (f)\, hf\, (\mathrm{DFinsupp.mapRange} (f_2)\, hf_2\, g) $$$
Lean4
theorem mapRange_comp (f : ∀ i, β₁ i → β₂ i) (f₂ : ∀ i, β i → β₁ i) (hf : ∀ i, f i 0 = 0) (hf₂ : ∀ i, f₂ i 0 = 0)
(h : ∀ i, (f i ∘ f₂ i) 0 = 0) (g : Π₀ i : ι, β i) :
mapRange (fun i => f i ∘ f₂ i) h g = mapRange f hf (mapRange f₂ hf₂ g) :=
by
ext
simp only [mapRange_apply]; rfl
