English
Corollary: for any real normed space E, there exists a separating dual (a functional of norm 1 that separates vectors).
Русский
Следствие: для любого вещественного нормированного пространства E существует разделяющий дуал (функционал нормы 1, разделяющий векторы).
LaTeX
$$$\\text{SeparatingDual}_{\\mathbb{R}}\\; E$$$
Lean4
/-- Corollary of Hahn-Banach. Given a nonzero element `x` of a normed space, there exists an
element of the dual space, of norm `1`, whose value on `x` is `‖x‖`. -/
theorem exists_dual_vector (x : E) (h : x ≠ 0) : ∃ g : StrongDual 𝕜 E, ‖g‖ = 1 ∧ g x = ‖x‖ :=
by
let p : Submodule 𝕜 E := 𝕜 ∙ x
let f := (‖x‖ : 𝕜) • coord 𝕜 x h
obtain ⟨g, hg⟩ := exists_extension_norm_eq p f
refine ⟨g, ?_, ?_⟩
· rw [hg.2, coord_norm']
·
calc
g x = g (⟨x, mem_span_singleton_self x⟩ : 𝕜 ∙ x) := by rw [Submodule.coe_mk]
_ = ((‖x‖ : 𝕜) • coord 𝕜 x h) (⟨x, mem_span_singleton_self x⟩ : 𝕜 ∙ x) := by rw [← hg.1]
_ = ‖x‖ := by simp [-algebraMap_smul]
