English
AddEquiv Transitivity compatibility: (mapRange.addEquiv f).trans (mapRange.addEquiv f2) equals mapRange.addEquiv (f.trans f2).
Русский
Совместимость с переходами: (mapRange.addEquiv f).trans (mapRange.addEquiv f2) = mapRange.addEquiv (f.trans f2).
LaTeX
$$$(\\mathrm{mapRange}.\\mathrm{addEquiv}\\; f).\\mathrm{trans} (\\mathrm{mapRange}.\\mathrm{addEquiv}\\; f_2) = \\mathrm{mapRange}.\\mathrm{addEquiv}\\; (f \\mathrm{.trans} f_2)$$$
Lean4
theorem addEquiv_trans (f : ∀ i, β i ≃+ β₁ i) (f₂ : ∀ i, β₁ i ≃+ β₂ i) :
(mapRange.addEquiv fun i => (f i).trans (f₂ i)) = (mapRange.addEquiv f).trans (mapRange.addEquiv f₂) :=
by
refine AddEquiv.ext <| mapRange_comp (fun i x => f₂ i x) (fun i x => f i x) ?_ ?_ ?_
· intros; apply map_zero
· intros; apply map_zero
· intros; dsimp; simp only [map_zero]
