R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
ι : Type u_1
U : ι → Submodule R M
⊢ (⨅ (i : ι), U i) ≤ ⨅ (i : ι), dualCoannihilator (dualAnnihilator (U i))
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
ι : Type u_1
U : ι → Submodule R M
⊢ (⨆ (i : ι), dualAnnihilator (U i)) ≤ dualAnnihilator (⨅ (i : ι), U i)
rw [le_dualAnnihilator_iff_le_dualCoannihilator, dualCoannihilator_iSup_eq]
case h
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
ι : Type u_1
U : ι → Submodule R M
⊢ ∀ (i : ι), U i ≤ dualCoannihilator (dualAnnihilator (U i))
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
ι : Type u_1
U : ι → Submodule R M
⊢ (⨅ (i : ι), U i) ≤ ⨅ (i : ι), dualCoannihilator (dualAnnihilator (U i))
apply iInf_mono
no goals
case h
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
ι : Type u_1
U : ι → Submodule R M
⊢ ∀ (i : ι), U i ≤ dualCoannihilator (dualAnnihilator (U i))
exact fun i : ι => le_dualAnnihilator_dualCoannihilator (U i)