chore(topology/metric/hausdorff_distance): use infi/supr (#6611)

src/data/real/ennreal.lean

@@ -1471,6 +1471,11 @@ end infi
 
 section supr
 
+@[simp] lemma supr_eq_zero {ι : Sort*} {f : ι → ℝ≥0∞} : (⨆ i, f i) = 0 ↔ ∀ i, f i = 0 :=
+supr_eq_bot
+
+lemma sup_eq_zero {a b : ℝ≥0∞} : a ⊔ b = 0 ↔ a = 0 ∧ b = 0 := sup_eq_bot_iff
+
 lemma supr_coe_nat : (⨆n:ℕ, (n : ℝ≥0∞)) = ∞ :=
 (supr_eq_top _).2 $ assume b hb, ennreal.exists_nat_gt (lt_top_iff_ne_top.1 hb)
 

src/topology/instances/ennreal.lean

@@ -448,9 +448,6 @@ have Inf ((λb, ↑r - b) '' range b) = ↑r - (⨆i, b i),
     (ennreal.tendsto_coe_sub.comp (tendsto_id' inf_le_left)),
 by rw [eq, ←this]; simp [Inf_image, infi_range, -mem_range]; exact le_refl _
 
-lemma supr_eq_zero {ι : Sort*} {f : ι → ℝ≥0∞} : (⨆ i, f i) = 0 ↔ ∀ i, f i = 0 :=
-by simp_rw [← nonpos_iff_eq_zero, supr_le_iff]
-
 end topological_space
 
 section tsum

src/topology/metric_space/hausdorff_distance.lean

@@ -40,55 +40,44 @@ variables {α : Type u} {β : Type v} [emetric_space α] [emetric_space β] {x y
 /-! ### Distance of a point to a set as a function into `ℝ≥0∞`. -/
 
 /-- The minimal edistance of a point to a set -/
-def inf_edist (x : α) (s : set α) : ℝ≥0∞ := Inf ((edist x) '' s)
+def inf_edist (x : α) (s : set α) : ℝ≥0∞ := ⨅ y ∈ s, edist x y
 
-@[simp] lemma inf_edist_empty : inf_edist x ∅ = ∞ :=
-by unfold inf_edist; simp
+@[simp] lemma inf_edist_empty : inf_edist x ∅ = ∞ := infi_emptyset
+
+lemma le_inf_edist {d} : d ≤ inf_edist x s ↔ ∀ y ∈ s, d ≤ edist x y :=
+by simp only [inf_edist, le_infi_iff]
 
 /-- The edist to a union is the minimum of the edists -/
 @[simp] lemma inf_edist_union : inf_edist x (s ∪ t) = inf_edist x s ⊓ inf_edist x t :=
-by simp [inf_edist, image_union, Inf_union]
+infi_union
 
 /-- The edist to a singleton is the edistance to the single point of this singleton -/
 @[simp] lemma inf_edist_singleton : inf_edist x {y} = edist x y :=
-by simp [inf_edist]
+infi_singleton
 
 /-- The edist to a set is bounded above by the edist to any of its points -/
 lemma inf_edist_le_edist_of_mem (h : y ∈ s) : inf_edist x s ≤ edist x y :=
-Inf_le ((mem_image _ _ _).2 ⟨y, h, by refl⟩)
+binfi_le _ h
 
 /-- If a point `x` belongs to `s`, then its edist to `s` vanishes -/
 lemma inf_edist_zero_of_mem (h : x ∈ s) : inf_edist x s = 0 :=
 nonpos_iff_eq_zero.1 $ @edist_self _ _ x ▸ inf_edist_le_edist_of_mem h
 
 /-- The edist is monotonous with respect to inclusion -/
 lemma inf_edist_le_inf_edist_of_subset (h : s ⊆ t) : inf_edist x t ≤ inf_edist x s :=
-Inf_le_Inf (image_subset _ h)
+infi_le_infi_of_subset h
 
 /-- If the edist to a set is `< r`, there exists a point in the set at edistance `< r` -/
 lemma exists_edist_lt_of_inf_edist_lt {r : ℝ≥0∞} (h : inf_edist x s < r) :
   ∃y∈s, edist x y < r :=
-let ⟨t, ⟨ht, tr⟩⟩ :=  Inf_lt_iff.1 h in
-let ⟨y, ⟨ys, hy⟩⟩ := (mem_image _ _ _).1 ht in
-⟨y, ys, by rwa ← hy at tr⟩
+by simpa only [inf_edist, infi_lt_iff] using h
 
 /-- The edist of `x` to `s` is bounded by the sum of the edist of `y` to `s` and
 the edist from `x` to `y` -/
 lemma inf_edist_le_inf_edist_add_edist : inf_edist x s ≤ inf_edist y s + edist x y :=
-begin
-  have : ∀z ∈ s, Inf (edist x '' s) ≤ edist y z + edist x y := λz hz, calc
-    Inf (edist x '' s) ≤ edist x z :
-      Inf_le ((mem_image _ _ _).2 ⟨z, hz, by refl⟩)
-    ... ≤ edist x y + edist y z : edist_triangle _ _ _
-    ... = edist y z + edist x y : add_comm _ _,
-  have : (λz, z + edist x y) (Inf (edist y '' s)) = Inf ((λz, z + edist x y) '' (edist y '' s)),
-  { refine map_Inf_of_continuous_at_of_monotone _ _ (by simp),
-    { exact continuous_at_id.add continuous_at_const },
-    { assume a b h, simp, apply add_le_add_right h _ }},
-  simp only [inf_edist] at this,
-  rw [inf_edist, inf_edist, this, ← image_comp],
-  simpa only [and_imp, function.comp_app, le_Inf_iff, exists_imp_distrib, ball_image_iff]
-end
+calc (⨅ z ∈ s, edist x z) ≤ ⨅ z ∈ s, edist y z + edist x y :
+  binfi_le_binfi $ λ z hz, (edist_triangle _ _ _).trans_eq (add_comm _ _)
+... = (⨅ z ∈ s, edist y z) + edist x y : by simp only [ennreal.infi_add]
 
 /-- The edist to a set depends continuously on the point -/
 lemma continuous_inf_edist : continuous (λx, inf_edist x s) :=
@@ -128,20 +117,7 @@ end
 /-- The infimum edistance is invariant under isometries -/
 lemma inf_edist_image (hΦ : isometry Φ) :
   inf_edist (Φ x) (Φ '' t) = inf_edist x t :=
-begin
-  simp only [inf_edist],
-  apply congr_arg,
-  ext b, split,
-  { assume hb,
-    rcases (mem_image _ _ _).1 hb with ⟨y, ⟨hy, hy'⟩⟩,
-    rcases (mem_image _ _ _).1 hy with ⟨z, ⟨hz, hz'⟩⟩,
-    rw [← hy', ← hz', hΦ x z],
-    exact mem_image_of_mem _ hz },
-  { assume hb,
-    rcases (mem_image _ _ _).1 hb with ⟨y, ⟨hy, hy'⟩⟩,
-    rw [← hy', ← hΦ x y],
-    exact mem_image_of_mem _ (mem_image_of_mem _ hy) }
-end
+by simp only [inf_edist, infi_image, hΦ.edist_eq]
 
 end inf_edist --section
 
@@ -150,10 +126,10 @@ end inf_edist --section
 /-- The Hausdorff edistance between two sets is the smallest `r` such that each set
 is contained in the `r`-neighborhood of the other one -/
 @[irreducible] def Hausdorff_edist {α : Type u} [emetric_space α] (s t : set α) : ℝ≥0∞ :=
-  Sup ((λx, inf_edist x t) '' s) ⊔ Sup ((λx, inf_edist x s) '' t)
+(⨆ x ∈ s, inf_edist x t) ⊔ (⨆ y ∈ t, inf_edist y s)
 
 lemma Hausdorff_edist_def {α : Type u} [emetric_space α] (s t : set α) :
-  Hausdorff_edist s t = Sup ((λx, inf_edist x t) '' s) ⊔ Sup ((λx, inf_edist x s) '' t) :=
+  Hausdorff_edist s t = (⨆ x ∈ s, inf_edist x t) ⊔ (⨆ y ∈ t, inf_edist y s) :=
 by rw Hausdorff_edist
 
 section Hausdorff_edist
@@ -164,9 +140,8 @@ variables {α : Type u} {β : Type v} [emetric_space α] [emetric_space β]
 /-- The Hausdorff edistance of a set to itself vanishes -/
 @[simp] lemma Hausdorff_edist_self : Hausdorff_edist s s = 0 :=
 begin
-  erw [Hausdorff_edist_def, sup_idem, ← le_bot_iff],
-  apply Sup_le _,
-  simp [le_bot_iff, inf_edist_zero_of_mem, le_refl] {contextual := tt},
+  simp only [Hausdorff_edist_def, sup_idem, ennreal.supr_eq_zero],
+  exact λ x hx, inf_edist_zero_of_mem hx
 end
 
 /-- The Haudorff edistances of `s` to `t` and of `t` to `s` coincide -/
@@ -179,7 +154,7 @@ lemma Hausdorff_edist_le_of_inf_edist {r : ℝ≥0∞}
   (H1 : ∀x ∈ s, inf_edist x t ≤ r) (H2 : ∀x ∈ t, inf_edist x s ≤ r) :
   Hausdorff_edist s t ≤ r :=
 begin
-  simp only [Hausdorff_edist, -mem_image, set.ball_image_iff, Sup_le_iff, sup_le_iff],
+  simp only [Hausdorff_edist, sup_le_iff, supr_le_iff],
   exact ⟨H1, H2⟩
 end
 
@@ -202,8 +177,8 @@ end
 lemma inf_edist_le_Hausdorff_edist_of_mem (h : x ∈ s) : inf_edist x t ≤ Hausdorff_edist s t :=
 begin
   rw Hausdorff_edist_def,
-  refine le_trans (le_Sup _) le_sup_left,
-  exact mem_image_of_mem _ h
+  refine le_trans _ le_sup_left,
+  exact le_bsupr x h
 end
 
 /-- If the Hausdorff distance is `<r`, then any point in one of the sets has
@@ -212,9 +187,8 @@ lemma exists_edist_lt_of_Hausdorff_edist_lt {r : ℝ≥0∞} (h : x ∈ s)
   (H : Hausdorff_edist s t < r) :
   ∃y∈t, edist x y < r :=
 exists_edist_lt_of_inf_edist_lt $ calc
-  inf_edist x t ≤ Sup ((λx, inf_edist x t) '' s) : le_Sup (mem_image_of_mem _ h)
-  ... ≤ Sup ((λx, inf_edist x t) '' s) ⊔ Sup ((λx, inf_edist x s) '' t) : le_sup_left
-  ... < r : by rwa Hausdorff_edist_def at H
+  inf_edist x t ≤ Hausdorff_edist s t : inf_edist_le_Hausdorff_edist_of_mem h
+  ... < r : H
 
 /-- The distance from `x` to `s` or `t` is controlled in terms of the Hausdorff distance
 between `s` and `t` -/
@@ -240,32 +214,7 @@ end
 /-- The Hausdorff edistance is invariant under eisometries -/
 lemma Hausdorff_edist_image (h : isometry Φ) :
   Hausdorff_edist (Φ '' s) (Φ '' t) = Hausdorff_edist s t :=
-begin
-  unfold Hausdorff_edist,
-  congr,
-  { ext b,
-    split,
-    { assume hb,
-      rcases (mem_image _ _ _ ).1 hb with ⟨y, ⟨hy, hy'⟩⟩,
-      rcases (mem_image _ _ _ ).1 hy with ⟨z, ⟨hz, hz'⟩⟩,
-      rw [← hy', ← hz', inf_edist_image h],
-      exact mem_image_of_mem _ hz },
-    { assume hb,
-      rcases (mem_image _ _ _ ).1 hb with ⟨y, ⟨hy, hy'⟩⟩,
-      rw [← hy', ← inf_edist_image h],
-      exact mem_image_of_mem _ (mem_image_of_mem _ hy) }},
-  { ext b,
-    split,
-    { assume hb,
-      rcases (mem_image _ _ _ ).1 hb with ⟨y, ⟨hy, hy'⟩⟩,
-      rcases (mem_image _ _ _ ).1 hy with ⟨z, ⟨hz, hz'⟩⟩,
-      rw [← hy', ← hz', inf_edist_image h],
-      exact mem_image_of_mem _ hz },
-    { assume hb,
-      rcases (mem_image _ _ _ ).1 hb with ⟨y, ⟨hy, hy'⟩⟩,
-      rw [← hy', ← inf_edist_image h],
-      exact mem_image_of_mem _ (mem_image_of_mem _ hy) }}
-end
+by simp only [Hausdorff_edist_def, supr_image, inf_edist_image h]
 
 /-- The Hausdorff distance is controlled by the diameter of the union -/
 lemma Hausdorff_edist_le_ediam (hs : s.nonempty) (ht : t.nonempty) :
@@ -284,8 +233,7 @@ end
 lemma Hausdorff_edist_triangle : Hausdorff_edist s u ≤ Hausdorff_edist s t + Hausdorff_edist t u :=
 begin
   rw Hausdorff_edist_def,
-  simp only [and_imp, set.mem_image, Sup_le_iff, exists_imp_distrib,
-             sup_le_iff, -mem_image, set.ball_image_iff],
+  simp only [sup_le_iff, supr_le_iff],
   split,
   show ∀x ∈ s, inf_edist x u ≤ Hausdorff_edist s t + Hausdorff_edist t u, from λx xs, calc
     inf_edist x u ≤ inf_edist x t + Hausdorff_edist t u : inf_edist_le_inf_edist_add_Hausdorff_edist
@@ -298,17 +246,21 @@ begin
     ... = Hausdorff_edist s t + Hausdorff_edist t u : by simp [Hausdorff_edist_comm, add_comm]
 end
 
+/-- Two sets are at zero Hausdorff edistance if and only if they have the same closure -/
+lemma Hausdorff_edist_zero_iff_closure_eq_closure :
+  Hausdorff_edist s t = 0 ↔ closure s = closure t :=
+calc Hausdorff_edist s t = 0 ↔ s ⊆ closure t ∧ t ⊆ closure s :
+  by simp only [Hausdorff_edist_def, ennreal.sup_eq_zero, ennreal.supr_eq_zero,
+    ← mem_closure_iff_inf_edist_zero, subset_def]
+... ↔ closure s = closure t :
+  ⟨λ h, subset.antisymm (closure_minimal h.1 is_closed_closure)
+     (closure_minimal h.2 is_closed_closure),
+   λ h, ⟨h ▸ subset_closure, h.symm ▸ subset_closure⟩⟩
+
 /-- The Hausdorff edistance between a set and its closure vanishes -/
 @[simp, priority 1100]
 lemma Hausdorff_edist_self_closure : Hausdorff_edist s (closure s) = 0 :=
-begin
-  erw ← le_bot_iff,
-  simp only [Hausdorff_edist, inf_edist_closure, -nonpos_iff_eq_zero, and_imp,
-    set.mem_image, Sup_le_iff, exists_imp_distrib, sup_le_iff,
-    set.ball_image_iff, ennreal.bot_eq_zero, -mem_image],
-  simp only [inf_edist_zero_of_mem, mem_closure_iff_inf_edist_zero, le_refl, and_self,
-             forall_true_iff] {contextual := tt}
-end
+by rw [Hausdorff_edist_zero_iff_closure_eq_closure, closure_closure]
 
 /-- Replacing a set by its closure does not change the Hausdorff edistance. -/
 @[simp] lemma Hausdorff_edist_closure₁ : Hausdorff_edist (closure s) t = Hausdorff_edist s t :=
@@ -330,33 +282,10 @@ by simp [@Hausdorff_edist_comm _ _ s _]
   Hausdorff_edist (closure s) (closure t) = Hausdorff_edist s t :=
 by simp
 
-/-- Two sets are at zero Hausdorff edistance if and only if they have the same closure -/
-lemma Hausdorff_edist_zero_iff_closure_eq_closure :
-  Hausdorff_edist s t = 0 ↔ closure s = closure t :=
-⟨begin
-  assume h,
-  refine subset.antisymm _ _,
-  { have : s ⊆ closure t := λx xs, mem_closure_iff_inf_edist_zero.2 $ begin
-      erw ← le_bot_iff,
-      have := @inf_edist_le_Hausdorff_edist_of_mem _ _ _ _ t xs,
-      rwa h at this,
-    end,
-    by rw ← @closure_closure _ _ t; exact closure_mono this },
-  { have : t ⊆ closure s := λx xt, mem_closure_iff_inf_edist_zero.2 $ begin
-      erw ← le_bot_iff,
-      have := @inf_edist_le_Hausdorff_edist_of_mem _ _ _ _ s xt,
-      rw Hausdorff_edist_comm at h,
-      rwa h at this,
-    end,
-    by rw ← @closure_closure _ _ s; exact closure_mono this }
-end,
-λh, by rw [← Hausdorff_edist_closure, h, Hausdorff_edist_self]⟩
-
 /-- Two closed sets are at zero Hausdorff edistance if and only if they coincide -/
 lemma Hausdorff_edist_zero_iff_eq_of_closed (hs : is_closed s) (ht : is_closed t) :
   Hausdorff_edist s t = 0 ↔ s = t :=
-by rw [Hausdorff_edist_zero_iff_closure_eq_closure, hs.closure_eq,
-       ht.closure_eq]
+by rw [Hausdorff_edist_zero_iff_closure_eq_closure, hs.closure_eq, ht.closure_eq]
 
 /-- The Haudorff edistance to the empty set is infinite -/
 lemma Hausdorff_edist_empty (ne : s.nonempty) : Hausdorff_edist s ∅ = ∞ :=