mem_invtSubmodule_iff_map_le — Mathlib

English

A symmetry version: for a linear equivalence e, p ∈ f.invtSubmodule.symm iff p ≤ p.map f.

Русский

Симметрическая версия: для эвалюируемости p ∈ f.symm.invtSubmodule тогда и только тогда, когда p ≤ p.map f.

LaTeX

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

Lean4

/-- `p` is `f` invariant if and only if `p.map f ≤ p`. -/
theorem mem_invtSubmodule_iff_map_le {p : Submodule R M} : p ∈ f.invtSubmodule ↔ p.map f ≤ p :=
  Submodule.map_le_iff_le_comap.symm

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