English
Corollary of Hahn-Banach: for any 𝕜 with IsRCLikeNormedField and a subspace p of E, every continuous linear map from p to F with finite-dim range extends to E without norm bounds specified.
Русский
Следствие Хана-Банаха для обобщённых полей: если 𝕜 удовлетворяет условиям, то любой непрерывный линейный отображение из подпространства p в F с конечномерным образом расширяется на всё пространство E без ограничений на норму.
LaTeX
$$$\\exists g : E \\toL[𝕜] F, \\; g|_p = f$ (при условии конечномерности диапазона и аналогичных предпосылок)$$
Lean4
/-- **Hahn-Banach theorem** for continuous linear functions over `ℝ`.
See also `exists_extension_norm_eq` in the root namespace for a more general version
that works both for `ℝ` and `ℂ`. -/
theorem exists_extension_norm_eq (p : Subspace ℝ E) (f : StrongDual ℝ p) :
∃ g : StrongDual ℝ E, (∀ x : p, g x = f x) ∧ ‖g‖ = ‖f‖ :=
by
rcases
exists_extension_of_le_sublinear ⟨p, f⟩ (fun x => ‖f‖ * ‖x‖)
(fun c hc x => by simp only [norm_smul c x, Real.norm_eq_abs, abs_of_pos hc, mul_left_comm])
(fun x y => by
rw [← left_distrib]
exact mul_le_mul_of_nonneg_left (norm_add_le x y) (@norm_nonneg _ _ f))
fun x => le_trans (le_abs_self _) (f.le_opNorm _) with
⟨g, g_eq, g_le⟩
set g' := g.mkContinuous ‖f‖ fun x => abs_le.2 ⟨neg_le.1 <| g.map_neg x ▸ norm_neg x ▸ g_le (-x), g_le x⟩
refine ⟨g', g_eq, ?_⟩
apply le_antisymm (g.mkContinuous_norm_le (norm_nonneg f) _)
refine f.opNorm_le_bound (norm_nonneg _) fun x => ?_
dsimp at g_eq
rw [← g_eq]
apply g'.le_opNorm
