Theorems · Theorem · linear algebra

Submodule.iSup_dualAnnihilator_le_iInf

∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Sort u_3}
  (U : ι → Submodule R M), ⨆ i, (U i).dualAnnihilator ≤ (⨅ i, U i).dualAnnihilator

See also Subspace.dualAnnihilator_iInf_eq for vector subspaces when ι is finite.

Defined in

Mathlib.LinearAlgebra.Dual.Defs

Cited by

0 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringAddCommMonoidModule