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

src/data/fin/interval.lean

@@ -19,6 +19,11 @@ variables (n : ℕ)
 instance : locally_finite_order (fin n) := subtype.locally_finite_order _
 
 namespace fin
+
+lemma last_eq_top (n : ℕ) : fin.last n = ⊤ := rfl
+
+lemma zero_eq_bot (n : ℕ) : (0 : fin (n + 1)) = ⊥ := rfl
+
 section bounded
 variables {n} (a b : fin n)
 
@@ -152,4 +157,80 @@ by rw [fintype.card_of_finset, card_Iic]
 by rw [fintype.card_of_finset, card_Iio]
 
 end unbounded
+
+section filter
+
+variable {n}
+
+@[simp]
+lemma card_filter_lt (a : fin n) : (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 (a : fin n) : (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 (a : fin n) : (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 (a : fin n) : (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 (a b : fin n) :
+  (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 (a b : fin n) :
+  (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 (a b : fin n) :
+  (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 (a b : fin n) :
+  (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 (λ (j : α), j < a)] :
+  finset.univ.filter (λ j, j < a) = Iio a := by { ext, simp }
+
+lemma filter_ge_eq_Iic [order_bot α] [decidable_pred (λ (j : α), j ≤ a)] :
+  finset.univ.filter (λ j, j ≤ a) = Iic a := by { ext, simp }
+
+end filter
+
 end preorder
 
 section partial_order