forall_dual_apply_eq_zero_iff — Mathlib

English

For every vector v in V, the condition that all dual functionals vanish on v is equivalent to v = 0.

Русский

Для каждого вектора v ∈ V верно, что все функционалы из двойственного пространства равны нулю на v тогда и только тогда, когда v = 0.

LaTeX

$$$\\forall v\\in V,\\; (\\forall \\varphi\\in V^*,\\; \\varphi(v)=0) \\iff v=0$$$

Lean4

theorem forall_dual_apply_eq_zero_iff (v : V) : (∀ φ : Module.Dual K V, φ v = 0) ↔ v = 0 :=
  by
  rw [← eval_apply_eq_zero_iff K v, LinearMap.ext_iff]
  simp only [eval_apply, zero_apply]

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