English
Composition of two families of linear equivalences is compatible with mapRange: the pointwise composition corresponds to composing the mapRange.linearEquiv maps.
Русский
Согласование композиции двух семейств линейных эквалентностей с mapRange: покомпонентная композиция соответствует композиции отображений mapRange.linearEquiv.
LaTeX
$$$\\mathrm{mapRange.linearEquiv}\\; (\\lambda i, f_i) \\;\\text{ and }\\; \\mathrm{mapRange.linearEquiv}\\; (\\lambda i, g_i) = \\mathrm{mapRange.linearEquiv}\\; (\\lambda i, f_i \\circ g_i)$$$
Lean4
theorem linearEquiv_trans (f : ∀ i, β i ≃ₗ[R] β₁ i) (f₂ : ∀ i, β₁ i ≃ₗ[R] β₂ i) :
(mapRange.linearEquiv fun i => (f i).trans (f₂ i)) = (mapRange.linearEquiv f).trans (mapRange.linearEquiv f₂) :=
LinearEquiv.ext <|
mapRange_comp (fun i x => f₂ i x) (fun i x => f i x) (fun i => (f₂ i).map_zero) (fun i => (f i).map_zero) (by simp)
