refactor(library/theories/analysis/metric_space): refactor some proofs

library/theories/analysis/metric_space.lean

@@ -57,7 +57,7 @@ eq_of_dist_eq_zero (eq_zero_of_nonneg_of_forall_le !dist_nonneg H)
 
 definition open_ball (x : M) (ε : ℝ) := {y | dist y x < ε}
 
-theorem open_ball_empty_of_nonpos (x : M) {ε : ℝ} (Hε : ε ≤ 0) : open_ball x ε = ∅ :=
+theorem open_ball_eq_empty_of_nonpos (x : M) {ε : ℝ} (Hε : ε ≤ 0) : open_ball x ε = ∅ :=
   begin
     apply eq_empty_of_forall_not_mem,
     intro y Hlt,
@@ -65,11 +65,11 @@ theorem open_ball_empty_of_nonpos (x : M) {ε : ℝ} (Hε : ε ≤ 0) : open_bal
     apply lt_of_lt_of_le Hlt Hε
   end
 
-theorem radius_pos_of_nonempty {x : M} {ε : ℝ} {u : M} (Hu : u ∈ open_ball x ε) : ε > 0 :=
+theorem pos_of_mem_open_ball {x : M} {ε : ℝ} {u : M} (Hu : u ∈ open_ball x ε) : ε > 0 :=
   begin
     apply lt_of_not_ge,
     intro Hge,
-    note Hop := open_ball_empty_of_nonpos x Hge,
+    note Hop := open_ball_eq_empty_of_nonpos x Hge,
     rewrite Hop at Hu,
     apply not_mem_empty _ Hu
   end
@@ -77,205 +77,94 @@ theorem radius_pos_of_nonempty {x : M} {ε : ℝ} {u : M} (Hu : u ∈ open_ball
 theorem mem_open_ball (x : M) {ε : ℝ} (H : ε > 0) : x ∈ open_ball x ε :=
   show dist x x < ε, by rewrite dist_self; assumption
 
-definition closed_ball (x : M) (ε : ℝ) := {y | dist x y ≤ ε}
+definition closed_ball (x : M) (ε : ℝ) := {y | dist y x ≤ ε}
 
-theorem closed_ball_eq_compl (x : M) (ε : ℝ) : closed_ball x ε = - {y | dist x y > ε} :=
+theorem closed_ball_eq_compl (x : M) (ε : ℝ) : closed_ball x ε = - {y | dist y x > ε} :=
-  begin
+ext (take y, iff.intro
-    apply ext,
+  (suppose dist y x ≤ ε, not_lt_of_ge this)
-    intro y,
+  (suppose ¬ dist y x > ε, le_of_not_gt this))
-    apply iff.intro,
-    intro Hle,
-    apply mem_compl,
-    intro Hgt,
-    apply not_le_of_gt Hgt Hle,
-    intro Hx,
-    note Hx' := not_mem_of_mem_compl Hx,
-    apply le_of_not_gt,
-    intro Hgt,
-    apply Hx',
-    exact Hgt
-  end
 
 variable (M)
 
-definition open_sets_basis :=
+definition open_sets_basis : set (set M) := { s | ∃ x, ∃ ε, s = open_ball x ε }
-  image (λ pair : M × ℝ, open_ball (pr1 pair) (pr2 pair)) univ
 
-definition metric_topology [instance] : topology M :=
+definition metric_topology [instance] : topology M := topology.generated_by (open_sets_basis M)
-  topology.generated_by (open_sets_basis M)
 
 variable {M}
 
 theorem open_ball_mem_open_sets_basis (x : M) (ε : ℝ) : open_ball x ε ∈ open_sets_basis M :=
-  mem_image !mem_univ rfl
+  exists.intro x (exists.intro ε rfl)
 
-theorem open_ball_open (x : M) (ε : ℝ) : Open (open_ball x ε) :=
+theorem Open_open_ball (x : M) (ε : ℝ) : Open (open_ball x ε) :=
   by apply generators_mem_topology_generated_by; apply open_ball_mem_open_sets_basis
 
-theorem closed_ball_closed (x : M) {ε : ℝ} (H : ε > 0) : closed (closed_ball x ε) :=
+theorem closed_closed_ball (x : M) {ε : ℝ} (H : ε > 0) : closed (closed_ball x ε) :=
-  begin
+Open_of_forall_exists_Open_nbhd
-    apply iff.mpr !closed_iff_Open_compl,
+  (take y, suppose ¬ dist y x ≤ ε,
-    rewrite closed_ball_eq_compl,
+    have dist y x > ε, from lt_of_not_ge this,
-    rewrite compl_compl,
+    let B := open_ball y (dist y x - ε) in
-    apply Open_of_forall_exists_Open_nbhd,
+    have y ∈ B, from mem_open_ball y (sub_pos_of_lt this),
-    intro y Hxy,
+    have B ⊆ - closed_ball x ε, from
-    existsi open_ball y (dist x y - ε),
+      take y',
-    split,
+      assume Hy'y : dist y' y < dist y x - ε,
-    apply open_ball_open,
+      assume Hy'x : dist y' x ≤ ε,
-    split,
+      show false, from not_lt_self (dist y x)
-    apply mem_open_ball,
+        (calc
-    apply sub_pos_of_lt Hxy,
+          dist y x ≤ dist y y' + dist y' x   : dist_triangle
-    intros y' Hxy'd,
+            ... < dist y x - ε + dist y' x   : by rewrite dist_comm; apply add_lt_add_right Hy'y
-    apply lt_of_not_ge,
+            ... ≤ dist y x - ε + ε           : add_le_add_left Hy'x
-    intro Hxy',
+            ... = dist y x                   : by rewrite [sub_add_cancel]),
-    apply not_lt_self (dist x y),
+    exists.intro B (and.intro (Open_open_ball _ _) (and.intro `y ∈ B` this)))
-    exact calc
-      dist x y ≤ dist x y' + dist y' y      : dist_triangle
-           ... ≤ ε         + dist y' y      : add_le_add_right Hxy'
-           ... < ε         + (dist x y - ε) : add_lt_add_left Hxy'd
-           ... = dist x y                   : by rewrite [add.comm, sub_add_cancel]
-  end
 
-private theorem not_mem_open_basis_of_boundary_pt {s : set M} (a : s ∈ open_sets_basis M) {x : M}
+proposition open_ball_subset_open_ball_of_le (x : M) {r₁ r₂ : ℝ} (H : r₁ ≤ r₂) :
-          (Hbd : ∀ ε : ℝ, ε > 0 → ∃ v : M, v ∉ s ∧ dist x v < ε) : ¬ x ∈ s :=
+  open_ball x r₁ ⊆ open_ball x r₂ :=
-  begin
+take y, assume ymem, lt_of_lt_of_le ymem H
-    intro HxU,
-    cases a with pr Hpr,
-    cases pr with y r,
-    cases Hpr with _ Hs,
-    rewrite -Hs at HxU,
-    have H : dist x y < r, from HxU,
-    cases Hbd _ (sub_pos_of_lt H) with v Hv,
-    cases Hv with Hv Hvdist,
-    apply Hv,
-    rewrite -Hs,
-    apply lt_of_le_of_lt,
-    apply dist_triangle,
-    exact x,
-    esimp,
-    rewrite dist_comm,
-    exact add_lt_of_lt_sub_right Hvdist
-  end
 
-private theorem not_mem_intersect_of_boundary_pt {s t : set M} (a : Open s) (a_1 : Open t) {x : M}
+theorem exists_open_ball_subset_of_Open_of_mem {U : set M} (HU : Open U) {x : M} (Hx : x ∈ U) :
-        (v_0 : (x ∈ s → ¬ (∀ (ε : ℝ), ε > 0 → (∃ (v : M), v ∉ s ∧ dist x v < ε))))
-        (v_1 : (x ∈ t → ¬ (∀ (ε : ℝ), ε > 0 → (∃ (v : M), v ∉ t ∧ dist x v < ε))))
-        (Hbd : ∀ (ε : ℝ), ε > 0 → (∃ (v : M), v ∉ s ∩ t ∧ dist x v < ε)) : ¬ (x ∈ s ∩ t) :=
-  begin
-    intro HxU,
-    have Hxs : x ∈ s, from mem_of_mem_inter_left HxU,
-    have Hxt : x ∈ t, from mem_of_mem_inter_right HxU,
-    note Hsih := exists_not_of_not_forall (v_0 Hxs),
-    note Htih := exists_not_of_not_forall (v_1 Hxt),
-    cases Hsih with ε1 Hε1,
-    cases Htih with ε2 Hε2,
-    note Hε1' := and_not_of_not_implies Hε1,
-    note Hε2' := and_not_of_not_implies Hε2,
-    cases Hε1' with Hε1p Hε1',
-    cases Hε2' with Hε2p Hε2',
-    note Hε1'' := forall_not_of_not_exists Hε1',
-    note Hε2'' := forall_not_of_not_exists Hε2',
-    have Hmin : min ε1 ε2 > 0, from lt_min Hε1p Hε2p,
-    cases Hbd _ Hmin with v Hv,
-    cases Hv with Hvint Hvdist,
-    note Hε1v := Hε1'' v,
-    note Hε2v := Hε2'' v,
-    cases em (v ∉ s) with Hnm Hmem,
-    apply Hε1v,
-    split,
-    exact Hnm,
-    apply lt_of_lt_of_le Hvdist,
-    apply min_le_left,
-    apply Hε2v,
-    have Hmem' : v ∈ s, from not_not_elim Hmem,
-    note Hnm := not_mem_of_mem_of_not_mem_inter_left Hmem' Hvint,
-    split,
-    exact Hnm,
-    apply lt_of_lt_of_le Hvdist,
-    apply min_le_right
-  end
-
-private theorem not_mem_sUnion_of_boundary_pt {S : set (set M)} (a : ∀₀ s ∈ S, Open s) {x : M}
-        (v_0 : ∀ ⦃x_1 : set M⦄,
-           x_1 ∈ S → x ∈ x_1 → ¬ (∀ (ε : ℝ), ε > 0 → (∃ (v : M), v ∉ x_1 ∧ dist x v < ε)))
-        (Hbd : ∀ (ε : ℝ), ε > 0 → (∃ (v : M), v ∉ ⋃₀ S ∧ dist x v < ε)) : ¬ x ∈ ⋃₀ S :=
-  begin
-    intro HxU,
-    have Hex : ∃₀ s ∈ S, x ∈ s, from HxU,
-    cases Hex with s Hs,
-    cases Hs with Hs Hxs,
-    cases exists_not_of_not_forall (v_0 Hs Hxs) with ε Hε,
-    cases and_not_of_not_implies Hε with Hεp Hv,
-    cases Hbd _ Hεp with v Hv',
-    cases Hv' with Hvnm Hdist,
-    apply Hv,
-    existsi v,
-    split,
-    apply not_mem_of_not_mem_sUnion Hvnm Hs,
-    exact Hdist
-  end
-
-/-
-   this should be doable by showing that the open-ball boundary definition
-   is equivalent to topology.on_boundary, and applying topology.not_open_of_on_boundary.
-   But the induction hypotheses don't work out nicely.
--/
-
-theorem not_open_of_ex_boundary_pt {U : set M} {x : M} (HxU : x ∈ U)
-        (Hbd : ∀ ε : ℝ, ε > 0 → ∃ v : M, v ∉ U ∧ dist x v < ε) : ¬ Open U :=
-  begin
-    intro HUopen,
-    induction HUopen,
-    {apply not_mem_open_basis_of_boundary_pt a Hbd HxU},
-    {cases Hbd 1 zero_lt_one with v Hv,
-    cases Hv with Hv _,
-    exact Hv !mem_univ},
-    {apply not_mem_intersect_of_boundary_pt a a_1 v_0 v_1 Hbd HxU},
-    {apply not_mem_sUnion_of_boundary_pt a v_0 Hbd HxU}
-  end
-
-theorem exists_Open_ball_subset_of_Open_of_mem {U : set M} (HU : Open U) {x : M} (Hx : x ∈ U) :
         ∃ (r : ℝ), r > 0 ∧ open_ball x r ⊆ U :=
 begin
-    let balloon := {r ∈ univ | r > 0 ∧ open_ball x r ⊆ U},
+  induction HU with s sbasis s t sbasis tbasis ihs iht S Sbasis ihS,
-    cases em (balloon = ∅),
+    {cases sbasis with x' aux, cases aux with ε seq,
-    have H : ∀ r : ℝ, r > 0 → ∃ v : M, v ∉ U ∧ dist x v < r, begin
+      have x ∈ open_ball x' ε, by rewrite -seq; exact Hx,
-      intro r Hr,
+      have εpos : ε > 0, from pos_of_mem_open_ball this,
-      note Hor := not_or_not_of_not_and (forall_not_of_sep_empty a (mem_univ r)),
+      have ε - dist x x' > 0, from sub_pos_of_lt `x ∈ open_ball x' ε`,
-      note Hor' := or.neg_resolve_left Hor Hr,
+      existsi (ε - dist x x'), split, exact this, rewrite seq,
-      apply exists_of_not_forall_not,
+      show open_ball x (ε - dist x x') ⊆ open_ball x' ε, from
-      intro Hall,
+        take y, suppose dist y x < ε - dist x x',
-      apply Hor',
+        calc
-      intro y Hy,
+          dist y x' ≤ dist y x + dist x x'      : dist_triangle
-      cases not_or_not_of_not_and (Hall y) with Hmem Hge,
+                ... < ε - dist x x' + dist x x' : add_lt_add_right this
-      apply not_not_elim Hmem,
+                ... = ε                         : sub_add_cancel},
-      rewrite dist_comm at Hge,
+    {existsi 1, split, exact zero_lt_one, exact subset_univ _},
-      apply absurd Hy Hge
+    {cases ihs (and.left Hx) with rs aux, cases aux with rspos ballrs_sub,
-    end,
+      cases iht (and.right Hx) with rt aux, cases aux with rtpos ballrt_sub,
-    apply absurd HU,
+      let rmin := min rs rt,
-    apply not_open_of_ex_boundary_pt Hx H,
+      existsi rmin, split, exact lt_min rspos rtpos,
-    cases exists_mem_of_ne_empty a with r Hr,
+      have open_ball x rmin ⊆ s,
-    cases Hr with _ Hr,
+        from subset.trans (open_ball_subset_open_ball_of_le x !min_le_left) ballrs_sub,
-    cases Hr with Hrpos HxrU,
+      have open_ball x rmin ⊆ t,
-    existsi r,
+        from subset.trans (open_ball_subset_open_ball_of_le x !min_le_right) ballrt_sub,
-    split,
+      show open_ball x (min rs rt) ⊆ s ∩ t,
-    repeat assumption
+        by apply subset_inter; repeat assumption},
+  cases Hx with s aux, cases aux with sS xs,
+  cases (ihS sS xs) with r aux, cases aux with rpos ballr_sub,
+  existsi r, split, exact rpos,
+  show open_ball x r ⊆ ⋃₀ S, from subset.trans ballr_sub (subset_sUnion_of_mem sS)
 end
 
-
 /- limits in metric spaces -/
 
 proposition eventually_nhds_intro {P : M → Prop} {ε : ℝ} (εpos : ε > 0) {x : M}
     (H : ∀ x', dist x' x < ε → P x') :
   eventually P (nhds x) :=
-topology.eventually_nhds_intro (open_ball_open x ε) (mem_open_ball x εpos) H
+topology.eventually_nhds_intro (Open_open_ball x ε) (mem_open_ball x εpos) H
 
 proposition eventually_nhds_dest {P : M → Prop} {x : M} (H : eventually P (nhds x)) :
   ∃ ε, ε > 0 ∧ ∀ x', dist x' x < ε → P x' :=
 obtain s [(Os : Open s) [(xs : x ∈ s) (Hs : ∀₀ x' ∈ s, P x')]],
   from topology.eventually_nhds_dest H,
 obtain ε [(εpos : ε > 0) (Hε : open_ball x ε ⊆ s)],
-  from exists_Open_ball_subset_of_Open_of_mem Os xs,
+  from exists_open_ball_subset_of_Open_of_mem Os xs,
 exists.intro ε (and.intro εpos
   (take x', suppose dist x' x < ε,
     have x' ∈ s, from Hε this,
@@ -293,7 +182,7 @@ eventually_nhds_intro εpos (λ x' H, H)
 proposition eventually_at_within_intro {P : M → Prop} {ε : ℝ} (εpos : ε > 0) {x : M} {s : set M}
   (H : ∀₀ x' ∈ s, dist x' x < ε → x' ≠ x → P x') :
  eventually P [at x within s] :=
-topology.eventually_at_within_intro (open_ball_open x ε) (mem_open_ball x εpos)
+topology.eventually_at_within_intro (Open_open_ball x ε) (mem_open_ball x εpos)
   (λ x' x'mem x'ne x's, H x's x'mem x'ne)
 
 proposition eventually_at_within_dest {P : M → Prop} {x : M} {s : set M}
@@ -302,7 +191,7 @@ proposition eventually_at_within_dest {P : M → Prop} {x : M} {s : set M}
 obtain t [(Ot : Open t) [(xt : x ∈ t) (Ht : ∀₀ x' ∈ t, x' ≠ x → x' ∈ s → P x')]],
   from topology.eventually_at_within_dest H,
 obtain ε [(εpos : ε > 0) (Hε : open_ball x ε ⊆ t)],
-  from exists_Open_ball_subset_of_Open_of_mem Ot xt,
+  from exists_open_ball_subset_of_Open_of_mem Ot xt,
 exists.intro ε (and.intro εpos
   (take x', assume x's distx'x x'nex,
     have x' ∈ t, from Hε distx'x,
@@ -316,7 +205,7 @@ iff.intro eventually_at_within_dest
 proposition eventually_at_intro {P : M → Prop} {ε : ℝ} (εpos : ε > 0) {x : M}
     (H : ∀ x', dist x' x < ε → x' ≠ x → P x') :
  eventually P [at x] :=
-topology.eventually_at_intro (open_ball_open x ε) (mem_open_ball x εpos)
+topology.eventually_at_intro (Open_open_ball x ε) (mem_open_ball x εpos)
   (λ x' x'mem x'ne, H x' x'mem x'ne)
 
 proposition eventually_at_dest {P : M → Prop} {x : M} (H : eventually P [at x]) :
@@ -662,13 +551,13 @@ theorem continuous_at_intro {f : M → N} {x : M}
   begin
     rewrite ↑continuous_at,
     intros U Uopen HfU,
-    cases exists_Open_ball_subset_of_Open_of_mem Uopen HfU with r Hr,
+    cases exists_open_ball_subset_of_Open_of_mem Uopen HfU with r Hr,
     cases Hr with Hr HUr,
     cases H Hr with δ Hδ,
     cases Hδ with Hδ Hx'δ,
     existsi open_ball x δ,
     split,
-    apply open_ball_open,
+    apply Open_open_ball,
     split,
     apply mem_open_ball,
     exact Hδ,
@@ -684,10 +573,10 @@ theorem continuous_at_elim {f : M → N} {x : M} (Hfx : continuous_at f x) :
   begin
     intros ε Hε,
     rewrite [↑continuous_at at Hfx],
-    cases @Hfx (open_ball (f x) ε) !open_ball_open (mem_open_ball _ Hε) with V HV,
+    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,
-    cases exists_Open_ball_subset_of_Open_of_mem HV HVx with δ Hδ,
+    cases exists_open_ball_subset_of_Open_of_mem HV HVx with δ Hδ,
     cases Hδ with Hδ Hδx,
     existsi δ,
     split,