English
The mapRange equivalence respects composition: mapRange.equiv (f.trans f₂) with appropriate proofs equals the composition of mapRange.equiv f and mapRange.equiv f₂.
Русский
Отображение mapRange эквивалентно композиции: эквивалентность для f.trans f₂ равна композиции mapRange эквивалентностей для f и для f₂.
LaTeX
$$Eq (mapRange.equiv (f.trans f₂) _ _ ) ((mapRange.equiv f hf hf').trans (mapRange.equiv f₂ hf₂ hf₂'))$$
Lean4
theorem equiv_trans (f : M ≃ N) (hf : f 0 = 0) (hf') (f₂ : N ≃ P) (hf₂ : f₂ 0 = 0) (hf₂') :
(mapRange.equiv (f.trans f₂) (by rw [Equiv.trans_apply, hf, hf₂]) (by rw [Equiv.symm_trans_apply, hf₂', hf']) :
(α →₀ _) ≃ _) =
(mapRange.equiv f hf hf').trans (mapRange.equiv f₂ hf₂ hf₂') :=
Equiv.ext <| mapRange_comp f₂ hf₂ f hf ((congrArg f₂ hf).trans hf₂)
