feat(library/theories): adapt analysis theory to use new topological limits

library/theories/analysis/bounded_linear_operator.lean

@@ -6,7 +6,8 @@ Author: Robert Y. Lewis
 Bounded linear operators
 -/
 import .normed_space .real_limit algebra.module algebra.homomorphism
-open real nat classical topology
+open real nat classical topology set
+--open normed_vector_space (this confuses lots of stuff??)
 noncomputable theory
 
 namespace analysis
@@ -156,21 +157,60 @@ variables [HV : normed_vector_space V] [HW : normed_vector_space W]
 include HV HW
 
 definition is_frechet_deriv_at (f A : V → W) [is_bdd_linear_map A] (x : V) :=
-  (λ h : V, ∥f (x + h) - f x - A h ∥ / ∥ h ∥) ⟶ 0 at 0
+  (λ h : V, ∥f (x + h) - f x - A h ∥ / ∥ h ∥) ⟶ 0 [at 0]
+
+lemma diff_quot_cts {f A : V → W} [HA : is_bdd_linear_map A] {y : V} (Hf : is_frechet_deriv_at f A y) :
+      continuous_at (λ h, ∥f (y + h) - f y - A h∥ / ∥h∥) 0 :=
+  begin
+    apply normed_vector_space.continuous_at_intro,
+    intro ε Hε,
+    cases normed_vector_space.approaches_at_dest Hf Hε with δ Hδ,
+    existsi δ,
+    split,
+    exact and.left Hδ,
+    intro x' Hx',
+    cases em (x' = 0) with Heq Hneq,
+    {rewrite [Heq, norm_zero, div_zero, sub_zero, norm_zero], apply Hε},
+    {rewrite [norm_zero, div_zero],
+    apply and.right Hδ,
+    repeat assumption}
+  end
+
+theorem is_bdd_linear_map_of_eq {A B : V → W} [HA : is_bdd_linear_map A] (HAB : A = B) :
+        is_bdd_linear_map B :=
+  begin
+    fapply is_bdd_linear_map.mk,
+    all_goals try rewrite -HAB,
+    {apply hom_add},
+    {apply hom_smul},
+    {exact op_norm A},
+    {exact op_norm_pos A},
+    {rewrite -HAB, apply op_norm_bound}
+  end
+
+definition is_frechet_deriv_at_of_eq {f A : V → W} [is_bdd_linear_map A] {x : V}
+           (Hfd : is_frechet_deriv_at f A x) {B : V → W} (HAB : A = B) :
+           @is_frechet_deriv_at _ _ _ _ f B (is_bdd_linear_map_of_eq HAB) x :=
+  begin
+    unfold is_frechet_deriv_at,
+    rewrite -HAB,
+    apply Hfd
+  end
+
 
 theorem is_frechet_deriv_at_intro {f A : V → W} [is_bdd_linear_map A] {x : V}
         (H : ∀ ⦃ε : ℝ⦄, ε > 0 →
               (∃ δ : ℝ, δ > 0 ∧ ∀ ⦃x' : V⦄, x' ≠ 0 ∧ ∥x'∥ < δ → ∥f (x + x') - f x - A x'∥ / ∥x'∥ < ε)) :
         is_frechet_deriv_at f A x :=
   begin
+    apply normed_vector_space.approaches_at_intro,
     intros ε Hε,
     cases H Hε with δ Hδ,
     cases Hδ with Hδ Hδ',
     existsi δ,
     split,
     assumption,
-    intros x' Hx',
+    intros x' Hx'1 Hx'2,
-    cases Hx' with Hx'1 Hx'2,
     show abs (∥f (x + x') - f x - A x'∥ / ∥x'∥ - 0) < ε, begin
       have H : ∥f (x + x') - f x - A x'∥ / ∥x'∥ ≥ 0,
         from div_nonneg_of_nonneg_of_nonneg !norm_nonneg !norm_nonneg,
@@ -179,7 +219,7 @@ theorem is_frechet_deriv_at_intro {f A : V → W} [is_bdd_linear_map A] {x : V}
       split,
       assumption,
       rewrite [-sub_zero x'],
-      apply Hx'2
+      apply Hx'1
     end
   end
 
@@ -188,14 +228,14 @@ theorem is_frechet_deriv_at_elim {f A : V → W} [is_bdd_linear_map A] {x : V} (
               (∃ δ : ℝ, δ > 0 ∧ ∀ ⦃x' : V⦄, x' ≠ 0 ∧ ∥x'∥ < δ → ∥f (x + x') - f x - A x'∥ / ∥x'∥ < ε) :=
   begin
     intros ε Hε,
-    cases H Hε with δ Hδ,
+    cases normed_vector_space.approaches_at_dest H Hε with δ Hδ,
     cases Hδ with Hδ Hδ',
     existsi δ,
     split,
     assumption,
     intros x' Hx',
     rewrite [-sub_zero x' at Hx' {2}],
-    have Hδ'' : abs (∥f (x + x') - f x - A x'∥ / ∥x'∥ - 0) < ε, from Hδ' Hx',
+    have Hδ'' : abs (∥f (x + x') - f x - A x'∥ / ∥x'∥ - 0) < ε, from Hδ' (and.right Hx') (and.left Hx'),
     have Hpos : ∥f (x + x') - f x - A x'∥ / ∥x'∥ ≥ 0, from div_nonneg_of_nonneg_of_nonneg !norm_nonneg !norm_nonneg,
     rewrite [sub_zero at Hδ'', abs_of_nonneg Hpos at Hδ''],
     assumption
@@ -215,22 +255,36 @@ definition frechet_deriv_at_is_bdd_linear_map [instance] (f : V → W) (x : V) [
   frechet_diffable_at.HA _ _ f x
 
 theorem frechet_deriv_spec [Hf : frechet_diffable_at f x] :
-        (λ h : V, ∥f (x + h) - f x - (frechet_deriv_at f x h) ∥ / ∥ h ∥) ⟶ 0 at 0 :=
+        (λ h : V, ∥f (x + h) - f x - (frechet_deriv_at f x h) ∥ / ∥ h ∥) ⟶ 0 [at 0] :=
   frechet_diffable_at.is_fr_der _ _ f x
 
 theorem frechet_deriv_at_const (w : W) : is_frechet_deriv_at (λ v : V, w) (λ v : V, 0) x :=
   begin
+    apply normed_vector_space.approaches_at_intro,
     intros ε Hε,
     existsi 1,
     split,
     exact zero_lt_one,
-    intros x' Hx',
+    intros x' Hx' _,
-    rewrite [sub_self, sub_zero, norm_zero],
+    rewrite [2 sub_self, norm_zero],
-    krewrite [zero_div, dist_self],
+    krewrite [zero_div, sub_zero, norm_zero],
     assumption
   end
 
-theorem frechet_deriv_at_smul {c : ℝ} {A : V → W} [is_bdd_linear_map A]
+theorem frechet_deriv_at_id : is_frechet_deriv_at (λ v : V, v) (λ v : V, v) x :=
+  begin
+    apply normed_vector_space.approaches_at_intro,
+    intros ε Hε,
+    existsi 1,
+    split,
+    exact zero_lt_one,
+    intros x' Hx' _,
+    have x + x' - x - x' = 0, by simp,
+    rewrite [this, norm_zero, zero_div, sub_self, norm_zero],
+    exact Hε
+  end
+
+theorem frechet_deriv_at_smul (c : ℝ) {A : V → W} [is_bdd_linear_map A]
         (Hf : is_frechet_deriv_at f A x) : is_frechet_deriv_at (λ y, c • f y) (λ y, c • A y) x :=
   begin
     eapply @decidable.cases_on (abs c = 0),
@@ -240,31 +294,32 @@ theorem frechet_deriv_at_smul {c : ℝ} {A : V → W} [is_bdd_linear_map A]
     have Hfz : (λ y : V, (0 : ℝ) • f y) = (λ y : V, 0), from funext (λ y, !zero_smul),
     --have Hfz' : (λ x : V, (0 : ℝ) • A x) = (λ x : V, 0), from funext (λ y, !zero_smul),
     -- rewriting Hfz' produces type-incorrect term
-    rewrite [Hz, Hfz, ↑is_frechet_deriv_at],
+    rewrite [Hz, Hfz],
+    apply metric_space.approaches_at_intro,
     intro ε Hε,
     existsi 1,
     split,
     exact zero_lt_one,
-    intro x' Hx',
+    intro x' Hx' _,
     rewrite [zero_smul, *sub_zero, norm_zero],
     krewrite [zero_div, dist_self],
     exact Hε},
     intro Hcnz,
-    rewrite ↑is_frechet_deriv_at,
+    apply normed_vector_space.approaches_at_intro,
     intros ε Hε,
     have Hεc : ε / abs c > 0, from div_pos_of_pos_of_pos Hε (lt_of_le_of_ne !abs_nonneg (ne.symm Hcnz)),
-    cases Hf Hεc with δ Hδ,
+    cases normed_vector_space.approaches_at_dest Hf Hεc with δ Hδ,
     cases Hδ with Hδp Hδ,
     existsi δ,
     split,
     assumption,
-    intro x' Hx',
+    intro x' Hx' _,
     show abs ((∥c • f (x + x') - c • f x - c • A x'∥ / ∥x'∥ - 0)) < ε, begin
       rewrite [sub_zero, -2 smul_sub_left_distrib, norm_smul],
       krewrite mul_div_assoc,
       rewrite [abs_mul, abs_abs, -{ε}mul_div_cancel' Hcnz],
       apply mul_lt_mul_of_pos_left,
-      have Hδ' : abs (∥f (x + x') - f x - A x'∥ / ∥x'∥ - 0) < ε / abs c, from Hδ Hx',
+      have Hδ' : abs (∥f (x + x') - f x - A x'∥ / ∥x'∥ - 0) < ε / abs c, from Hδ Hx' a,
       rewrite sub_zero at Hδ',
       apply Hδ',
       apply lt_of_le_of_ne,
@@ -309,17 +364,19 @@ theorem frechet_deriv_at_add (A B : V → W) [is_bdd_linear_map A] [is_bdd_linea
       krewrite [Hhe, *div_zero, zero_add],
       eapply le.refl
     end,
-    have Hlimge : (λ h, ∥f (x + h) - f x - A h∥ / ∥h∥ + ∥g (x + h) - g x - B h∥ / ∥h∥) ⟶ 0 at 0, begin
+    have Hlimge : (λ h, ∥f (x + h) - f x - A h∥ / ∥h∥ + ∥g (x + h) - g x - B h∥ / ∥h∥) ⟶ 0 [at 0], begin
       rewrite [-zero_add 0],
-      apply add_converges_to_at,
+      apply add_approaches,
       apply Hf,
       apply Hg
     end,
-    have Hlimle : (λ (h : V), (0 : ℝ)) ⟶ 0 at 0, from converges_to_at_constant 0 0,
+    have Hlimle : (λ (h : V), (0 : ℝ)) ⟶ 0 [at 0], by apply approaches_constant,
-    apply converges_to_at_squeeze Hlimle Hlimge,
+    apply approaches_squeeze Hlimle Hlimge,
+    apply filter.eventually_of_forall,
     intro y,
     apply div_nonneg_of_nonneg_of_nonneg,
     repeat apply norm_nonneg,
+    apply filter.eventually_of_forall,
     apply Hle
   end
 
@@ -329,7 +386,7 @@ theorem continuous_at_of_diffable_at [Hf : frechet_diffable_at f x] : continuous
   begin
     apply normed_vector_space.continuous_at_intro,
     intros ε Hε,
-    note Hfds := frechet_deriv_spec f x Hε,
+    note Hfds := normed_vector_space.approaches_at_dest (frechet_deriv_spec f x) Hε,
     cases Hfds with δ Hδ,
     cases Hδ with Hδ Hδ',
     existsi min δ ((ε / 2) / (ε + op_norm (frechet_deriv_at f x))),
@@ -343,15 +400,15 @@ theorem continuous_at_of_diffable_at [Hf : frechet_diffable_at f x] : continuous
     {intro x' Hx',
     cases em (x' - x = 0) with Heq Hneq,
     rewrite [eq_of_sub_eq_zero Heq, sub_self, norm_zero], assumption,
-    have Hx'x : x' - x ≠ 0 ∧ dist (x' - x) 0 < δ, from and.intro Hneq begin
+    have Hx'x : x' - x ≠ 0 ∧ ∥(x' - x) - 0∥ < δ, from and.intro Hneq begin
-      change ∥(x' - x) - 0∥ < δ,
       rewrite sub_zero,
       apply lt_of_lt_of_le,
       apply Hx',
       apply min_le_left
     end,
     have Hx'xp : ∥x' - x∥ > 0, from norm_pos_of_ne_zero Hneq,
-    have Hδ'' : abs (∥f (x + (x' - x)) - f x - frechet_deriv_at f x (x' - x)∥ / ∥x' - x∥ - 0) < ε, from Hδ' Hx'x,
+    have Hδ'' : abs (∥f (x + (x' - x)) - f x - frechet_deriv_at f x (x' - x)∥ / ∥x' - x∥ - 0) < ε,
+      from Hδ' (and.right Hx'x) (and.left Hx'x),
     have Hnn : ∥f (x + (x' - x)) - f x - frechet_deriv_at f x (x' - x)∥ / ∥x' - x∥ ≥ 0,
       from div_nonneg_of_nonneg_of_nonneg !norm_nonneg !norm_nonneg,
     rewrite [sub_zero at Hδ'', abs_of_nonneg Hnn at Hδ'', add.comm at Hδ'', sub_add_cancel at Hδ''],
@@ -378,9 +435,31 @@ theorem continuous_at_of_diffable_at [Hf : frechet_diffable_at f x] : continuous
                ... < ε / 2 : mul_div_add_self_lt (div_pos_of_pos_of_pos Hε two_pos) Hε !op_norm_pos}
   end
 
+theorem continuous_at_of_is_frechet_deriv_at {A : V → W} [is_bdd_linear_map A]
+        (H : is_frechet_deriv_at f A x) : continuous_at f x :=
+  begin
+    apply @continuous_at_of_diffable_at,
+    existsi A,
+    exact H
+  end
+
 end frechet_deriv
 
-/-section comp
+section comp
+
+lemma div_mul_div_cancel {A : Type} [field A] (a b : A) {c : A} (Hc : c ≠ 0) : (a / c) * (c / b) = a / b :=
+  by rewrite [-mul_div_assoc, div_mul_cancel _ Hc]
+
+lemma div_add_eq_add_mul_div {A : Type} [field A] (a b c : A) (Hb : b ≠ 0) : (a / b) + c = (a + c * b) / b :=
+  by rewrite [-div_add_div_same, mul_div_cancel _ Hb]
+
+-- I'm not sure why smul_approaches doesn't unify where I use this?
+lemma real_limit_helper {U : Type} [normed_vector_space U] {f : U → ℝ} {a : ℝ} {x : U}
+      (Hf : f ⟶ a [at x]) (c : ℝ) : (λ y, c * f y) ⟶ c * a [at x] :=
+  begin
+    apply smul_approaches,
+    exact Hf
+  end
 
 variables {U V W : Type}
 variables [HU : normed_vector_space U] [HV : normed_vector_space V] [HW : normed_vector_space W]
@@ -388,15 +467,122 @@ variables {f : V → W} {g : U → V}
 variables {A : V → W} {B : U → V}
 variables [HA : is_bdd_linear_map A] [HB : is_bdd_linear_map B]
 variable {x : U}
+
 include HU HV HW HA HB
 
+-- this takes 2 seconds without clearing the contexts before simp
 theorem frechet_derivative_at_comp (Hg : is_frechet_deriv_at g B x) (Hf : is_frechet_deriv_at f A (g x)) :
         @is_frechet_deriv_at _ _ _ _ (λ y, f (g y)) (λ y, A (B y)) !is_bdd_linear_map_comp x :=
   begin
-    rewrite ↑is_frechet_deriv_at,
+    unfold is_frechet_deriv_at,
-    intros ε Hε,
+    note Hf' := is_frechet_deriv_at_elim Hf,
+    note Hg' := is_frechet_deriv_at_elim Hg,
+    have H : ∀ h, f (g (x + h)) - f (g x) - A (B h) =
+             (A (g (x + h) - g x - B h)) + (-f (g x) + f (g (x + h)) + A (g x - g (x + h))),
+      begin intro; rewrite [3 hom_sub A], clear [Hf, Hg, Hf', Hg'], simp end, -- .5 seconds for simp
+    have H' : (λ h, ∥f (g (x + h)) - f (g x) - A (B h)∥ / ∥h∥) =
+              (λ h, ∥(A (g (x + h) - g x - B h)) + (-f (g x) + f (g (x + h)) + A (g x - g (x + h)))∥ / ∥h∥),
+      from funext (λ h, by rewrite H),
+    rewrite H',
+    clear [H, H'],
+    apply approaches_squeeze, -- show the limit holds by bounding it by something that vanishes
+    {apply approaches_constant},
+    rotate 1,
+    {apply filter.eventually_of_forall, intro, apply div_nonneg_of_nonneg_of_nonneg, repeat apply norm_nonneg},
+    {apply filter.eventually_of_forall, intro,
+    apply div_le_div_of_le_of_nonneg,
+    apply norm_triangle,
+    apply norm_nonneg},
+    have H : (λ (y : U), (∥A (g (x + y) - g x - B y)∥ + ∥-f (g x) + f (g (x + y)) + A (g x - g (x + y))∥) / ∥y∥) =
+      (λ (y : U), (∥A (g (x + y) - g x - B y)∥ / ∥y∥ + ∥-f (g x) + f (g (x + y)) + A (g x - g (x + y))∥ / ∥y∥)),
+      from funext (λ y, by rewrite [div_add_div_same]),
+    rewrite [H, -zero_add 0], -- the function is a sum of two things that both vanish
+    clear H,
+    apply add_approaches,
+    {apply approaches_squeeze, -- show the lhs vanishes by squeezing it again
+    {apply approaches_constant},
+    rotate 1,
+    {apply filter.eventually_of_forall, intro, apply div_nonneg_of_nonneg_of_nonneg, repeat apply norm_nonneg},
+    {apply filter.eventually_of_forall, intro y,
+    show ∥A (g (x + y) - g x - B y)∥ / ∥y∥ ≤ op_norm A * (∥(g (x + y) - g x - B y)∥ / ∥y∥), begin
+      rewrite -mul_div_assoc,
+      apply div_le_div_of_le_of_nonneg,
+      apply op_norm_bound A,
+      apply norm_nonneg
+    end},
+    {rewrite [-mul_zero (op_norm A)],
+    apply real_limit_helper,
+    apply Hg}}, -- we have shown the lhs vanishes. now the rhs
+    {have H : ∀ y, (∥-f (g x) + f (g (x + y)) + A (g x - g (x + y))∥ / ∥y∥) =
+      ((∥(f (g (x + y)) - f (g x)) - A (g (x + y) - g x) ∥ / ∥g (x + y) - g x∥) * (∥g (x + y) - g x∥ / ∥y∥)),
+    begin
+      intro,
+      cases em (g (x + y) - g x = 0) with Heq Hneq,
+      {note Heq' := eq_of_sub_eq_zero Heq,
+      rewrite [Heq', neg_add_eq_sub, *sub_self, hom_zero A, add_zero, *norm_zero, div_zero, zero_div]},
+      {rewrite [div_mul_div_cancel _ _ (norm_ne_zero_of_ne_zero Hneq), *sub_eq_add_neg,
+        -hom_neg A],
+      simp} --(.5 seconds)
+    end,
+    apply approaches_squeeze, -- again, by squeezing
+    {apply approaches_constant},
+    rotate 1,
+    {apply filter.eventually_of_forall, intro, apply div_nonneg_of_nonneg_of_nonneg, repeat apply norm_nonneg},
+    {apply filter.eventually_of_forall, intro y, rewrite H,
+    apply mul_le_mul_of_nonneg_left,
+    {show ∥g (x + y) - g x∥ / ∥y∥ ≤  ∥g (x + y) - g x - B y∥ / ∥y∥ + op_norm B, begin
+      cases em (y = 0) with Heq Hneq,
+      {rewrite [Heq, norm_zero, *div_zero, zero_add], apply le_of_lt, apply op_norm_pos},
+      rewrite [div_add_eq_add_mul_div _ _ _ (norm_ne_zero_of_ne_zero Hneq)],
+      apply div_le_div_of_le_of_nonneg,
+      apply le.trans,
+      rotate 1,
+      apply add_le_add_left,
+      apply op_norm_bound,
+      apply norm_nonneg,
+      rewrite [-neg_add_cancel_right (g (x + y) - g x) (B y) at {1}, -sub_eq_add_neg],
+      apply norm_triangle
+    end},
+    {apply div_nonneg_of_nonneg_of_nonneg, repeat apply norm_nonneg}},
+    -- now to show the bounding function vanishes. it is a product of a vanishing function and a convergent one
+    apply mul_approaches_zero_of_approaches_zero_of_approaches,
+    {have H' : (λ (y : U), ∥f (g (x + y)) - f (g x) - A (g (x + y) - g x)∥ / ∥g (x + y) - g x∥) =
+            (λ (y : U), ∥f (g x + (g (x + y) - g x)) - f (g x) - A (g (x + y) - g x)∥ / ∥g (x + y) - g x∥),
+      from funext (λ y, by rewrite [add.comm (g x), sub_add_cancel]), -- first, show lhs vanishes
+    rewrite H',
+    have Hgcts : continuous_at (λ y, g (x + y) - g x) 0, begin
+      apply normed_vector_space.continuous_at_intro,
+      intro ε Hε,
+      cases normed_vector_space.continuous_at_dest (continuous_at_of_is_frechet_deriv_at g x Hg) _ Hε with δ Hδ,
+      existsi δ,
+      split,
+      exact and.left Hδ,
+      intro x' Hx',
+      rewrite [add_zero, sub_self],
+      rewrite sub_zero,
+      apply and.right Hδ,
+      have (x + x') - x = x' - 0, begin clear [Hg, Hf, Hf', Hg', H, H', Hδ, Hx'], simp end, -- (.6 seconds w/o clear, .1 with)
+      rewrite this,
+      apply Hx'
+    end,
+    have Hfcts : continuous_at (λ (x' : V), ∥f (g x + x') - f (g x) - A x'∥ / ∥x'∥) (g (x + 0) - g x), begin
+      rewrite [add_zero, sub_self],
+      apply diff_quot_cts,
+      exact Hf
+    end,
+    have Heqz : ∥f (g x + (g (x + 0) - g x)) - f (g x) - A (g (x + 0) - g x)∥ / ∥g (x + 0) - g x∥ = 0,
+      by rewrite [*add_zero, sub_self, norm_zero, div_zero],
+    apply @tendsto_comp _ _ _ (λ y, g (x + y) - g x),
+    apply tendsto_inf_left,
+    apply tendsto_at_of_continuous_at Hgcts,
+    note Hfcts' := tendsto_at_of_continuous_at Hfcts,
+    rewrite Heqz at Hfcts',
+    exact Hfcts'}, -- finally, show rhs converges to op_norm B
+    {apply add_approaches,
+    apply Hg,
+    apply approaches_constant}}
   end
 
-end comp-/
+end comp
 
 end analysis

library/theories/analysis/ivt.lean

@@ -204,7 +204,7 @@ theorem intermediate_value_decr_zero {f : ℝ → ℝ} (Hf : continuous f) {a b
   begin
     have Ha' : - f a < 0, from neg_neg_of_pos Ha,
     have Hb' : - f b > 0, from neg_pos_of_neg Hb,
-    have Hcon : continuous (λ x, - f x), from continuous_neg_of_continuous Hf,
+    have Hcon : continuous (λ x, - f x), from neg_continuous Hf,
     let Hiv := intermediate_value_incr_zero Hcon Hab Ha' Hb',
     cases Hiv with c Hc,
     existsi c,
@@ -220,7 +220,7 @@ theorem intermediate_value_incr {f : ℝ → ℝ} (Hf : continuous f) {a b : ℝ
         (Hav : f a < v) (Hbv : f b > v) : ∃ c, a < c ∧ c < b ∧ f c = v :=
   have Hav' : f a - v < 0, from sub_neg_of_lt Hav,
   have Hbv' : f b - v > 0, from sub_pos_of_lt Hbv,
-  have Hcon : continuous (λ x, f x - v), from continuous_offset_of_continuous Hf _,
+  have Hcon : continuous (λ x, f x - v), from sub_continuous Hf (continuous_const _),
   have Hiv : ∃ c, a < c ∧ c < b ∧ f c - v = 0, from intermediate_value_incr_zero Hcon Hab Hav' Hbv',
   obtain c Hc, from Hiv,
   exists.intro c
@@ -230,7 +230,7 @@ theorem intermediate_value_decr {f : ℝ → ℝ} (Hf : continuous f) {a b : ℝ
         (Hav : f a > v) (Hbv : f b < v) : ∃ c, a < c ∧ c < b ∧ f c = v :=
   have Hav' : f a - v > 0, from sub_pos_of_lt Hav,
   have Hbv' : f b - v < 0, from sub_neg_of_lt Hbv,
-  have Hcon : continuous (λ x, f x - v), from continuous_offset_of_continuous Hf _,
+  have Hcon : continuous (λ x, f x - v), from sub_continuous Hf (continuous_const _),
   have Hiv : ∃ c, a < c ∧ c < b ∧ f c - v = 0, from intermediate_value_decr_zero Hcon Hab Hav' Hbv',
   obtain c Hc, from Hiv,
   exists.intro c

library/theories/analysis/metric_space.lean

@@ -2,6 +2,8 @@
 Copyright (c) 2015 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Metric spaces.
+
+Authors: Jeremy Avigad, Robert Y. Lewis
 -/
 import data.real.complete data.pnat ..topology.continuous ..topology.limit data.set
 open nat real eq.ops classical set prod set.filter topology interval
@@ -215,6 +217,11 @@ proposition eventually_at_iff (P : M → Prop) (x : M) :
   eventually P [at x] ↔  ∃ ε, ε > 0 ∧ ∀ ⦃x'⦄, dist x' x < ε → x' ≠ x → P x' :=
 iff.intro eventually_at_dest (λ H, obtain ε [εpos Hε], from H, eventually_at_intro εpos Hε)
 
+end metric_space_M
+
+namespace metric_space
+variables {M : Type} [metric_space M]
+
 section approaches
   variables {X : Type} {F : filter X} {f : X → M} {y : M}
 
@@ -236,13 +243,11 @@ section approaches
   proposition approaches_iff : (f ⟶ y) F ↔ (∀ ε, ε > 0 → eventually (λ x, dist (f x) y < ε) F) :=
   iff.intro approaches_dest approaches_intro
 
-  -- TODO: prove this in greater generality in topology.limit
-  proposition approaches_constant : ((λ x, y) ⟶ y) F :=
-  approaches_intro (λ ε εpos, eventually_of_forall F (λ x,
-    show dist y y < ε, by rewrite dist_self; apply εpos))
 end approaches
 
 -- here we full unwrap two particular kinds of convergence3
+-- TODO: put these in metric space namespace? (will have similar in normed_space
+
 
 proposition approaches_at_infty_intro {f : ℕ → M} {y : M}
     (H : ∀ ε, ε > 0 → ∃ N, ∀ n, n ≥ N → dist (f n) y < ε) :
@@ -282,8 +287,13 @@ proposition approaches_at_iff (f : M → N) (y : N) (x : M) : f ⟶ y [at x] ↔
 iff.intro approaches_at_dest approaches_at_intro
 
 end metric_space_N
+end metric_space -- close namespace
 
--- TODO: remove this. It is only here temporarily, because it is used in normed_space
+section metric_space_M
+variables {M : Type} [metric_space M]
+-- TODO: remove this. It is only here temporarily, because it is used in normed_space (JA)
+-- It is used in the definition of a complete metric space below, but I think it doesn't
+-- have to be a class (RL)
 abbreviation converges_seq [class] (X : ℕ → M) : Prop := ∃ y, X ⟶ y [at ∞]
 
 -- TODO: refactor
@@ -291,7 +301,7 @@ abbreviation converges_seq [class] (X : ℕ → M) : Prop := ∃ y, X ⟶ y [at
 definition approaches_at_infty_intro' {X : ℕ → M} {y : M}
     (H : ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → dist (X n) y ≤ ε) :
   (X ⟶ y) [at ∞] :=
-approaches_at_infty_intro
+metric_space.approaches_at_infty_intro
 take ε, assume epos : ε > 0,
   have e2pos : ε / 2 > 0, from  div_pos_of_pos_of_pos `ε > 0` two_pos,
   obtain N HN, from H e2pos,
@@ -308,9 +318,9 @@ eq_of_forall_dist_le
   (take ε, suppose ε > 0,
     have e2pos : ε / 2 > 0, from  div_pos_of_pos_of_pos `ε > 0` two_pos,
     obtain N₁ (HN₁ : ∀ {n}, n ≥ N₁ → dist (X n) y₁ < ε / 2),
-      from approaches_at_infty_dest H₁ e2pos,
+      from metric_space.approaches_at_infty_dest H₁ e2pos,
     obtain N₂ (HN₂ : ∀ {n}, n ≥ N₂ → dist (X n) y₂ < ε / 2),
-      from approaches_at_infty_dest H₂ e2pos,
+      from metric_space.approaches_at_infty_dest H₂ e2pos,
     let N := max N₁ N₂ in
     have dN₁ : dist (X N) y₁ < ε / 2, from HN₁ !le_max_left,
     have dN₂ : dist (X N) y₂ < ε / 2, from HN₂ !le_max_right,
@@ -347,11 +357,10 @@ have aux : (λ n, X (k + n)) = (λ n, X (n + k)), from funext (take n, by rewrit
 by rewrite aux at H; exact converges_to_seq_of_converges_to_seq_offset H
 -/
 
---<<<<<<< HEAD
 proposition bounded_of_converges_seq {X : ℕ → M} {x : M} (H : X ⟶ x [at ∞]) :
             ∃ K : ℝ, ∀ n : ℕ, dist (X n) x ≤ K :=
   have eventually (λ n, dist (X n) x < 1) [at ∞],
-    from approaches_dest H zero_lt_one,
+    from metric_space.approaches_dest H zero_lt_one,
   obtain N (HN : ∀ n, n ≥ N → dist (X n) x < 1),
     from eventually_at_infty_dest this,
   let K := max 1 (Max i ∈ '(-∞, N), dist (X i) x) in
@@ -363,12 +372,22 @@ proposition bounded_of_converges_seq {X : ℕ → M} {x : M} (H : X ⟶ x [at
       else
         show dist (X n) x ≤ K,
           from le.trans (le_of_lt (HN n (le_of_not_gt Hn))) !le_max_left)
---=======
-/-proposition converges_to_seq_of_converges_to_seq_offset_succ
-    {X : ℕ → M} {y : M} (H : (λ n, X (succ n)) ⟶ y in ℕ) :
-  X ⟶ y in ℕ :=
-@converges_to_seq_of_converges_to_seq_offset M _ X y 1 H
 
+proposition bounded_of_converges {A : Type} {X : A → M} {x : M} {F} (H : (X ⟶ x) F) :
+            ∃ K : ℝ, eventually (λ n, dist (X n) x ≤ K) F :=
+  begin
+    note H' := metric_space.approaches_dest H zero_lt_one,
+    existsi 1,
+    apply eventually_mono H',
+    intro x' Hx',
+    apply le_of_lt Hx'
+  end
+
+/-proposition converges_to_seq_of_converges_to_seq_offset_succ
+    {X : ℕ → M} {y : M} (H : (λ n, X (succ n)) ⟶ y [at ∞]) :
+  X ⟶ y [at ∞] :=
+@converges_to_seq_of_converges_to_seq_offset M _ X y 1 H-/
+/-
 proposition converges_to_seq_offset_iff (X : ℕ → M) (y : M) (k : ℕ) :
   ((λ n, X (n + k)) ⟶ y in ℕ) ↔ (X ⟶ y in ℕ) :=
 iff.intro converges_to_seq_of_converges_to_seq_offset !converges_to_seq_offset
@@ -380,49 +399,7 @@ iff.intro converges_to_seq_of_converges_to_seq_offset_left !converges_to_seq_off
 proposition converges_to_seq_offset_succ_iff (X : ℕ → M) (y : M) :
   ((λ n, X (succ n)) ⟶ y in ℕ) ↔ (X ⟶ y in ℕ) :=
 iff.intro converges_to_seq_of_converges_to_seq_offset_succ !converges_to_seq_offset_succ
-
+-/
-section
-open list
-private definition r_trans : transitive (@le ℝ _) := λ a b c, !le.trans
-private definition r_refl : reflexive (@le ℝ _) := λ a, !le.refl
-
-proposition bounded_of_converges_seq {X : ℕ → M} {x : M} (H : X ⟶ x in ℕ) :
-            ∃ K : ℝ, ∀ n : ℕ, dist (X n) x ≤ K :=
-  begin
-    cases H zero_lt_one with N HN,
-    cases em (N = 0),
-    existsi 1,
-    intro n,
-    apply le_of_lt,
-    apply HN,
-    rewrite a,
-    apply zero_le,
-    let l := map (λ n : ℕ, -dist (X n) x) (upto N),
-    have Hnenil : l ≠ nil, from (map_ne_nil_of_ne_nil _ (upto_ne_nil_of_ne_zero a)),
-    existsi max (-list.min (λ a b : ℝ, le a b) l Hnenil) 1,
-    intro n,
-    have Hsmn : ∀ m : ℕ, m < N → dist (X m) x ≤ max (-list.min (λ a b : ℝ, le a b) l Hnenil) 1, begin
-      intro m Hm,
-      apply le.trans,
-      rotate 1,
-      apply le_max_left,
-      note Hall := min_lemma real.le_total r_trans r_refl Hnenil,
-      have Hmem : -dist (X m) x ∈ (map (λ (n : ℕ), -dist (X n) x) (upto N)), from mem_map _ (mem_upto_of_lt Hm),
-      note Hallm' := of_mem_of_all Hmem Hall,
-      apply le_neg_of_le_neg,
-      exact Hallm'
-    end,
-    cases em (n < N) with Elt Ege,
-    apply Hsmn,
-    exact Elt,
-    apply le_of_lt,
-    apply lt_of_lt_of_le,
-    apply HN,
-    apply le_of_not_gt Ege,
-    apply le_max_right
-  end
-end
->>>>>>> feat(library/analysis): basic properties about real derivatives-/
 
 /- cauchy sequences -/
 
@@ -433,7 +410,7 @@ proposition cauchy_of_converges_seq {X : ℕ → M} (H : ∃ y, X ⟶ y [at ∞]
 take ε, suppose ε > 0,
   obtain y (Hy : X ⟶ y [at ∞]), from H,
   have e2pos : ε / 2 > 0, from div_pos_of_pos_of_pos `ε > 0` two_pos,
-  have eventually (λ n, dist (X n) y < ε / 2) [at ∞], from approaches_dest Hy e2pos,
+  have eventually (λ n, dist (X n) y < ε / 2) [at ∞], from metric_space.approaches_dest Hy e2pos,
   obtain N (HN : ∀ {n}, n ≥ N → dist (X n) y < ε / 2), from eventually_at_infty_dest this,
     exists.intro N
       (take m n, suppose m ≥ N, suppose n ≥ N,
@@ -452,41 +429,10 @@ end metric_space_M
 section metric_space_M_N
 variables {M N : Type} [metric_space M] [metric_space N]
 
-/-
-definition converges_to_at (f : M → N) (y : N) (x : M) :=
-∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ≠ x ∧ dist x' x < δ → dist (f x') y < ε
-
-notation f `⟶` y `at` x := converges_to_at f y x
-
-theorem converges_to_at_constant (y : N) (x : M) : (λ m, y) ⟶ y at x :=
-  begin
-    intros ε Hε,
-    existsi 1,
-    split,
-    exact zero_lt_one,
-    intros x' Hx',
-    rewrite dist_self,
-    apply Hε
-  end
-
-definition converges_at [class] (f : M → N) (x : M) :=
-∃ y, converges_to_at f y x
-
-noncomputable definition limit_at (f : M → N) (x : M) [H : converges_at f x] : N :=
-some H
-
-proposition converges_to_limit_at (f : M → N) (x : M) [H : converges_at f x] :
-  (f ⟶ limit_at f x at x) :=
-some_spec H
-
--/
 
 -- TODO: refactor
 section
 open pnat rat
-private lemma of_rat_rat_of_pnat_eq_of_nat_nat_of_pnat (p : pnat) :
-        of_rat (rat_of_pnat p) = of_nat (nat_of_pnat p) :=
-  rfl
 
 theorem cnv_real_of_cnv_nat {X : ℕ → M} {c : M} (H : ∀ n : ℕ, dist (X n) c < 1 / (real.of_nat n + 1)) :
         ∀ ε : ℝ, ε > 0 → ∃ N : ℕ, ∀ n : ℕ, n ≥ N → dist (X n) c < ε :=
@@ -512,51 +458,33 @@ theorem cnv_real_of_cnv_nat {X : ℕ → M} {c : M} (H : ∀ n : ℕ, dist (X n)
     krewrite -of_rat_zero,
     apply of_rat_lt_of_rat_of_lt,
     apply rat_of_pnat_is_pos,
-    krewrite [of_rat_rat_of_pnat_eq_of_nat_nat_of_pnat, -real.of_nat_add],
+    change of_nat (nat_of_pnat p) ≤ n + 1,
+    krewrite [-real.of_nat_add],
     apply real.of_nat_le_of_nat_of_le,
     apply le_add_of_le_right,
     assumption
   end
 end
 
--- a nice illustration of the limit library: [at c] and [at ∞] can be replaced by any filters
+-- TODO : refactor
-theorem comp_approaches_at_infty {f : M → N} {c : M} {l : N} (Hf : f ⟶ l [at c])
-    {X : ℕ → M} (HX₁ : X ⟶ c [at ∞]) (HX₂ : eventually (λ n, X n ≠ c) [at ∞]) :
-  (λ n, f (X n)) ⟶ l [at ∞] :=
-  tendsto_comp_of_approaches_of_tendsto_at HX₁ HX₂ Hf
-
--- TODO: refactor
-
 theorem converges_to_at_of_all_conv_seqs {f : M → N} (c : M) (l : N)
-  (Hseq : ∀ X : ℕ → M, ((∀ n : ℕ, ((X n) ≠ c) ∧ (X ⟶ c [at ∞])) → ((λ n : ℕ, f (X n)) ⟶ l [at ∞])))
+  (Hseq : ∀ X : ℕ → M, (eventually (λ n, X n ≠ c) [at ∞] ∧ (X ⟶ c [at ∞])) → ((λ n : ℕ, f (X n)) ⟶ l [at ∞]))
   : f ⟶ l [at c] :=
-  by_contradiction
+  begin
-    (assume Hnot : ¬ (f ⟶ l [at c]),
+    eapply by_contradiction,
-    obtain ε Hε, from exists_not_of_not_forall (λ H, Hnot (approaches_at_intro H)),
+    intro Hnot,
-    let Hε' := and_not_of_not_implies Hε in
+    cases exists_not_of_not_forall (λ H, Hnot (metric_space.approaches_at_intro H)) with ε Hε,
-    obtain (H1 : ε > 0) H2, from Hε',
+    cases and_not_of_not_implies Hε with H1 H2,
-    have H3 : ∀ δ : ℝ, (δ > 0 → ∃ x' : M, x' ≠ c ∧ dist x' c < δ ∧ dist (f x') l ≥ ε), begin -- tedious!!
+    note H3' := forall_not_of_not_exists H2,
-      intros δ Hδ,
+    have H3 : ∀ δ, δ > 0 → (∃ x', dist x' c < δ ∧ x' ≠ c ∧ dist (f x') l ≥ ε), begin
-      note Hε'' := forall_not_of_not_exists H2,
+      intro δ Hδ,
-      note H4 := forall_not_of_not_exists H2 δ,
+      cases exists_not_of_not_forall (or.resolve_left (not_or_not_of_not_and' (H3' δ)) (not_not_intro Hδ))
-      have ¬ (∀ x' : M, dist x' c < δ → x' ≠ c → dist (f x') l < ε),
+        with x' Hx',
-        from λ H', H4 (and.intro Hδ H'),
-      note H5 := exists_not_of_not_forall this,
-      cases H5 with x' Hx',
       existsi x',
-      note H6 := and_not_of_not_implies Hx',
+      rewrite [2 not_implies_iff_and_not at Hx', ge_iff_not_lt],
---      rewrite and.assoc at H6,
+      exact Hx'
-      cases H6 with H6a H6b,
-      split,
-      cases (and_not_of_not_implies H6b),
-      assumption,
-      split,
-      assumption,
-      apply le_of_not_gt,
-      cases (and_not_of_not_implies H6b),
-      assumption
     end,
-    let S : ℕ → M → Prop := λ n x, 0 < dist x c ∧ dist x c < 1 / (of_nat n + 1) ∧ dist (f x) l ≥ ε in
+    let S := λ (n : ℕ) (x : M), 0 < dist x c ∧ dist x c < 1 / (of_nat n + 1) ∧ dist (f x) l ≥ ε,
     have HS : ∀ n : ℕ, ∃ m : M, S n m, begin
       intro k,
       have Hpos : 0 < of_nat k + 1, from of_nat_succ_pos k,
@@ -571,55 +499,57 @@ theorem converges_to_at_of_all_conv_seqs {f : M → N} (c : M) (l : N)
       split,
       repeat assumption
     end,
-    let X : ℕ → M := λ n, some (HS n) in
+    let X := λ n, some (HS n),
-    have H4 : ∀ n : ℕ, ((X n) ≠ c) ∧ (X ⟶ c [at ∞]), from
+    have H4 : (eventually (λ n, X n ≠ c) [at ∞]) ∧ (X ⟶ c [at ∞]), begin
-      (take n, and.intro
+      split,
-        (begin
+      {fapply @eventually_at_infty_intro,
-          note Hspec := some_spec (HS n),
+      exact 0,
-          esimp, esimp at Hspec,
+      intro n Hn,
-          cases Hspec,
+      note Hspec := some_spec (HS n),
-          apply ne_of_dist_pos,
+      esimp, esimp at Hspec,
-          assumption
+      cases Hspec,
-        end)
+      apply ne_of_dist_pos,
-        (begin
+      assumption},
-          apply approaches_at_infty_intro,
+      {intro,
-          apply cnv_real_of_cnv_nat,
+      apply metric_space.approaches_at_infty_intro,
-          intro m,
+      apply cnv_real_of_cnv_nat,
-          note Hspec := some_spec (HS m),
+      intro m,
-          esimp, esimp at Hspec,
+      note Hspec := some_spec (HS m),
-          cases Hspec with Hspec1 Hspec2,
+      esimp, esimp at Hspec,
-          cases Hspec2,
+      cases Hspec with Hspec1 Hspec2,
-          assumption
+      cases Hspec2,
-        end)),
+      assumption}
-    have H5 : (λ n : ℕ, f (X n)) ⟶ l [at ∞], from Hseq X H4,
+    end,
-    begin
+    have H5 : (λ n, f (X n)) ⟶ l [at ∞], from Hseq X H4,
-      note H6 := approaches_at_infty_dest H5 H1,
+    note H6 := metric_space.approaches_at_infty_dest H5 H1,
-      cases H6 with Q HQ,
+    cases H6 with Q HQ,
-      note HQ' := HQ !le.refl,
+    note HQ' := HQ !le.refl,
-      esimp at HQ',
+    esimp at HQ',
-      apply absurd HQ',
+    apply absurd HQ',
-      apply not_lt_of_ge,
+    apply not_lt_of_ge,
-      note H7 := some_spec (HS Q),
+    note H7 := some_spec (HS Q),
-      esimp at H7,
+    esimp at H7,
-      cases H7 with H71 H72,
+    cases H7 with H71 H72,
-      cases H72,
+    cases H72,
-      assumption
+    assumption
-    end)
+  end
 
 end metric_space_M_N
 
+namespace metric_space
+
 section continuity
 variables {M N : Type} [Hm : metric_space M] [Hn : metric_space N]
 include Hm Hn
 open topology set
 
 -- the ε - δ definition of continuity is equivalent to the topological definition
-theorem continuous_at_intro {f : M → N} {x : M}
+
-        (H : ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, dist x' x < δ → dist (f x') (f x) < ε) :
+theorem continuous_at_within_intro {f : M → N} {x : M} {s : set M}
-        continuous_at f x :=
+        (H : ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ∈ s → dist x' x < δ → dist (f x') (f x) < ε) :
+  continuous_at_on f x s :=
   begin
-    rewrite ↑continuous_at,
+    intro U Uopen HfU,
-    intros U Uopen HfU,
     cases exists_open_ball_subset_of_Open_of_mem Uopen HfU with r Hr,
     cases Hr with Hr HUr,
     cases H Hr with δ Hδ,
@@ -633,15 +563,15 @@ theorem continuous_at_intro {f : M → N} {x : M}
     intro y Hy,
     apply mem_preimage,
     apply HUr,
-    note Hy'' := Hx'δ Hy,
+    apply Hx'δ,
-    exact Hy''
+    apply and.right Hy,
+    apply and.left Hy
   end
 
-theorem continuous_at_elim {f : M → N} {x : M} (Hfx : continuous_at f x) :
+theorem continuous_at_on_dest {f : M → N} {x : M} {s : set M} (Hfx : continuous_at_on f x s) :
-        ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, dist x' x < δ → dist (f x') (f x) < ε :=
+         ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ∈ s → dist x' x < δ → dist (f x') (f x) < ε :=
   begin
     intros ε Hε,
-    rewrite [↑continuous_at at Hfx],
     cases @Hfx (open_ball (f x) ε) !Open_open_ball (mem_open_ball _ Hε) with V HV,
     cases HV with HV HVx,
     cases HVx with HVx HVf,
@@ -650,94 +580,58 @@ theorem continuous_at_elim {f : M → N} {x : M} (Hfx : continuous_at f x) :
     existsi δ,
     split,
     exact Hδ,
-    intro x' Hx',
+    intro x' Hx's Hx',
     apply HVf,
+    apply and.intro,
     apply Hδx,
-    apply Hx',
+    exact Hx',
+    exact Hx's
   end
 
---<<<<<<< HEAD
+theorem continuous_at_intro {f : M → N} {x : M}
-theorem continuous_at_of_converges_to_at {f : M → N} {x : M} (Hf : f ⟶ f x [at x]) :
+        (H : ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, dist x' x < δ → dist (f x') (f x) < ε) :
-/-=======
+        continuous_at f x :=
-theorem continuous_at_on_intro {f : M → N} {x : M} {s : set M}
+  continuous_at_of_continuous_at_on_univ
-        (H : ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀₀ x' ∈ s, dist x' x < δ → dist (f x') (f x) < ε) :
+    (continuous_at_within_intro
-        continuous_at_on f x s :=
+      (take ε, suppose ε > 0,
-  begin
+      obtain δ (Hδ : δ > 0 ∧ ∀ ⦃x'⦄, dist x' x < δ → dist (f x') (f x) < ε), from H this,
-    intro t HOt Hfxt,
+      exists.intro δ (and.intro
-    cases ex_Open_ball_subset_of_Open_of_nonempty HOt Hfxt with ε Hε,
+      (show δ > 0, from and.left Hδ)
-    cases H (and.left Hε) with δ Hδ,
+      (take x' H' Hx', and.right Hδ _ Hx'))))
-    existsi (open_ball x δ),
-    split,
-    apply open_ball_open,
-    split,
-    apply mem_open_ball,
-    apply and.left Hδ,
-    intro x' Hx',
-    apply mem_preimage,
-    apply mem_of_subset_of_mem,
-    apply and.right Hε,
-    apply and.intro !mem_univ,
-    rewrite dist_comm,
-    apply and.right Hδ,
-    apply and.right Hx',
-    rewrite dist_comm,
-    apply and.right (and.left Hx')
-  end
 
-theorem continuous_at_on_elim {f : M → N} {x : M} {s : set M} (Hfs : continuous_at_on f x s) :
+theorem continuous_at_dest {f : M → N} {x : M} (Hfx : continuous_at f x) :
-         ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀₀ x' ∈ s, dist x' x < δ → dist (f x') (f x) < ε :=
+        ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, dist x' x < δ → dist (f x') (f x) < ε :=
   begin
     intro ε Hε,
-    unfold continuous_at_on at Hfs,
+    cases continuous_at_on_dest (continuous_at_on_univ_of_continuous_at Hfx) Hε with δ Hδ,
-    cases @Hfs (open_ball (f x) ε) !open_ball_open (mem_open_ball _ Hε) with u Hu,
-    cases Hu with Huo Hu,
-    cases Hu with Hxu Hu,
-    cases ex_Open_ball_subset_of_Open_of_nonempty Huo Hxu with δ Hδ,
     existsi δ,
     split,
     exact and.left Hδ,
-    intros x' Hx's Hx'x,
+    intro x' Hx',
-    have Hims : f ' (u ∩ s) ⊆ open_ball (f x) ε, begin
+    apply and.right Hδ,
-      apply subset.trans (image_subset f Hu),
+    apply mem_univ,
-      apply image_preimage_subset
+    apply Hx'
-    end,
-    have Hx'int : x' ∈ u ∩ s, begin
-      apply and.intro,
-      apply mem_of_subset_of_mem,
-      apply and.right Hδ,
-      apply and.intro !mem_univ,
-      rewrite dist_comm,
-      repeat assumption
-    end,
-    have Hxx' : f x' ∈ open_ball (f x) ε, begin
-      apply mem_of_subset_of_mem,
-      apply Hims,
-      apply mem_image_of_mem,
-      apply Hx'int
-    end,
-    rewrite dist_comm,
-    apply and.right Hxx'
   end
 
 theorem continuous_on_intro {f : M → N} {s : set M}
-        (H : ∀ x, ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀₀ x' ∈ s, dist x' x < δ → dist (f x') (f x) < ε) :
+        (H : ∀ x ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ∈ s → dist x' x < δ → dist (f x') (f x) < ε) :
         continuous_on f s :=
-  begin
+  continuous_on_of_forall_continuous_at_on (λ x, continuous_at_within_intro (H x))
-    apply continuous_on_of_forall_continuous_at_on,
-    intro x,
-    apply continuous_at_on_intro,
-    apply H
-  end
 
-theorem continuous_on_elim {f : M → N} {s : set M} (Hfs : continuous_on f s) :
+theorem continuous_on_dest {f : M → N} {s : set M} (H : continuous_on f s) {x : M} (Hxs : x ∈ s) :
-        ∀₀ x ∈ s, ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀₀ x' ∈ s, dist x' x < δ → dist (f x') (f x) < ε :=
+        ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ∈ s → dist x' x < δ → dist (f x') (f x) < ε :=
-  begin
+  continuous_at_on_dest (continuous_at_on_of_continuous_on H Hxs)
-    intros x Hx,
-    exact continuous_at_on_elim (continuous_at_on_of_continuous_on Hfs Hx)
-  end-/
 
---theorem continuous_at_of_converges_to_at {f : M → N} {x : M} (Hf : f ⟶ f x at x) :
+theorem continuous_intro {f : M → N}
--->>>>>>> feat(theories/analysis): intro/elim rules for continuous_on, etc
+        (H : ∀ x ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, dist x' x < δ → dist (f x') (f x) < ε) :
+        continuous f :=
+  continuous_of_forall_continuous_at (λ x, continuous_at_intro (H x))
+
+theorem continuous_dest {f : M → N} (H : continuous f) (x : M) :
+         ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, dist x' x < δ → dist (f x') (f x) < ε :=
+  continuous_at_dest (forall_continuous_at_of_continuous H x)
+
+theorem continuous_at_of_converges_to_at {f : M → N} {x : M} (Hf : f ⟶ f x [at x]) :
   continuous_at f x :=
 continuous_at_intro
 (take ε, suppose ε > 0,
@@ -755,11 +649,9 @@ theorem converges_to_at_of_continuous_at {f : M → N} {x : M} (Hf : continuous_
   f ⟶ f x [at x] :=
 approaches_at_intro
   (take ε, suppose ε > 0,
-    obtain δ [δpos Hδ], from continuous_at_elim Hf this,
+    obtain δ [δpos Hδ], from continuous_at_dest Hf this,
     exists.intro δ (and.intro δpos (λ x' Hx' xnex', Hδ x' Hx')))
 
---definition continuous (f : M → N) : Prop := ∀ x, continuous_at f x
-
 theorem converges_seq_comp_of_converges_seq_of_cts (X : ℕ → M) [HX : converges_seq X] {f : M → N}
         (Hf : continuous f) :
         converges_seq (λ n, f (X n)) :=
@@ -768,7 +660,7 @@ theorem converges_seq_comp_of_converges_seq_of_cts (X : ℕ → M) [HX : converg
     existsi f xlim,
     apply approaches_at_infty_intro,
     intros ε Hε,
-    let Hcont := (continuous_at_elim (forall_continuous_at_of_continuous Hf xlim)) Hε,
+    let Hcont := (continuous_at_dest (forall_continuous_at_of_continuous Hf xlim)) Hε,
     cases Hcont with δ Hδ,
     cases approaches_at_infty_dest Hxlim (and.left Hδ) with B HB,
     existsi B,
@@ -777,22 +669,10 @@ theorem converges_seq_comp_of_converges_seq_of_cts (X : ℕ → M) [HX : converg
     apply HB Hn
   end
 
-omit Hn
-theorem id_continuous : continuous (λ x : M, x) :=
-  begin
-    apply continuous_of_forall_continuous_at,
-    intros x,
-    apply continuous_at_intro,
-    intro ε Hε,
-    existsi ε,
-    split,
-    assumption,
-    intros,
-    assumption
-  end
-
 end continuity
 
+end metric_space
+
 end analysis
 
 

library/theories/analysis/normed_space.lean

@@ -6,7 +6,7 @@ Author: Jeremy Avigad
 Normed spaces.
 -/
 import algebra.module .metric_space
-open real nat classical topology analysis
+open real nat classical topology analysis analysis.metric_space
 noncomputable theory
 
 structure has_norm [class] (M : Type) : Type :=
@@ -79,6 +79,8 @@ namespace analysis
   proposition norm_sub (u v : V) : ∥u - v∥ = ∥v - u∥ :=
     by rewrite [-norm_neg, neg_sub]
 
+  proposition norm_ne_zero_of_ne_zero {u : V} (H : u ≠ 0) : ∥u∥ ≠ 0 :=
+  suppose ∥u∥ = 0, H (eq_zero_of_norm_eq_zero this)
 
 end analysis
 
@@ -117,7 +119,7 @@ section
 
   open nat
 
-  proposition converges_to_seq_norm_elim {X : ℕ → V} {x : V} (H : X ⟶ x [at ∞]) :
+  proposition approaches_seq_norm_elim {X : ℕ → V} {x : V} (H : X ⟶ x [at ∞]) :
     ∀ {ε : ℝ}, ε > 0 → ∃ N₁ : ℕ, ∀ {n : ℕ}, n ≥ N₁ → ∥ X n - x ∥ < ε :=
   approaches_at_infty_dest H
 
@@ -147,137 +149,274 @@ definition banach_space_to_metric_space [trans_instance] (V : Type) [bsV : banac
 ⦄
 
 namespace analysis
+
+-- unfold some common definitions fully (copied from metric space, updated for normed_space notation)
+-- TODO: copy these for ℝ as well?
+namespace normed_vector_space
+section
+open set topology set.filter
+variables {M N : Type}
+--variable [HU : normed_vector_space U]
+variable [normed_vector_space M]
+--variables {f g : U → V}
+
+section approaches
+  variables {X : Type} {F : filter X} {f : X → M} {y : M}
+
+  proposition approaches_intro (H : ∀ ε, ε > 0 → eventually (λ x, ∥(f x) - y∥ < ε) F) :
+    (f ⟶ y) F :=
+  approaches_intro H
+
+  proposition approaches_dest (H : (f ⟶ y) F) {ε : ℝ} (εpos : ε > 0) :
+    eventually (λ x, ∥(f x) - y∥ < ε) F :=
+  approaches_dest H εpos
+
+  variables (F f y)
+
+  proposition approaches_iff : ((f ⟶ y) F) ↔ (∀ ε, ε > 0 → eventually (λ x, ∥(f x) - y∥ < ε) F) :=
+  iff.intro approaches_dest approaches_intro
+
+end approaches
+
+proposition approaches_at_infty_intro {f : ℕ → M} {y : M}
+    (H : ∀ ε, ε > 0 → ∃ N, ∀ n, n ≥ N → ∥(f n) - y∥ < ε) :
+  f ⟶ y [at ∞] :=
+approaches_at_infty_intro H
+
+proposition approaches_at_infty_dest {f : ℕ → M} {y : M}
+    (H : f ⟶ y [at ∞]) ⦃ε : ℝ⦄ (εpos : ε > 0) :
+  ∃ N, ∀ ⦃n⦄, n ≥ N → ∥(f n) - y∥ < ε :=
+approaches_at_infty_dest H εpos
+
+proposition approaches_at_infty_iff (f : ℕ → M) (y : M) :
+  f ⟶ y [at ∞] ↔ (∀ ε, ε > 0 → ∃ N, ∀ ⦃n⦄, n ≥ N → ∥(f n) - y∥ < ε) :=
+iff.intro approaches_at_infty_dest approaches_at_infty_intro
+
+variable [normed_vector_space N]
+
+proposition approaches_at_dest {f : M → N} {y : N} {x : M}
+    (H : f ⟶ y [at x]) ⦃ε : ℝ⦄ (εpos : ε > 0) :
+  ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, ∥x' - x∥ < δ → x' ≠ x → ∥(f x') - y∥ < ε :=
+approaches_at_dest H εpos
+
+proposition approaches_at_intro {f : M → N} {y : N} {x : M}
+    (H : ∀ ε, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, ∥x' - x∥ < δ → x' ≠ x → ∥(f x') - y∥ < ε) :
+  f ⟶ y [at x] :=
+approaches_at_intro H
+
+proposition approaches_at_iff (f : M → N) (y : N) (x : M) : f ⟶ y [at x] ↔
+    (∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, ∥x' - x∥ < δ → x' ≠ x → ∥(f x') - y∥ < ε) :=
+iff.intro approaches_at_dest approaches_at_intro
+
+end
+end normed_vector_space
+
+
+section
 variable {V : Type}
 variable [normed_vector_space V]
+variable {A : Type}
+variables {X : A → V}
+variables {x : V}
 
-variables {X Y : ℕ → V}
+proposition neg_approaches {F} (HX : (X ⟶ x) F) :
-variables {x y : V}
+  ((λ n, - X n) ⟶ - x) F :=
-
-proposition add_converges_to_seq (HX : X ⟶ x [at ∞]) (HY : Y ⟶ y [at ∞]) :
-  (λ n, X n + Y n) ⟶ x + y [at ∞] :=
-approaches_at_infty_intro
-take ε : ℝ, suppose ε > 0,
-have e2pos : ε / 2 > 0, from  div_pos_of_pos_of_pos `ε > 0` two_pos,
-obtain (N₁ : ℕ) (HN₁ : ∀ {n}, n ≥ N₁ → ∥ X n - x ∥ < ε / 2),
-  from converges_to_seq_norm_elim HX e2pos,
-obtain (N₂ : ℕ) (HN₂ : ∀ {n}, n ≥ N₂ → ∥ Y n - y ∥ < ε / 2),
-  from converges_to_seq_norm_elim HY e2pos,
-let N := max N₁ N₂ in
-exists.intro N
-  (take n,
-    suppose n ≥ N,
-    have ngtN₁ : n ≥ N₁, from nat.le_trans !le_max_left `n ≥ N`,
-    have ngtN₂ : n ≥ N₂, from nat.le_trans !le_max_right `n ≥ N`,
-    show ∥ (X n + Y n) - (x + y) ∥ < ε, from calc
-      ∥ (X n + Y n) - (x + y) ∥
-            = ∥ (X n - x) + (Y n - y) ∥   : by rewrite [sub_add_eq_sub_sub, *sub_eq_add_neg,
-                                                         *add.assoc, add.left_comm (-x)]
-        ... ≤ ∥ X n - x ∥ + ∥ Y n - y ∥   : norm_triangle
-        ... < ε / 2 + ε / 2               : add_lt_add (HN₁ ngtN₁) (HN₂ ngtN₂)
-        ... = ε                           : add_halves)
-
-private lemma smul_converges_to_seq_aux {c : ℝ} (cnz : c ≠ 0) (HX : X ⟶ x [at ∞]) :
-  (λ n, c • X n) ⟶ c • x [at ∞] :=
-approaches_at_infty_intro
-take ε : ℝ, suppose ε > 0,
-have abscpos : abs c > 0, from abs_pos_of_ne_zero cnz,
-have epos : ε / abs c > 0, from div_pos_of_pos_of_pos `ε > 0` abscpos,
-obtain N (HN : ∀ {n}, n ≥ N → norm (X n - x) < ε / abs c), from converges_to_seq_norm_elim HX epos,
-exists.intro N
-  (take n,
-    suppose n ≥ N,
-    have H : norm (X n - x) < ε / abs c, from HN this,
-    show norm (c • X n - c • x) < ε, from calc
-      norm (c • X n - c • x)
-            = abs c * norm (X n - x) : by rewrite [-smul_sub_left_distrib, norm_smul]
-        ... < abs c * (ε / abs c)    : mul_lt_mul_of_pos_left H abscpos
-        ... = ε                      : mul_div_cancel' (ne_of_gt abscpos))
-
-proposition smul_converges_to_seq (c : ℝ) (HX : X ⟶ x [at ∞]) :
-  (λ n, c • X n) ⟶ c • x [at ∞] :=
-by_cases
-  (assume cz : c = 0,
-    have (λ n, c • X n) = (λ n, 0), from funext (take x, by rewrite [cz, zero_smul]),
-    begin rewrite [this, cz, zero_smul], apply approaches_constant end)
-  (suppose c ≠ 0, smul_converges_to_seq_aux this HX)
-
-proposition neg_converges_to_seq (HX : X ⟶ x [at ∞]) :
-  (λ n, - X n) ⟶ - x [at ∞] :=
-approaches_at_infty_intro
-take ε, suppose ε > 0,
-obtain N (HN : ∀ {n}, n ≥ N → norm (X n - x) < ε), from converges_to_seq_norm_elim HX this,
-exists.intro N
-  (take n,
-    suppose n ≥ N,
-    show norm (- X n - (- x)) < ε,
-      by rewrite [-neg_neg_sub_neg, *neg_neg, norm_neg]; exact HN `n ≥ N`)
-
-proposition neg_converges_to_seq_iff : ((λ n, - X n) ⟶ - x [at ∞]) ↔ (X ⟶ x [at ∞]) :=
-have aux : X = λ n, (- (- X n)), from funext (take n, by rewrite neg_neg),
-iff.intro
-  (assume H : (λ n, -X n)⟶ -x [at ∞],
-    show X ⟶ x [at ∞], by rewrite [aux, -neg_neg x]; exact neg_converges_to_seq H)
-  neg_converges_to_seq
-
-proposition norm_converges_to_seq_zero (HX : X ⟶ 0 [at ∞]) : (λ n, norm (X n)) ⟶ 0 [at ∞] :=
-approaches_at_infty_intro
-take ε, suppose ε > 0,
-obtain N (HN : ∀ n, n ≥ N → norm (X n - 0) < ε), from approaches_at_infty_dest HX `ε > 0`,
-exists.intro N
-  (take n, assume Hn : n ≥ N,
-    have norm (X n) < ε, begin rewrite -(sub_zero (X n)), apply HN n Hn end,
-    show abs (norm (X n) - 0) < ε,
-      by rewrite [sub_zero, abs_of_nonneg !norm_nonneg]; apply this)
-
-proposition converges_to_seq_zero_of_norm_converges_to_seq_zero
-    (HX : (λ n, norm (X n)) ⟶ 0 [at ∞]) :
-  X ⟶ 0 [at ∞] :=
-approaches_at_infty_intro
-take ε, suppose ε > 0,
-obtain N (HN : ∀ n, n ≥ N → abs (norm (X n) - 0) < ε), from approaches_at_infty_dest HX `ε > 0`,
-exists.intro (N : ℕ)
-  (take n : ℕ, assume Hn : n ≥ N,
-    have HN' : abs (norm (X n) - 0) < ε, from HN n Hn,
-    have norm (X n) < ε,
-      by rewrite [sub_zero at HN', abs_of_nonneg !norm_nonneg at HN']; apply HN',
-    show norm (X n - 0) < ε,
-      by rewrite sub_zero; apply this)
-
-proposition norm_converges_to_seq_zero_iff (X : ℕ → V) :
-  ((λ n, norm (X n)) ⟶ 0 [at ∞]) ↔ (X ⟶ 0 [at ∞]) :=
-iff.intro converges_to_seq_zero_of_norm_converges_to_seq_zero norm_converges_to_seq_zero
-
-end analysis
-
-namespace analysis
-variables {U V : Type}
-variable [HU : normed_vector_space U]
-variable [HV : normed_vector_space V]
-variables f g : U → V
-
-include HU HV
-
-theorem add_converges_to_at {lf lg : V} {x : U} (Hf : f ⟶ lf at x) (Hg : g ⟶ lg at x) :
-        (λ y, f y + g y) ⟶ lf + lg at x :=
   begin
-    apply converges_to_at_of_all_conv_seqs,
+    apply normed_vector_space.approaches_intro,
-    intro X HX,
+    intro ε Hε,
-    apply add_converges_to_seq,
+    apply set.filter.eventually_mono (approaches_dest HX Hε),
-    apply all_conv_seqs_of_converges_to_at Hf,
+    intro x' Hx',
-    apply HX,
+    rewrite [-norm_neg, neg_neg_sub_neg],
-    apply all_conv_seqs_of_converges_to_at Hg,
+    apply Hx'
-    apply HX
   end
 
-open topology
+proposition approaches_neg {F} (Hx : ((λ n, - X n) ⟶ - x) F) : (X ⟶ x) F :=
+  have aux : X = λ n, (- (- X n)), from funext (take n, by rewrite neg_neg),
+  by rewrite [aux, -neg_neg x]; exact neg_approaches Hx
 
-theorem normed_vector_space.continuous_at_intro {x : U}
+proposition neg_approaches_iff {F} : (((λ n, - X n) ⟶ - x) F) ↔ ((X ⟶ x) F) :=
+have aux : X = λ n, (- (- X n)), from funext (take n, by rewrite neg_neg),
+iff.intro approaches_neg neg_approaches
+
+proposition norm_approaches_zero_of_approaches_zero {F} (HX : (X ⟶ 0) F) : ((λ n, norm (X n)) ⟶ 0) F :=
+  begin
+    apply metric_space.approaches_intro,
+    intro ε Hε,
+    apply set.filter.eventually_mono (approaches_dest HX Hε),
+    intro x Hx,
+    change abs (∥X x∥ - 0) < ε,
+    rewrite [sub_zero, abs_of_nonneg !norm_nonneg, -sub_zero (X x)],
+    apply Hx
+  end
+
+proposition approaches_zero_of_norm_approaches_zero
+    {F} (HX : ((λ n, norm (X n)) ⟶ 0) F) :
+  (X ⟶ 0) F :=
+  begin
+    apply normed_vector_space.approaches_intro,
+    intro ε Hε,
+    apply set.filter.eventually_mono (approaches_dest HX Hε),
+    intro x Hx,
+    apply lt_of_abs_lt,
+    rewrite [sub_zero, -sub_zero ∥X x∥],
+    apply Hx
+  end
+
+proposition norm_approaches_zero_iff (X : ℕ → V) (F) :
+  (((λ n, norm (X n)) ⟶ 0) F) ↔ ((X ⟶ 0) F) :=
+iff.intro approaches_zero_of_norm_approaches_zero norm_approaches_zero_of_approaches_zero
+
+end
+
+
+section
+variables {U V : Type}
+--variable [HU : normed_vector_space U]
+variable [HV : normed_vector_space V]
+variables {f g : U → V}
+open set-- filter causes error??
+include  HV
+
+theorem add_approaches {lf lg : V} {F : filter U} (Hf : (f ⟶ lf) F) (Hg : (g ⟶ lg) F) :
+        ((λ y, f y + g y) ⟶ lf + lg) F :=
+  begin
+    apply normed_vector_space.approaches_intro,
+    intro ε Hε,
+    have e2pos : ε / 2 > 0, from div_pos_of_pos_of_pos Hε two_pos,
+    have Hfl : filter.eventually (λ x, dist (f x) lf < ε / 2) F, from approaches_dest Hf e2pos,
+    have Hgl : filter.eventually (λ x, dist (g x) lg < ε / 2) F, from approaches_dest Hg e2pos,
+    apply filter.eventually_mono,
+    apply filter.eventually_and Hfl Hgl,
+    intro x Hfg,
+    rewrite [add_sub_comm, -add_halves ε],
+    apply lt_of_le_of_lt,
+    apply norm_triangle,
+    cases Hfg with Hf' Hg',
+    apply add_lt_add,
+    exact Hf', exact Hg'
+  end
+
+theorem smul_approaches {lf : V} {F : filter U} (Hf : (f ⟶ lf) F) (s : ℝ) :
+        ((λ y, s • f y) ⟶ s • lf) F :=
+  begin
+    apply normed_vector_space.approaches_intro,
+    intro ε Hε,
+    cases em (s = 0) with seq sneq,
+    {have H : (λ x, ∥(s • f x) - (s • lf)∥ < ε) = (λ x, true),
+      begin apply funext, intro x, rewrite [seq, 2 zero_smul, sub_zero, norm_zero, eq_true], exact Hε end,
+    rewrite H,
+    apply filter.eventually_true},
+    {have e2pos : ε / abs s > 0, from div_pos_of_pos_of_pos Hε (abs_pos_of_ne_zero sneq),
+    have H : filter.eventually (λ x, ∥(f x) - lf∥ < ε / abs s) F, from approaches_dest Hf e2pos,
+    apply filter.eventually_mono H,
+    intro x Hx,
+    rewrite [-smul_sub_left_distrib, norm_smul, mul.comm],
+    apply mul_lt_of_lt_div,
+    apply abs_pos_of_ne_zero sneq,
+    apply Hx}
+  end
+
+end
+
+namespace normed_vector_space
+variables {U V : Type}
+variables [HU : normed_vector_space U] [HV : normed_vector_space V]
+variables {f g : U → V}
+include HU HV
+open set
+
+theorem continuous_at_within_intro {x : U} {s : set U}
+        (H : ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ∈ s → ∥x' - x∥ < δ → ∥(f x') - (f x)∥ < ε) :
+  continuous_at_on f x s :=
+  metric_space.continuous_at_within_intro H
+
+theorem continuous_at_on_dest {x : U} {s : set U} (Hfx : continuous_at_on f x s) :
+         ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ∈ s → ∥x' - x∥ < δ → ∥(f x') - (f x)∥ < ε :=
+  metric_space.continuous_at_on_dest Hfx
+
+theorem continuous_on_intro {s : set U}
+        (H : ∀ x ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ∈ s → ∥x' - x∥ < δ → ∥(f x') - (f x)∥ < ε) :
+        continuous_on f s :=
+  metric_space.continuous_on_intro H
+
+theorem continuous_on_dest {s : set U} (H : continuous_on f s) {x : U} (Hxs : x ∈ s) :
+        ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ∈ s → ∥x' - x∥ < δ → ∥(f x') - (f x)∥ < ε :=
+  metric_space.continuous_on_dest H Hxs
+
+theorem continuous_intro
+        (H : ∀ x ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, ∥x' - x∥ < δ → ∥(f x') - (f x)∥ < ε) :
+        continuous f :=
+  metric_space.continuous_intro H
+
+theorem continuous_dest (H : continuous f) (x : U) :
+         ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, ∥x' - x∥ < δ → ∥(f x') - (f x)∥ < ε :=
+  metric_space.continuous_dest H x
+
+theorem continuous_at_intro {x : U}
         (H : ∀ ε : ℝ, ε > 0 → (∃ δ : ℝ, δ > 0 ∧ ∀ x' : U, ∥x' - x∥ < δ → ∥f x' - f x∥ < ε)) :
         continuous_at f x :=
-  continuous_at_intro H
+  metric_space.continuous_at_intro H
 
-theorem normed_vector_space.continuous_at_elim {x : U} (H : continuous_at f x) :
+theorem continuous_at_dest {x : U} (H : continuous_at f x) :
          ∀ ε : ℝ, ε > 0 → (∃ δ : ℝ, δ > 0 ∧ ∀ x' : U, ∥x' - x∥ < δ → ∥f x' - f x∥ < ε) :=
-  continuous_at_elim H
+  metric_space.continuous_at_dest H
+
+end normed_vector_space
+
+section
+
+open topology
+variables {U V : Type}
+variables [HU : normed_vector_space U] [HV : normed_vector_space V]
+variables {f g : U → V}
+include HU HV
+
+theorem neg_continuous (Hf : continuous f) : continuous (λ x : U, - f x) :=
+  begin
+    apply continuous_of_forall_continuous_at,
+    intro x,
+    apply continuous_at_of_tendsto_at,
+    apply neg_approaches,
+    apply tendsto_at_of_continuous_at,
+    apply forall_continuous_at_of_continuous,
+    apply Hf
+  end
+
+theorem add_continuous (Hf : continuous f) (Hg : continuous g) : continuous (λ x, f x + g x) :=
+  begin
+    apply continuous_of_forall_continuous_at,
+    intro y,
+    apply continuous_at_of_tendsto_at,
+    apply add_approaches,
+    all_goals apply tendsto_at_of_continuous_at,
+    all_goals apply forall_continuous_at_of_continuous,
+    repeat assumption
+  end
+
+theorem sub_continuous (Hf : continuous f) (Hg : continuous g) : continuous (λ x, f x - g x) :=
+  begin
+    apply continuous_of_forall_continuous_at,
+    intro y,
+    apply continuous_at_of_tendsto_at,
+    apply add_approaches,
+    all_goals apply tendsto_at_of_continuous_at,
+    all_goals apply forall_continuous_at_of_continuous,
+    assumption,
+    apply neg_continuous,
+    assumption
+  end
+
+theorem smul_continuous (s : ℝ) (Hf : continuous f) : continuous (λ x : U, s • f x) :=
+  begin
+    apply continuous_of_forall_continuous_at,
+    intro y,
+    apply continuous_at_of_tendsto_at,
+    apply smul_approaches,
+    apply tendsto_at_of_continuous_at,
+    apply forall_continuous_at_of_continuous,
+    assumption
+  end
+
+end
 
 end analysis

library/theories/analysis/real_deriv.lean

@@ -6,7 +6,7 @@ Author: Robert Y. Lewis
 Derivatives on ℝ
 -/
 import .bounded_linear_operator
-open real nat classical topology analysis
+open real nat classical topology analysis set
 noncomputable theory
 
 namespace real
@@ -19,42 +19,42 @@ theorem add_sub_self (a b : ℝ) : a + b - a = b :=
 
 definition derivative_at (f : ℝ → ℝ) (d x : ℝ) := is_frechet_deriv_at f (λ t, d • t) x
 
-theorem derivative_at_intro (f : ℝ → ℝ) (d x : ℝ) (H : (λ h, (f (x + h) - f x) / h) ⟶ d at 0) :
+theorem derivative_at_intro (f : ℝ → ℝ) (d x : ℝ) (H : (λ h, (f (x + h) - f x) / h) ⟶ d [at 0]) :
         derivative_at f d x :=
   begin
     apply is_frechet_deriv_at_intro,
     intros ε Hε,
-    cases H Hε with δ Hδ,
+    cases approaches_at_dest H Hε with δ Hδ,
     existsi δ,
     split,
     exact and.left Hδ,
     intro y Hy,
     rewrite [-sub_zero y at Hy{2}],
-    note Hδ' := and.right Hδ y Hy,
+    note Hδ' := and.right Hδ y (and.right Hy) (and.left Hy),
     have Hδ'' : abs ((f (x + y) - f x - d * y) / y) < ε,
       by rewrite [-div_sub_div_same, mul_div_cancel _ (and.left Hy)]; apply Hδ',
     show abs (f (x + y) - f x - d * y) / abs y < ε, by rewrite -abs_div; apply Hδ''
   end
 
+theorem derivative_at_of_frechet_derivative_at {f g : ℝ → ℝ} [is_bdd_linear_map g] {d x : ℝ}
+        (H : is_frechet_deriv_at f g x) (Hg : g = λ x, d * x) :
+        derivative_at f d x :=
+  by apply is_frechet_deriv_at_of_eq H Hg
+
 theorem deriv_at_const (c x : ℝ) : derivative_at (λ t, c) 0 x :=
-  begin
+  derivative_at_of_frechet_derivative_at
-    apply derivative_at_intro,
+    (@frechet_deriv_at_const ℝ ℝ _ _ _ c)
-    have (λ h, (c - c) / h) = (λ h, 0), from funext (λ h, by rewrite [sub_self, zero_div]),
+    (funext (λ v, by rewrite zero_mul))
-    rewrite this,
-    apply converges_to_at_constant
-  end
 
 theorem deriv_at_id (x : ℝ) : derivative_at (λ t, t) 1 x :=
-  begin
+  derivative_at_of_frechet_derivative_at
-    apply derivative_at_intro,
+    (@frechet_deriv_at_id ℝ ℝ _ _ _)
-    apply converges_to_at_real_intro,
+    (funext (λ v, by rewrite one_mul))
-    intros ε Hε,
+
-    existsi 1,
+theorem deriv_at_mul {f : ℝ → ℝ} {d x : ℝ} (H : derivative_at f d x) (c : ℝ) :
-    split,
+        derivative_at (λ t, c * f t) (c * d) x :=
-    exact zero_lt_one,
+  derivative_at_of_frechet_derivative_at
-    intros x' Hx',
+    (frechet_deriv_at_smul _ _ c H)
-    rewrite [add_sub_self, div_self (and.left Hx'), sub_self, abs_zero],
+    (funext (λ v, by rewrite mul.assoc))
-    exact Hε
-  end
 
 end real

library/theories/analysis/real_limit.lean

@@ -150,17 +150,19 @@ namespace analysis
 
 theorem dist_eq_abs (x y : real) : dist x y = abs (x - y) := rfl
 
-proposition converges_to_seq_real_intro {X : ℕ → ℝ} {y : ℝ}
+namespace real
+proposition approaches_at_infty_intro {X : ℕ → ℝ} {y : ℝ}
     (H : ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → abs (X n - y) < ε) :
-  (X ⟶ y [at ∞]) := approaches_at_infty_intro H
+  (X ⟶ y [at ∞]) := metric_space.approaches_at_infty_intro H
 
-proposition converges_to_seq_real_elim {X : ℕ → ℝ} {y : ℝ} (H : X ⟶ y [at ∞]) :
+proposition approaches_at_infty_dest {X : ℕ → ℝ} {y : ℝ} (H : X ⟶ y [at ∞]) :
-    ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → abs (X n - y) < ε := approaches_at_infty_dest H
+    ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → abs (X n - y) < ε := metric_space.approaches_at_infty_dest H
 
-proposition converges_to_seq_real_intro' {X : ℕ → ℝ} {y : ℝ}
+proposition approaches_at_infty_intro' {X : ℕ → ℝ} {y : ℝ}
     (H : ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → abs (X n - y) ≤ ε) :
   (X ⟶ y [at ∞]) :=
 approaches_at_infty_intro' H
+end real
 
 open pnat subtype
 local postfix ⁻¹ := pnat.inv
@@ -205,7 +207,7 @@ theorem converges_seq_of_cauchy {X : ℕ → ℝ} (H : cauchy X) : converges_seq
 obtain l Nb (conv : converges_to_with_rate (r_seq_of X) l Nb),
   from converges_to_with_rate_of_cauchy H,
 exists.intro l
-  (approaches_at_infty_intro
+  (real.approaches_at_infty_intro
     take ε : ℝ,
     suppose ε > 0,
     obtain (k' : ℕ) (Hn : 1 / succ k' < ε), from archimedean_small `ε > 0`,
@@ -249,184 +251,271 @@ definition banach_space_real [trans_instance] : banach_space ℝ :=
   complete                := λ X H, analysis.complete ℝ H
 ⦄
 
+namespace real
+open topology set
+open normed_vector_space
+
+section
+variable {f : ℝ → ℝ}
+
+theorem continuous_dest (H : continuous f) :
+  ∀ x : ℝ, ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ δ : ℝ, δ > 0 ∧ ∀ x' : ℝ,
+    abs (x' - x) < δ → abs (f x' - f x) < ε :=
+normed_vector_space.continuous_dest H
+
+theorem continuous_intro
+  (H : ∀ x : ℝ, ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ δ : ℝ, δ > 0 ∧ ∀ x' : ℝ,
+    abs (x' - x) < δ → abs (f x' - f x) < ε) :
+  continuous f :=
+normed_vector_space.continuous_intro H
+
+theorem continuous_at_dest {x : ℝ} (H : continuous_at f x) :
+         ∀ ε : ℝ, ε > 0 → (∃ δ : ℝ, δ > 0 ∧ ∀ x' : ℝ, abs (x' - x) < δ → abs (f x' - f x) < ε) :=
+normed_vector_space.continuous_at_dest H
+
+theorem continuous_at_intro {x : ℝ}
+  (H : ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ δ : ℝ, δ > 0 ∧ ∀ x' : ℝ,
+    abs (x' - x) < δ → abs (f x' - f x) < ε) :
+  continuous_at f x :=
+normed_vector_space.continuous_at_intro H
+
+theorem continuous_at_within_intro {x : ℝ} {s : set ℝ}
+        (H : ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ∈ s → abs (x' - x) < δ → abs ((f x') - (f x)) < ε) :
+  continuous_at_on f x s :=
+normed_vector_space.continuous_at_within_intro H
+
+
+theorem continuous_at_on_dest {x : ℝ} {s : set ℝ} (Hfx : continuous_at_on f x s) :
+         ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ∈ s → abs (x' - x) < δ → abs ((f x') - (f x)) < ε :=
+normed_vector_space.continuous_at_on_dest Hfx
+
+theorem continuous_on_intro {s : set ℝ}
+        (H : ∀ x ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ∈ s → abs (x' - x) < δ → abs ((f x') - (f x)) < ε) :
+        continuous_on f s :=
+normed_vector_space.continuous_on_intro H
+
+theorem continuous_on_dest {s : set ℝ} (H : continuous_on f s) {x : ℝ} (Hxs : x ∈ s) :
+        ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ∈ s → abs (x' - x) < δ → abs ((f x') - (f x)) < ε :=
+normed_vector_space.continuous_on_dest H Hxs
+
+end
+
+section approaches
+open set.filter set topology
+  variables {X : Type} {F : filter X} {f : X → ℝ} {y : ℝ}
+
+  proposition approaches_intro (H : ∀ ε, ε > 0 → eventually (λ x, abs ((f x) - y) < ε) F) :
+    (f ⟶ y) F :=
+  normed_vector_space.approaches_intro H
+
+  proposition approaches_dest (H : (f ⟶ y) F) {ε : ℝ} (εpos : ε > 0) :
+    eventually (λ x, abs ((f x) - y) < ε) F :=
+  normed_vector_space.approaches_dest H εpos
+
+  variables (F f y)
+
+  proposition approaches_iff : ((f ⟶ y) F) ↔ (∀ ε, ε > 0 → eventually (λ x, abs ((f x) - y) < ε) F) :=
+  iff.intro approaches_dest approaches_intro
+
+end approaches
+
+proposition approaches_at_infty_intro {f : ℕ → ℝ} {y : ℝ}
+    (H : ∀ ε, ε > 0 → ∃ N, ∀ n, n ≥ N → abs ((f n) - y) < ε) :
+  f ⟶ y [at ∞] :=
+normed_vector_space.approaches_at_infty_intro H
+
+proposition approaches_at_infty_dest {f : ℕ → ℝ} {y : ℝ}
+    (H : f ⟶ y [at ∞]) ⦃ε : ℝ⦄ (εpos : ε > 0) :
+  ∃ N, ∀ ⦃n⦄, n ≥ N → abs ((f n) - y) < ε :=
+normed_vector_space.approaches_at_infty_dest H εpos
+
+proposition approaches_at_infty_iff (f : ℕ → ℝ) (y : ℝ) :
+  f ⟶ y [at ∞] ↔ (∀ ε, ε > 0 → ∃ N, ∀ ⦃n⦄, n ≥ N → abs ((f n) - y) < ε) :=
+iff.intro approaches_at_infty_dest approaches_at_infty_intro
+
+section
+variable {f : ℝ → ℝ}
+proposition approaches_at_dest  {y x : ℝ}
+    (H : f ⟶ y [at x]) ⦃ε : ℝ⦄ (εpos : ε > 0) :
+  ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, abs (x' - x) < δ → x' ≠ x → abs ((f x') - y) < ε :=
+metric_space.approaches_at_dest H εpos
+
+proposition approaches_at_intro {y x : ℝ}
+    (H : ∀ ε, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, abs (x' - x) < δ → x' ≠ x → abs ((f x') - y) < ε) :
+  f ⟶ y [at x] :=
+metric_space.approaches_at_intro H
+
+proposition approaches_at_iff (y x : ℝ) : f ⟶ y [at x] ↔
+    (∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, abs (x' - x) < δ → x' ≠ x → abs ((f x') - y) < ε) :=
+iff.intro approaches_at_dest approaches_at_intro
+
+end
+
+end real
+
 /- limits under pointwise operations -/
 
 section limit_operations
-variables {X Y : ℕ → ℝ}
+open set
+variable {A : Type}
+variables {X Y : A → ℝ}
 variables {x y : ℝ}
+variable {F : filter A}
 
-proposition mul_left_converges_to_seq (c : ℝ) (HX : X ⟶ x [at ∞]) :
+proposition mul_left_approaches (c : ℝ) (HX : (X ⟶ x) F) :
-  (λ n, c * X n) ⟶ c * x [at ∞] :=
+  ((λ n, c * X n) ⟶ c * x) F :=
-smul_converges_to_seq c HX
+smul_approaches HX c
 
-proposition mul_right_converges_to_seq (c : ℝ) (HX : X ⟶ x [at ∞]) :
+proposition mul_right_approaches (c : ℝ) (HX : (X ⟶ x) F) :
-  (λ n, X n * c) ⟶ x * c [at ∞] :=
+  ((λ n, X n * c) ⟶ x * c) F :=
-have (λ n, X n * c) = (λ n, c * X n), from funext (take x, !mul.comm),
+have (λ n, X n * c) = (λ n, c * X n), from funext (λ n, !mul.comm),
-by rewrite [this, mul.comm]; apply mul_left_converges_to_seq c HX
+by rewrite [this, mul.comm]; apply mul_left_approaches _ HX
 
-theorem converges_to_seq_squeeze (HX : X ⟶ x [at ∞]) (HY : Y ⟶ x [at ∞]) {Z : ℕ → ℝ} (HZX : ∀ n, X n ≤ Z n)
+theorem approaches_squeeze (HX : (X ⟶ x) F) (HY : (Y ⟶ x) F)
-        (HZY : ∀ n, Z n ≤ Y n) : Z ⟶ x [at ∞] :=
+        {Z : A → ℝ} (HZX : filter.eventually (λ n, X n ≤ Z n) F) (HZY : filter.eventually (λ n, Z n ≤ Y n) F) :
+        (Z ⟶ x) F :=
   begin
-    apply approaches_at_infty_intro,
+    apply real.approaches_intro,
-    intros ε Hε,
+    intro ε Hε,
-    have Hε4 : ε / 4 > 0, from div_pos_of_pos_of_pos Hε four_pos,
+    apply filter.eventually_mp,
-    cases approaches_at_infty_dest HX Hε4 with N1 HN1,
+    rotate 1,
-    cases approaches_at_infty_dest HY Hε4 with N2 HN2,
+    apply filter.eventually_and,
-    existsi max N1 N2,
+    apply real.approaches_dest HX Hε,
-    intro n Hn,
+    apply real.approaches_dest HY Hε,
-    have HXY : abs (Y n - X n) < ε / 2, begin
+    apply filter.eventually_mono,
-      apply lt_of_le_of_lt,
+    apply filter.eventually_and HZX HZY,
-      apply abs_sub_le _ x,
+    intros x' Hlo Hdst,
-      have Hε24 : ε / 2 = ε / 4 + ε / 4, from eq.symm !add_quarters,
+    change abs (Z x' - x) < ε,
-      rewrite Hε24,
+    cases em (x ≤ Z x') with HxleZ HxnleZ, -- annoying linear arith
-      apply add_lt_add,
+    {have Y x' - x = (Z x' - x) + (Y x' - Z x'), by rewrite -sub_eq_sub_add_sub,
-      apply HN2,
+    have H : abs (Y x' - x) < ε, from and.right Hdst,
-      apply ge.trans Hn !le_max_right,
+    rewrite this at H,
-      rewrite abs_sub,
+    have H'' : Y x' - Z x' ≥ 0, from sub_nonneg_of_le (and.right Hlo),
-      apply HN1,
+    have H' : Z x' - x ≥ 0, from sub_nonneg_of_le HxleZ,
-      apply ge.trans Hn !le_max_left
+    krewrite [abs_of_nonneg H', abs_of_nonneg (add_nonneg H' H'') at H],
-    end,
+    apply lt_of_add_lt_of_nonneg_left H H''},
-    have HZX : abs (Z n - X n) < ε / 2, begin
+    {have X x' - x = (Z x' - x) + (X x' - Z x'), by rewrite -sub_eq_sub_add_sub,
-      have HZXnp : Z n - X n ≥ 0, from sub_nonneg_of_le !HZX,
+    have H : abs (X x' - x) < ε, from and.left Hdst,
-      have HXYnp : Y n - X n ≥ 0, from sub_nonneg_of_le (le.trans !HZX !HZY),
+    rewrite this at H,
-      rewrite [abs_of_nonneg HZXnp, abs_of_nonneg HXYnp at HXY],
+    have H' : x - Z x' > 0, from sub_pos_of_lt (lt_of_not_ge HxnleZ),
-      note Hgt := lt_add_of_sub_lt_right HXY,
+    have H'2 : Z x' - x < 0,
-      have Hlt : Z n < ε / 2 + X n, from calc
+      by rewrite [-neg_neg (Z x' - x)]; apply neg_neg_of_pos; rewrite [neg_sub]; apply H',
-        Z n ≤ Y n : HZY
+    have H'' : X x' - Z x' ≤ 0, from sub_nonpos_of_le (and.left Hlo),
-        ... < ε / 2 + X n : Hgt,
+    krewrite [abs_of_neg H'2, abs_of_neg (add_neg_of_neg_of_nonpos H'2 H'') at H, neg_add at H],
-      apply sub_lt_right_of_lt_add Hlt
+    apply lt_of_add_lt_of_nonneg_left H,
-    end,
+    apply neg_nonneg_of_nonpos H''}
-    have H : abs (Z n - x) < ε, begin
-      apply lt_of_le_of_lt,
-      apply abs_sub_le _ (X n),
-      apply lt.trans,
-      apply add_lt_add,
-      apply HZX,
-      apply HN1,
-      apply ge.trans Hn !le_max_left,
-      apply div_two_add_div_four_lt Hε
-    end,
-    exact H
   end
 
-proposition converges_to_seq_of_abs_sub_converges_to_seq (Habs : (λ n, abs (X n - x)) ⟶ 0 [at ∞]) :
+proposition approaches_of_abs_sub_approaches {F} (Habs : ((λ n, abs (X n - x)) ⟶ 0) F) :
-            X ⟶ x [at ∞] :=
+            (X ⟶ x) F :=
   begin
-    apply approaches_at_infty_intro,
+    apply real.approaches_intro,
-    intros ε Hε,
+    intro ε Hε,
-    cases approaches_at_infty_dest Habs Hε with N HN,
+    apply set.filter.eventually_mono,
-    existsi N,
+    apply real.approaches_dest Habs Hε,
     intro n Hn,
-    have Hn' : abs (abs (X n - x) - 0) < ε, from HN Hn,
+    have Hn' : abs (abs (X n - x) - 0) < ε, from Hn,
     rewrite [sub_zero at Hn', abs_abs at Hn'],
     exact Hn'
   end
 
-proposition abs_sub_converges_to_seq_of_converges_to_seq (HX : X ⟶ x [at ∞]) :
+proposition abs_sub_approaches_of_approaches {F} (HX : (X ⟶ x) F) :
-            (λ n, abs (X n - x)) ⟶ 0 [at ∞] :=
+            ((λ n, abs (X n - x)) ⟶ 0) F :=
   begin
-    apply approaches_at_infty_intro,
+    apply real.approaches_intro,
     intros ε Hε,
-    cases approaches_at_infty_dest HX Hε with N HN,
+    apply set.filter.eventually_mono,
-    existsi N,
+    apply real.approaches_dest HX Hε,
     intro n Hn,
-    have Hn' : abs (abs (X n - x) - 0) < ε, by rewrite [sub_zero, abs_abs]; apply HN Hn,
+    have Hn' : abs (abs (X n - x) - 0) < ε, by rewrite [sub_zero, abs_abs]; apply Hn,
     exact Hn'
   end
 
-proposition mul_converges_to_seq (HX : X ⟶ x [at ∞]) (HY : Y ⟶ y [at ∞]) :
+proposition bounded_of_approaches_real {F} (HX : (X ⟶ x) F) :
-            (λ n, X n * Y n) ⟶ x * y [at ∞] :=
+            ∃ K : ℝ, filter.eventually (λ n, abs (X n) ≤ K) F :=
-    have Hbd : ∃ K : ℝ, ∀ n : ℕ, abs (X n) ≤ K, begin
+  begin
-      cases bounded_of_converges_seq HX with K HK,
+    cases bounded_of_converges HX with K HK,
-      existsi K + abs x,
+    existsi K + abs x,
-      intro n,
+    apply filter.eventually_mono HK,
-      note Habs := le.trans (abs_abs_sub_abs_le_abs_sub (X n) x) !HK,
+    intro x' Hx',
-      apply le_add_of_sub_right_le,
+    note Hle := abs_sub_abs_le_abs_sub (X x') x,
-      apply le.trans,
+    apply le.trans,
-      apply le_abs_self,
+    apply le_add_of_sub_right_le,
-      assumption
+    apply Hle,
-    end,
+    apply add_le_add_right,
-    obtain K HK, from Hbd,
+    apply Hx'
-    have Habsle : ∀ n, abs (X n * Y n - x * y) ≤ K * abs (Y n - y) + abs y * abs (X n - x), begin
+  end
-      intro,
+
-      have Heq : X n * Y n - x * y = (X n * Y n - X n * y) + (X n * y - x * y), by
+proposition mul_approaches {F} (HX : (X ⟶ x) F) (HY : (Y ⟶ y) F) :
-        rewrite [-sub_add_cancel (X n * Y n) (X n * y) at {1}, sub_eq_add_neg, *add.assoc],
+            ((λ n, X n * Y n) ⟶ x * y) F :=
+    obtain K HK, from bounded_of_approaches_real HX,
+    have Habsle : filter.eventually
+         (λ n, abs (X n * Y n - x * y) ≤ K * abs (Y n - y) + abs y * abs (X n - x)) F, begin
+      have Heq : ∀ n, X n * Y n - x * y = (X n * Y n - X n * y) + (X n * y - x * y),
+        by intro n; rewrite [-sub_add_cancel (X n * Y n) (X n * y) at {1}, sub_eq_add_neg, *add.assoc],
+      apply filter.eventually_mono HK,
+      intro x' Hx',
       apply le.trans,
       rewrite Heq,
       apply abs_add_le_abs_add_abs,
       apply add_le_add,
       rewrite [-mul_sub_left_distrib, abs_mul],
       apply mul_le_mul_of_nonneg_right,
-      apply HK,
+      apply Hx',
       apply abs_nonneg,
       rewrite [-mul_sub_right_distrib, abs_mul, mul.comm],
       apply le.refl
     end,
-    have Hdifflim : (λ n, abs (X n * Y n - x * y)) ⟶ 0 [at ∞], begin
+    have Hdifflim : ((λ n, abs (X n * Y n - x * y)) ⟶ 0) F, begin
-      apply converges_to_seq_squeeze,
+      apply approaches_squeeze,
       rotate 2,
-      intro, apply abs_nonneg,
+      intro,
+      apply filter.eventually_mono HK,
+      intro x' Hx',
+      apply abs_nonneg,
       apply Habsle,
       apply approaches_constant,
       rewrite -{0}zero_add,
-      apply add_converges_to_seq,
+      apply add_approaches,
       krewrite -(mul_zero K),
-      apply mul_left_converges_to_seq,
+      apply mul_left_approaches,
-      apply abs_sub_converges_to_seq_of_converges_to_seq,
+      apply abs_sub_approaches_of_approaches,
       exact HY,
       krewrite -(mul_zero (abs y)),
-      apply mul_left_converges_to_seq,
+      apply mul_left_approaches,
-      apply abs_sub_converges_to_seq_of_converges_to_seq,
+      apply abs_sub_approaches_of_approaches,
       exact HX
     end,
-    converges_to_seq_of_abs_sub_converges_to_seq Hdifflim
+    approaches_of_abs_sub_approaches Hdifflim
 
-
+proposition mul_approaches_zero_of_approaches_zero_of_approaches (HX : (X ⟶ 0) F) (HY : (Y ⟶ y) F) :
--- TODO: converges_to_seq_div, converges_to_seq_mul_left_iff, etc.
+            ((λ z, X z * Y z) ⟶ 0) F :=
-
-proposition abs_converges_to_seq_zero (HX : X ⟶ 0 [at ∞]) : (λ n, abs (X n)) ⟶ 0 [at ∞] :=
-norm_converges_to_seq_zero HX
-
-proposition converges_to_seq_zero_of_abs_converges_to_seq_zero (HX : (λ n, abs (X n)) ⟶ 0 [at ∞]) :
-  X ⟶ 0 [at ∞] :=
-converges_to_seq_zero_of_norm_converges_to_seq_zero HX
-
-proposition abs_converges_to_seq_zero_iff (X : ℕ → ℝ) :
-  ((λ n, abs (X n)) ⟶ 0 [at ∞]) ↔ (X ⟶ 0 [at ∞]) :=
-iff.intro converges_to_seq_zero_of_abs_converges_to_seq_zero abs_converges_to_seq_zero
-
--- TODO: products of two sequences, converges_seq, limit_seq
-
-end limit_operations
-
-/- properties of converges_to_at -/
-
-section limit_operations_continuous
-variables {f g h : ℝ → ℝ}
-variables {a b x y : ℝ}
-
---<<<<<<< HEAD
-theorem mul_converges_to_at (Hf : f ⟶ a [at x]) (Hg : g ⟶ b [at x]) : (λ z, f z * g z) ⟶ a * b [at x] :=
-/-=======
-theorem converges_to_at_real_intro (Hf : ∀ ⦃ε⦄, ε > 0 →
-        (∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ≠ x ∧ abs (x' - x) < δ → abs (f x' - y) < ε)) :
-        converges_to_at f y x := Hf
-
-theorem mul_converges_to_at (Hf : f ⟶ a at x) (Hg : g ⟶ b at x) : (λ z, f z * g z) ⟶ a * b at x :=
->>>>>>> feat(library/analysis): basic properties about real derivatives-/
   begin
-    apply converges_to_at_of_all_conv_seqs,
+    krewrite [-zero_mul y],
-    intro X HX,
+    apply mul_approaches,
-    apply mul_converges_to_seq,
+    exact HX, exact HY
-    apply comp_approaches_at_infty Hf,
-    apply and.right (HX 0),
-    apply (set.filter.eventually_of_forall _ (λ n, and.left (HX n))),
-    apply comp_approaches_at_infty Hg,
-    apply and.right (HX 0),
-    apply (set.filter.eventually_of_forall _ (λ n, and.left (HX n)))
   end
 
-end limit_operations_continuous
+proposition mul_approaches_zero_of_approaches_of_approaches_zero (HX : (X ⟶ y) F) (HY : (Y ⟶ 0) F) :
+            ((λ z, X z * Y z) ⟶ 0) F :=
+  begin
+    have H : (λ z, X z * Y z) = (λ z, Y z * X z), from funext (λ a, !mul.comm),
+    rewrite H,
+    exact mul_approaches_zero_of_approaches_zero_of_approaches HY HX
+  end
+
+proposition abs_approaches_zero_of_approaches_zero (HX : (X ⟶ 0) F) : ((λ n, abs (X n)) ⟶ 0) F :=
+norm_approaches_zero_of_approaches_zero HX
+
+proposition approaches_zero_of_abs_approaches_zero (HX : ((λ n, abs (X n)) ⟶ 0) F) :
+  (X ⟶ 0) F :=
+approaches_zero_of_norm_approaches_zero HX
+
+proposition abs_approaches_zero_iff :
+  ((λ n, abs (X n)) ⟶ 0) F ↔ (X ⟶ 0) F :=
+iff.intro approaches_zero_of_abs_approaches_zero abs_approaches_zero_of_approaches_zero
+end limit_operations
+
 
 /- monotone sequences -/
 
@@ -436,7 +525,7 @@ variable {X : ℕ → ℝ}
 
 proposition converges_to_seq_sup_of_nondecreasing (nondecX : nondecreasing X) {b : ℝ}
     (Hb : ∀ i, X i ≤ b) : X ⟶ sup (X ' univ) [at ∞] :=
-approaches_at_infty_intro
+real.approaches_at_infty_intro
 (let sX := sup (X ' univ) in
 have Xle : ∀ i, X i ≤ sX, from
   take i,
@@ -475,7 +564,7 @@ have H₃ : {x : ℝ | -x ∈ X ' univ} = {x : ℝ | x ∈ (λ n, -X n) ' univ},
                        ... = {x : ℝ | x ∈ (λ n, -X n) ' univ} : image_comp,
 have H₄ : ∀ i, - X i ≤ - b, from take i, neg_le_neg (Hb i),
 begin
-  apply iff.mp !neg_converges_to_seq_iff,
+  apply approaches_neg,
   -- need krewrite here
   krewrite [-sup_neg H₁ H₂, H₃, -nondecreasing_neg_iff at nonincX],
   apply converges_to_seq_sup_of_nondecreasing nonincX H₄
@@ -488,11 +577,11 @@ end monotone_sequences
 section xn
 open nat set
 
-theorem pow_converges_to_seq_zero {x : ℝ} (H : abs x < 1) :
+theorem pow_approaches_zero_at_infty {x : ℝ} (H : abs x < 1) :
   (λ n, x^n) ⟶ 0 [at ∞] :=
 suffices H' : (λ n, (abs x)^n) ⟶ 0 [at ∞], from
   have (λ n, (abs x)^n) = (λ n, abs (x^n)), from funext (take n, eq.symm !abs_pow),
-    by rewrite this at H'; exact converges_to_seq_zero_of_abs_converges_to_seq_zero H',
+    by rewrite this at H'; exact approaches_zero_of_abs_approaches_zero H',
 let  aX := (λ n, (abs x)^n),
     iaX := real.inf (aX ' univ),
     asX := (λ n, (abs x)^(succ n)) in
@@ -506,7 +595,7 @@ have noninc_aX : nonincreasing aX, from
 have bdd_aX : ∀ i, 0 ≤ aX i, from take i, !pow_nonneg_of_nonneg !abs_nonneg,
 have aXconv : aX ⟶ iaX [at ∞], proof converges_to_seq_inf_of_nonincreasing noninc_aX bdd_aX qed,
 have asXconv : asX ⟶ iaX [at ∞], from tendsto_succ_at_infty aXconv,
-have asXconv' : asX ⟶ (abs x) * iaX [at ∞], from mul_left_converges_to_seq (abs x) aXconv,
+have asXconv' : asX ⟶ (abs x) * iaX [at ∞], from mul_left_approaches (abs x) aXconv,
 have iaX = (abs x) * iaX, from sorry, -- converges_to_seq_unique asXconv asXconv',
 have iaX = 0, from eq_zero_of_mul_eq_self_left (ne_of_lt H) (eq.symm this),
 show aX ⟶ 0 [at ∞], begin rewrite -this, exact aXconv end --from this ▸ aXconv
@@ -515,36 +604,115 @@ end xn
 
 /- continuity on the reals -/
 
-section continuous
+/-namespace real
-open topology
+open topology set
+open normed_vector_space
+
+section
 variable {f : ℝ → ℝ}
 
-theorem continuous_real_elim (H : continuous f) :
+theorem continuous_dest (H : continuous f) :
   ∀ x : ℝ, ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ δ : ℝ, δ > 0 ∧ ∀ x' : ℝ,
     abs (x' - x) < δ → abs (f x' - f x) < ε :=
-take x, continuous_at_elim (forall_continuous_at_of_continuous H x)
+normed_vector_space.continuous_dest H
 
-theorem continuous_real_intro
+theorem continuous_intro
   (H : ∀ x : ℝ, ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ δ : ℝ, δ > 0 ∧ ∀ x' : ℝ,
     abs (x' - x) < δ → abs (f x' - f x) < ε) :
   continuous f :=
-continuous_of_forall_continuous_at (take x, continuous_at_intro (H x))
+normed_vector_space.continuous_intro H
 
-section
+theorem continuous_at_dest {x : ℝ} (H : continuous_at f x) :
-open set
+         ∀ ε : ℝ, ε > 0 → (∃ δ : ℝ, δ > 0 ∧ ∀ x' : ℝ, abs (x' - x) < δ → abs (f x' - f x) < ε) :=
-variable {s : set ℝ}
+normed_vector_space.continuous_at_dest H
---theorem continuous_on_real_elim (H : continuous_on f s) :
+
---  ∀₀ x ∈ s, x = x := sorry
+theorem continuous_at_intro {x : ℝ}
+  (H : ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ δ : ℝ, δ > 0 ∧ ∀ x' : ℝ,
+    abs (x' - x) < δ → abs (f x' - f x) < ε) :
+  continuous_at f x :=
+normed_vector_space.continuous_at_intro H
+
+theorem continuous_at_within_intro {x : ℝ} {s : set ℝ}
+        (H : ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ∈ s → abs (x' - x) < δ → abs ((f x') - (f x)) < ε) :
+  continuous_at_on f x s :=
+normed_vector_space.continuous_at_within_intro H
+
+
+theorem continuous_at_on_dest {x : ℝ} {s : set ℝ} (Hfx : continuous_at_on f x s) :
+         ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ∈ s → abs (x' - x) < δ → abs ((f x') - (f x)) < ε :=
+normed_vector_space.continuous_at_on_dest Hfx
+
+theorem continuous_on_intro {s : set ℝ}
+        (H : ∀ x ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ∈ s → abs (x' - x) < δ → abs ((f x') - (f x)) < ε) :
+        continuous_on f s :=
+normed_vector_space.continuous_on_intro H
+
+theorem continuous_on_dest {s : set ℝ} (H : continuous_on f s) {x : ℝ} (Hxs : x ∈ s) :
+        ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ∈ s → abs (x' - x) < δ → abs ((f x') - (f x)) < ε :=
+normed_vector_space.continuous_on_dest H Hxs
 
 end
 
+section
+variable {f : ℕ → ℝ}
+proposition approaches_at_infty_intro {y : ℝ}
+    (H : ∀ ε, ε > 0 → ∃ N, ∀ n, n ≥ N → abs ((f n) - y) < ε) :
+  f ⟶ y [at ∞] :=
+normed_vector_space.approaches_at_infty_intro H
+
+proposition approaches_at_infty_dest {y : ℝ}
+    (H : f ⟶ y [at ∞]) ⦃ε : ℝ⦄ (εpos : ε > 0) :
+  ∃ N, ∀ ⦃n⦄, n ≥ N → abs ((f n) - y) < ε :=
+approaches_at_infty_dest H εpos
+
+proposition approaches_at_infty_iff (y : ℝ) :
+  f ⟶ y [at ∞] ↔ (∀ ε, ε > 0 → ∃ N, ∀ ⦃n⦄, n ≥ N → abs((f n) - y) < ε) :=
+iff.intro approaches_at_infty_dest approaches_at_infty_intro
+
+end
+
+section
+variable {f : ℝ → ℝ}
+proposition approaches_at_dest  {y x : ℝ}
+    (H : f ⟶ y [at x]) ⦃ε : ℝ⦄ (εpos : ε > 0) :
+  ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, abs (x' - x) < δ → x' ≠ x → abs ((f x') - y) < ε :=
+approaches_at_dest H εpos
+
+proposition approaches_at_intro {y x : ℝ}
+    (H : ∀ ε, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, abs (x' - x) < δ → x' ≠ x → abs ((f x') - y) < ε) :
+  f ⟶ y [at x] :=
+approaches_at_intro H
+
+proposition approaches_at_iff (y x : ℝ) : f ⟶ y [at x] ↔
+    (∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, abs (x' - x) < δ → x' ≠ x → abs ((f x') - y) < ε) :=
+iff.intro approaches_at_dest approaches_at_intro
+
+/-proposition approaches_seq_real_intro {X : ℕ → ℝ} {y : ℝ}
+    (H : ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → abs (X n - y) < ε) :
+  (X ⟶ y [at ∞]) := metric_space.approaches_at_infty_intro H
+
+proposition approaches_seq_real_elim {X : ℕ → ℝ} {y : ℝ} (H : X ⟶ y [at ∞]) :
+    ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → abs (X n - y) < ε := metric_space.approaches_at_infty_dest H
+
+proposition approaches_seq_real_intro' {X : ℕ → ℝ} {y : ℝ}
+    (H : ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → abs (X n - y) ≤ ε) :
+  (X ⟶ y [at ∞]) :=
+approaches_at_infty_intro' H-/
+
+end
+
+end real-/
+
+section continuous
+open topology
+variable {f : ℝ → ℝ}
 variable (Hf : continuous f)
 include Hf
 
 theorem pos_on_nbhd_of_cts_of_pos {b : ℝ} (Hb : f b > 0) :
                 ∃ δ : ℝ, δ > 0 ∧ ∀ y, abs (y - b) < δ → f y > 0 :=
   begin
-    let Hcont := continuous_real_elim Hf b Hb,
+    let Hcont := real.continuous_dest Hf b Hb,
     cases Hcont with δ Hδ,
     existsi δ,
     split,
@@ -559,7 +727,7 @@ theorem pos_on_nbhd_of_cts_of_pos {b : ℝ} (Hb : f b > 0) :
 theorem neg_on_nbhd_of_cts_of_neg {b : ℝ} (Hb : f b < 0) :
                 ∃ δ : ℝ, δ > 0 ∧ ∀ y, abs (y - b) < δ → f y < 0 :=
   begin
-    let Hcont := continuous_real_elim Hf b (neg_pos_of_neg Hb),
+    let Hcont := real.continuous_dest Hf b (neg_pos_of_neg Hb),
     cases Hcont with δ Hδ,
     existsi δ,
     split,
@@ -572,66 +740,17 @@ theorem neg_on_nbhd_of_cts_of_neg {b : ℝ} (Hb : f b < 0) :
     assumption
   end
 
-theorem continuous_neg_of_continuous : continuous (λ x, - f x) :=
-  begin
-    apply continuous_real_intro,
-    intros x ε Hε,
-    cases continuous_real_elim Hf x Hε with δ Hδ,
-    cases Hδ with Hδ₁ Hδ₂,
-    existsi δ,
-    split,
-    assumption,
-    intros x' Hx',
-    let HD := Hδ₂ x' Hx',
-    rewrite [-abs_neg, neg_neg_sub_neg],
-    exact HD
-  end
-
-theorem continuous_offset_of_continuous (a : ℝ) :
-        continuous (λ x, (f x) + a) :=
-  begin
-    apply continuous_real_intro,
-    intros x ε Hε,
-    cases continuous_real_elim Hf x Hε with δ Hδ,
-    cases Hδ with Hδ₁ Hδ₂,
-    existsi δ,
-    split,
-    assumption,
-    intros x' Hx',
-    rewrite [add_sub_comm, sub_self, add_zero],
-    apply Hδ₂,
-    assumption
-  end
-
 theorem continuous_mul_of_continuous {g : ℝ → ℝ} (Hcong : continuous g) :
         continuous (λ x, f x * g x) :=
   begin
     apply continuous_of_forall_continuous_at,
     intro x,
-    apply continuous_at_of_converges_to_at,
+    apply continuous_at_of_tendsto_at,
-    apply mul_converges_to_at,
+    apply mul_approaches,
-    all_goals apply converges_to_at_of_continuous_at,
+    all_goals apply tendsto_at_of_continuous_at,
     all_goals apply forall_continuous_at_of_continuous,
     apply Hf,
     apply Hcong
   end
 
 end continuous
-
--- this can be strengthened: Hle and Hge only need to hold around x
-theorem converges_to_at_squeeze {M : Type} [Hm : metric_space M] {f g h : M → ℝ} {a : ℝ} {x : M}
-        (Hf : f ⟶ a at x) (Hh : h ⟶ a at x) (Hle : ∀ y : M, f y ≤ g y)
-        (Hge : ∀ y : M, g y ≤ h y) : g ⟶ a at x :=
-  begin
-    apply converges_to_at_of_all_conv_seqs,
-    intro X HX,
-    apply converges_to_seq_squeeze,
-    apply all_conv_seqs_of_converges_to_at Hf,
-    apply HX,
-    apply all_conv_seqs_of_converges_to_at Hh,
-    apply HX,
-    intro,
-    apply Hle,
-    intro,
-    apply Hge
-  end

library/theories/analysis/sqrt.lean

@@ -34,7 +34,7 @@ private theorem lb_le_ub (x : ℝ) (H : x ≥ 0) : sqr_lb x ≤ sqr_ub x :=
     apply zero_le_one
   end
 
-private lemma sqr_cts : continuous (λ x : ℝ, x * x) := continuous_mul_of_continuous id_continuous id_continuous
+private lemma sqr_cts : continuous (λ x : ℝ, x * x) := continuous_mul_of_continuous continuous_id continuous_id
 
 definition sqrt (x : ℝ) : ℝ :=
   if H : x ≥ 0 then

library/theories/move.lean

@@ -6,6 +6,7 @@ Temporary file; move in Lean3.
 -/
 import data.set algebra.order_bigops
 import data.finset data.list.sort
+import data.real
 
 -- move this to init.function
 
@@ -20,6 +21,24 @@ theorem eq_of_inv_mul_eq_one {A : Type} {a b : A} [group A] (H : b⁻¹ * a = 1)
 have a⁻¹ * 1 = a⁻¹, by inst_simp,
 by inst_simp
 
+theorem lt_neg_self_of_neg {A : Type} {a : A} [ordered_comm_group A] (Ha : a < 0) : a < -a :=
+calc
+    a < 0  : Ha
+  ... = -0 : by rewrite neg_zero
+  ... < -a : neg_lt_neg Ha
+
+theorem lt_of_add_lt_of_nonneg_left {A : Type} {a b c : A} [ordered_comm_group A]
+        (H : a + b < c) (Hb : b ≥ 0) : a < c :=
+calc
+    a < c - b : lt_sub_right_of_add_lt H
+  ... ≤ c : sub_le_self _ Hb
+
+theorem lt_of_add_lt_of_nonneg_right {A : Type} {a b c : A} [ordered_comm_group A]
+        (H : a + b < c) (Hb : a ≥ 0) : b < c :=
+calc
+    b < c - a : lt_sub_left_of_add_lt H
+  ... ≤ c : sub_le_self _ Hb
+
 -- move to init.quotient
 
 namespace quot
@@ -502,3 +521,18 @@ have succ (Max₀ s) ≤ Max₀ s, from le_Max₀ this,
 show false, from not_succ_le_self this
 
 end nat
+
+
+-- move to real
+
+namespace real
+theorem lt_of_abs_lt {a b : ℝ} (Ha : abs a < b) : a < b :=
+if Hnn : a ≥ 0 then
+  by rewrite [-abs_of_nonneg Hnn]; exact Ha
+else
+  have Hlt : a < 0, from lt_of_not_ge Hnn,
+  have -a < b, by rewrite [-abs_of_neg Hlt]; exact Ha,
+  calc
+    a < -a : lt_neg_self_of_neg Hlt
+  ... < b  : this
+end real

library/theories/topology/continuous.lean

@@ -5,7 +5,7 @@ Authors: Jacob Gross, Jeremy Avigad
 
 Continuous functions.
 -/
-import theories.topology.basic algebra.category ..move
+import theories.topology.basic algebra.category ..move .limit
 open algebra eq.ops set topology function category sigma.ops
 
 namespace topology
@@ -291,6 +291,41 @@ theorem forall_continuous_at_of_continuous {f : X → Y} (H : continuous f) :
     apply mem_univ
   end
 
+section limit
+open set
+theorem tendsto_at_of_continuous_at {f : X → Y} {x : X} (H : continuous_at f x) :
+        (f ⟶ f x) (nhds x) :=
+  begin
+    apply approaches_intro,
+    intro s HOs Hfxs,
+    cases H HOs Hfxs with u Hu,
+    apply eventually_nhds_intro,
+    exact and.left Hu,
+    exact and.left (and.right Hu),
+    intro x' Hx',
+    apply @mem_of_mem_preimage _ _ f,
+    apply and.right (and.right Hu),
+    exact Hx'
+  end
+
+theorem continuous_at_of_tendsto_at  {f : X → Y} {x : X} (H : (f ⟶ f x) (nhds x)) :
+        continuous_at f x :=
+  begin
+    intro s HOs Hfxs,
+    cases eventually_nhds_dest (approaches_elim H HOs Hfxs) with u Hu,
+    existsi u,
+    split,
+    exact and.left Hu,
+    split,
+    exact and.left (and.right Hu),
+    intro x Hx,
+    apply mem_preimage,
+    apply and.right (and.right Hu),
+    apply Hx
+  end
+
+end limit
+
 /- The Category TOP -/
 
 section TOP

library/theories/topology/limit.lean

@@ -703,6 +703,16 @@ section approaches
   have eventually (λ x, f x ∈ univ ∧ f x ≠ y) F₁,
     from eventually_congr (take x, by rewrite [mem_univ_iff, true_and]) Hf₂,
   tendsto_comp_of_approaches_of_tendsto_at_within Hf₁ this Hg
+
+  proposition approaches_constant : ((λ x, y) ⟶ y) F :=
+  begin
+    apply approaches_intro,
+    intro s Hs Hys,
+    have H : (λ x : X, y ∈ s) = (λ x : X, true), from funext (λ x, by rewrite classical.eq_true; exact Hys),
+    rewrite H,
+    apply eventually_true
+  end
+
 end approaches
 
 /-