compatibility with #3054

src/analysis/normed_space/dual.lean

@@ -32,8 +32,8 @@ instance : inhabited (dual 𝕜 E) := ⟨0⟩
 def inclusion_in_double_dual' (x : E) : (dual 𝕜 (dual 𝕜 E)) :=
 linear_map.mk_continuous
   { to_fun := λ f, f x,
-    add    := by simp,
-    smul   := by simp }
+    map_add'    := by simp,
+    map_smul'   := by simp }
   ∥x∥
   (λ f, by { rw mul_comm, exact f.le_op_norm x } )
 
@@ -52,8 +52,8 @@ end
 def inclusion_in_double_dual : E →L[𝕜] (dual 𝕜 (dual 𝕜 E)) :=
 linear_map.mk_continuous
   { to_fun := λ (x : E), (inclusion_in_double_dual' 𝕜 E) x,
-    add    := λ x y, by { ext, simp },
-    smul   := λ (c : 𝕜) x, by { ext, simp } }
+    map_add'    := λ x y, by { ext, simp },
+    map_smul'   := λ (c : 𝕜) x, by { ext, simp } }
   1
   (λ x, by { convert double_dual_bound _ _ _, simp } )
 
@@ -63,18 +63,21 @@ section real
 variables (E : Type*) [normed_group E] [normed_space ℝ E]
 
 /-- The inclusion of a real normed space in its double dual is an isometry onto its image.-/
-lemma inclusion_in_double_dual_isometry (x : E) (h : vector_space.dim ℝ E > 0) :
+lemma inclusion_in_double_dual_isometry (x : E) :
   ∥inclusion_in_double_dual ℝ E x∥ = ∥x∥ :=
 begin
-  refine le_antisymm_iff.mpr ⟨double_dual_bound ℝ E x, _⟩,
-  rw continuous_linear_map.norm_def,
-  apply real.lb_le_Inf _ continuous_linear_map.bounds_nonempty,
-  intros c, simp only [and_imp, set.mem_set_of_eq], intros h₁ h₂,
-  cases exists_dual_vector' h x with f hf,
-  calc ∥x∥ = f x : hf.2.symm
-  ... ≤ ∥f x∥ : le_max_left (f x) (-f x)
-  ... ≤ c * ∥f∥ : h₂ f
-  ... = c : by rw [ hf.1, mul_one ],
+  by_cases h : vector_space.dim ℝ E = 0,
+  { rw dim_zero_iff_forall_zero.mp h x, simp },
+  { have h' : 0 < vector_space.dim ℝ E := zero_lt_iff_ne_zero.mpr h,
+    refine le_antisymm_iff.mpr ⟨double_dual_bound ℝ E x, _⟩,
+    rw continuous_linear_map.norm_def,
+    apply real.lb_le_Inf _ continuous_linear_map.bounds_nonempty,
+    intros c, simp only [and_imp, set.mem_set_of_eq], intros h₁ h₂,
+    cases exists_dual_vector' h' x with f hf,
+    calc ∥x∥ = f x : hf.2.symm
+    ... ≤ ∥f x∥ : le_max_left (f x) (-f x)
+    ... ≤ c * ∥f∥ : h₂ f
+    ... = c : by rw [ hf.1, mul_one ] }
 end
 
 -- TODO: This is also true over ℂ.

src/analysis/normed_space/hahn_banach.lean

@@ -63,25 +63,23 @@ by rw [norm_smul, norm_norm, coord_norm, mul_inv_cancel (mt norm_eq_zero.mp h)]
 
 /-- Corollary of Hahn-Banach.  Given a nonzero element `x` of a normed space, there exists an
     element of the dual space, of norm 1, whose value on `x` is `∥x∥`. -/
-theorem exists_dual_vector (x : E) (h : x ≠ 0) : ∃ d : E →L[ℝ] ℝ, ∥d∥ = 1 ∧ d x = ∥x∥ :=
+theorem exists_dual_vector (x : E) (h : x ≠ 0) : ∃ g : E →L[ℝ] ℝ, ∥g∥ = 1 ∧ g x = ∥x∥ :=
 begin
-  cases exists_extension_norm_eq (submodule.span ℝ {x}) (coord ℝ x h) with g hg,
-  use ∥x∥ • g, split,
-  { rw ← (coord_norm' x h), rw norm_smul, rw norm_smul, rw ← hg.2 },
-  { calc (∥x∥ • g) x = ∥x∥ • (g x) : rfl
-    ... = ∥x∥ • coord ℝ x h (⟨x, submodule.mem_span_singleton_self x⟩ : submodule.span ℝ {x}) : _
-    ... = (∥x∥ • coord ℝ x h) ⟨x, submodule.mem_span_singleton_self x⟩ : rfl
-    ... = ∥x∥ : by rw coord_self',
-    rw ← hg.1, simp }
+  cases exists_extension_norm_eq (submodule.span ℝ {x}) (∥x∥ • coord ℝ x h) with g hg,
+  use g, split,
+  { rw [hg.2, coord_norm'] },
+  { calc g x = g (⟨x, submodule.mem_span_singleton_self x⟩ : submodule.span ℝ {x}) : by simp
+  ... = (∥x∥ • coord ℝ x h) (⟨x, submodule.mem_span_singleton_self x⟩ : submodule.span ℝ {x}) : by rw ← hg.1
+  ... = ∥x∥ : by rw coord_self' }
 end
 
 /-- Variant of the above theorem, eliminating the hypothesis that `x` be nonzero, and choosing
     the dual element arbitrarily when `x = 0`. -/
-theorem exists_dual_vector' (h : vector_space.dim ℝ E > 0) (x : E) : ∃ g : E →L[ℝ] ℝ,
+theorem exists_dual_vector' (h : 0 < vector_space.dim ℝ E) (x : E) : ∃ g : E →L[ℝ] ℝ,
   ∥g∥ = 1 ∧ g x = ∥x∥ :=
 begin
   by_cases hx : x = 0,
-  { cases exists_mem_ne_zero_of_dim_pos' h with y hy,
+  { cases dim_pos_iff_exists_ne_zero.mp h with y hy,
     cases exists_dual_vector y hy with g hg,
     use g, refine ⟨hg.left, _⟩, simp [hx] },
   { exact exists_dual_vector x hx }

src/analysis/normed_space/operator_norm.lean

@@ -362,7 +362,7 @@ begin
   { exact continuous_linear_map.op_norm_le_bound f ha (λ y, le_of_eq (hf y)) },
   { rw continuous_linear_map.norm_def,
     apply real.lb_le_Inf _ continuous_linear_map.bounds_nonempty,
-    cases exists_mem_ne_zero_of_dim_pos' hE with x hx,
+    cases dim_pos_iff_exists_ne_zero.mp hE with x hx,
     intros c h, rw mem_set_of_eq at h,
     apply (mul_le_mul_right (norm_pos_iff.mpr hx)).mp,
     rw ← hf x, exact h.2 x }