addEquiv_trans — Mathlib

English

The mapRange.addEquiv respects composition of additive equivalences: (f.trans f₂) corresponds to the composition of mapRange.addEquiv f and mapRange.addEquiv f₂.

Русский

MapRange.addEquiv сохраняет композицию аддитивных эквивалентностей: эквивалентность для f.trans f₂ равна композиции addEquiv(f) и addEquiv(f₂).

LaTeX

$$mapRange.addEquiv (f.trans f₂) = (mapRange.addEquiv f).trans (mapRange.addEquiv f₂)$$

Lean4

theorem addEquiv_trans (f : M ≃+ N) (f₂ : N ≃+ P) :
    (mapRange.addEquiv (f.trans f₂) : (α →₀ M) ≃+ (α →₀ P)) = (mapRange.addEquiv f).trans (mapRange.addEquiv f₂) :=
  AddEquiv.ext (mapRange_comp _ f₂.map_zero _ f.map_zero (by simp))

Похожие утверждения