English
Variant of Hahn-Banach removing nonzero requirement and choosing dual arbitrarily when x = 0.
Русский
Вариант Хана-Банаха без требования x ≠ 0 и произвольный выбор дуального элемента в случае x = 0.
LaTeX
$$$\\exists g : StrongDual 𝕜 E, \\|g\\| = 1 \\land g x = \\|x\\|$ для всех x, включая x = 0$$
Lean4
/-- Variant of Hahn-Banach, eliminating the hypothesis that `x` be nonzero, and choosing
the dual element arbitrarily when `x = 0`. -/
theorem exists_dual_vector' [Nontrivial E] (x : E) : ∃ g : StrongDual 𝕜 E, ‖g‖ = 1 ∧ g x = ‖x‖ :=
by
by_cases hx : x = 0
· obtain ⟨y, hy⟩ := exists_ne (0 : E)
obtain ⟨g, hg⟩ : ∃ g : StrongDual 𝕜 E, ‖g‖ = 1 ∧ g y = ‖y‖ := exists_dual_vector 𝕜 y hy
refine ⟨g, hg.left, ?_⟩
simp [hx]
· exact exists_dual_vector 𝕜 x hx
