refactor(data/*/interval): generalize finset.Ico to locally finite orders (#7987)

`finset.Ico` currently goes `ℕ → ℕ → finset ℕ`. This generalizes it to `α → α → finset α` where `locally_finite_order α`.
This also ports all the existing `finset.Ico` lemmas to the new API, which involves renaming and moving them to `data.finset.interval` or `data.nat.interval` depending on whether I could generalize them away from `ℕ` or not.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

Author: YaelDillies

src/algebra/big_operators/intervals.lean

@@ -5,7 +5,7 @@ Authors: Johannes Hölzl
 -/
 
 import algebra.big_operators.basic
-import data.finset.intervals
+import data.nat.interval
 import tactic.linarith
 
 /-!
@@ -25,7 +25,7 @@ variables {α : Type u} {β : Type v} {γ : Type w} {s₂ s₁ s : finset α} {a
 
 lemma sum_Ico_add {δ : Type*} [add_comm_monoid δ] (f : ℕ → δ) (m n k : ℕ) :
   (∑ l in Ico m n, f (k + l)) = (∑ l in Ico (m + k) (n + k), f l) :=
-Ico.image_add m n k ▸ eq.symm $ sum_image $ λ x hx y hy h, nat.add_left_cancel h
+image_add_const_Ico m n k ▸ eq.symm $ sum_image $ λ x hx y hy h, nat.add_left_cancel h
 
 @[to_additive]
 lemma prod_Ico_add (f : ℕ → β) (m n k : ℕ) :
@@ -34,7 +34,7 @@ lemma prod_Ico_add (f : ℕ → β) (m n k : ℕ) :
 
 lemma sum_Ico_succ_top {δ : Type*} [add_comm_monoid δ] {a b : ℕ}
   (hab : a ≤ b) (f : ℕ → δ) : (∑ k in Ico a (b + 1), f k) = (∑ k in Ico a b, f k) + f b :=
-by rw [Ico.succ_top hab, sum_insert Ico.not_mem_top, add_comm]
+by rw [nat.Ico_succ_right_eq_insert_Ico hab, sum_insert right_not_mem_Ico, add_comm]
 
 @[to_additive]
 lemma prod_Ico_succ_top {a b : ℕ} (hab : a ≤ b) (f : ℕ → β) :
@@ -44,7 +44,7 @@ lemma prod_Ico_succ_top {a b : ℕ} (hab : a ≤ b) (f : ℕ → β) :
 lemma sum_eq_sum_Ico_succ_bot {δ : Type*} [add_comm_monoid δ] {a b : ℕ}
   (hab : a < b) (f : ℕ → δ) : (∑ k in Ico a b, f k) = f a + (∑ k in Ico (a + 1) b, f k) :=
 have ha : a ∉ Ico (a + 1) b, by simp,
-by rw [← sum_insert ha, Ico.insert_succ_bot hab]
+by rw [← sum_insert ha, nat.Ico_insert_succ_left hab]
 
 @[to_additive]
 lemma prod_eq_prod_Ico_succ_bot {a b : ℕ} (hab : a < b) (f : ℕ → β) :
@@ -54,12 +54,12 @@ lemma prod_eq_prod_Ico_succ_bot {a b : ℕ} (hab : a < b) (f : ℕ → β) :
 @[to_additive]
 lemma prod_Ico_consecutive (f : ℕ → β) {m n k : ℕ} (hmn : m ≤ n) (hnk : n ≤ k) :
   (∏ i in Ico m n, f i) * (∏ i in Ico n k, f i) = (∏ i in Ico m k, f i) :=
-Ico.union_consecutive hmn hnk ▸ eq.symm $ prod_union $ Ico.disjoint_consecutive m n k
+Ico_union_Ico_eq_Ico hmn hnk ▸ eq.symm $ prod_union $ Ico_disjoint_Ico_consecutive m n k
 
 @[to_additive]
 lemma prod_range_mul_prod_Ico (f : ℕ → β) {m n : ℕ} (h : m ≤ n) :
   (∏ k in range m, f k) * (∏ k in Ico m n, f k) = (∏ k in range n, f k) :=
-Ico.zero_bot m ▸ Ico.zero_bot n ▸ prod_Ico_consecutive f (nat.zero_le m) h
+m.Ico_zero_eq_range ▸ n.Ico_zero_eq_range ▸ prod_Ico_consecutive f m.zero_le h
 
 @[to_additive]
 lemma prod_Ico_eq_mul_inv {δ : Type*} [comm_group δ] (f : ℕ → δ) {m n : ℕ} (h : m ≤ n) :
@@ -81,7 +81,7 @@ begin
     (λ (x : Σ (i : ℕ), ℕ) _, (⟨x.2, x.1⟩ : Σ (i : ℕ), ℕ)) _ (λ _ _, rfl)
     (λ (x : Σ (i : ℕ), ℕ) _, (⟨x.2, x.1⟩ : Σ (i : ℕ), ℕ)) _
     (by rintro ⟨⟩ _; refl) (by rintro ⟨⟩ _; refl);
-  simp only [finset.Ico.mem, sigma.forall, finset.mem_sigma];
+  simp only [finset.mem_Ico, sigma.forall, finset.mem_sigma];
   rintros a b ⟨⟨h₁,h₂⟩, ⟨h₃, h₄⟩⟩; refine ⟨⟨_, _⟩, ⟨_, _⟩⟩; linarith
 end
 
@@ -90,9 +90,9 @@ lemma prod_Ico_eq_prod_range (f : ℕ → β) (m n : ℕ) :
   (∏ k in Ico m n, f k) = (∏ k in range (n - m), f (m + k)) :=
 begin
   by_cases h : m ≤ n,
-  { rw [← Ico.zero_bot, prod_Ico_add, zero_add, nat.sub_add_cancel h] },
+  { rw [←nat.Ico_zero_eq_range, prod_Ico_add, zero_add, nat.sub_add_cancel h] },
   { replace h : n ≤ m :=  le_of_not_ge h,
-     rw [Ico.eq_empty_of_le h, nat.sub_eq_zero_of_le h, range_zero, prod_empty, prod_empty] }
+     rw [Ico_eq_empty_of_le h, nat.sub_eq_zero_of_le h, range_zero, prod_empty, prod_empty] }
 end
 
 lemma prod_Ico_reflect (f : ℕ → β) (k : ℕ) {m n : ℕ} (h : m ≤ n + 1) :
@@ -102,12 +102,12 @@ begin
   { intros i hi,
     exact (add_le_add_iff_right 1).1 (le_trans (nat.lt_iff_add_one_le.1 hi) h) },
   cases lt_or_le k m with hkm hkm,
-  { rw [← finset.Ico.image_const_sub (this _ hkm)],
+  { rw [← nat.Ico_image_const_sub_eq_Ico (this _ hkm)],
     refine (prod_image _).symm,
-    simp only [Ico.mem],
+    simp only [mem_Ico],
     rintros i ⟨ki, im⟩ j ⟨kj, jm⟩ Hij,
     rw [← nat.sub_sub_self (this _ im), Hij, nat.sub_sub_self (this _ jm)] },
-  { simp [Ico.eq_empty_of_le, nat.sub_le_sub_left, hkm] }
+  { simp [Ico_eq_empty_of_le, nat.sub_le_sub_left, hkm] }
 end
 
 lemma sum_Ico_reflect {δ : Type*} [add_comm_monoid δ] (f : ℕ → δ) (k : ℕ) {m n : ℕ}
@@ -120,8 +120,8 @@ lemma prod_range_reflect (f : ℕ → β) (n : ℕ) :
 begin
   cases n,
   { simp },
-  { simp only [range_eq_Ico, nat.succ_sub_succ_eq_sub, nat.sub_zero],
-    rw [prod_Ico_reflect _ _ (le_refl _)],
+  { simp only [←nat.Ico_zero_eq_range, nat.succ_sub_succ_eq_sub, nat.sub_zero],
+    rw prod_Ico_reflect _ _ le_rfl,
     simp }
 end
 

src/algebra/geom_sum.lean

@@ -353,15 +353,15 @@ lemma nat.geom_sum_Ico_le {b : ℕ} (hb : 2 ≤ b) (a n : ℕ) :
   ∑ i in Ico 1 n, a/b^i ≤ a/(b - 1) :=
 begin
   cases n,
-  { rw [Ico.eq_empty_of_le zero_le_one, sum_empty],
+  { rw [Ico_eq_empty_of_le zero_le_one, sum_empty],
     exact nat.zero_le _ },
   rw ←add_le_add_iff_left a,
   calc
     a + ∑ (i : ℕ) in Ico 1 n.succ, a/b^i
         = a/b^0 + ∑ (i : ℕ) in Ico 1 n.succ, a/b^i : by rw [pow_zero, nat.div_one]
     ... = ∑ i in range n.succ, a/b^i : begin
-          rw [range_eq_Ico, ←finset.Ico.insert_succ_bot (nat.succ_pos _), sum_insert],
-          exact λ h, zero_lt_one.not_le (Ico.mem.1 h).1,
+          rw [range_eq_Ico, ←nat.Ico_insert_succ_left (nat.succ_pos _), sum_insert],
+          exact λ h, zero_lt_one.not_le (mem_Ico.1 h).1,
         end
     ... ≤ a * b/(b - 1) : nat.geom_sum_le hb a _
     ... = (a * 1 + a * (b - 1))/(b - 1)

src/analysis/analytic/composition.lean

@@ -537,7 +537,7 @@ finset.sigma (finset.Ico m M) (λ (n : ℕ), fintype.pi_finset (λ (i : fin n),
 @[simp] lemma mem_comp_partial_sum_source_iff (m M N : ℕ) (i : Σ n, (fin n) → ℕ) :
   i ∈ comp_partial_sum_source m M N ↔
     (m ≤ i.1 ∧ i.1 < M) ∧ ∀ (a : fin i.1), 1 ≤ i.2 a ∧ i.2 a < N :=
-by simp only [comp_partial_sum_source, finset.Ico.mem, fintype.mem_pi_finset, finset.mem_sigma,
+by simp only [comp_partial_sum_source, finset.mem_Ico, fintype.mem_pi_finset, finset.mem_sigma,
   iff_self]
 
 /-- Change of variables appearing to compute the composition of partial sums of formal

src/analysis/analytic/inverse.lean

@@ -370,7 +370,7 @@ begin
   refine sum_le_sum_of_subset_of_nonneg _ (λ x hx1 hx2,
     prod_nonneg (λ j hj, mul_nonneg hr (mul_nonneg (pow_nonneg ha _) (hp _)))),
   rintros ⟨k, c⟩ hd,
-  simp only [set.mem_to_finset, Ico.mem, mem_sigma, set.mem_set_of_eq] at hd,
+  simp only [set.mem_to_finset, mem_Ico, mem_sigma, set.mem_set_of_eq] at hd,
   simp only [mem_comp_partial_sum_target_iff],
   refine ⟨hd.2, c.length_le.trans_lt hd.1.2, λ j, _⟩,
   have : c ≠ composition.single k (zero_lt_two.trans_le hd.1.1),
@@ -417,15 +417,15 @@ let I := ∥(i.symm : F →L[𝕜] E)∥ in calc
 ∑ k in Ico 1 (n + 1), a ^ k * ∥p.right_inv i k∥
     = a * I + ∑ k in Ico 2 (n + 1), a ^ k * ∥p.right_inv i k∥ :
 by simp only [linear_isometry_equiv.norm_map, pow_one, right_inv_coeff_one,
-              Ico.succ_singleton, sum_singleton, ← sum_Ico_consecutive _ one_le_two hn]
+              nat.Ico_succ_singleton, sum_singleton, ← sum_Ico_consecutive _ one_le_two hn]
 ... = a * I + ∑ k in Ico 2 (n + 1), a ^ k *
         ∥(i.symm : F →L[𝕜] E).comp_continuous_multilinear_map
           (∑ c in ({c | 1 < composition.length c}.to_finset : finset (composition k)),
             p.comp_along_composition (p.right_inv i) c)∥ :
 begin
   congr' 1,
   apply sum_congr rfl (λ j hj, _),
-  rw [right_inv_coeff _ _ _ (Ico.mem.1 hj).1, norm_neg],
+  rw [right_inv_coeff _ _ _ (mem_Ico.1 hj).1, norm_neg],
 end
 ... ≤ a * ∥(i.symm : F →L[𝕜] E)∥ + ∑ k in Ico 2 (n + 1), a ^ k * (I *
       (∑ c in ({c | 1 < composition.length c}.to_finset : finset (composition k)),
@@ -487,7 +487,7 @@ begin
   have IRec : ∀ n, 1 ≤ n → S n ≤ (I + 1) * a,
   { apply nat.le_induction,
     { simp only [S],
-      rw [Ico.eq_empty_of_le (le_refl 1), sum_empty],
+      rw [Ico_eq_empty_of_le (le_refl 1), sum_empty],
       exact mul_nonneg (add_nonneg (norm_nonneg _) zero_le_one) apos.le },
     { assume n one_le_n hn,
       have In : 2 ≤ n + 1, by linarith,

src/analysis/p_series.lean

@@ -50,7 +50,7 @@ begin
     exact add_le_add ihn this,
     exacts [n.one_le_two_pow, nat.pow_le_pow_of_le_right zero_lt_two n.le_succ] },
   have : ∀ k ∈ Ico (2 ^ n) (2 ^ (n + 1)), f k ≤ f (2 ^ n) :=
-    λ k hk, hf (pow_pos zero_lt_two _) (Ico.mem.mp hk).1,
+    λ k hk, hf (pow_pos zero_lt_two _) (mem_Ico.mp hk).1,
   convert sum_le_sum this,
   simp [pow_succ, two_mul]
 end
@@ -72,8 +72,8 @@ begin
     exacts [add_le_add_right n.one_le_two_pow _,
       add_le_add_right (nat.pow_le_pow_of_le_right zero_lt_two n.le_succ) _] },
   have : ∀ k ∈ Ico (2 ^ n + 1) (2 ^ (n + 1) + 1), f (2 ^ (n + 1)) ≤ f k :=
-    λ k hk, hf (n.one_le_two_pow.trans_lt $ (nat.lt_succ_of_le le_rfl).trans_le (Ico.mem.mp hk).1)
-      (nat.le_of_lt_succ $ (Ico.mem.mp hk).2),
+    λ k hk, hf (n.one_le_two_pow.trans_lt $ (nat.lt_succ_of_le le_rfl).trans_le (mem_Ico.mp hk).1)
+      (nat.le_of_lt_succ $ (mem_Ico.mp hk).2),
   convert sum_le_sum this,
   simp [pow_succ, two_mul]
 end

src/analysis/special_functions/exp_log.lean

@@ -796,9 +796,9 @@ begin
     eventually_at_top.1 ((tendsto_pow_const_div_const_pow_of_one_lt n
       (one_lt_exp_iff.2 zero_lt_one)).eventually (gt_mem_nhds this)),
   simp only [← exp_nat_mul, mul_one, div_lt_iff, exp_pos, ← div_eq_inv_mul] at hN,
-  refine ⟨N, trivial, λ x hx, _⟩, rw mem_Ioi at hx,
+  refine ⟨N, trivial, λ x hx, _⟩, rw set.mem_Ioi at hx,
   have hx₀ : 0 < x, from N.cast_nonneg.trans_lt hx,
-  rw [mem_Ici, le_div_iff (pow_pos hx₀ _), ← le_div_iff' hC₀],
+  rw [set.mem_Ici, le_div_iff (pow_pos hx₀ _), ← le_div_iff' hC₀],
   calc x ^ n ≤ ⌈x⌉₊ ^ n : pow_le_pow_of_le_left hx₀.le (le_nat_ceil _) _
   ... ≤ exp ⌈x⌉₊ / (exp 1 * C) : (hN _ (lt_nat_ceil.2 hx).le).le
   ... ≤ exp (x + 1) / (exp 1 * C) : div_le_div_of_le (mul_pos (exp_pos _) hC₀).le

src/data/fin/interval.lean

@@ -10,10 +10,6 @@ import data.nat.interval
 
 This file proves that `fin n` is a `locally_finite_order` and calculates the cardinality of its
 intervals as finsets and fintypes.
-
-## TODO
-
-@Yaël: Add `finset.Ico`. Coming very soon.
 -/
 
 open finset fin
@@ -26,13 +22,18 @@ namespace fin
 variables {n} (a b : fin n)
 
 lemma Icc_eq_finset_subtype : Icc a b = (Icc (a : ℕ) b).subtype (λ x, x < n) := rfl
+lemma Ico_eq_finset_subtype : Ico a b = (Ico (a : ℕ) b).subtype (λ x, x < n) := rfl
 lemma Ioc_eq_finset_subtype : Ioc a b = (Ioc (a : ℕ) b).subtype (λ x, x < n) := rfl
 lemma Ioo_eq_finset_subtype : Ioo a b = (Ioo (a : ℕ) b).subtype (λ x, x < n) := rfl
 
 @[simp] lemma map_subtype_embedding_Icc :
   (Icc a b).map (function.embedding.subtype _) = Icc (a : ℕ) b :=
 map_subtype_embedding_Icc _ _ _ (λ _ c x _ hx _, hx.trans_lt)
 
+@[simp] lemma map_subtype_embedding_Ico :
+  (Ico a b).map (function.embedding.subtype _) = Ico (a : ℕ) b :=
+map_subtype_embedding_Ico _ _ _ (λ _ c x _ hx _, hx.trans_lt)
+
 @[simp] lemma map_subtype_embedding_Ioc :
   (Ioc a b).map (function.embedding.subtype _) = Ioc (a : ℕ) b :=
 map_subtype_embedding_Ioc _ _ _ (λ _ c x _ hx _, hx.trans_lt)
@@ -44,6 +45,9 @@ map_subtype_embedding_Ioo _ _ _ (λ _ c x _ hx _, hx.trans_lt)
 @[simp] lemma card_Icc : (Icc a b).card = b + 1 - a :=
 by rw [←nat.card_Icc, ←map_subtype_embedding_Icc, card_map]
 
+@[simp] lemma card_Ico : (Ico a b).card = b - a :=
+by rw [←nat.card_Ico, ←map_subtype_embedding_Ico, card_map]
+
 @[simp] lemma card_Ioc : (Ioc a b).card = b - a :=
 by rw [←nat.card_Ioc, ←map_subtype_embedding_Ioc, card_map]
 
@@ -53,6 +57,9 @@ by rw [←nat.card_Ioo, ←map_subtype_embedding_Ioo, card_map]
 @[simp] lemma card_fintype_Icc : fintype.card (set.Icc a b) = b + 1 - a :=
 by rw [←card_Icc, fintype.card_of_finset]
 
+@[simp] lemma card_fintype_Ico : fintype.card (set.Ico a b) = b - a :=
+by rw [←card_Ico, fintype.card_of_finset]
+
 @[simp] lemma card_fintype_Ioc : fintype.card (set.Ioc a b) = b - a :=
 by rw [←card_Ioc, fintype.card_of_finset]
 

src/data/finset/default.lean

@@ -1,6 +1,6 @@
 import data.finset.basic
 import data.finset.fold
-import data.finset.intervals
+import data.finset.interval
 import data.finset.lattice
 import data.finset.nat_antidiagonal
 import data.finset.pi