English
If f is a linear equivalence and f2 is another linear equivalence, then the linear equivalence induced by the composition f.trans f2 equals the composition of the induced linear equivalences.
Русский
Если f — линейное эквивалентное отображение и f2 — другое линейное эквивалентное отображение, то линейное эквивалентное отображение, получаемое от композиции f.trans f2, равно композиции полученных линейных эквивалентов.
LaTeX
$$$$ mapRange.linearEquiv(f.trans f_2) = (mapRange.linearEquiv f).trans (mapRange.linearEquiv f_2). $$$$
Lean4
theorem linearEquiv_trans (f : M ≃ₛₗ[σ₁₂] N) (f₂ : N ≃ₛₗ[σ₂₃] P) :
(mapRange.linearEquiv (f.trans f₂) : (α →₀ _) ≃ₛₗ[σ₁₃] _) =
(mapRange.linearEquiv f).trans (mapRange.linearEquiv f₂) :=
LinearEquiv.ext <| mapRange_comp f₂ f₂.map_zero f f.map_zero (f.trans f₂).map_zero
