diff --git a/src/algebra/ordered_group.lean b/src/algebra/ordered_group.lean index 2dc34338c0595..3f294e46a6732 100644 --- a/src/algebra/ordered_group.lean +++ b/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 diff --git a/src/analysis/calculus/fderiv.lean b/src/analysis/calculus/fderiv.lean index f4dfcd9c8271e..97f4a5a3744cd 100644 --- a/src/analysis/calculus/fderiv.lean +++ b/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, diff --git a/src/data/real/basic.lean b/src/data/real/basic.lean index 560671d1deafb..df2366b566761 100644 --- a/src/data/real/basic.lean +++ b/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 := diff --git a/src/data/real/ennreal.lean b/src/data/real/ennreal.lean index 1ff7cf3009a49..944e969fe1e51 100644 --- a/src/data/real/ennreal.lean +++ b/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) := diff --git a/src/data/real/nnreal.lean b/src/data/real/nnreal.lean index 5501285a68b11..446c328cfb85d 100644 --- a/src/data/real/nnreal.lean +++ 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⟩, diff --git a/src/measure_theory/lebesgue_measure.lean b/src/measure_theory/lebesgue_measure.lean index ee8f3cf660f84..b93316b152de8 100644 --- a/src/measure_theory/lebesgue_measure.lean +++ b/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ε) _), diff --git a/src/measure_theory/outer_measure.lean b/src/measure_theory/outer_measure.lean index b7482998b925d..010f656c7375d 100644 --- a/src/measure_theory/outer_measure.lean +++ b/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) _), diff --git a/src/topology/metric_space/gluing.lean b/src/topology/metric_space/gluing.lean index 30b5b1d7e2ba2..a4cb5116934e7 100644 --- a/src/topology/metric_space/gluing.lean +++ b/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⟩, diff --git a/src/topology/metric_space/gromov_hausdorff.lean b/src/topology/metric_space/gromov_hausdorff.lean index 1a5fc54b9a46d..1fb7abaa39c8c 100644 --- a/src/topology/metric_space/gromov_hausdorff.lean +++ b/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⟩, diff --git a/src/topology/metric_space/hausdorff_distance.lean b/src/topology/metric_space/hausdorff_distance.lean index 087c331b08a60..f64986d379062 100644 --- a/src/topology/metric_space/hausdorff_distance.lean +++ b/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'), diff --git a/src/topology/metric_space/isometry.lean b/src/topology/metric_space/isometry.lean index e2ee77ec722c4..3ca928c8ea023 100644 --- a/src/topology/metric_space/isometry.lean +++ b/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 -/