[Merged by Bors] - feat(data/fin/interval): add lemmas

src/data/fin/basic.lean

@@ -260,6 +260,10 @@ by simp [lt_iff_coe_lt_coe]
 lemma eq_last_of_not_lt {i : fin (n+1)} (h : ¬ (i : ℕ) < n) : i = last n :=
 le_antisymm (le_last i) (not_lt.1 h)
 
+lemma top_eq_last (n : ℕ) : ⊤ = fin.last n := rfl
+
+lemma bot_eq_zero (n : ℕ) : ⊥ = (0 : fin (n + 1)) := rfl
+
 section
 
 variables {α : Type*} [preorder α]

src/data/fin/interval.lean

@@ -19,6 +19,7 @@ variables (n : ℕ)
 instance : locally_finite_order (fin n) := subtype.locally_finite_order _
 
 namespace fin
+
 section bounded
 variables {n} (a b : fin n)
 
@@ -152,4 +153,76 @@ by rw [fintype.card_of_finset, card_Iic]
 by rw [fintype.card_of_finset, card_Iio]
 
 end unbounded
+
+section filter
+
+variables {n} (a b : fin n)
+
+@[simp]
+lemma card_filter_lt : (finset.univ.filter (λ j, a < j)).card = n - a - 1 :=
+begin
+  cases n,
+  { simp },
+  { rw [filter_lt_eq_Ioi, card_Ioi, tsub_tsub],
+    exact (add_tsub_add_eq_tsub_right _ 1 _).symm }
+end
+
+@[simp]
+lemma card_filter_le : (univ.filter (λ j, a ≤ j)).card = n - a :=
+begin
+  cases n,
+  { simp },
+  { rw [filter_le_eq_Ici, card_Ici] }
+end
+
+@[simp]
+lemma card_filter_gt : (finset.univ.filter (λ j, j < a)).card = a :=
+begin
+  cases n,
+  { exact fin.elim0 a },
+  { rw [filter_gt_eq_Iio, card_Iio] }
+end
+
+@[simp]
+lemma card_filter_ge : (finset.univ.filter (λ j, j ≤ a)).card = a + 1 :=
+begin
+  cases n,
+  { exact fin.elim0 a },
+  { rw [filter_ge_eq_Iic, card_Iic] }
+end
+
+@[simp]
+lemma card_filter_lt_lt : (finset.univ.filter (λ j, a < j ∧ j < b)).card = b - a - 1 :=
+begin
+  cases n,
+  { exact fin.elim0 a },
+  { rw [filter_lt_lt_eq_Ioo, card_Ioo] }
+end
+
+@[simp]
+lemma card_filter_lt_le : (finset.univ.filter (λ j, a < j ∧ j ≤ b)).card = b - a :=
+begin
+  cases n,
+  { exact fin.elim0 a },
+  { rw [filter_lt_le_eq_Ioc, card_Ioc] }
+end
+
+@[simp]
+lemma card_filter_le_lt : (finset.univ.filter (λ j, a ≤ j ∧ j < b)).card = b - a :=
+begin
+  cases n,
+  { exact fin.elim0 a },
+  { rw [filter_le_lt_eq_Ico, card_Ico] }
+end
+
+@[simp]
+lemma card_filter_le_le : (finset.univ.filter (λ j, a ≤ j ∧ j ≤ b)).card = b + 1 - a :=
+begin
+  cases n,
+  { exact fin.elim0 a },
+  { rw [filter_le_le_eq_Icc, card_Icc] }
+end
+
+end filter
+
 end fin

src/data/finset/locally_finite.lean

@@ -119,6 +119,36 @@ lemma _root_.bdd_below.finite_of_bdd_above {s : set α} (h₀ : bdd_below s) (h
   s.finite :=
 let ⟨a, ha⟩ := h₀, ⟨b, hb⟩ := h₁ in by { classical, exact ⟨set.fintype_of_mem_bounds ha hb⟩ }
 
+section filter
+
+variables (a b) [fintype α]
+
+lemma filter_lt_lt_eq_Ioo [decidable_pred (λ (j : α), a < j ∧ j < b)] :
+  finset.univ.filter (λ j, a < j ∧ j < b) = Ioo a b := by { ext, simp }
+
+lemma filter_lt_le_eq_Ioc [decidable_pred (λ (j : α), a < j ∧ j ≤ b)] :
+  finset.univ.filter (λ j, a < j ∧ j ≤ b) = Ioc a b := by { ext, simp }
+
+lemma filter_le_lt_eq_Ico [decidable_pred (λ (j : α), a ≤ j ∧ j < b)] :
+  finset.univ.filter (λ j, a ≤ j ∧ j < b) = Ico a b := by { ext, simp }
+
+lemma filter_le_le_eq_Icc [decidable_pred (λ (j : α), a ≤ j ∧ j ≤ b)] :
+  finset.univ.filter (λ j, a ≤ j ∧ j ≤ b) = Icc a b := by { ext, simp }
+
+lemma filter_lt_eq_Ioi [order_top α] [decidable_pred ((<) a)] :
+  finset.univ.filter (λ j, a < j) = Ioi a := by { ext, simp }
+
+lemma filter_le_eq_Ici [order_top α] [decidable_pred ((≤) a)] :
+  finset.univ.filter (λ j, a ≤ j) = Ici a := by { ext, simp }
+
+lemma filter_gt_eq_Iio [order_bot α] [decidable_pred (< a)] :
+  finset.univ.filter (λ j, j < a) = Iio a := by { ext, simp }
+
+lemma filter_ge_eq_Iic [order_bot α] [decidable_pred (≤ a)] :
+  finset.univ.filter (λ j, j ≤ a) = Iic a := by { ext, simp }
+
+end filter
+
 end preorder
 
 section partial_order