From 5744f8975a45a7a59da61aa4e68e7035234ac029 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Thu, 4 Jun 2020 04:42:31 +0000 Subject: [PATCH] chore(*): fix some `ge_or_gt` lint issues (#2945) Also rename a few definitions: * `ge_of_forall_ge_sub` : `le_of_forall_sub_le`; * `power_series.order_ge_nat` : `power_series.nat_le_order`; * `power_series.order_ge`: `power_series.le_order`; --- src/algebra/ordered_field.lean | 4 +- src/algebra/ordered_group.lean | 42 +++++----- src/analysis/normed_space/basic.lean | 1 + src/data/complex/exponential.lean | 1 + src/data/real/pi.lean | 8 +- src/group_theory/order_of_element.lean | 4 + src/measure_theory/integration.lean | 2 +- src/number_theory/dioph.lean | 18 ++--- src/number_theory/pell.lean | 81 ++++++++++--------- src/order/complete_lattice.lean | 2 + src/ring_theory/noetherian.lean | 2 + src/ring_theory/power_series.lean | 22 ++--- src/tactic/lint/misc.lean | 2 - src/topology/algebra/polynomial.lean | 1 + src/topology/instances/ennreal.lean | 3 + src/topology/instances/real.lean | 2 +- src/topology/metric_space/baire.lean | 2 +- src/topology/metric_space/basic.lean | 23 ++++-- src/topology/metric_space/completion.lean | 3 + src/topology/metric_space/emetric_space.lean | 19 ++++- .../uniform_space/absolute_value.lean | 1 + 21 files changed, 144 insertions(+), 99 deletions(-) diff --git a/src/algebra/ordered_field.lean b/src/algebra/ordered_field.lean index a23f7fcc49f93..4a30fc9938200 100644 --- a/src/algebra/ordered_field.lean +++ b/src/algebra/ordered_field.lean @@ -322,7 +322,7 @@ begin apply one_div_pos_of_pos he end -lemma exists_add_lt_and_pos_of_lt {a b : α} (h : b < a) : ∃ c : α, b + c < a ∧ c > 0 := +lemma exists_add_lt_and_pos_of_lt {a b : α} (h : b < a) : ∃ c : α, b + c < a ∧ 0 < c := begin apply exists.intro ((a - b) / (1 + 1)), split, @@ -340,7 +340,7 @@ begin exact div_pos_of_pos_of_pos (sub_pos_of_lt h) two_pos end -lemma ge_of_forall_ge_sub {a b : α} (h : ∀ ε : α, ε > 0 → a ≥ b - ε) : a ≥ b := +lemma le_of_forall_sub_le {a b : α} (h : ∀ ε > 0, b - ε ≤ a) : b ≤ a := begin apply le_of_not_gt, intro hb, diff --git a/src/algebra/ordered_group.lean b/src/algebra/ordered_group.lean index 4dcbcb6fe6075..e33420a72091f 100644 --- a/src/algebra/ordered_group.lean +++ b/src/algebra/ordered_group.lean @@ -42,7 +42,7 @@ lemma add_le_add' (h₁ : a ≤ b) (h₂ : c ≤ d) : a + c ≤ b + d := le_trans (add_le_add_right' h₁) (add_le_add_left' h₂) lemma le_add_of_nonneg_right' (h : 0 ≤ b) : a ≤ a + b := -have a + b ≥ a + 0, from add_le_add_left' h, +have a + 0 ≤ a + b, from add_le_add_left' h, by rwa add_zero at this lemma le_add_of_nonneg_left' (h : 0 ≤ b) : a ≤ b + a := @@ -452,11 +452,11 @@ end lemma add_le_add {a b c d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) : a + c ≤ b + d := le_trans (add_le_add_right h₁ c) (add_le_add_left h₂ b) -lemma le_add_of_nonneg_right (h : b ≥ 0) : a ≤ a + b := -have a + b ≥ a + 0, from add_le_add_left h a, +lemma le_add_of_nonneg_right (h : 0 ≤ b) : a ≤ a + b := +have a + 0 ≤ a + b, from add_le_add_left h a, by rwa add_zero at this -lemma le_add_of_nonneg_left (h : b ≥ 0) : a ≤ b + a := +lemma le_add_of_nonneg_left (h : 0 ≤ b) : a ≤ b + a := have 0 + a ≤ b + a, from add_le_add_right h a, by rwa zero_add at this @@ -469,11 +469,11 @@ lt_of_le_of_lt (add_le_add_right h₁ c) (add_lt_add_left h₂ b) lemma add_lt_add_of_lt_of_le (h₁ : a < b) (h₂ : c ≤ d) : a + c < b + d := lt_of_lt_of_le (add_lt_add_right h₁ c) (add_le_add_left h₂ b) -lemma lt_add_of_pos_right (a : α) {b : α} (h : b > 0) : a < a + b := +lemma lt_add_of_pos_right (a : α) {b : α} (h : 0 < b) : a < a + b := have a + 0 < a + b, from add_lt_add_left h a, by rwa [add_zero] at this -lemma lt_add_of_pos_left (a : α) {b : α} (h : b > 0) : a < b + a := +lemma lt_add_of_pos_left (a : α) {b : α} (h : 0 < b) : a < b + a := have 0 + a < b + a, from add_lt_add_right h a, by rwa [zero_add] at this @@ -1077,13 +1077,13 @@ add_lt_add_of_le_of_lt hab (neg_lt_neg hcd) lemma sub_lt_sub_of_lt_of_le (hab : a < b) (hcd : c ≤ d) : a - d < b - c := add_lt_add_of_lt_of_le hab (neg_le_neg hcd) -lemma sub_le_self (a : α) {b : α} (h : b ≥ 0) : a - b ≤ a := +lemma sub_le_self (a : α) {b : α} (h : 0 ≤ b) : a - b ≤ a := calc a - b = a + -b : rfl ... ≤ a + 0 : add_le_add_left (neg_nonpos_of_nonneg h) _ ... = a : by rw add_zero -lemma sub_lt_self (a : α) {b : α} (h : b > 0) : a - b < a := +lemma sub_lt_self (a : α) {b : α} (h : 0 < b) : a - b < a := calc a - b = a + -b : rfl ... < a + 0 : add_lt_add_left (neg_neg_of_pos h) _ @@ -1362,11 +1362,11 @@ by rw [min_neg_neg, neg_neg] def abs (a : α) : α := max a (-a) -lemma abs_of_nonneg {a : α} (h : a ≥ 0) : abs a = a := +lemma abs_of_nonneg {a : α} (h : 0 ≤ a) : abs a = a := have h' : -a ≤ a, from le_trans (neg_nonpos_of_nonneg h) h, max_eq_left h' -lemma abs_of_pos {a : α} (h : a > 0) : abs a = a := +lemma abs_of_pos {a : α} (h : 0 < a) : abs a = a := abs_of_nonneg (le_of_lt h) lemma abs_of_nonpos {a : α} (h : a ≤ 0) : abs a = -a := @@ -1382,10 +1382,10 @@ abs_of_nonneg (le_refl _) lemma abs_neg (a : α) : abs (-a) = abs a := begin unfold abs, rw [max_comm, neg_neg] end -lemma abs_pos_of_pos {a : α} (h : a > 0) : abs a > 0 := +lemma abs_pos_of_pos {a : α} (h : 0 < a) : 0 < abs a := by rwa (abs_of_pos h) -lemma abs_pos_of_neg {a : α} (h : a < 0) : abs a > 0 := +lemma abs_pos_of_neg {a : α} (h : a < 0) : 0 < abs a := abs_neg a ▸ abs_pos_of_pos (neg_pos_of_neg h) lemma abs_sub (a b : α) : abs (a - b) = abs (b - a) := @@ -1399,7 +1399,7 @@ assume ha, h (eq.symm ha ▸ abs_zero) lemma eq_zero_of_neg_eq {a : α} (h : -a = a) : a = 0 := match lt_trichotomy a 0 with | or.inl h₁ := - have a > 0, from h ▸ neg_pos_of_neg h₁, + have 0 < a, from h ▸ neg_pos_of_neg h₁, absurd h₁ (lt_asymm this) | or.inr (or.inl h₁) := h₁ | or.inr (or.inr h₁) := @@ -1407,7 +1407,7 @@ match lt_trichotomy a 0 with absurd h₁ (lt_asymm this) end -lemma abs_nonneg (a : α) : abs a ≥ 0 := +lemma abs_nonneg (a : α) : 0 ≤ abs a := or.elim (le_total 0 a) (assume h : 0 ≤ a, by rwa (abs_of_nonneg h)) (assume h : a ≤ 0, calc @@ -1435,7 +1435,7 @@ lemma eq_of_abs_sub_eq_zero {a b : α} (h : abs (a - b) = 0) : a = b := have a - b = 0, from eq_zero_of_abs_eq_zero h, show a = b, from eq_of_sub_eq_zero this -lemma abs_pos_of_ne_zero {a : α} (h : a ≠ 0) : abs a > 0 := +lemma abs_pos_of_ne_zero {a : α} (h : a ≠ 0) : 0 < abs a := or.elim (lt_or_gt_of_ne h) abs_pos_of_neg abs_pos_of_pos lemma abs_by_cases (P : α → Prop) {a : α} (h1 : P a) (h2 : P (-a)) : P (abs a) := @@ -1449,14 +1449,14 @@ abs_by_cases (λ x : α, x ≤ b) h1 h2 lemma abs_lt_of_lt_of_neg_lt {a b : α} (h1 : a < b) (h2 : -a < b) : abs a < b := abs_by_cases (λ x : α, x < b) h1 h2 -private lemma aux1 {a b : α} (h1 : a + b ≥ 0) (h2 : a ≥ 0) : abs (a + b) ≤ abs a + abs b := +private lemma aux1 {a b : α} (h1 : 0 ≤ a + b) (h2 : 0 ≤ a) : abs (a + b) ≤ abs a + abs b := decidable.by_cases - (assume h3 : b ≥ 0, calc + (assume h3 : 0 ≤ b, calc abs (a + b) ≤ abs (a + b) : by apply le_refl ... = a + b : by rw (abs_of_nonneg h1) ... = abs a + b : by rw (abs_of_nonneg h2) ... = abs a + abs b : by rw (abs_of_nonneg h3)) - (assume h3 : ¬ b ≥ 0, + (assume h3 : ¬ 0 ≤ b, have h4 : b ≤ 0, from le_of_lt (lt_of_not_ge h3), calc abs (a + b) = a + b : by rw (abs_of_nonneg h1) @@ -1465,7 +1465,7 @@ decidable.by_cases ... ≤ abs a + -b : add_le_add_left (neg_nonneg_of_nonpos h4) _ ... = abs a + abs b : by rw (abs_of_nonpos h4)) -private lemma aux2 {a b : α} (h1 : a + b ≥ 0) : abs (a + b) ≤ abs a + abs b := +private lemma aux2 {a b : α} (h1 : 0 ≤ a + b) : abs (a + b) ≤ abs a + abs b := or.elim (le_total b 0) (assume h2 : b ≤ 0, have h3 : ¬ a < 0, from @@ -1493,8 +1493,8 @@ or.elim (le_total 0 (a + b)) (assume h2 : 0 ≤ a + b, aux2 h2) (assume h2 : a + b ≤ 0, have h3 : -a + -b = -(a + b), by rw neg_add, - have h4 : -(a + b) ≥ 0, from neg_nonneg_of_nonpos h2, - have h5 : -a + -b ≥ 0, begin rw [← h3] at h4, exact h4 end, + have h4 : 0 ≤ -(a + b), from neg_nonneg_of_nonpos h2, + have h5 : 0 ≤ -a + -b, begin rw [← h3] at h4, exact h4 end, calc abs (a + b) = abs (-a + -b) : by rw [← abs_neg, neg_add] ... ≤ abs (-a) + abs (-b) : aux2 h5 diff --git a/src/analysis/normed_space/basic.lean b/src/analysis/normed_space/basic.lean index 5b4d6d1dc9e04..77e0d1d51f353 100644 --- a/src/analysis/normed_space/basic.lean +++ b/src/analysis/normed_space/basic.lean @@ -195,6 +195,7 @@ calc ... ≤ ∥g∥ + ∥h - g∥ : norm_add_le _ _ ... < ∥g∥ + r : by { apply add_lt_add_left, rw ← dist_eq_norm, exact H } +@[nolint ge_or_gt] -- see Note [nolint_ge] theorem normed_group.tendsto_nhds_zero {f : γ → α} {l : filter γ} : tendsto f l (𝓝 0) ↔ ∀ ε > 0, ∀ᶠ x in l, ∥ f x ∥ < ε := metric.tendsto_nhds.trans $ by simp only [dist_zero_right] diff --git a/src/data/complex/exponential.lean b/src/data/complex/exponential.lean index 5b10a7774540b..7a24dafefb0ec 100644 --- a/src/data/complex/exponential.lean +++ b/src/data/complex/exponential.lean @@ -208,6 +208,7 @@ begin (λ _ _, rfl), end +@[nolint ge_or_gt] -- see Note [nolint_ge] lemma cauchy_product {a b : ℕ → β} (ha : is_cau_seq abs (λ m, (range m).sum (λ n, abv (a n)))) (hb : is_cau_seq abv (λ m, (range m).sum b)) (ε : α) (ε0 : 0 < ε) : diff --git a/src/data/real/pi.lean b/src/data/real/pi.lean index d053659b3fc6e..0c92bb802bcf8 100644 --- a/src/data/real/pi.lean +++ b/src/data/real/pi.lean @@ -19,11 +19,11 @@ lemma sqrt_two_add_series_zero : sqrt_two_add_series x 0 = x := by simp lemma sqrt_two_add_series_one : sqrt_two_add_series 0 1 = sqrt 2 := by simp lemma sqrt_two_add_series_two : sqrt_two_add_series 0 2 = sqrt (2 + sqrt 2) := by simp -lemma sqrt_two_add_series_zero_nonneg : ∀(n : ℕ), sqrt_two_add_series 0 n ≥ 0 +lemma sqrt_two_add_series_zero_nonneg : ∀(n : ℕ), 0 ≤ sqrt_two_add_series 0 n | 0 := le_refl 0 | (n+1) := sqrt_nonneg _ -lemma sqrt_two_add_series_nonneg {x : ℝ} (h : 0 ≤ x) : ∀(n : ℕ), sqrt_two_add_series x n ≥ 0 +lemma sqrt_two_add_series_nonneg {x : ℝ} (h : 0 ≤ x) : ∀(n : ℕ), 0 ≤ sqrt_two_add_series x n | 0 := h | (n+1) := sqrt_nonneg _ @@ -122,9 +122,9 @@ by { transitivity cos (pi / 2 ^ 5), congr, norm_num, simp } lemma sin_pi_div_thirty_two : sin (pi / 32) = sqrt (2 - sqrt (2 + sqrt (2 + sqrt 2))) / 2 := by { transitivity sin (pi / 2 ^ 5), congr, norm_num, simp } -lemma pi_gt_sqrt_two_add_series (n : ℕ) : pi > 2 ^ (n+1) * sqrt (2 - sqrt_two_add_series 0 n) := +lemma pi_gt_sqrt_two_add_series (n : ℕ) : 2 ^ (n+1) * sqrt (2 - sqrt_two_add_series 0 n) < pi := begin - have : pi > sqrt (2 - sqrt_two_add_series 0 n) / 2 * 2 ^ (n+2), + have : sqrt (2 - sqrt_two_add_series 0 n) / 2 * 2 ^ (n+2) < pi, { apply mul_lt_of_lt_div, apply pow_pos, norm_num, rw [←sin_pi_over_two_pow_succ], apply sin_lt, apply div_pos pi_pos, apply pow_pos, norm_num }, apply lt_of_le_of_lt (le_of_eq _) this, diff --git a/src/group_theory/order_of_element.lean b/src/group_theory/order_of_element.lean index 0f92a91c9f345..561ea9d318a3f 100644 --- a/src/group_theory/order_of_element.lean +++ b/src/group_theory/order_of_element.lean @@ -79,6 +79,7 @@ have a ^ (i - j) = 1, by simp [sub_eq_add_neg, gpow_add, gpow_neg, a_eq], ⟨i - j, sub_ne_zero.mpr ne, this⟩ +@[nolint ge_or_gt] -- see Note [nolint_ge] lemma exists_pow_eq_one (a : α) : ∃i > 0, a ^ i = 1 := let ⟨i, hi, eq⟩ := exists_gpow_eq_one a in begin @@ -279,9 +280,12 @@ section cyclic local attribute [instance] set_fintype +/-- A group is called *cyclic* if it is generated by a single element. -/ class is_cyclic (α : Type*) [group α] : Prop := (exists_generator [] : ∃ g : α, ∀ x, x ∈ gpowers g) +/-- A cyclic group is always commutative. This is not an `instance` because often we have a better +proof of `comm_group`. -/ def is_cyclic.comm_group [hg : group α] [is_cyclic α] : comm_group α := { mul_comm := λ x y, show x * y = y * x, from let ⟨g, hg⟩ := is_cyclic.exists_generator α in diff --git a/src/measure_theory/integration.lean b/src/measure_theory/integration.lean index 2f8eaca9af266..91203b10b791d 100644 --- a/src/measure_theory/integration.lean +++ b/src/measure_theory/integration.lean @@ -692,7 +692,7 @@ lemma monotone_lintegral (α : Type*) [measure_space α] : lemma lintegral_eq_nnreal (f : α → ennreal) : (∫⁻ a, f a) = - (⨆ (s : α →ₛ nnreal) (hf : f ≥ s.map (coe : nnreal → ennreal)), + (⨆ (s : α →ₛ nnreal) (hf : ⇑(s.map (coe : nnreal → ennreal)) ≤ f), (s.map (coe : nnreal → ennreal)).integral) := begin let c : nnreal → ennreal := coe, diff --git a/src/number_theory/dioph.lean b/src/number_theory/dioph.lean index 396b39a4c8ebb..291495d11b036 100644 --- a/src/number_theory/dioph.lean +++ b/src/number_theory/dioph.lean @@ -751,17 +751,17 @@ localized "infix ` D/ `:80 := dioph.div_dioph" in dioph omit df dg open pell -theorem pell_dioph : dioph (λv:vector3 ℕ 4, ∃ h : v &0 > 1, +theorem pell_dioph : dioph (λv:vector3 ℕ 4, ∃ h : 1 < v &0, xn h (v &1) = v &2 ∧ yn h (v &1) = v &3) := have dioph {v : vector3 ℕ 4 | -v &0 > 1 ∧ v &1 ≤ v &3 ∧ +1 < v &0 ∧ v &1 ≤ v &3 ∧ (v &2 = 1 ∧ v &3 = 0 ∨ ∃ (u w s t b : ℕ), v &2 * v &2 - (v &0 * v &0 - 1) * v &3 * v &3 = 1 ∧ u * u - (v &0 * v &0 - 1) * w * w = 1 ∧ s * s - (b * b - 1) * t * t = 1 ∧ - b > 1 ∧ (b ≡ 1 [MOD 4 * v &3]) ∧ (b ≡ v &0 [MOD u]) ∧ - w > 0 ∧ v &3 * v &3 ∣ w ∧ + 1 < b ∧ (b ≡ 1 [MOD 4 * v &3]) ∧ (b ≡ v &0 [MOD u]) ∧ + 0 < w ∧ v &3 * v &3 ∣ w ∧ (s ≡ v &2 [MOD u]) ∧ (t ≡ v &1 [MOD 4 * v &3]))}, from D.1 D< D&0 D∧ D&1 D≤ D&3 D∧ @@ -776,18 +776,18 @@ D.1 D< D&0 D∧ D&1 D≤ D&3 D∧ (D≡ (D&1) (D&6) (D.4 D* D&8)))), dioph.ext this $ λv, matiyasevic.symm -theorem xn_dioph : dioph_pfun (λv:vector3 ℕ 2, ⟨v &0 > 1, λh, xn h (v &1)⟩) := -have dioph (λv:vector3 ℕ 3, ∃ y, ∃ h : v &1 > 1, xn h (v &2) = v &0 ∧ yn h (v &2) = y), from +theorem xn_dioph : dioph_pfun (λv:vector3 ℕ 2, ⟨1 < v &0, λh, xn h (v &1)⟩) := +have dioph (λv:vector3 ℕ 3, ∃ y, ∃ h : 1 < v &1, xn h (v &2) = v &0 ∧ yn h (v &2) = y), from let D_pell := @reindex_dioph _ (fin2 4) _ pell_dioph [&2, &3, &1, &0] in D∃3 D_pell, (dioph_pfun_vec _).2 $ dioph.ext this $ λv, ⟨λ⟨y, h, xe, ye⟩, ⟨h, xe⟩, λ⟨h, xe⟩, ⟨_, h, xe, rfl⟩⟩ include df dg theorem pow_dioph : dioph_fn (λv, f v ^ g v) := have dioph {v : vector3 ℕ 3 | -v &2 = 0 ∧ v &0 = 1 ∨ v &2 > 0 ∧ -(v &1 = 0 ∧ v &0 = 0 ∨ v &1 > 0 ∧ +v &2 = 0 ∧ v &0 = 1 ∨ 0 < v &2 ∧ +(v &1 = 0 ∧ v &0 = 0 ∨ 0 < v &1 ∧ ∃ (w a t z x y : ℕ), - (∃ (a1 : a > 1), xn a1 (v &2) = x ∧ yn a1 (v &2) = y) ∧ + (∃ (a1 : 1 < a), xn a1 (v &2) = x ∧ yn a1 (v &2) = y) ∧ (x ≡ y * (a - v &1) + v &0 [MOD t]) ∧ 2 * a * v &1 = t + (v &1 * v &1 + 1) ∧ v &0 < t ∧ v &1 ≤ w ∧ v &2 ≤ w ∧ diff --git a/src/number_theory/pell.lean b/src/number_theory/pell.lean index 57e38c6f2d921..7214d5c01ef52 100644 --- a/src/number_theory/pell.lean +++ b/src/number_theory/pell.lean @@ -11,12 +11,13 @@ namespace pell open nat section - parameters {a : ℕ} (a1 : a > 1) + parameters {a : ℕ} (a1 : 1 < a) include a1 private def d := a*a - 1 - @[simp] theorem d_pos : 0 < d := nat.sub_pos_of_lt (mul_lt_mul a1 (le_of_lt a1) dec_trivial dec_trivial : 1*1 0 := + theorem x_pos (n) : 0 < xn n := lt_of_le_of_lt (nat.zero_le n) (n_lt_xn n) - lemma eq_pell_lem : ∀n (b:ℤ√d), 1 ≤ b → is_pell b → pell_zd n ≥ b → ∃n, b = pell_zd n + lemma eq_pell_lem : ∀n (b:ℤ√d), 1 ≤ b → is_pell b → b ≤ pell_zd n → ∃n, b = pell_zd n | 0 b := λh1 hp hl, ⟨0, @zsqrtd.le_antisymm _ dnsq _ _ hl h1⟩ | (n+1) b := λh1 hp h, have a1p : (0:ℤ√d) ≤ ⟨a, 1⟩, from trivial, have am1p : (0:ℤ√d) ≤ ⟨a, -1⟩, from show (_:nat) ≤ _, by simp; exact nat.pred_le _, have a1m : (⟨a, 1⟩ * ⟨a, -1⟩ : ℤ√d) = 1, from is_pell_norm.1 is_pell_one, - if ha : b ≥ ⟨↑a, 1⟩ then + if ha : (⟨↑a, 1⟩ : ℤ√d) ≤ b then let ⟨m, e⟩ := eq_pell_lem n (b * ⟨a, -1⟩) (by rw ← a1m; exact mul_le_mul_of_nonneg_right ha am1p) (is_pell_mul hp (is_pell_conj.1 is_pell_one)) @@ -230,7 +231,7 @@ section ⟨λh, nat.dvd_of_mod_eq_zero $ (nat.eq_zero_or_pos _).resolve_right $ λhp, have co : nat.coprime (yn m) (xn (m * (n / m))), from nat.coprime.symm $ (xy_coprime _).coprime_dvd_right (y_mul_dvd m (n / m)), - have m0 : m > 0, from m.eq_zero_or_pos.resolve_left $ + have m0 : 0 < m, from m.eq_zero_or_pos.resolve_left $ λe, by rw [e, nat.mod_zero] at hp; rw [e] at h; exact have 0 < yn a1 n, from y_increasing _ hp, ne_of_lt (y_increasing a1 hp) (eq_zero_of_zero_dvd h).symm, @@ -269,7 +270,7 @@ section theorem dvd_of_ysq_dvd {n t} (h : yn n * yn n ∣ yn t) : yn n ∣ t := have nt : n ∣ t, from (y_dvd_iff n t).1 $ dvd_of_mul_left_dvd h, - n.eq_zero_or_pos.elim (λn0, by rw n0; rw n0 at nt; exact nt) $ λ(n0l : n > 0), + n.eq_zero_or_pos.elim (λn0, by rw n0; rw n0 at nt; exact nt) $ λ(n0l : 0 < n), let ⟨k, ke⟩ := nt in have yn n ∣ k * (xn n)^(k-1), from nat.dvd_of_mul_dvd_mul_right (y_increasing n0l) $ modeq.modeq_zero_iff.1 $ @@ -396,7 +397,7 @@ section (nat.lt_add_of_pos_right $ mul_pos (d_pos a1) (y_increasing a1 np))) h, by cases this; simp at h; exact ⟨h.symm, rfl⟩ - theorem eq_of_xn_modeq_lem3 {i n} (npos : n > 0) : + theorem eq_of_xn_modeq_lem3 {i n} (npos : 0 < n) : Π {j}, i < j → j ≤ 2 * n → j ≠ n → ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2) → xn i % xn n < xn j % xn n | 0 ij _ _ _ := absurd ij (nat.not_lt_zero _) | (j+1) ij j2n jnn ntriv := @@ -450,34 +451,34 @@ section rw [nat.sub_succ], exact nat.pred_lt (ne_of_gt $ nat.sub_pos_of_lt j2n) }) - theorem eq_of_xn_modeq_le {i j n} (npos : n > 0) (ij : i ≤ j) (j2n : j ≤ 2 * n) (h : xn i ≡ xn j [MOD xn n]) + theorem eq_of_xn_modeq_le {i j n} (npos : 0 < n) (ij : i ≤ j) (j2n : j ≤ 2 * n) (h : xn i ≡ xn j [MOD xn n]) (ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2)) : i = j := (lt_or_eq_of_le ij).resolve_left $ λij', if jn : j = n then by { refine ne_of_gt _ h, rw [jn, nat.mod_self], - have x0 : xn a1 0 % xn a1 n > 0 := by rw [nat.mod_eq_of_lt (x_increasing a1 npos)]; exact dec_trivial, + have x0 : 0 < xn a1 0 % xn a1 n := by rw [nat.mod_eq_of_lt (x_increasing a1 npos)]; exact dec_trivial, cases i with i, exact x0, rw jn at ij', exact lt_trans x0 (eq_of_xn_modeq_lem3 _ npos (nat.succ_pos _) (le_trans ij j2n) (ne_of_lt ij') $ λ⟨a1, n1, _, i2⟩, by rw [n1, i2] at ij'; exact absurd ij' dec_trivial) } else ne_of_lt (eq_of_xn_modeq_lem3 npos ij' j2n jn ntriv) h - theorem eq_of_xn_modeq {i j n} (npos : n > 0) (i2n : i ≤ 2 * n) (j2n : j ≤ 2 * n) (h : xn i ≡ xn j [MOD xn n]) + theorem eq_of_xn_modeq {i j n} (npos : 0 < n) (i2n : i ≤ 2 * n) (j2n : j ≤ 2 * n) (h : xn i ≡ xn j [MOD xn n]) (ntriv : a = 2 → n = 1 → (i = 0 → j ≠ 2) ∧ (i = 2 → j ≠ 0)) : i = j := (le_total i j).elim (λij, eq_of_xn_modeq_le npos ij j2n h $ λ⟨a2, n1, i0, j2⟩, (ntriv a2 n1).left i0 j2) (λij, (eq_of_xn_modeq_le npos ij i2n h.symm $ λ⟨a2, n1, j0, i2⟩, (ntriv a2 n1).right i2 j0).symm) - theorem eq_of_xn_modeq' {i j n} (ipos : i > 0) (hin : i ≤ n) (j4n : j ≤ 4 * n) (h : xn j ≡ xn i [MOD xn n]) : + theorem eq_of_xn_modeq' {i j n} (ipos : 0 < i) (hin : i ≤ n) (j4n : j ≤ 4 * n) (h : xn j ≡ xn i [MOD xn n]) : j = i ∨ j + i = 4 * n := have i2n : i ≤ 2*n, by apply le_trans hin; rw two_mul; apply nat.le_add_left, - have npos : n > 0, from lt_of_lt_of_le ipos hin, + have npos : 0 < n, from lt_of_lt_of_le ipos hin, (le_or_gt j (2 * n)).imp - (λj2n : j ≤ 2*n, eq_of_xn_modeq npos j2n i2n h $ + (λj2n : j ≤ 2 * n, eq_of_xn_modeq npos j2n i2n h $ λa2 n1, ⟨λj0 i2, by rw [n1, i2] at hin; exact absurd hin dec_trivial, λj2 i0, ne_of_gt ipos i0⟩) - (λj2n : j > 2*n, suffices i = 4*n - j, by rw [this, nat.add_sub_of_le j4n], + (λj2n : 2 * n < j, suffices i = 4*n - j, by rw [this, nat.add_sub_of_le j4n], have j42n : 4*n - j ≤ 2*n, from @nat.le_of_add_le_add_right j _ _ $ by rw [nat.sub_add_cancel j4n, show 4*n = 2*n + 2*n, from right_distrib 2 2 n]; exact nat.add_le_add_left (le_of_lt j2n) _, @@ -485,10 +486,10 @@ section (h.symm.trans $ let t := xn_modeq_x4n_sub j42n in by rwa [nat.sub_sub_self j4n] at t) (λa2 n1, ⟨λi0, absurd i0 (ne_of_gt ipos), λi2, by rw[n1, i2] at hin; exact absurd hin dec_trivial⟩)) - theorem modeq_of_xn_modeq {i j n} (ipos : i > 0) (hin : i ≤ n) (h : xn j ≡ xn i [MOD xn n]) : + theorem modeq_of_xn_modeq {i j n} (ipos : 0 < i) (hin : i ≤ n) (h : xn j ≡ xn i [MOD xn n]) : j ≡ i [MOD 4 * n] ∨ j + i ≡ 0 [MOD 4 * n] := let j' := j % (4 * n) in - have n4 : 4 * n > 0, from mul_pos dec_trivial (lt_of_lt_of_le ipos hin), + have n4 : 0 < 4 * n, from mul_pos dec_trivial (lt_of_lt_of_le ipos hin), have jl : j' < 4 * n, from nat.mod_lt _ n4, have jj : j ≡ j' [MOD 4 * n], by delta modeq; rw nat.mod_eq_of_lt jl, have ∀j q, xn (j + 4 * n * q) ≡ xn j [MOD xn n], begin @@ -504,7 +505,7 @@ section (modeq.symm (by rw ← nat.mod_add_div j (4*n); exact this j' _)).trans h) end -theorem xy_modeq_of_modeq {a b c} (a1 : a > 1) (b1 : b > 1) (h : a ≡ b [MOD c]) : +theorem xy_modeq_of_modeq {a b c} (a1 : 1 < a) (b1 : 1 < b) (h : a ≡ b [MOD c]) : ∀ n, xn a1 n ≡ xn b1 n [MOD c] ∧ yn a1 n ≡ yn b1 n [MOD c] | 0 := by constructor; refl | 1 := by simp; exact ⟨h, modeq.refl 1⟩ @@ -516,15 +517,15 @@ theorem xy_modeq_of_modeq {a b c} (a1 : a > 1) (b1 : b > 1) (h : a ≡ b [MOD c] by rw [yn_succ_succ a1, yn_succ_succ b1]; exact modeq.modeq_mul (modeq.modeq_mul_left _ h) (xy_modeq_of_modeq (n+1)).right⟩ -theorem matiyasevic {a k x y} : (∃ a1 : a > 1, xn a1 k = x ∧ yn a1 k = y) ↔ -a > 1 ∧ k ≤ y ∧ +theorem matiyasevic {a k x y} : (∃ a1 : 1 < a, xn a1 k = x ∧ yn a1 k = y) ↔ +1 < a ∧ k ≤ y ∧ (x = 1 ∧ y = 0 ∨ ∃ (u v s t b : ℕ), x * x - (a * a - 1) * y * y = 1 ∧ u * u - (a * a - 1) * v * v = 1 ∧ s * s - (b * b - 1) * t * t = 1 ∧ - b > 1 ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ - v > 0 ∧ y * y ∣ v ∧ + 1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ + 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y]) := ⟨λ⟨a1, hx, hy⟩, by rw [← hx, ← hy]; @@ -547,10 +548,10 @@ a > 1 ∧ k ≤ y ∧ have m1 : 1 < m, from have 0 < k * y, from mul_pos kpos (y_increasing a1 kpos), nat.mul_le_mul_left 2 this, - have vp : v > 0, from y_increasing a1 (lt_trans zero_lt_one m1), - have b1 : b > 1, from - have u > xn a1 1, from x_increasing a1 m1, - have u > a, by simp at this; exact this, + have vp : 0 < v, from y_increasing a1 (lt_trans zero_lt_one m1), + have b1 : 1 < b, from + have xn a1 1 < u, from x_increasing a1 m1, + have a < u, by simp at this; exact this, lt_of_lt_of_le a1 $ by delta modeq at ba; rw nat.mod_eq_of_lt this at ba; rw ← ba; apply nat.mod_le, let s := xn b1 k, t := yn b1 k in @@ -569,7 +570,7 @@ a > 1 ∧ k ≤ y ∧ | ._, ._, ⟨i, rfl, rfl⟩, ._, ._, ⟨n, rfl, rfl⟩, ._, ._, ⟨j, rfl, rfl⟩, ⟨(bm1 : b ≡ 1 [MOD 4 * yn a1 i]), (ba : b ≡ a [MOD xn a1 n]), - (vp : yn a1 n > 0), + (vp : 0 < yn a1 n), (yv : yn a1 i * yn a1 i ∣ yn a1 n), (sx : xn b1 j ≡ xn a1 i [MOD xn a1 n]), (tk : yn b1 j ≡ k [MOD 4 * yn a1 i])⟩, @@ -601,14 +602,14 @@ a > 1 ∧ k ≤ y ∧ end end⟩⟩ -lemma eq_pow_of_pell_lem {a y k} (a1 : 1 < a) (ypos : y > 0) : k > 0 → a > y^k → +lemma eq_pow_of_pell_lem {a y k} (a1 : 1 < a) (ypos : 0 < y) : 0 < k → y^k < a → (↑(y^k) : ℤ) < 2*a*y - y*y - 1 := -have y < a → 2*a*y ≥ a + (y*y + 1), begin +have y < a → a + (y*y + 1) ≤ 2*a*y, begin intro ya, induction y with y IH, exact absurd ypos (lt_irrefl _), cases nat.eq_zero_or_pos y with y0 ypos, { rw y0, simpa [two_mul], }, { rw [nat.mul_succ, nat.mul_succ, nat.succ_mul y], - have : 2 * a ≥ y + nat.succ y, + have : y + nat.succ y ≤ 2 * a, { change y + y < 2 * a, rw ← two_mul, exact mul_lt_mul_of_pos_left (nat.lt_of_succ_lt ya) dec_trivial }, have := add_le_add (IH ypos (nat.lt_of_succ_lt ya)) this, @@ -622,9 +623,9 @@ by rw sub_sub; apply le_sub_right_of_add_le; exact this (lt_of_le_of_lt y1 yak) theorem eq_pow_of_pell {m n k} : (n^k = m ↔ -k = 0 ∧ m = 1 ∨ k > 0 ∧ -(n = 0 ∧ m = 0 ∨ n > 0 ∧ -∃ (w a t z : ℕ) (a1 : a > 1), +k = 0 ∧ m = 1 ∨ 0 < k ∧ +(n = 0 ∧ m = 0 ∨ 0 < n ∧ +∃ (w a t z : ℕ) (a1 : 1 < a), xn a1 k ≡ yn a1 k * (a - n) + m [MOD t] ∧ 2 * a * n = t + (n * n + 1) ∧ m < t ∧ n ≤ w ∧ k ≤ w ∧ @@ -639,10 +640,10 @@ k = 0 ∧ m = 1 ∨ k > 0 ∧ let w := _root_.max n k in have nw : n ≤ w, from le_max_left _ _, have kw : k ≤ w, from le_max_right _ _, - have wpos : w > 0, from lt_of_lt_of_le npos nw, - have w1 : w + 1 > 1, from nat.succ_lt_succ wpos, + have wpos : 0 < w, from lt_of_lt_of_le npos nw, + have w1 : 1 < w + 1, from nat.succ_lt_succ wpos, let a := xn w1 w in - have a1 : a > 1, from x_increasing w1 wpos, + have a1 : 1 < a, from x_increasing w1 wpos, let x := xn a1 k, y := yn a1 k in let ⟨z, ze⟩ := show w ∣ yn w1 w, from modeq.modeq_zero_iff.1 $ modeq.trans (yn_modeq_a_sub_one w1 w) (modeq.modeq_zero_iff.2 $ dvd_refl _) in @@ -672,18 +673,18 @@ k = 0 ∧ m = 1 ∨ k > 0 ∧ | or.inl ⟨k0, m1⟩ := by rw [k0, m1]; refl | or.inr ⟨kpos, or.inl ⟨n0, m0⟩⟩ := by rw [n0, m0, nat.zero_pow kpos] | or.inr ⟨kpos, or.inr ⟨npos, w, a, t, z, - (a1 : a > 1), + (a1 : 1 < a), (tm : xn a1 k ≡ yn a1 k * (a - n) + m [MOD t]), (ta : 2 * a * n = t + (n * n + 1)), (mt : m < t), (nw : n ≤ w), (kw : k ≤ w), (zp : a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1)⟩⟩ := - have wpos : w > 0, from lt_of_lt_of_le npos nw, - have w1 : w + 1 > 1, from nat.succ_lt_succ wpos, + have wpos : 0 < w, from lt_of_lt_of_le npos nw, + have w1 : 1 < w + 1, from nat.succ_lt_succ wpos, let ⟨j, xj, yj⟩ := eq_pell w1 zp in by clear _match o _let_match; exact - have jpos : j > 0, from (nat.eq_zero_or_pos j).resolve_left $ λj0, + have jpos : 0 < j, from (nat.eq_zero_or_pos j).resolve_left $ λj0, have a1 : a = 1, by rw j0 at xj; exact xj, have 2 * n = t + (n * n + 1), by rw a1 at ta; exact ta, have n1 : n = 1, from diff --git a/src/order/complete_lattice.lean b/src/order/complete_lattice.lean index 80bd20882a6b8..a3d20798b60c1 100644 --- a/src/order/complete_lattice.lean +++ b/src/order/complete_lattice.lean @@ -192,6 +192,7 @@ iff.intro let ⟨a, ha, h⟩ := h _ h' in lt_irrefl a $ lt_of_le_of_lt (le_Sup ha) h) +@[nolint ge_or_gt] -- see Note [nolint_ge] lemma Inf_eq_bot : Inf s = ⊥ ↔ (∀b>⊥, ∃a∈s, a < b) := iff.intro (assume (h : Inf s = ⊥) b (hb : ⊥ < b), by rwa [←h, Inf_lt_iff] at hb) @@ -763,6 +764,7 @@ lemma supr_eq_top (f : ι → α) : supr f = ⊤ ↔ (∀b<⊤, ∃i, b < f i) : by rw [← Sup_range, Sup_eq_top]; from forall_congr (assume b, forall_congr (assume hb, set.exists_range_iff)) +@[nolint ge_or_gt] -- see Note [nolint_ge] lemma infi_eq_bot (f : ι → α) : infi f = ⊥ ↔ (∀b>⊥, ∃i, b > f i) := by rw [← Inf_range, Inf_eq_bot]; from forall_congr (assume b, forall_congr (assume hb, set.exists_range_iff)) diff --git a/src/ring_theory/noetherian.lean b/src/ring_theory/noetherian.lean index 1b7c5c21fc38d..55f3ba6460830 100644 --- a/src/ring_theory/noetherian.lean +++ b/src/ring_theory/noetherian.lean @@ -280,6 +280,7 @@ end open is_noetherian submodule function +@[nolint ge_or_gt] -- see Note [nolint_ge] theorem is_noetherian_iff_well_founded {R M} [ring R] [add_comm_group M] [module R M] : is_noetherian R M ↔ well_founded ((>) : submodule R M → submodule R M → Prop) := @@ -332,6 +333,7 @@ theorem is_noetherian_iff_well_founded rw [← hs₂, sup_assoc, ← submodule.span_union], simp } end⟩ +@[nolint ge_or_gt] -- see Note [nolint_ge] lemma well_founded_submodule_gt (R M) [ring R] [add_comm_group M] [module R M] : ∀ [is_noetherian R M], well_founded ((>) : submodule R M → submodule R M → Prop) := is_noetherian_iff_well_founded.mp diff --git a/src/ring_theory/power_series.lean b/src/ring_theory/power_series.lean index 6fa4eee5a8d9d..e2b148ad2d6f9 100644 --- a/src/ring_theory/power_series.lean +++ b/src/ring_theory/power_series.lean @@ -37,7 +37,7 @@ then formal power series in one variable form an integral domain. The `order` of a formal power series `φ` is the multiplicity of the variable `X` in `φ`. If the coefficients form an integral domain, then `order` is a valuation -(`order_mul`, `order_add_ge`). +(`order_mul`, `le_order_add`). ## Implementation notes @@ -1296,8 +1296,8 @@ multiplicity.zero _ /-- The order of a formal power series is at least `n` if the `i`th coefficient is `0` for all `i < n`.-/ -lemma order_ge_nat (φ : power_series α) (n : ℕ) (h : ∀ i < n, coeff α i φ = 0) : - order φ ≥ n := +lemma nat_le_order (φ : power_series α) (n : ℕ) (h : ∀ i < n, coeff α i φ = 0) : + ↑n ≤ order φ := begin by_contra H, rw not_le at H, have : (order φ).dom := enat.dom_of_le_some (le_of_lt H), @@ -1307,13 +1307,13 @@ end /-- The order of a formal power series is at least `n` if the `i`th coefficient is `0` for all `i < n`.-/ -lemma order_ge (φ : power_series α) (n : enat) (h : ∀ i : ℕ, ↑i < n → coeff α i φ = 0) : - order φ ≥ n := +lemma le_order (φ : power_series α) (n : enat) (h : ∀ i : ℕ, ↑i < n → coeff α i φ = 0) : + n ≤ order φ := begin induction n using enat.cases_on, { show _ ≤ _, rw [top_le_iff, order_eq_top], ext i, exact h _ (enat.coe_lt_top i) }, - { apply order_ge_nat, simpa only [enat.coe_lt_coe] using h } + { apply nat_le_order, simpa only [enat.coe_lt_coe] using h } end /-- The order of a formal power series is exactly `n` if the `n`th coefficient is nonzero, @@ -1346,8 +1346,8 @@ end /-- The order of the sum of two formal power series is at least the minimum of their orders.-/ -lemma order_add_ge (φ ψ : power_series α) : - order (φ + ψ) ≥ min (order φ) (order ψ) := +lemma le_order_add (φ ψ : power_series α) : + min (order φ) (order ψ) ≤ order (φ + ψ) := multiplicity.min_le_multiplicity_add private lemma order_add_of_order_eq.aux (φ ψ : power_series α) @@ -1369,7 +1369,7 @@ end lemma order_add_of_order_eq (φ ψ : power_series α) (h : order φ ≠ order ψ) : order (φ + ψ) = order φ ⊓ order ψ := begin - refine le_antisymm _ (order_add_ge _ _), + refine le_antisymm _ (le_order_add _ _), by_cases H₁ : order φ < order ψ, { apply order_add_of_order_eq.aux _ _ h H₁ }, by_cases H₂ : order ψ < order φ, @@ -1380,9 +1380,9 @@ end /-- The order of the product of two formal power series is at least the sum of their orders.-/ lemma order_mul_ge (φ ψ : power_series α) : - order (φ * ψ) ≥ order φ + order ψ := + order φ + order ψ ≤ order (φ * ψ) := begin - apply order_ge, + apply le_order, intros n hn, rw [coeff_mul, finset.sum_eq_zero], rintros ⟨i,j⟩ hij, by_cases hi : ↑i < order φ, diff --git a/src/tactic/lint/misc.lean b/src/tactic/lint/misc.lean index 2df6766329c3c..7ffbeaa424694 100644 --- a/src/tactic/lint/misc.lean +++ b/src/tactic/lint/misc.lean @@ -65,8 +65,6 @@ failures. -/ library_note "nolint_ge" - - /-! ## Linter for duplicate namespaces -/ diff --git a/src/topology/algebra/polynomial.lean b/src/topology/algebra/polynomial.lean index a154c2ead650f..d4d08c7ff8e77 100644 --- a/src/topology/algebra/polynomial.lean +++ b/src/topology/algebra/polynomial.lean @@ -11,6 +11,7 @@ import data.real.cau_seq open polynomial is_absolute_value +@[nolint ge_or_gt] -- see Note [nolint_ge] lemma polynomial.tendsto_infinity {α β : Type*} [comm_ring α] [discrete_linear_ordered_field β] (abv : α → β) [is_absolute_value abv] {p : polynomial α} (h : 0 < degree p) : ∀ x : β, ∃ r > 0, ∀ z : α, r < abv z → x < abv (p.eval z) := diff --git a/src/topology/instances/ennreal.lean b/src/topology/instances/ennreal.lean index 63caca6103efa..a67277248f6f9 100644 --- a/src/topology/instances/ennreal.lean +++ b/src/topology/instances/ennreal.lean @@ -157,6 +157,7 @@ by refine (homeomorph.set_congr $ set.ext $ λ x, _).trans ne_top_homeomorph_nnr -- using Icc because -- • don't have 'Ioo (x - ε) (x + ε) ∈ 𝓝 x' unless x > 0 -- • (x - y ≤ ε ↔ x ≤ ε + y) is true, while (x - y < ε ↔ x < ε + y) is not +@[nolint ge_or_gt] -- see Note [nolint_ge] lemma Icc_mem_nhds : x ≠ ⊤ → ε > 0 → Icc (x - ε) (x + ε) ∈ 𝓝 x := begin assume xt ε0, rw mem_nhds_sets_iff, @@ -168,6 +169,7 @@ begin exact ⟨is_open_Ioo, mem_Ioo_self_sub_add xt x0 ε0 ε0 ⟩ } end +@[nolint ge_or_gt] -- see Note [nolint_ge] lemma nhds_of_ne_top : x ≠ ⊤ → 𝓝 x = ⨅ε > 0, principal (Icc (x - ε) (x + ε)) := begin assume xt, refine le_antisymm _ _, @@ -195,6 +197,7 @@ end /-- Characterization of neighborhoods for `ennreal` numbers. See also `tendsto_order` for a version with strict inequalities. -/ +@[nolint ge_or_gt] -- see Note [nolint_ge] protected theorem tendsto_nhds {f : filter α} {u : α → ennreal} {a : ennreal} (ha : a ≠ ⊤) : tendsto u f (𝓝 a) ↔ ∀ ε > 0, ∀ᶠ x in f, (u x) ∈ Icc (a - ε) (a + ε) := by simp only [nhds_of_ne_top ha, tendsto_infi, tendsto_principal, mem_Icc] diff --git a/src/topology/instances/real.lean b/src/topology/instances/real.lean index 8ae95f6a1ede6..1e07deee3013b 100644 --- a/src/topology/instances/real.lean +++ b/src/topology/instances/real.lean @@ -244,7 +244,7 @@ metric.totally_bounded_iff.2 $ λ ε ε0, begin { have := lt_floor_add_one ((x - a) / ε), rwa [div_lt_iff' ε0, mul_add, mul_one] at this }, { have := floor_le ((x - a) / ε), - rwa [ge, sub_nonneg, ← le_sub_iff_add_le', ← le_div_iff' ε0] } } + rwa [sub_nonneg, ← le_sub_iff_add_le', ← le_div_iff' ε0] } } end lemma real.totally_bounded_ball (x ε : ℝ) : totally_bounded (ball x ε) := diff --git a/src/topology/metric_space/baire.lean b/src/topology/metric_space/baire.lean index 086dfa4a60fd5..70d3756823cfc 100644 --- a/src/topology/metric_space/baire.lean +++ b/src/topology/metric_space/baire.lean @@ -318,7 +318,7 @@ end /-- One of the most useful consequences of Baire theorem: if a countable union of closed sets covers the space, then one of the sets has nonempty interior. -/ theorem nonempty_interior_of_Union_of_closed [nonempty α] [encodable β] {f : β → set α} - (hc : ∀s, is_closed (f s)) (hU : (⋃s, f s) = univ) : ∃s x ε, ε > 0 ∧ ball x ε ⊆ f s := + (hc : ∀s, is_closed (f s)) (hU : (⋃s, f s) = univ) : ∃s x ε, 0 < ε ∧ ball x ε ⊆ f s := begin have : ∃s, (interior (f s)).nonempty, { by_contradiction h, diff --git a/src/topology/metric_space/basic.lean b/src/topology/metric_space/basic.lean index f9811dd5d9ad7..b327cf8052818 100644 --- a/src/topology/metric_space/basic.lean +++ b/src/topology/metric_space/basic.lean @@ -177,7 +177,8 @@ by simpa only [not_le] using not_congr dist_le_zero @[simp] theorem abs_dist {a b : α} : abs (dist a b) = dist a b := abs_of_nonneg dist_nonneg -theorem eq_of_forall_dist_le {x y : α} (h : ∀ε, ε > 0 → dist x y ≤ ε) : x = y := +@[nolint ge_or_gt] -- see Note [nolint_ge] +theorem eq_of_forall_dist_le {x y : α} (h : ∀ ε > 0, dist x y ≤ ε) : x = y := eq_of_dist_eq_zero (eq_of_le_of_forall_le_of_dense dist_nonneg h) /-- Distance as a nonnegative real number. -/ @@ -278,13 +279,13 @@ by rw [← ball_union_sphere, set.union_diff_cancel_right sphere_disjoint_ball.s @[simp] theorem closed_ball_diff_ball : closed_ball x ε \ ball x ε = sphere x ε := by rw [← ball_union_sphere, set.union_diff_cancel_left sphere_disjoint_ball.symm] -theorem pos_of_mem_ball (hy : y ∈ ball x ε) : ε > 0 := +theorem pos_of_mem_ball (hy : y ∈ ball x ε) : 0 < ε := lt_of_le_of_lt dist_nonneg hy -theorem mem_ball_self (h : ε > 0) : x ∈ ball x ε := +theorem mem_ball_self (h : 0 < ε) : x ∈ ball x ε := show dist x x < ε, by rw dist_self; assumption -theorem mem_closed_ball_self (h : ε ≥ 0) : x ∈ closed_ball x ε := +theorem mem_closed_ball_self (h : 0 ≤ ε) : x ∈ closed_ball x ε := show dist x x ≤ ε, by rw dist_self; assumption theorem mem_ball_comm : x ∈ ball y ε ↔ y ∈ ball x ε := @@ -312,6 +313,7 @@ lt_of_le_of_lt (dist_triangle z x y) (add_lt_add_of_lt_of_le zx h) theorem ball_half_subset (y) (h : y ∈ ball x (ε / 2)) : ball y (ε / 2) ⊆ ball x ε := ball_subset $ by rw sub_self_div_two; exact le_of_lt h +@[nolint ge_or_gt] -- see Note [nolint_ge] theorem exists_ball_subset_ball (h : y ∈ ball x ε) : ∃ ε' > 0, ball y ε' ⊆ ball x ε := ⟨_, sub_pos.2 h, ball_subset $ by rw sub_sub_self⟩ @@ -393,6 +395,7 @@ theorem uniformity_basis_dist_le : (𝓤 α).has_basis (λ ε : ℝ, 0 < ε) (λ ε, {p:α×α | dist p.1 p.2 ≤ ε}) := metric.mk_uniformity_basis_le (λ _, id) (λ ε ε₀, ⟨ε, ε₀, le_refl ε⟩) +@[nolint ge_or_gt] -- see Note [nolint_ge] theorem mem_uniformity_dist {s : set (α×α)} : s ∈ 𝓤 α ↔ (∃ε>0, ∀{a b:α}, dist a b < ε → (a, b) ∈ s) := uniformity_basis_dist.mem_uniformity_iff @@ -402,11 +405,13 @@ theorem dist_mem_uniformity {ε:ℝ} (ε0 : 0 < ε) : {p:α×α | dist p.1 p.2 < ε} ∈ 𝓤 α := mem_uniformity_dist.2 ⟨ε, ε0, λ a b, id⟩ +@[nolint ge_or_gt] -- see Note [nolint_ge] theorem uniform_continuous_iff [metric_space β] {f : α → β} : uniform_continuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀{a b:α}, dist a b < δ → dist (f a) (f b) < ε := uniformity_basis_dist.uniform_continuous_iff uniformity_basis_dist +@[nolint ge_or_gt] -- see Note [nolint_ge] theorem uniform_embedding_iff [metric_space β] {f : α → β} : uniform_embedding f ↔ function.injective f ∧ uniform_continuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ := @@ -419,6 +424,7 @@ uniform_embedding_def'.trans $ and_congr iff.rfl $ and_congr iff.rfl /-- A map between metric spaces is a uniform embedding if and only if the distance between `f x` and `f y` is controlled in terms of the distance between `x` and `y` and conversely. -/ +@[nolint ge_or_gt] -- see Note [nolint_ge] theorem uniform_embedding_iff' [metric_space β] {f : α → β} : uniform_embedding f ↔ (∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε) ∧ @@ -439,6 +445,7 @@ begin simpa using this } end +@[nolint ge_or_gt] -- see Note [nolint_ge] theorem totally_bounded_iff {s : set α} : totally_bounded s ↔ ∀ ε > 0, ∃t : set α, finite t ∧ s ⊆ ⋃y∈t, ball y ε := ⟨λ H ε ε0, H _ (dist_mem_uniformity ε0), @@ -448,6 +455,7 @@ theorem totally_bounded_iff {s : set α} : /-- A metric space space is totally bounded if one can reconstruct up to any ε>0 any element of the space from finitely many data. -/ +@[nolint ge_or_gt] -- see Note [nolint_ge] lemma totally_bounded_of_finite_discretization {α : Type u} [metric_space α] {s : set α} (H : ∀ε > (0 : ℝ), ∃ (β : Type u) [fintype β] (F : s → β), ∀x y, F x = F y → dist (x:α) y < ε) : @@ -615,6 +623,7 @@ theorem continuous_iff' [topological_space β] {f : β → α} : continuous f ↔ ∀a (ε > 0), ∀ᶠ x in 𝓝 a, dist (f x) (f a) < ε := continuous_iff_continuous_at.trans $ forall_congr $ λ b, tendsto_nhds +@[nolint ge_or_gt] -- see Note [nolint_ge] theorem tendsto_at_top [nonempty β] [semilattice_sup β] {u : β → α} {a : α} : tendsto u at_top (𝓝 a) ↔ ∀ε>0, ∃N, ∀n≥N, dist (u n) a < ε := (at_top_basis.tendsto_iff nhds_basis_ball).trans $ @@ -831,11 +840,13 @@ variables [nonempty β] [semilattice_sup β] /-- In a metric space, Cauchy sequences are characterized by the fact that, eventually, the distance between its elements is arbitrarily small -/ +@[nolint ge_or_gt] -- see Note [nolint_ge] theorem metric.cauchy_seq_iff {u : β → α} : cauchy_seq u ↔ ∀ε>0, ∃N, ∀m n≥N, dist (u m) (u n) < ε := uniformity_basis_dist.cauchy_seq_iff /-- A variation around the metric characterization of Cauchy sequences -/ +@[nolint ge_or_gt] -- see Note [nolint_ge] theorem metric.cauchy_seq_iff' {u : β → α} : cauchy_seq u ↔ ∀ε>0, ∃N, ∀n≥N, dist (u n) (u N) < ε := uniformity_basis_dist.cauchy_seq_iff' @@ -1597,14 +1608,14 @@ begin end /-- The diameter of a closed ball of radius `r` is at most `2 r`. -/ -lemma diam_closed_ball {r : ℝ} (h : r ≥ 0) : diam (closed_ball x r) ≤ 2 * r := +lemma diam_closed_ball {r : ℝ} (h : 0 ≤ r) : diam (closed_ball x r) ≤ 2 * r := diam_le_of_forall_dist_le (mul_nonneg (le_of_lt two_pos) h) $ λa ha b hb, calc dist a b ≤ dist a x + dist b x : dist_triangle_right _ _ _ ... ≤ r + r : add_le_add ha hb ... = 2 * r : by simp [mul_two, mul_comm] /-- The diameter of a ball of radius `r` is at most `2 r`. -/ -lemma diam_ball {r : ℝ} (h : r ≥ 0) : diam (ball x r) ≤ 2 * r := +lemma diam_ball {r : ℝ} (h : 0 ≤ r) : diam (ball x r) ≤ 2 * r := le_trans (diam_mono ball_subset_closed_ball bounded_closed_ball) (diam_closed_ball h) end diam diff --git a/src/topology/metric_space/completion.lean b/src/topology/metric_space/completion.lean index 5e0de9a0096ed..e5dae51338c9b 100644 --- a/src/topology/metric_space/completion.lean +++ b/src/topology/metric_space/completion.lean @@ -79,6 +79,7 @@ end /-- Elements of the uniformity (defined generally for completions) can be characterized in terms of the distance. -/ +@[nolint ge_or_gt] -- see Note [nolint_ge] protected lemma completion.mem_uniformity_dist (s : set (completion α × completion α)) : s ∈ uniformity (completion α) ↔ (∃ε>0, ∀{a b}, dist a b < ε → (a, b) ∈ s) := begin @@ -150,6 +151,7 @@ end /- Reformulate `completion.mem_uniformity_dist` in terms that are suitable for the definition of the metric space structure. -/ +@[nolint ge_or_gt] -- see Note [nolint_ge] protected lemma completion.uniformity_dist' : uniformity (completion α) = (⨅ε:{ε:ℝ // ε>0}, principal {p | dist p.1 p.2 < ε.val}) := begin @@ -160,6 +162,7 @@ begin { exact ⟨⟨1, zero_lt_one⟩⟩ } end +@[nolint ge_or_gt] -- see Note [nolint_ge] protected lemma completion.uniformity_dist : uniformity (completion α) = (⨅ ε>0, principal {p | dist p.1 p.2 < ε}) := by simpa [infi_subtype] using @completion.uniformity_dist' α _ diff --git a/src/topology/metric_space/emetric_space.lean b/src/topology/metric_space/emetric_space.lean index 13b45ae746fed..2fc74cc22641d 100644 --- a/src/topology/metric_space/emetric_space.lean +++ b/src/topology/metric_space/emetric_space.lean @@ -32,6 +32,7 @@ variables {α : Type u} {β : Type v} {γ : Type w} /-- Characterizing uniformities associated to a (generalized) distance function `D` in terms of the elements of the uniformity. -/ +@[nolint ge_or_gt] -- see Note [nolint_ge] theorem uniformity_dist_of_mem_uniformity [linear_order β] {U : filter (α × α)} (z : β) (D : α → α → β) (H : ∀ s, s ∈ U ↔ ∃ε>z, ∀{a b:α}, D a b < ε → (a, b) ∈ s) : U = ⨅ ε>z, principal {p:α×α | D p.1 p.2 < ε} := @@ -103,6 +104,7 @@ on a product. Continuity of `edist` is finally proving in `topology.instances.ennreal` -/ +@[nolint ge_or_gt] -- see Note [nolint_ge] class emetric_space (α : Type u) extends has_edist α : Type u := (edist_self : ∀ x : α, edist x x = 0) (eq_of_edist_eq_zero : ∀ {x y : α}, edist x y = 0 → x = y) @@ -185,7 +187,7 @@ lemma edist_le_range_sum_of_edist_le {f : ℕ → α} (n : ℕ) finset.Ico.zero_bot n ▸ edist_le_Ico_sum_of_edist_le (zero_le n) (λ _ _, hd) /-- Two points coincide if their distance is `< ε` for all positive ε -/ -theorem eq_of_forall_edist_le {x y : α} (h : ∀ε, ε > 0 → edist x y ≤ ε) : x = y := +theorem eq_of_forall_edist_le {x y : α} (h : ∀ε > 0, edist x y ≤ ε) : x = y := eq_of_edist_eq_zero (eq_of_le_of_forall_le_of_dense bot_le h) /-- Reformulation of the uniform structure in terms of the extended distance -/ @@ -202,6 +204,7 @@ theorem uniformity_basis_edist : ⟨1, ennreal.zero_lt_one⟩ /-- Characterization of the elements of the uniformity in terms of the extended distance -/ +@[nolint ge_or_gt] -- see Note [nolint_ge] theorem mem_uniformity_edist {s : set (α×α)} : s ∈ 𝓤 α ↔ (∃ε>0, ∀{a b:α}, edist a b < ε → (a, b) ∈ s) := uniformity_basis_edist.mem_uniformity_iff @@ -279,12 +282,14 @@ theorem uniformity_has_countable_basis : is_countably_generated (𝓤 α) := is_countably_generated_of_seq ⟨_, uniformity_basis_edist_inv_nat.eq_infi⟩ /-- ε-δ characterization of uniform continuity on emetric spaces -/ +@[nolint ge_or_gt] -- see Note [nolint_ge] theorem uniform_continuous_iff [emetric_space β] {f : α → β} : uniform_continuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀{a b:α}, edist a b < δ → edist (f a) (f b) < ε := uniformity_basis_edist.uniform_continuous_iff uniformity_basis_edist /-- ε-δ characterization of uniform embeddings on emetric spaces -/ +@[nolint ge_or_gt] -- see Note [nolint_ge] theorem uniform_embedding_iff [emetric_space β] {f : α → β} : uniform_embedding f ↔ function.injective f ∧ uniform_continuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ := @@ -297,6 +302,7 @@ uniform_embedding_def'.trans $ and_congr iff.rfl $ and_congr iff.rfl /-- A map between emetric spaces is a uniform embedding if and only if the edistance between `f x` and `f y` is controlled in terms of the distance between `x` and `y` and conversely. -/ +@[nolint ge_or_gt] -- see Note [nolint_ge] theorem uniform_embedding_iff' [emetric_space β] {f : α → β} : uniform_embedding f ↔ (∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, edist a b < δ → edist (f a) (f b) < ε) ∧ @@ -318,6 +324,7 @@ begin end /-- ε-δ characterization of Cauchy sequences on emetric spaces -/ +@[nolint ge_or_gt] -- see Note [nolint_ge] protected lemma cauchy_iff {f : filter α} : cauchy f ↔ f ≠ ⊥ ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x y ∈ t, edist x y < ε := uniformity_basis_edist.cauchy_iff @@ -546,6 +553,7 @@ theorem ball_subset (h : edist x y + ε₁ ≤ ε₂) (h' : edist x y < ⊤) : b ... < edist x y + ε₁ : (ennreal.add_lt_add_iff_left h').2 zx ... ≤ ε₂ : h +@[nolint ge_or_gt] -- see Note [nolint_ge] theorem exists_ball_subset_ball (h : y ∈ ball x ε) : ∃ ε' > 0, ball y ε' ⊆ ball x ε := begin have : 0 < ε - edist y x := by simpa using h, @@ -572,11 +580,14 @@ by rw [emetric.ball_eq_empty_iff] theorem nhds_basis_eball : (𝓝 x).has_basis (λ ε:ennreal, 0 < ε) (ball x) := nhds_basis_uniformity uniformity_basis_edist +@[nolint ge_or_gt] -- see Note [nolint_ge] theorem nhds_eq : 𝓝 x = (⨅ε>0, principal (ball x ε)) := nhds_basis_eball.eq_binfi +@[nolint ge_or_gt] -- see Note [nolint_ge] theorem mem_nhds_iff : s ∈ 𝓝 x ↔ ∃ε>0, ball x ε ⊆ s := nhds_basis_eball.mem_iff +@[nolint ge_or_gt] -- see Note [nolint_ge] theorem is_open_iff : is_open s ↔ ∀x∈s, ∃ε>0, ball x ε ⊆ s := by simp [is_open_iff_nhds, mem_nhds_iff] @@ -597,10 +608,12 @@ theorem mem_closure_iff : (mem_closure_iff_nhds_basis nhds_basis_eball).trans $ by simp only [mem_ball, edist_comm x] +@[nolint ge_or_gt] -- see Note [nolint_ge] theorem tendsto_nhds {f : filter β} {u : β → α} {a : α} : tendsto u f (𝓝 a) ↔ ∀ ε > 0, ∀ᶠ x in f, edist (u x) a < ε := nhds_basis_eball.tendsto_right_iff +@[nolint ge_or_gt] -- see Note [nolint_ge] theorem tendsto_at_top [nonempty β] [semilattice_sup β] (u : β → α) {a : α} : tendsto u at_top (𝓝 a) ↔ ∀ε>0, ∃N, ∀n≥N, edist (u n) a < ε := (at_top_basis.tendsto_iff nhds_basis_eball).trans $ @@ -608,11 +621,13 @@ theorem tendsto_at_top [nonempty β] [semilattice_sup β] (u : β → α) {a : /-- In an emetric space, Cauchy sequences are characterized by the fact that, eventually, the edistance between its elements is arbitrarily small -/ +@[nolint ge_or_gt] -- see Note [nolint_ge] theorem cauchy_seq_iff [nonempty β] [semilattice_sup β] {u : β → α} : cauchy_seq u ↔ ∀ε>0, ∃N, ∀m n≥N, edist (u m) (u n) < ε := uniformity_basis_edist.cauchy_seq_iff /-- A variation around the emetric characterization of Cauchy sequences -/ +@[nolint ge_or_gt] -- see Note [nolint_ge] theorem cauchy_seq_iff' [nonempty β] [semilattice_sup β] {u : β → α} : cauchy_seq u ↔ ∀ε>(0 : ennreal), ∃N, ∀n≥N, edist (u n) (u N) < ε := uniformity_basis_edist.cauchy_seq_iff' @@ -623,6 +638,7 @@ theorem cauchy_seq_iff_nnreal [nonempty β] [semilattice_sup β] {u : β → α} cauchy_seq u ↔ ∀ ε : nnreal, 0 < ε → ∃ N, ∀ n, N ≤ n → edist (u n) (u N) < ε := uniformity_basis_edist_nnreal.cauchy_seq_iff' +@[nolint ge_or_gt] -- see Note [nolint_ge] theorem totally_bounded_iff {s : set α} : totally_bounded s ↔ ∀ ε > 0, ∃t : set α, finite t ∧ s ⊆ ⋃y∈t, ball y ε := ⟨λ H ε ε0, H _ (edist_mem_uniformity ε0), @@ -630,6 +646,7 @@ theorem totally_bounded_iff {s : set α} : ⟨t, ft, h⟩ := H ε ε0 in ⟨t, ft, subset.trans h $ Union_subset_Union $ λ y, Union_subset_Union $ λ yt z, hε⟩⟩ +@[nolint ge_or_gt] -- see Note [nolint_ge] theorem totally_bounded_iff' {s : set α} : totally_bounded s ↔ ∀ ε > 0, ∃t⊆s, finite t ∧ s ⊆ ⋃y∈t, ball y ε := ⟨λ H ε ε0, (totally_bounded_iff_subset.1 H) _ (edist_mem_uniformity ε0), diff --git a/src/topology/uniform_space/absolute_value.lean b/src/topology/uniform_space/absolute_value.lean index 049e6b26152a3..3579ef6359c17 100644 --- a/src/topology/uniform_space/absolute_value.lean +++ b/src/topology/uniform_space/absolute_value.lean @@ -58,6 +58,7 @@ def uniform_space_core : uniform_space.core R := def uniform_space : uniform_space R := uniform_space.of_core (uniform_space_core abv) +@[nolint ge_or_gt] -- see Note [nolint_ge] theorem mem_uniformity {s : set (R×R)} : s ∈ (uniform_space_core abv).uniformity ↔ (∃ε>0, ∀{a b:R}, abv (b - a) < ε → (a, b) ∈ s) :=