exists_dual_vector'' — Mathlib

English

There exists g with ‖g‖ ≤ 1 and g x = ‖x‖ for all x, in particular the bound is tight for nonzero x.

Русский

Существует g с ≤ 1 и g x = ‖x‖ для всех x; для не нулевых x граница достигается.

LaTeX

$$$\\exists g : StrongDual 𝕜 E, \\|g\\| \\le 1 \\land g x = \\|x\\|$$$

Lean4

/-- Variant of Hahn-Banach, eliminating the hypothesis that `x` be nonzero, but only ensuring that
the dual element has norm at most `1` (this cannot be improved for the trivial
vector space). -/
theorem exists_dual_vector'' (x : E) : ∃ g : StrongDual 𝕜 E, ‖g‖ ≤ 1 ∧ g x = ‖x‖ :=
  by
  by_cases hx : x = 0
  · refine ⟨0, by simp, ?_⟩
    symm
    simp [hx]
  · rcases exists_dual_vector 𝕜 x hx with ⟨g, g_norm, g_eq⟩
    exact ⟨g, g_norm.le, g_eq⟩

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