eq_zero_iff_forall_dual_eq_zero — Mathlib

English

As in previous variants, x = 0 iff all duals annihilate x.

Русский

Как и в предыдущих версиях, x = 0 тогда и только тогда, когда все двойственные уничтожают x.

LaTeX

$$$x=0 \\iff ∀ f:\\StrongDual 𝕜 E, f(x)=0$$$

Lean4

theorem eq_zero_iff_forall_dual_eq_zero (x : E) : x = 0 ↔ ∀ g : StrongDual 𝕜 E, g x = 0 :=
  ⟨fun hx => by simp [hx], fun h => eq_zero_of_forall_dual_eq_zero 𝕜 h⟩

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