comap_equiv_eq_map_symm — Mathlib

English

Let e be a linear equivalence M ≃ M₂. Then K.comap e = K.map e.symm.

Русский

Пусть e — линейное эквивалентное отображение M ≃ M₂. Тогда K.comap e = K.map e.symm.

LaTeX

$$$ K.comap e = K.map e.symm $$$

Lean4

theorem comap_equiv_eq_map_symm (e : M ≃ₛₗ[τ₁₂] M₂) (K : Submodule R₂ M₂) :
    K.comap (e : M →ₛₗ[τ₁₂] M₂) = K.map (e.symm : M₂ →ₛₗ[τ₂₁] M) :=
  (map_equiv_eq_comap_symm e.symm K).symm

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