English
The same equivalence as above: x = 0 iff all duals send x to 0.
Русский
То же соотношение: x = 0 тогда и только тогда, когда все двойственные отображают x в 0.
LaTeX
$$$x=0 \\iff \\forall g:\\StrongDual 𝕜 E, g(x)=0$$$
Lean4
/-- If one controls the norm of every `f x`, then one controls the norm of `x`.
Compare `ContinuousLinearMap.opNorm_le_bound`. -/
theorem norm_le_dual_bound (x : E) {M : ℝ} (hMp : 0 ≤ M) (hM : ∀ f : StrongDual 𝕜 E, ‖f x‖ ≤ M * ‖f‖) : ‖x‖ ≤ M := by
classical
by_cases h : x = 0
· simp only [h, hMp, norm_zero]
· obtain ⟨f, hf₁, hfx⟩ : ∃ f : StrongDual 𝕜 E, ‖f‖ = 1 ∧ f x = ‖x‖ := exists_dual_vector 𝕜 x h
calc
‖x‖ = ‖(‖x‖ : 𝕜)‖ := RCLike.norm_coe_norm.symm
_ = ‖f x‖ := by rw [hfx]
_ ≤ M * ‖f‖ := (hM f)
_ = M := by rw [hf₁, mul_one]
