diff --git a/analysis/bounded_linear_maps.lean b/analysis/bounded_linear_maps.lean
new file mode 100644
index 0000000000000..ada0606a1ffce
--- /dev/null
+++ b/analysis/bounded_linear_maps.lean
@@ -0,0 +1,125 @@
+/-
+Copyright (c) 2018 Patrick Massot. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Patrick Massot, Johannes Hölzl
+
+Continuous linear functions -- functions between normed vector spaces which are bounded and linear.
+-/
+import algebra.field
+import tactic.norm_num
+import analysis.normed_space
+
+@[simp] lemma mul_inv_eq' {α} [discrete_field α] (a b : α) : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
+classical.by_cases (assume : a = 0, by simp [this]) $ assume ha,
+classical.by_cases (assume : b = 0, by simp [this]) $ assume hb,
+mul_inv_eq hb ha
+
+noncomputable theory
+local attribute [instance] classical.prop_decidable
+
+local notation f `→_{`:50 a `}`:0 b := filter.tendsto f (nhds a) (nhds b)
+
+open filter (tendsto)
+
+variables {k : Type*} [normed_field k]
+variables {E : Type*} [normed_space k E]
+variables {F : Type*} [normed_space k F]
+variables {G : Type*} [normed_space k G]
+
+structure is_bounded_linear_map {k : Type*}
+  [normed_field k] {E : Type*} [normed_space k E] {F : Type*} [normed_space k F] (L : E → F)
+  extends is_linear_map L : Prop :=
+(bound : ∃ M, M > 0 ∧ ∀ x : E, ∥ L x ∥ ≤ M * ∥ x ∥)
+
+include k
+
+lemma is_linear_map.with_bound
+  {L : E → F} (hf : is_linear_map L) (M : ℝ) (h : ∀ x : E, ∥ L x ∥ ≤ M * ∥ x ∥) :
+  is_bounded_linear_map L :=
+⟨ hf, classical.by_cases
+  (assume : M ≤ 0, ⟨1, zero_lt_one, assume x,
+    le_trans (h x) $ mul_le_mul_of_nonneg_right (le_trans this zero_le_one) (norm_nonneg x)⟩)
+  (assume : ¬ M ≤ 0, ⟨M, lt_of_not_ge this, h⟩)⟩
+
+namespace is_bounded_linear_map
+
+lemma zero : is_bounded_linear_map (λ (x:E), (0:F)) :=
+is_linear_map.map_zero.with_bound 0 $ by simp [le_refl]
+
+lemma id : is_bounded_linear_map (λ (x:E), x) :=
+is_linear_map.id.with_bound 1 $ by simp [le_refl]
+
+lemma smul {f : E → F} (c : k) : is_bounded_linear_map f → is_bounded_linear_map (λ e, c • f e)
+| ⟨hf, ⟨M, hM, h⟩⟩ := hf.map_smul_right.with_bound (∥c∥ * M) $ assume x,
+  calc ∥c • f x∥ = ∥c∥ * ∥f x∥ : norm_smul c (f x)
+    ... ≤ ∥c∥ * (M * ∥x∥) : mul_le_mul_of_nonneg_left (h x) (norm_nonneg c)
+    ... = (∥c∥ * M) * ∥x∥ : (mul_assoc _ _ _).symm
+
+lemma neg {f : E → F} (hf : is_bounded_linear_map f) : is_bounded_linear_map (λ e, -f e) :=
+begin
+  rw show (λ e, -f e) = (λ e, (-1) • f e), { funext, simp },
+  exact smul (-1) hf
+end
+
+lemma add {f : E → F} {g : E → F} :
+  is_bounded_linear_map f → is_bounded_linear_map g → is_bounded_linear_map (λ e, f e + g e)
+| ⟨hlf, Mf, hMf, hf⟩  ⟨hlg, Mg, hMg, hg⟩ := (hlf.map_add hlg).with_bound (Mf + Mg) $ assume x,
+  calc ∥f x + g x∥ ≤ ∥f x∥ + ∥g x∥ : norm_triangle _ _
+    ... ≤ Mf * ∥x∥ + Mg * ∥x∥ : add_le_add (hf x) (hg x)
+    ... ≤ (Mf + Mg) * ∥x∥ : by rw add_mul
+
+lemma sub {f : E → F} {g : E → F} (hf : is_bounded_linear_map f) (hg : is_bounded_linear_map g) :
+  is_bounded_linear_map (λ e, f e - g e) := add hf (neg hg)
+
+lemma comp {f : E → F} {g : F → G} :
+  is_bounded_linear_map g → is_bounded_linear_map f → is_bounded_linear_map (g ∘ f)
+| ⟨hlg, Mg, hMg, hg⟩ ⟨hlf, Mf, hMf, hf⟩ := (hlg.comp hlf).with_bound (Mg * Mf) $ assume x,
+  calc ∥g (f x)∥ ≤ Mg * ∥f x∥ : hg _
+    ... ≤ Mg * (Mf * ∥x∥) : mul_le_mul_of_nonneg_left (hf _) (le_of_lt hMg)
+    ... = Mg * Mf * ∥x∥ : (mul_assoc _ _ _).symm
+
+lemma tendsto {L : E → F} (x : E) : is_bounded_linear_map L → tendsto L (nhds x) (nhds (L x))
+| ⟨hL, M, hM, h_ineq⟩ := tendsto_iff_norm_tendsto_zero.2 $
+  squeeze_zero (assume e, norm_nonneg _)
+    (assume e, calc ∥L e - L x∥ = ∥L (e - x)∥ : by rw ← hL.sub e x
+      ... ≤ M*∥e-x∥ : h_ineq (e-x))
+    (suffices (λ (e : E), M * ∥e - x∥) →_{x} (M * 0), by simpa,
+      tendsto_mul tendsto_const_nhds (lim_norm _))
+
+lemma continuous {L : E → F} (hL : is_bounded_linear_map L) : continuous L :=
+continuous_iff_tendsto.2 $ assume x, hL.tendsto x
+
+lemma lim_zero_bounded_linear_map {L : E → F} (H : is_bounded_linear_map L) : (L →_{0} 0) :=
+by simpa [H.to_is_linear_map.zero] using continuous_iff_tendsto.1 H.continuous 0
+
+end is_bounded_linear_map
+
+-- Next lemma is stated for real normed space but it would work as soon as the base field is an extension of ℝ
+lemma bounded_continuous_linear_map
+  {E : Type*} [normed_space ℝ E] {F : Type*} [normed_space ℝ F] {L : E → F}
+  (lin : is_linear_map L) (cont : continuous L) : is_bounded_linear_map L :=
+let ⟨δ, δ_pos, hδ⟩ := exists_delta_of_continuous cont zero_lt_one 0 in
+have H : ∀{a}, ∥a∥ ≤ δ → ∥L a∥ < 1, by simpa [lin.zero, dist_zero_right] using hδ,
+lin.with_bound (δ⁻¹) $ assume x,
+classical.by_cases (assume : x = 0, by simp [this, lin.zero]) $
+assume h : x ≠ 0,
+let p := ∥x∥ * δ⁻¹, q := p⁻¹ in
+have p_inv : p⁻¹ = δ*∥x∥⁻¹, by simp,
+
+have norm_x_pos : ∥x∥ > 0 := (norm_pos_iff x).2 h,
+have norm_x : ∥x∥ ≠ 0 := mt (norm_eq_zero x).1 h,
+
+have p_pos : p > 0 := mul_pos norm_x_pos (inv_pos δ_pos),
+have p0 : _ := ne_of_gt p_pos,
+have q_pos : q > 0 := inv_pos p_pos,
+have q0 : _ := ne_of_gt q_pos,
+
+have ∥p⁻¹ • x∥ = δ := calc
+  ∥p⁻¹ • x∥ = abs p⁻¹ * ∥x∥ : by rw norm_smul; refl
+  ... = p⁻¹ * ∥x∥ : by rw [abs_of_nonneg $ le_of_lt q_pos]
+  ... = δ : by simp [mul_assoc, inv_mul_cancel norm_x],
+
+calc ∥L x∥ = (p * q) * ∥L x∥ : begin dsimp [q], rw [mul_inv_cancel p0, one_mul] end
+  ... = p * ∥L (q • x)∥ : by simp [lin.smul, norm_smul, real.norm_eq_abs, abs_of_pos q_pos, mul_assoc]
+  ... ≤ p * 1 : mul_le_mul_of_nonneg_left (le_of_lt $ H $ le_of_eq $ this) (le_of_lt p_pos)
+  ... = δ⁻¹ * ∥x∥ : by rw [mul_one, mul_comm]
diff --git a/analysis/continuous_linear_maps.lean b/analysis/continuous_linear_maps.lean
deleted file mode 100644
index 74b0fe4e2834e..0000000000000
--- a/analysis/continuous_linear_maps.lean
+++ /dev/null
@@ -1,170 +0,0 @@
-import algebra.field
-import tactic.norm_num
-import analysis.normed_space
-
-noncomputable theory
-local attribute [instance] classical.prop_decidable
-
-local notation f `→_{`:50 a `}`:0 b := filter.tendsto f (nhds a) (nhds b)
-
-
-variables {k : Type*} [normed_field k] 
-variables {E : Type*}  [normed_space k E] 
-variables {F : Type*} [normed_space k F]
-variables {G : Type*} [normed_space k G]
-
-include k
-def is_bounded_linear_map (L : E → F) := (is_linear_map L) ∧  ∃ M, M > 0 ∧ ∀ x : E, ∥ L x ∥ ≤ M *∥ x ∥ 
-
-namespace is_bounded_linear_map
-
-lemma zero : is_bounded_linear_map (λ (x:E), (0:F)) :=
-⟨is_linear_map.map_zero, exists.intro (1:ℝ) $ by norm_num⟩
-
-lemma id : is_bounded_linear_map (λ (x:E), x) :=
-⟨is_linear_map.id, exists.intro (1:ℝ) $ by { norm_num, finish }⟩
-
-lemma smul {L : E → F} (H : is_bounded_linear_map L) (c : k) :
-is_bounded_linear_map (λ e, c•L e) :=
-begin
-  by_cases h : c = 0,
-  { simp[h], exact zero },
-
-  rcases H with ⟨lin , M, Mpos, ineq⟩,
-  split,
-  { exact is_linear_map.map_smul_right lin },
-  { existsi ∥c∥*M,
-    split, 
-    { exact mul_pos ((norm_pos_iff c).2 h) Mpos },
-    intro x,
-    simp,
-    exact  calc ∥c • L x∥ = ∥c∥*∥L x∥ : norm_smul c (L x)
-    ... ≤ ∥c∥ * M * ∥x∥ : by {simp[mul_assoc, mul_le_mul_of_nonneg_left (ineq x) (norm_nonneg c)]} }
-end
-
-lemma neg {L : E → F} (H : is_bounded_linear_map L) :
-is_bounded_linear_map (λ e, -L e) :=
-begin
-  rw [show (λ e, -L e) = (λ e, (-1)•L e), by { funext, simp }],
-  exact smul H (-1)
-end
-
-lemma add {L : E → F} {P : E → F} (HL : is_bounded_linear_map L) (HP :is_bounded_linear_map P) : 
-is_bounded_linear_map (λ e, L e + P e) :=
-begin
-  rcases HL with ⟨lin_L , M, Mpos, ineq_L⟩,
-  rcases HP with ⟨lin_P , M', M'pos, ineq_P⟩,
-  split, exact (is_linear_map.map_add lin_L lin_P),
-  existsi (M+M'),
-  split, exact add_pos Mpos M'pos,
-  intro x, simp,
-  exact calc
-  ∥L x + P x∥ ≤ ∥L x∥ + ∥P x∥ : norm_triangle _ _
-  ... ≤ M * ∥x∥ + M' * ∥x∥ : add_le_add (ineq_L x) (ineq_P x)
- ... ≤ (M + M') * ∥x∥ : by rw  ←add_mul
-end
-
-lemma sub {L : E → F} {P : E → F} (HL : is_bounded_linear_map L) (HP :is_bounded_linear_map P) : 
-is_bounded_linear_map (λ e, L e - P e) := add HL (neg HP)
-
-lemma comp {L : E → F} {P : F → G} (HL : is_bounded_linear_map L) (HP :is_bounded_linear_map P) : is_bounded_linear_map (P ∘ L) :=
-begin
-  rcases HL with ⟨lin_L , M, Mpos, ineq_L⟩,
-  rcases HP with ⟨lin_P , M', M'pos, ineq_P⟩,
-  split,
-  { exact is_linear_map.comp lin_P lin_L },
-  { existsi M'*M,
-    split,
-    { exact mul_pos M'pos Mpos },
-    { intro x,
-      exact calc
-        ∥P (L x)∥ ≤ M' * ∥L x∥ : ineq_P (L x)
-              ... ≤  M'*M*∥x∥ : by simp[mul_assoc, mul_le_mul_of_nonneg_left (ineq_L x) (le_of_lt M'pos)] } }
-end
-
-lemma continuous {L : E → F} (H : is_bounded_linear_map L) : continuous L :=
-begin
-  rcases H with ⟨lin, M, Mpos, ineq⟩,
-  apply continuous_iff_tendsto.2,
-  intro x,
-  apply tendsto_iff_norm_tendsto_zero.2,
-  replace ineq := λ e, calc ∥L e - L x∥ = ∥L (e - x)∥ : by rw [←(lin.sub e x)]
-  ... ≤ M*∥e-x∥ : ineq (e-x),
-  have lim1 : (λ (x:E), M) →_{x} M := tendsto_const_nhds,
-
-  have lim2 : (λ e, e-x) →_{x} 0 := 
-  begin 
-    have limId := continuous_iff_tendsto.1 continuous_id x,
-    have limx : (λ (e : E), -x) →_{x} -x := tendsto_const_nhds,
-    have := tendsto_add limId limx, 
-    simp at this,
-    simpa using this,
-  end,
-  replace lim2 := filter.tendsto.comp lim2 lim_norm_zero,
-  apply squeeze_zero,
-  { simp[norm_nonneg] },
-  { exact ineq },
-  { simpa using tendsto_mul lim1 lim2 }
-end
-
-
-lemma lim_zero_bounded_linear_map {L : E → F} (H : is_bounded_linear_map L) : (L →_{0} 0) :=
-by simpa [H.left.zero] using continuous_iff_tendsto.1 H.continuous 0
-
-end is_bounded_linear_map
-
--- Next lemma is stated for real normed space but it would work as soon as the base field is an extension of ℝ
-lemma bounded_continuous_linear_map {E : Type*}  [normed_space ℝ E] {F : Type*}  [normed_space ℝ F] {L : E → F} 
-(lin : is_linear_map L) (cont : continuous L ) : is_bounded_linear_map L :=
-begin
-  split,
-  exact lin,
-
-  replace cont := continuous_of_metric.1 cont 1 (by norm_num),
-  swap, exact 0,
-  rw[lin.zero] at cont,
-  rcases cont with ⟨δ, δ_pos, H⟩,
-  revert H,
-  repeat { conv in (_ < _ ) { rw norm_dist } },
-  intro H,
-  existsi (δ/2)⁻¹,
-  have half_δ_pos := half_pos δ_pos,
-  split,
-  exact (inv_pos half_δ_pos),
-  intro x,
-  by_cases h : x = 0,
-  { simp [h, lin.zero] }, -- case x = 0
-  { -- case x ≠ 0   
-    have norm_x_pos : ∥x∥ > 0 := (norm_pos_iff x).2 h,
-    have norm_x : ∥x∥ ≠ 0 := mt (norm_eq_zero x).1 h,
-    
-    let p := ∥x∥*(δ/2)⁻¹,
-    have p_pos : p > 0 := mul_pos norm_x_pos (inv_pos $ half_δ_pos),
-    have p0 := ne_of_gt p_pos,
-
-    let q := (δ/2)*∥x∥⁻¹,
-    have q_pos : q > 0 := div_pos half_δ_pos norm_x_pos,
-    have q0 := ne_of_gt q_pos,
-
-    have triv := calc
-     p*q = ∥x∥*((δ/2)⁻¹*(δ/2))*∥x∥⁻¹ : by simp[mul_assoc]
-     ... = 1 : by simp [(inv_mul_cancel $ ne_of_gt half_δ_pos), mul_inv_cancel norm_x],
-      
-    have norm_calc := calc ∥q•x∥ = abs(q)*∥x∥ : by {rw norm_smul, refl}
-    ... = q*∥x∥ : by rw [abs_of_nonneg $ le_of_lt q_pos]
-    ... = δ/2 :  by simp [mul_assoc, inv_mul_cancel norm_x]
-    ... < δ : half_lt_self δ_pos,
-
-    replace H : ∀ {a : E}, ∥a∥ < δ → ∥L a∥ < 1 := by simp [dist_zero_right] at H ; assumption,
-
-    exact calc 
-    ∥L x∥ = ∥L (1•x)∥: by simp
-    ... = ∥L ((p*q)•x) ∥ : by {rw [←triv] }
-    ... = ∥L (p•q•x) ∥ : by rw mul_smul
-    ... = ∥p•L (q•x) ∥ : by rw lin.smul
-    ... = abs(p)*∥L (q•x) ∥ : by { rw norm_smul, refl}
-    ... = p*∥L (q•x) ∥ : by rw [abs_of_nonneg $ le_of_lt $ p_pos]
-    ... ≤ p*1 : le_of_lt $ mul_lt_mul_of_pos_left (H norm_calc) p_pos
-    ... = p : by simp
-    ... = (δ/2)⁻¹*∥x∥ : by simp[mul_comm] }
-end
\ No newline at end of file
diff --git a/analysis/metric_space.lean b/analysis/metric_space.lean
index 43665c395dc1a..636a91be4e6d1 100644
--- a/analysis/metric_space.lean
+++ b/analysis/metric_space.lean
@@ -288,10 +288,16 @@ theorem tendsto_nhds_of_metric [metric_space β] {f : α → β} {a b} :
   mem_nhds_iff_metric.2 ⟨δ, δ0, λ x h, hε (hδ h)⟩⟩
 
 theorem continuous_of_metric [metric_space β] {f : α → β} :
-  continuous f ↔ ∀ {b} (ε > 0), ∃ δ > 0, ∀{a},
+  continuous f ↔ ∀b (ε > 0), ∃ δ > 0, ∀a,
     dist a b < δ → dist (f a) (f b) < ε :=
 continuous_iff_tendsto.trans $ forall_congr $ λ b, tendsto_nhds_of_metric
 
+theorem exists_delta_of_continuous [metric_space β] {f : α → β} {ε:ℝ}
+  (hf : continuous f) (hε : ε > 0) (b : α) :
+  ∃ δ > 0, ∀a, dist a b ≤ δ → dist (f a) (f b) < ε :=
+let ⟨δ, δ_pos, hδ⟩ := continuous_of_metric.1 hf b ε hε in
+⟨δ / 2, half_pos δ_pos, assume a ha, hδ a $ lt_of_le_of_lt ha $ div_two_lt_of_pos δ_pos⟩
+
 theorem eq_of_forall_dist_le {x y : α} (h : ∀ε, ε > 0 → dist x y ≤ ε) : x = y :=
 eq_of_dist_eq_zero (eq_of_le_of_forall_le_of_dense dist_nonneg h)
 
diff --git a/analysis/normed_space.lean b/analysis/normed_space.lean
index 688fe9782d147..e525681d88299 100644
--- a/analysis/normed_space.lean
+++ b/analysis/normed_space.lean
@@ -218,6 +218,8 @@ instance : normed_field ℝ :=
   dist_eq := assume x y, rfl,
   norm_mul := abs_mul }
 
+lemma real.norm_eq_abs (r : ℝ): norm r = abs r := rfl
+
 end normed_field
 
 section normed_space