Theorems · Theorem · functional analysis
exists_dual_vector
∀ (𝕜 : Type v) [inst : RCLike 𝕜] {E : Type u} [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] (x : E),
‖x‖ ≠ 0 → ∃ g, ‖g‖ = 1 ∧ g x = ↑‖x‖Corollary of Hahn-Banach. Given an element x of a normed space with ‖x‖ ≠ 0, there
exists an element of the dual space, of norm 1, whose value on x is ‖x‖.
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 173 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites40
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Realstatement and proof · cited by 25,697
- RingHom.idstatement and proof · cited by 18,349
- NormedSpacestatement and proof · cited by 12,499
- Norm.normstatement and proof · cited by 5,413
- ContinuousLinearMapproof · cited by 5,352
- mul_oneproof · cited by 3,885
- RCLikestatement and proof · cited by 2,829
- SeminormedAddCommGroupstatement and proof · cited by 2,671
- le_antisymmproof · cited by 2,068
- le_reflproof · cited by 2,061
- Submodule.spanproof · cited by 1,504
Cited by3
Results whose statement or proof uses this declaration.
- exists_dual_vector''proof · cited by 3
- Complex.dist_le_mul_div_pow_of_mapsTo_ball_of_isLittleOproof · cited by 1
- exists_dual_vector'proof · cited by 0