theorem
Finset.Ico_union_Icc_eq_Icc
{α : Type u_1}
[LinearOrder α]
[LocallyFiniteOrder α]
{a b c : α}
(h₁ : a ≤ b)
(h₂ : b ≤ 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)
:
theorem
prod_Icc_eq_prod_range_mul_prod_Icc
{d : ℕ}
{α : Type u_1}
[CommMonoid α]
{f : ℕ → α}
{t : ℕ}
(ht : t ≤ d + 1)
:
theorem
sum_Icc_eq_sum_range_add_sum_Icc
{d : ℕ}
{α : Type u_1}
[AddCommMonoid α]
{f : ℕ → α}
{t : ℕ}
(ht : t ≤ d + 1)
:
@[simp]
theorem
Iic_sdiff_Icc_eq_inter
{α : Type u_1}
[LinearOrder α]
[LocallyFiniteOrder α]
[LocallyFiniteOrderBot α]
{x y : α}
:
theorem
Iic_sdiff_Icc_of_le
{α : Type u_1}
[LinearOrder α]
[LocallyFiniteOrder α]
[LocallyFiniteOrderBot α]
{x y : α}
(h : y ≤ x)
: