feat(analysis/normed_space/dual): add eq_zero_of_forall_dual_eq_zero (#…

…7929)

The variable `𝕜` is made explicit in `norm_le_dual_bound` because lean can otherwise not guess it in the proof of `eq_zero_of_forall_dual_eq_zero`.

src/analysis/normed_space/dual.lean

@@ -93,8 +93,8 @@ end general
 
 section bidual_isometry
 
-variables {𝕜 : Type v} [is_R_or_C 𝕜]
-{E : Type u} [normed_group E] [normed_space 𝕜 E]
+variables (𝕜 : Type v) [is_R_or_C 𝕜]
+  {E : Type u} [normed_group E] [normed_space 𝕜 E]
 
 /-- If one controls the norm of every `f x`, then one controls the norm of `x`.
     Compare `continuous_linear_map.op_norm_le_bound`. -/
@@ -111,6 +111,9 @@ begin
     ... = M : by rw [hf.1, mul_one] }
 end
 
+lemma eq_zero_of_forall_dual_eq_zero {x : E} (h : ∀ f : dual 𝕜 E, f x = (0 : 𝕜)) : x = 0 :=
+norm_eq_zero.mp (le_antisymm (norm_le_dual_bound 𝕜 x le_rfl (λ f, by simp [h f])) (norm_nonneg _))
+
 /-- The inclusion of a normed space in its double dual is an isometry onto its image.-/
 lemma inclusion_in_double_dual_isometry (x : E) : ∥inclusion_in_double_dual 𝕜 E x∥ = ∥x∥ :=
 begin
@@ -119,7 +122,7 @@ begin
   { rw continuous_linear_map.norm_def,
     apply real.lb_le_Inf _ continuous_linear_map.bounds_nonempty,
     rintros c ⟨hc1, hc2⟩,
-    exact norm_le_dual_bound x hc1 hc2 },
+    exact norm_le_dual_bound 𝕜 x hc1 hc2 },
 end
 
 end bidual_isometry