map_dualCoannihilator_le — Mathlib

English

For Φ ⊆ M^*, the image of Φ.dualCoannihilator under Dual.eval is bounded above by Φ.dualAnnihilator.

Русский

Для Φ ⊆ M^*, образ Φ.dualCoannihilator под Dual.eval ограничен сверху Φ.dualAnnihilator.

LaTeX

$$Φ.dualCoannihilator.map (Module.Dual.eval R M) ≤ Φ.dualAnnihilator.$$

Lean4

theorem map_dualCoannihilator_le (Φ : Submodule R (Module.Dual R M)) :
    Φ.dualCoannihilator.map (Module.Dual.eval R M) ≤ Φ.dualAnnihilator :=
  map_le_iff_le_comap.mpr (comap_dualAnnihilator Φ).le

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