English
For a family U(i) of submodules, the supremum of their dual annihilators is bounded above by the infimum of their dual annihilators: ⨆ i (U(i)).dualAnnihilator ≤ ⨅ i (U(i)).dualAnnihilator.
Русский
Для семейства U(i) верно неравенство: ⨆ i (U(i)).dualAnnihilator ≤ ⨅ i (U(i)).dualAnnihilator.
LaTeX
$$$ \\big(\\big\\vee_{i} (U(i)).dualAnnihilator \\big) \\le \\big(\\bigwedge_{i} (U(i)).dualAnnihilator \\big) $$$
Lean4
/-- See also `Subspace.dualAnnihilator_iInf_eq` for vector subspaces when `ι` is finite. -/
theorem iSup_dualAnnihilator_le_iInf {ι : Sort*} (U : ι → Submodule R M) :
⨆ i : ι, (U i).dualAnnihilator ≤ (⨅ i : ι, U i).dualAnnihilator :=
by
rw [le_dualAnnihilator_iff_le_dualCoannihilator, dualCoannihilator_iSup_eq]
apply iInf_mono
exact fun i : ι => le_dualAnnihilator_dualCoannihilator (U i)
