chore(data/real/*): rename le_of_forall_epsilon_le to `le_of_forall…

…_pos_le_add` (#5761)

* generalize the `real` version to a `linear_ordered_add_comm_group`;
* rename `nnreal` and `ennreal` versions.

src/algebra/ordered_group.lean

@@ -576,6 +576,11 @@ lemma linear_ordered_add_comm_group.add_lt_add_left
   (a b : α) (h : a < b) (c : α) : c + a < c + b :=
 ordered_add_comm_group.add_lt_add_left a b h c
 
+lemma le_of_forall_pos_le_add [densely_ordered α] (h : ∀ ε : α, 0 < ε → a ≤ b + ε) : a ≤ b :=
+le_of_forall_le_of_dense $ λ c hc,
+calc a ≤ b + (c - b) : h _ (sub_pos_of_lt hc)
+   ... = c           : add_sub_cancel'_right _ _
+
 lemma min_neg_neg (a b : α) : min (-a) (-b) = -max a b :=
 eq.symm $ @monotone.map_max α (order_dual α) _ _ has_neg.neg a b $ λ a b, neg_le_neg
 

src/analysis/calculus/fderiv.lean

@@ -294,7 +294,7 @@ on a neighborhood of `x₀` then it its derivative at `x₀` has norm bounded by
 lemma has_fderiv_at.le_of_lip {f : E → F} {f' : E →L[𝕜] F} {x₀ : E} (hf : has_fderiv_at f f' x₀)
   {s : set E} (hs : s ∈ 𝓝 x₀) {C : ℝ≥0} (hlip : lipschitz_on_with C f s) : ∥f'∥ ≤ C :=
 begin
-  refine real.le_of_forall_epsilon_le (λ ε ε0, op_norm_le_of_nhds_zero _ _),
+  refine le_of_forall_pos_le_add (λ ε ε0, op_norm_le_of_nhds_zero _ _),
   exact add_nonneg C.coe_nonneg ε0.le,
   have hs' := hs, rw [← map_add_left_nhds_zero x₀, mem_map] at hs',
   filter_upwards [is_o_iff.1 (has_fderiv_at_iff_is_o_nhds_zero.1 hf) ε0, hs'], intros y hy hys,

src/data/real/basic.lean

@@ -159,11 +159,6 @@ noncomputable instance decidable_lt (a b : ℝ) : decidable (a < b) := by apply_
 noncomputable instance decidable_le (a b : ℝ) : decidable (a ≤ b) := by apply_instance
 noncomputable instance decidable_eq (a b : ℝ) : decidable (a = b) := by apply_instance
 
-lemma le_of_forall_epsilon_le {a b : real} (h : ∀ε, 0 < ε → a ≤ b + ε) : a ≤ b :=
-le_of_forall_le_of_dense $ assume x hxb,
-calc  a ≤ b + (x - b) : h (x-b) $ sub_pos.2 hxb
-    ... = x : by rw [add_comm]; simp
-
 open rat
 
 @[simp] theorem of_rat_eq_cast : ∀ x : ℚ, of_rat x = x :=

src/data/real/ennreal.lean

@@ -411,14 +411,14 @@ with_top.add_lt_add_iff_right
 lemma lt_add_right (ha : a < ∞) (hb : 0 < b) : a < a + b :=
 by rwa [← add_lt_add_iff_left ha, add_zero] at hb
 
-lemma le_of_forall_epsilon_le : ∀{a b : ennreal}, (∀ε:ℝ≥0, 0 < ε → b < ∞ → a ≤ b + ε) → a ≤ b
+lemma le_of_forall_pos_le_add : ∀{a b : ennreal}, (∀ε:ℝ≥0, 0 < ε → b < ∞ → a ≤ b + ε) → a ≤ b
 | a    none     h := le_top
 | none (some a) h :=
   have ∞ ≤ ↑a + ↑(1:ℝ≥0), from h 1 zero_lt_one coe_lt_top,
   by rw [← coe_add] at this; exact (not_top_le_coe this).elim
 | (some a) (some b) h :=
     by simp only [none_eq_top, some_eq_coe, coe_add.symm, coe_le_coe, coe_lt_top, true_implies_iff]
-      at *; exact nnreal.le_of_forall_epsilon_le h
+      at *; exact nnreal.le_of_forall_pos_le_add h
 
 lemma lt_iff_exists_rat_btwn :
   a < b ↔ (∃q:ℚ, 0 ≤ q ∧ a < nnreal.of_real q ∧ (nnreal.of_real q:ennreal) < b) :=

src/data/real/nnreal.lean

@@ -305,7 +305,7 @@ instance : archimedean ℝ≥0 :=
   let ⟨n, hr⟩ := archimedean.arch (x:ℝ) (pos_y : (0 : ℝ) < y) in
   ⟨n, show (x:ℝ) ≤ (n •ℕ y : ℝ≥0), by simp [*, -nsmul_eq_mul, nsmul_coe]⟩ ⟩
 
-lemma le_of_forall_epsilon_le {a b : ℝ≥0} (h : ∀ε, 0 < ε → a ≤ b + ε) : a ≤ b :=
+lemma le_of_forall_pos_le_add {a b : ℝ≥0} (h : ∀ε, 0 < ε → a ≤ b + ε) : a ≤ b :=
 le_of_forall_le_of_dense $ assume x hxb,
 begin
   rcases le_iff_exists_add.1 (le_of_lt hxb) with ⟨ε, rfl⟩,

src/measure_theory/lebesgue_measure.lean

@@ -49,7 +49,7 @@ begin
     (infi_le_infi $ λ a, infi_le_infi $ λ b, infi_le_infi2 $ λ h,
       ⟨subset.trans h Ioo_subset_Ico_self, le_refl _⟩) _,
   refine le_infi (λ a, le_infi $ λ b, le_infi $ λ h, _),
-  refine ennreal.le_of_forall_epsilon_le (λ ε ε0 _, _),
+  refine ennreal.le_of_forall_pos_le_add (λ ε ε0 _, _),
   refine infi_le_of_le (a - ε) (infi_le_of_le b $ infi_le_of_le
     (subset.trans h $ Ico_subset_Ioo_left $ (sub_lt_self_iff _).2 ε0) _),
   rw ← sub_add,
@@ -77,7 +77,7 @@ begin
     (infi_le_infi $ λ a, infi_le_infi $ λ b, infi_le_infi2 $ λ h,
       ⟨subset.trans h Ico_subset_Icc_self, le_refl _⟩),
   refine le_infi (λ a, le_infi $ λ b, le_infi $ λ h, _),
-  refine ennreal.le_of_forall_epsilon_le (λ ε ε0 _, _),
+  refine ennreal.le_of_forall_pos_le_add (λ ε ε0 _, _),
   refine infi_le_of_le a (infi_le_of_le (b + ε) $ infi_le_of_le
     (subset.trans h $ Icc_subset_Ico_right $ (lt_add_iff_pos_right _).2 ε0) _),
   rw [← sub_add_eq_add_sub],
@@ -137,7 +137,7 @@ end
   lebesgue_outer (Icc a b) = of_real (b - a) :=
 begin
   refine le_antisymm (by rw ← lebesgue_length_Icc; apply lebesgue_outer_le_length)
-    (le_binfi $ λ f hf, ennreal.le_of_forall_epsilon_le $ λ ε ε0 h, _),
+    (le_binfi $ λ f hf, ennreal.le_of_forall_pos_le_add $ λ ε ε0 h, _),
   rcases ennreal.exists_pos_sum_of_encodable
     (ennreal.zero_lt_coe_iff.2 ε0) ℕ with ⟨ε', ε'0, hε⟩,
   refine le_trans _ (add_le_add_left (le_of_lt hε) _),
@@ -189,7 +189,7 @@ begin
   refine le_antisymm (λ s, _) (outer_measure.le_trim _),
   rw outer_measure.trim_eq_infi,
   refine le_infi (λ f, le_infi $ λ hf,
-    ennreal.le_of_forall_epsilon_le $ λ ε ε0 h, _),
+    ennreal.le_of_forall_pos_le_add $ λ ε ε0 h, _),
   rcases ennreal.exists_pos_sum_of_encodable
     (ennreal.zero_lt_coe_iff.2 ε0) ℕ with ⟨ε', ε'0, hε⟩,
   refine le_trans _ (add_le_add_left (le_of_lt hε) _),

src/measure_theory/outer_measure.lean

@@ -310,7 +310,7 @@ let μ := λs, ⨅{f : ℕ → set α} (h : s ⊆ ⋃i, f i), ∑'i, m (f i) in
     (zero_le _),
   mono       := assume s₁ s₂ hs, infi_le_infi $ assume f,
     infi_le_infi2 $ assume hb, ⟨subset.trans hs hb, le_refl _⟩,
-  Union_nat := assume s, ennreal.le_of_forall_epsilon_le $ begin
+  Union_nat := assume s, ennreal.le_of_forall_pos_le_add $ begin
     assume ε hε (hb : ∑'i, μ (s i) < ⊤),
     rcases ennreal.exists_pos_sum_of_encodable (ennreal.coe_lt_coe.2 hε) ℕ with ⟨ε', hε', hl⟩,
     refine le_trans _ (add_le_add_left (le_of_lt hl) _),

src/topology/metric_space/gluing.lean

@@ -172,7 +172,7 @@ private lemma glue_dist_triangle (Φ : γ → α) (Ψ : γ → β) (ε : ℝ)
         ... = dist x (Φ p) + dist y (Ψ p) + dist y z : by ring },
     linarith
   end
-| (inl x) (inr y) (inl z) := real.le_of_forall_epsilon_le $ λδ δpos, begin
+| (inl x) (inr y) (inl z) := le_of_forall_pos_le_add $ λδ δpos, begin
     have : ∃a ∈ range (λp, dist x (Φ p) + dist y (Ψ p)), a < infi (λp, dist x (Φ p) + dist y (Ψ p)) + δ/2 :=
       exists_lt_of_cInf_lt (range_nonempty _) (by rw [infi]; linarith),
     rcases this with ⟨a, arange, ha⟩,
@@ -192,7 +192,7 @@ private lemma glue_dist_triangle (Φ : γ → α) (Ψ : γ → β) (ε : ℝ)
       ... ≤ (infi (λp, dist x (Φ p) + dist y (Ψ p)) + ε) + (infi (λp, dist z (Φ p) + dist y (Ψ p)) + ε) + δ :
         by linarith
   end
-| (inr x) (inl y) (inr z) := real.le_of_forall_epsilon_le $ λδ δpos, begin
+| (inr x) (inl y) (inr z) := le_of_forall_pos_le_add $ λδ δpos, begin
     have : ∃a ∈ range (λp, dist y (Φ p) + dist x (Ψ p)), a < infi (λp, dist y (Φ p) + dist x (Ψ p)) + δ/2 :=
       exists_lt_of_cInf_lt (range_nonempty _) (by rw [infi]; linarith),
     rcases this with ⟨a, arange, ha⟩,

src/topology/metric_space/gromov_hausdorff.lean

@@ -531,7 +531,7 @@ theorem GH_dist_le_of_approx_subsets {s : set α} (Φ : s → β) {ε₁ ε₂ 
   (H : ∀x y : s, abs (dist x y - dist (Φ x) (Φ y)) ≤ ε₂) :
   GH_dist α β ≤ ε₁ + ε₂ / 2 + ε₃ :=
 begin
-  refine real.le_of_forall_epsilon_le (λδ δ0, _),
+  refine le_of_forall_pos_le_add (λδ δ0, _),
   rcases exists_mem_of_nonempty α with ⟨xα, _⟩,
   rcases hs xα with ⟨xs, hxs, Dxs⟩,
   have sne : s.nonempty := ⟨xs, hxs⟩,

src/topology/metric_space/hausdorff_distance.lean

@@ -99,7 +99,7 @@ continuous_of_le_add_edist 1 (by simp) $
 lemma inf_edist_closure : inf_edist x (closure s) = inf_edist x s :=
 begin
   refine le_antisymm (inf_edist_le_inf_edist_of_subset subset_closure) _,
-  refine ennreal.le_of_forall_epsilon_le (λε εpos h, _),
+  refine ennreal.le_of_forall_pos_le_add (λε εpos h, _),
   have εpos' : (0 : ennreal) < ε := by simpa,
   have : inf_edist x (closure s) < inf_edist x (closure s) + ε/2 :=
     ennreal.lt_add_right h (ennreal.half_pos εpos'),
@@ -221,7 +221,7 @@ exists_edist_lt_of_inf_edist_lt $ calc
 between `s` and `t` -/
 lemma inf_edist_le_inf_edist_add_Hausdorff_edist :
   inf_edist x t ≤ inf_edist x s + Hausdorff_edist s t :=
-ennreal.le_of_forall_epsilon_le $ λε εpos h, begin
+ennreal.le_of_forall_pos_le_add $ λε εpos h, begin
   have εpos' : (0 : ennreal) < ε := by simpa,
   have : inf_edist x s < inf_edist x s + ε/2 :=
     ennreal.lt_add_right (ennreal.add_lt_top.1 h).1 (ennreal.half_pos εpos'),

src/topology/metric_space/isometry.lean

@@ -343,7 +343,7 @@ end
 lemma embedding_of_subset_isometry (H : dense_range x) : isometry (embedding_of_subset x) :=
 begin
   refine isometry_emetric_iff_metric.2 (λa b, _),
-  refine (embedding_of_subset_dist_le x a b).antisymm (real.le_of_forall_epsilon_le (λe epos, _)),
+  refine (embedding_of_subset_dist_le x a b).antisymm (le_of_forall_pos_le_add (λe epos, _)),
   /- First step: find n with dist a (x n) < e -/
   rcases metric.mem_closure_range_iff.1 (H a) (e/2) (half_pos epos) with ⟨n, hn⟩,
   /- Second step: use the norm control at index n to conclude -/