R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W U V : Submodule R M
⊢ U ⊓ V ≤ dualCoannihilator (dualAnnihilator U) ⊓ dualCoannihilator (dualAnnihilator V)
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W U V : Submodule R M
⊢ dualAnnihilator U ⊔ dualAnnihilator V ≤ dualAnnihilator (U ⊓ V)
rw [le_dualAnnihilator_iff_le_dualCoannihilator, dualCoannihilator_sup_eq]
no goals
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W U V : Submodule R M
⊢ U ⊓ V ≤ dualCoannihilator (dualAnnihilator U) ⊓ dualCoannihilator (dualAnnihilator V)
apply inf_le_inf <;> exact le_dualAnnihilator_dualCoannihilator _