orderIsoMapComap_apply' — Mathlib

English

For a linear equivalence e, the order isomorphism between submodules satisfies orderIsoMapComap e p = comap e.symm p.

Русский

Для линейного эквивалентного отображения e отображение между подмодулями сохраняется: orderIsoMapComap e p = comap e.symm p.

LaTeX

$$$ orderIsoMapComap e p = comap e.symm p $$$

Lean4

theorem orderIsoMapComap_apply' (e : M ≃ₛₗ[τ₁₂] M₂) (p : Submodule R M) : orderIsoMapComap e p = comap e.symm p :=
  p.map_equiv_eq_comap_symm _

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