mem_invtSubmodule_symm_iff_le_map

English

If f is a linear equivalence, then p ∈ invtSubmodule f.symm iff p ≤ p.map f.

Русский

Если f — линейное эквивалентное отображение, тогда p ∈ invtSubmodule f.symm эквивалентно p ≤ p.map f.

LaTeX

$$mem_invtSubmodule_symm_iff_le_map: p ∈ invtSubmodule f.symm ↔ p ≤ p.map f$$

Lean4

/-- `p` is `f.symm` invariant if and only if `p ≤ p.map f`. -/
theorem mem_invtSubmodule_symm_iff_le_map {f : M ≃ₗ[R] M} {p : Submodule R M} :
    p ∈ invtSubmodule f.symm ↔ p ≤ p.map f :=
  (mem_invtSubmodule_iff_map_le _).trans (f.toEquiv.symm.subset_symm_image _ _).symm

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