mem_map_equiv — Mathlib

English

Let e be a linear equivalence M ≃ M₂. Then K.map e.symm = p if and only if 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

@[simp high]
theorem mem_map_equiv {e : M ≃ₛₗ[τ₁₂] M₂} {x : M₂} : x ∈ p.map (e : M →ₛₗ[τ₁₂] M₂) ↔ e.symm x ∈ p :=
  by
  rw [Submodule.mem_map]; constructor
  · rintro ⟨y, hy, hx⟩
    simp [← hx, hy]
  · intro hx
    exact ⟨e.symm x, hx, by simp⟩

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