map_symm_eq_iff — Mathlib

English

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

Русский

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

LaTeX

$$$ K.map e.symm = p \\iff p.map e = K $$$

Lean4

theorem map_symm_eq_iff (e : M ≃ₛₗ[τ₁₂] M₂) {K : Submodule R₂ M₂} : K.map e.symm = p ↔ p.map e = K :=
  by
  constructor <;> rintro rfl
  ·
    calc
      map e (map e.symm K) = comap e.symm (map e.symm K) := map_equiv_eq_comap_symm _ _
      _ = K := comap_map_eq_of_injective e.symm.injective _
  ·
    calc
      map e.symm (map e p) = comap e (map e p) := (comap_equiv_eq_map_symm _ _).symm
      _ = p := comap_map_eq_of_injective e.injective _

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