coe_dualCoannihilator_span — Mathlib

English

For a set s of functionals on M, the dual coannihilator of span s is the set of x in M such that all f in s satisfy f(x)=0.

Русский

Для множества функционалов s: span_R s дуальный коаннигиллятор состоит из элементов x ∈ M, для которых все f ∈ s удовлетворяют f(x)=0.

LaTeX

$$$ (\\mathrm{span}_R s).dualCoannihilator = \\{ x \\in M \\mid \\forall f \\in s, f(x) = 0 \\} $$$

Lean4

@[simp]
theorem coe_dualCoannihilator_span (s : Set (Module.Dual R M)) :
    ((span R s).dualCoannihilator : Set M) = {x | ∀ f ∈ s, f x = 0} :=
  by
  ext x
  have (φ : _) : x ∈ LinearMap.ker φ ↔ φ ∈ LinearMap.ker (Module.Dual.eval R M x) := by simp
  simp only [SetLike.mem_coe, mem_dualCoannihilator, Set.mem_setOf_eq, ← LinearMap.mem_ker, this]
  exact span_le

Похожие утверждения