mem_dualCoannihilator — Mathlib

English

For Φ a submodule of M^*, and x ∈ M, x ∈ Φ.dualCoannihilator iff ∀ φ ∈ Φ, φ(x) = 0.

Русский

Для Φ ⊆ M^*, и x ∈ M, x ∈ Φ.dualCoannihilator тогда и только тогда, когда для всех φ ∈ Φ выполняется φ(x)=0.

LaTeX

$$x ∈ Φ.dualCoannihilator ↔ ∀ φ ∈ Φ, (φ x) = 0.$$

Lean4

@[simp]
theorem mem_dualCoannihilator {Φ : Submodule R (Module.Dual R M)} (x : M) :
    x ∈ Φ.dualCoannihilator ↔ ∀ φ ∈ Φ, (φ x : R) = 0 := by
  simp_rw [dualCoannihilator, mem_comap, mem_dualAnnihilator, Module.Dual.eval_apply]

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