addEquiv_toEquiv — Mathlib

English

The underlying map of mapRange.addEquiv f is the same as mapRange.equiv for the corresponding equivalence f.

Русский

Умолчательное отображение mapRange.addEquiv f совпадает с mapRange.equiv для соответствующей эквивалентности f.

LaTeX

$$↑(mapRange.addEquiv f) = (mapRange.equiv (EquivLike.toEquiv f) f.map_zero f.symm.map_zero : (\\alpha \\to_0 _) \\simeq _)$$

Lean4

@[simp]
theorem addEquiv_toEquiv (f : M ≃+ N) :
    ↑(mapRange.addEquiv f : (α →₀ _) ≃+ _) = (mapRange.equiv (f : M ≃ N) f.map_zero f.symm.map_zero : (α →₀ _) ≃ _) :=
  Equiv.ext fun _ => rfl

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