LeanPool.ABCExceptions.ForMathlib.Misc

theorem Nat.Iic_eq_Icc (n : ℕ) : Finset.Iic n = Finset.Icc 0 n

theorem Finset.Ico_union_Icc_eq_Icc {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] {a b c : α} (h₁ : a ≤ b) (h₂ : b ≤ c) : Ico a b ∪ Icc b c = Icc a c

theorem Finset.Ico_union_Icc_eq_Icc' {α : Type u_1} [LinearOrder α] [Add α] [One α] [SuccAddOrder α] [LocallyFiniteOrder α] {a b c : α} (h₁ : a ≤ b) (h₂ : b ≤ c + 1) : Ico a b ∪ Icc b c = Icc a c

theorem Nat.Icc_union_Icc_eq_Icc {a b c : ℕ} (h₁ : a ≤ b) (h₂ : b ≤ c) : Finset.Icc a b ∪ Finset.Icc (b + 1) c = Finset.Icc a c

theorem Finset.prod_Icc_succ_bot {M : Type u_1} [CommMonoid M] {a b : ℕ} (hab : a ≤ b) (f : ℕ → M) : ∏ k ∈ Icc a b, f k = f a * ∏ k ∈ Icc (a + 1) b, f k

theorem Finset.sum_Icc_succ_bot {M : Type u_1} [AddCommMonoid M] {a b : ℕ} (hab : a ≤ b) (f : ℕ → M) : ∑ k ∈ Icc a b, f k = f a + ∑ k ∈ Icc (a + 1) b, f k

theorem Finset.finite_subsets (s : Finset ℕ) : {a : Finset ℕ | a ⊆ s}.Finite

theorem prod_Icc_eq_prod_range_mul_prod_Icc {d : ℕ} {α : Type u_1} [CommMonoid α] {f : ℕ → α} {t : ℕ} (ht : t ≤ d + 1) : ∏ i ≤ d, f i = (∏ i ∈ Finset.range t, f i) * ∏ i ∈ Finset.Icc t d, f i

theorem sum_Icc_eq_sum_range_add_sum_Icc {d : ℕ} {α : Type u_1} [AddCommMonoid α] {f : ℕ → α} {t : ℕ} (ht : t ≤ d + 1) : ∑ i ≤ d, f i = ∑ i ∈ Finset.range t, f i + ∑ i ∈ Finset.Icc t d, f i

theorem Iic_sdiff_Icc_eq_inter {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [LocallyFiniteOrderBot α] {x y : α} : Finset.Iic x \ Finset.Icc y x = Finset.Iic x ∩ Finset.Iio y

theorem Iic_sdiff_Icc_of_le {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] [LocallyFiniteOrderBot α] {x y : α} (h : y ≤ x) : Finset.Iic x \ Finset.Icc y x = Finset.Iio y