eq_iff_forall_dual_eq — Mathlib

English

Equality of vectors is characterized by equality of their images under all dual functionals.

Русский

Равенство векторов характеризуется равенством их образов под всеми двойственными функционалами.

LaTeX

$$$x=y \\iff \\forall g:\\StrongDual 𝕜 E, g(x)=g(y)$$$

Lean4

/-- See also `geometric_hahn_banach_point_point`. -/
theorem eq_iff_forall_dual_eq {x y : E} : x = y ↔ ∀ g : StrongDual 𝕜 E, g x = g y :=
  by
  rw [← sub_eq_zero, eq_zero_iff_forall_dual_eq_zero 𝕜 (x - y)]
  simp [sub_eq_zero]

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