def HahnBanach.IsHamelBasis (K : Type u_3) {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] (H : Set V) : Prop

A Hamel basis of a vector space $V$ over a field $K$ is a subset $H \subseteq V$ that is linearly independent and whose $K$-linear span is all of $V$. Equivalently, every element of $V$ can be written uniquely as a finite $K$-linear combination of elements of $H$.

theorem HahnBanach.zorns_lemma {α : Type u_3} [Preorder α] (h : ∀ (c : Set α), IsChain (fun (x1 x2 : α) => x1 ≤ x2) c → BddAbove c) : ∃ (m : α), IsMax m

Zorn's lemma. If every chain in a nonempty partially ordered set $\alpha$ has an upper bound, then $\alpha$ contains a maximal element.

theorem HahnBanach.hahn_banach_theorem {𝕜 : Type u_3} [RCLike 𝕜] {V : Type u_4} [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] (M : Subspace 𝕜 V) (f : ↥M →L[𝕜] 𝕜) : ∃ (F : V →L[𝕜] 𝕜), (∀ (m : ↥M), F ↑m = f m) ∧ ‖F‖ = ‖f‖

Hahn-Banach theorem. Let $V$ be a normed vector space and $M \subseteq V$ a subspace. Any bounded linear functional $f : M \to \mathbb{K}$ extends to a bounded linear functional $F : V \to \mathbb{K}$ with the same operator norm, $\|F\| = \|f\|$.

theorem HahnBanach.exists_norm_one_functional_achieving_norm {𝕜 : Type u_3} [RCLike 𝕜] {V : Type u_4} [NormedAddCommGroup V] [NormedSpace 𝕜 V] (v : V) (hv : v ≠ 0) : ∃ (f : V →L[𝕜] 𝕜), ‖f‖ = 1 ∧ f v = ↑‖v‖

For any nonzero vector $v$ in a normed space $V$, there exists a bounded linear functional $f \in V'$ with $\|f\| = 1$ and $f(v) = \|v\|$.

theorem HahnBanach.hahn_banach_one_step_extension_bound {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (M : Subspace 𝕜 E) (f : ↥M →L[𝕜] 𝕜) (C : ℝ) (hC : 0 ≤ C) (hf_bound : ∀ (m : ↥M), ‖f m‖ ≤ C * ‖↑m‖) (x₀ : E) (hx₀ : x₀ ∉ M) : ∃ (g : ↥(M ⊔ 𝕜 ∙ x₀) →L[𝕜] 𝕜), (∀ (m : ↥M), g ⟨↑m, ⋯⟩ = f m) ∧ (∀ (v : ↥(M ⊔ 𝕜 ∙ x₀)), ‖g v‖ ≤ C * ‖↑v‖) ∧ M < M ⊔ 𝕜 ∙ x₀

One-step Hahn-Banach extension. Let $V$ be a normed space, $M \subseteq V$ a subspace, and $f : M \to \mathbb{K}$ a bounded linear functional with $\|f(m)\| \le C \|m\|$ for all $m \in M$. If $x_0 \notin M$, then there exists a bounded linear functional $g$ on the strictly larger subspace $M'' = M + \mathbb{K} \cdot x_0$ extending $f$ and satisfying the same bound $\|g(v)\| \le C \|v\|$ for all $v \in M''$.