English
For submodules U,V of M, the sum of their dual annihilators is contained in the dual annihilator of their intersection: U.dualAnnihilator ⊔ V.dualAnnihilator ≤ (U ∩ V).dualAnnihilator.
Русский
Для подмножеств U,V модулей M сумма их двойных аннигиляторов содержится в двойном аннигиляторе пересечения: U.dualAnnihilator ⊔ V.dualAnnihilator ≤ (U ∩ V).dualAnnihilator.
LaTeX
$$$ U.dualAnnihilator \\sqcup V.dualAnnihilator \\le (U \\cap V).dualAnnihilator $$$
Lean4
/-- See also `Subspace.dualAnnihilator_inf_eq` for vector subspaces. -/
theorem sup_dualAnnihilator_le_inf (U V : Submodule R M) :
U.dualAnnihilator ⊔ V.dualAnnihilator ≤ (U ⊓ V).dualAnnihilator :=
by
rw [le_dualAnnihilator_iff_le_dualCoannihilator, dualCoannihilator_sup_eq]
apply inf_le_inf <;> exact le_dualAnnihilator_dualCoannihilator _
