Documentation

Mathlib.Data.Finset.LocallyFinite

Intervals as finsets #

This file provides basic results about all the Finset.Ixx, which are defined in Order.LocallyFinite.

TODO #

This file was originally only about finset.Ico a b where a b : ℕ. No care has yet been taken to generalize these lemmas properly and many lemmas about Icc, Ioc, Ioo are missing. In general, what's to do is taking the lemmas in Data.X.Intervals and abstract away the concrete structure.

Complete the API. See https://github.com/leanprover-community/mathlib/pull/14448#discussion_r906109235 for some ideas.

@[simp]
theorem Finset.nonempty_Icc {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} :
@[simp]
theorem Finset.nonempty_Ico {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} :
@[simp]
theorem Finset.nonempty_Ioc {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} :
@[simp]
theorem Finset.nonempty_Ioo {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} [inst : DenselyOrdered α] :
@[simp]
theorem Finset.Icc_eq_empty_iff {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} :
@[simp]
theorem Finset.Ico_eq_empty_iff {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} :
@[simp]
theorem Finset.Ioc_eq_empty_iff {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} :
@[simp]
theorem Finset.Ioo_eq_empty_iff {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} [inst : DenselyOrdered α] :
theorem Finset.Icc_eq_empty {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} :
¬a bFinset.Icc a b =

Alias of the reverse direction of Finset.Icc_eq_empty_iff.

theorem Finset.Ico_eq_empty {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} :
¬a < bFinset.Ico a b =

Alias of the reverse direction of Finset.Ico_eq_empty_iff.

theorem Finset.Ioc_eq_empty {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} :
¬a < bFinset.Ioc a b =

Alias of the reverse direction of Finset.Ioc_eq_empty_iff.

@[simp]
theorem Finset.Ioo_eq_empty {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} (h : ¬a < b) :
@[simp]
theorem Finset.Icc_eq_empty_of_lt {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} (h : b < a) :
@[simp]
theorem Finset.Ico_eq_empty_of_le {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} (h : b a) :
@[simp]
theorem Finset.Ioc_eq_empty_of_le {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} (h : b a) :
@[simp]
theorem Finset.Ioo_eq_empty_of_le {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} (h : b a) :
theorem Finset.left_mem_Icc {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} :
a Finset.Icc a b a b
theorem Finset.left_mem_Ico {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} :
a Finset.Ico a b a < b
theorem Finset.right_mem_Icc {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} :
b Finset.Icc a b a b
theorem Finset.right_mem_Ioc {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} :
b Finset.Ioc a b a < b
theorem Finset.left_not_mem_Ioc {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} :
theorem Finset.left_not_mem_Ioo {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} :
theorem Finset.right_not_mem_Ico {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} :
theorem Finset.right_not_mem_Ioo {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} :
theorem Finset.Icc_subset_Icc {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (ha : a₂ a₁) (hb : b₁ b₂) :
Finset.Icc a₁ b₁ Finset.Icc a₂ b₂
theorem Finset.Ico_subset_Ico {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (ha : a₂ a₁) (hb : b₁ b₂) :
Finset.Ico a₁ b₁ Finset.Ico a₂ b₂
theorem Finset.Ioc_subset_Ioc {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (ha : a₂ a₁) (hb : b₁ b₂) :
Finset.Ioc a₁ b₁ Finset.Ioc a₂ b₂
theorem Finset.Ioo_subset_Ioo {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (ha : a₂ a₁) (hb : b₁ b₂) :
Finset.Ioo a₁ b₁ Finset.Ioo a₂ b₂
theorem Finset.Icc_subset_Icc_left {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b : α} (h : a₁ a₂) :
Finset.Icc a₂ b Finset.Icc a₁ b
theorem Finset.Ico_subset_Ico_left {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b : α} (h : a₁ a₂) :
Finset.Ico a₂ b Finset.Ico a₁ b
theorem Finset.Ioc_subset_Ioc_left {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b : α} (h : a₁ a₂) :
Finset.Ioc a₂ b Finset.Ioc a₁ b
theorem Finset.Ioo_subset_Ioo_left {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b : α} (h : a₁ a₂) :
Finset.Ioo a₂ b Finset.Ioo a₁ b
theorem Finset.Icc_subset_Icc_right {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b₁ : α} {b₂ : α} (h : b₁ b₂) :
Finset.Icc a b₁ Finset.Icc a b₂
theorem Finset.Ico_subset_Ico_right {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b₁ : α} {b₂ : α} (h : b₁ b₂) :
Finset.Ico a b₁ Finset.Ico a b₂
theorem Finset.Ioc_subset_Ioc_right {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b₁ : α} {b₂ : α} (h : b₁ b₂) :
Finset.Ioc a b₁ Finset.Ioc a b₂
theorem Finset.Ioo_subset_Ioo_right {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b₁ : α} {b₂ : α} (h : b₁ b₂) :
Finset.Ioo a b₁ Finset.Ioo a b₂
theorem Finset.Ico_subset_Ioo_left {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b : α} (h : a₁ < a₂) :
Finset.Ico a₂ b Finset.Ioo a₁ b
theorem Finset.Ioc_subset_Ioo_right {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b₁ : α} {b₂ : α} (h : b₁ < b₂) :
Finset.Ioc a b₁ Finset.Ioo a b₂
theorem Finset.Icc_subset_Ico_right {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b₁ : α} {b₂ : α} (h : b₁ < b₂) :
Finset.Icc a b₁ Finset.Ico a b₂
theorem Finset.Ioo_subset_Ico_self {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} :
theorem Finset.Ioo_subset_Ioc_self {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} :
theorem Finset.Ico_subset_Icc_self {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} :
theorem Finset.Ioc_subset_Icc_self {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} :
theorem Finset.Ioo_subset_Icc_self {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} :
theorem Finset.Icc_subset_Icc_iff {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (h₁ : a₁ b₁) :
Finset.Icc a₁ b₁ Finset.Icc a₂ b₂ a₂ a₁ b₁ b₂
theorem Finset.Icc_subset_Ioo_iff {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (h₁ : a₁ b₁) :
Finset.Icc a₁ b₁ Finset.Ioo a₂ b₂ a₂ < a₁ b₁ < b₂
theorem Finset.Icc_subset_Ico_iff {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (h₁ : a₁ b₁) :
Finset.Icc a₁ b₁ Finset.Ico a₂ b₂ a₂ a₁ b₁ < b₂
theorem Finset.Icc_subset_Ioc_iff {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (h₁ : a₁ b₁) :
Finset.Icc a₁ b₁ Finset.Ioc a₂ b₂ a₂ < a₁ b₁ b₂
theorem Finset.Icc_ssubset_Icc_left {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (hI : a₂ b₂) (ha : a₂ < a₁) (hb : b₁ b₂) :
Finset.Icc a₁ b₁ Finset.Icc a₂ b₂
theorem Finset.Icc_ssubset_Icc_right {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (hI : a₂ b₂) (ha : a₂ a₁) (hb : b₁ < b₂) :
Finset.Icc a₁ b₁ Finset.Icc a₂ b₂
theorem Finset.Ico_self {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] (a : α) :
theorem Finset.Ioc_self {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] (a : α) :
theorem Finset.Ioo_self {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] (a : α) :
def Set.fintypeOfMemBounds {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {s : Set α} [inst : DecidablePred fun x => x s] (ha : a lowerBounds s) (hb : b upperBounds s) :
Fintype s

A set with upper and lower bounds in a locally finite order is a fintype

Equations
theorem BddBelow.finite_of_bddAbove {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {s : Set α} (h₀ : BddBelow s) (h₁ : BddAbove s) :
theorem Finset.Ico_filter_lt_of_le_left {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} [inst : DecidablePred fun x => x < c] (hca : c a) :
Finset.filter (fun x => x < c) (Finset.Ico a b) =
theorem Finset.Ico_filter_lt_of_right_le {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} [inst : DecidablePred fun x => x < c] (hbc : b c) :
Finset.filter (fun x => x < c) (Finset.Ico a b) = Finset.Ico a b
theorem Finset.Ico_filter_lt_of_le_right {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} [inst : DecidablePred fun x => x < c] (hcb : c b) :
Finset.filter (fun x => x < c) (Finset.Ico a b) = Finset.Ico a c
theorem Finset.Ico_filter_le_of_le_left {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} [inst : DecidablePred ((fun x x_1 => x x_1) c)] (hca : c a) :
Finset.filter ((fun x x_1 => x x_1) c) (Finset.Ico a b) = Finset.Ico a b
theorem Finset.Ico_filter_le_of_right_le {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} [inst : DecidablePred ((fun x x_1 => x x_1) b)] :
Finset.filter ((fun x x_1 => x x_1) b) (Finset.Ico a b) =
theorem Finset.Ico_filter_le_of_left_le {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} [inst : DecidablePred ((fun x x_1 => x x_1) c)] (hac : a c) :
Finset.filter ((fun x x_1 => x x_1) c) (Finset.Ico a b) = Finset.Ico c b
theorem Finset.Icc_filter_lt_of_lt_right {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} [inst : DecidablePred fun x => x < c] (h : b < c) :
Finset.filter (fun x => x < c) (Finset.Icc a b) = Finset.Icc a b
theorem Finset.Ioc_filter_lt_of_lt_right {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} [inst : DecidablePred fun x => x < c] (h : b < c) :
Finset.filter (fun x => x < c) (Finset.Ioc a b) = Finset.Ioc a b
theorem Finset.Iic_filter_lt_of_lt_right {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderBot α] {a : α} {c : α} [inst : DecidablePred fun x => x < c] (h : a < c) :
Finset.filter (fun x => x < c) (Finset.Iic a) = Finset.Iic a
theorem Finset.filter_lt_lt_eq_Ioo {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) [inst : Fintype α] [inst : DecidablePred fun j => a < j j < b] :
Finset.filter (fun j => a < j j < b) Finset.univ = Finset.Ioo a b
theorem Finset.filter_lt_le_eq_Ioc {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) [inst : Fintype α] [inst : DecidablePred fun j => a < j j b] :
Finset.filter (fun j => a < j j b) Finset.univ = Finset.Ioc a b
theorem Finset.filter_le_lt_eq_Ico {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) [inst : Fintype α] [inst : DecidablePred fun j => a j j < b] :
Finset.filter (fun j => a j j < b) Finset.univ = Finset.Ico a b
theorem Finset.filter_le_le_eq_Icc {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) [inst : Fintype α] [inst : DecidablePred fun j => a j j b] :
Finset.filter (fun j => a j j b) Finset.univ = Finset.Icc a b
theorem Finset.Icc_subset_Ici_self {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} [inst : LocallyFiniteOrderTop α] :
theorem Finset.Ico_subset_Ici_self {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} [inst : LocallyFiniteOrderTop α] :
theorem Finset.Ioc_subset_Ioi_self {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} [inst : LocallyFiniteOrderTop α] :
theorem Finset.Ioo_subset_Ioi_self {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} [inst : LocallyFiniteOrderTop α] :
theorem Finset.Ioc_subset_Ici_self {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} [inst : LocallyFiniteOrderTop α] :
theorem Finset.Ioo_subset_Ici_self {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} [inst : LocallyFiniteOrderTop α] :
theorem Finset.Icc_subset_Iic_self {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} [inst : LocallyFiniteOrderBot α] :
theorem Finset.Ioc_subset_Iic_self {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} [inst : LocallyFiniteOrderBot α] :
theorem Finset.Ico_subset_Iio_self {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} [inst : LocallyFiniteOrderBot α] :
theorem Finset.Ioo_subset_Iio_self {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} [inst : LocallyFiniteOrderBot α] :
theorem Finset.Ico_subset_Iic_self {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} [inst : LocallyFiniteOrderBot α] :
theorem Finset.Ioo_subset_Iic_self {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} [inst : LocallyFiniteOrderBot α] :
theorem Finset.Ioi_subset_Ici_self {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderTop α] {a : α} :
theorem BddBelow.finite {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderTop α] {s : Set α} (hs : BddBelow s) :
theorem Finset.filter_lt_eq_Ioi {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderTop α] {a : α} [inst : Fintype α] [inst : DecidablePred ((fun x x_1 => x < x_1) a)] :
Finset.filter ((fun x x_1 => x < x_1) a) Finset.univ = Finset.Ioi a
theorem Finset.filter_le_eq_Ici {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderTop α] {a : α} [inst : Fintype α] [inst : DecidablePred ((fun x x_1 => x x_1) a)] :
Finset.filter ((fun x x_1 => x x_1) a) Finset.univ = Finset.Ici a
theorem Finset.Iio_subset_Iic_self {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderBot α] {a : α} :
theorem BddAbove.finite {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderBot α] {s : Set α} (hs : BddAbove s) :
theorem Finset.filter_gt_eq_Iio {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderBot α] {a : α} [inst : Fintype α] [inst : DecidablePred fun x => x < a] :
Finset.filter (fun x => x < a) Finset.univ = Finset.Iio a
theorem Finset.filter_ge_eq_Iic {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderBot α] {a : α} [inst : Fintype α] [inst : DecidablePred fun x => x a] :
Finset.filter (fun x => x a) Finset.univ = Finset.Iic a
theorem Finset.disjoint_Ioi_Iio {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderTop α] [inst : LocallyFiniteOrderBot α] (a : α) :
@[simp]
theorem Finset.Icc_self {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] (a : α) :
Finset.Icc a a = {a}
@[simp]
theorem Finset.Icc_eq_singleton_iff {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} :
Finset.Icc a b = {c} a = c b = c
theorem Finset.Ico_disjoint_Ico_consecutive {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) (c : α) :
@[simp]
theorem Finset.Icc_erase_left {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] [inst : DecidableEq α] (a : α) (b : α) :
@[simp]
theorem Finset.Icc_erase_right {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] [inst : DecidableEq α] (a : α) (b : α) :
@[simp]
theorem Finset.Ico_erase_left {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] [inst : DecidableEq α] (a : α) (b : α) :
@[simp]
theorem Finset.Ioc_erase_right {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] [inst : DecidableEq α] (a : α) (b : α) :
@[simp]
theorem Finset.Icc_diff_both {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] [inst : DecidableEq α] (a : α) (b : α) :
Finset.Icc a b \ {a, b} = Finset.Ioo a b
@[simp]
theorem Finset.Ico_insert_right {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} [inst : DecidableEq α] (h : a b) :
@[simp]
theorem Finset.Ioc_insert_left {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} [inst : DecidableEq α] (h : a b) :
@[simp]
theorem Finset.Ioo_insert_left {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} [inst : DecidableEq α] (h : a < b) :
@[simp]
theorem Finset.Ioo_insert_right {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} [inst : DecidableEq α] (h : a < b) :
@[simp]
theorem Finset.Icc_diff_Ico_self {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} [inst : DecidableEq α] (h : a b) :
Finset.Icc a b \ Finset.Ico a b = {b}
@[simp]
theorem Finset.Icc_diff_Ioc_self {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} [inst : DecidableEq α] (h : a b) :
Finset.Icc a b \ Finset.Ioc a b = {a}
@[simp]
theorem Finset.Icc_diff_Ioo_self {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} [inst : DecidableEq α] (h : a b) :
Finset.Icc a b \ Finset.Ioo a b = {a, b}
@[simp]
theorem Finset.Ico_diff_Ioo_self {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} [inst : DecidableEq α] (h : a < b) :
Finset.Ico a b \ Finset.Ioo a b = {a}
@[simp]
theorem Finset.Ioc_diff_Ioo_self {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} [inst : DecidableEq α] (h : a < b) :
Finset.Ioc a b \ Finset.Ioo a b = {b}
@[simp]
theorem Finset.Ico_inter_Ico_consecutive {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] [inst : DecidableEq α] (a : α) (b : α) (c : α) :
theorem Finset.Icc_eq_cons_Ico {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} (h : a b) :

Finset.cons version of Finset.Ico_insert_right.

theorem Finset.Icc_eq_cons_Ioc {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} (h : a b) :

Finset.cons version of Finset.Ioc_insert_left.

theorem Finset.Ioc_eq_cons_Ioo {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} (h : a < b) :

Finset.cons version of Finset.Ioo_insert_right.

theorem Finset.Ico_eq_cons_Ioo {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} (h : a < b) :

Finset.cons version of Finset.Ioo_insert_left.

theorem Finset.Ico_filter_le_left {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} [inst : DecidablePred fun x => x a] (hab : a < b) :
Finset.filter (fun x => x a) (Finset.Ico a b) = {a}
theorem Finset.card_Ico_eq_card_Icc_sub_one {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) :
theorem Finset.card_Ioc_eq_card_Icc_sub_one {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) :
theorem Finset.card_Ioo_eq_card_Ico_sub_one {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) :
theorem Finset.card_Ioo_eq_card_Ioc_sub_one {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) :
theorem Finset.card_Ioo_eq_card_Icc_sub_two {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) :
@[simp]
theorem Finset.Ici_erase {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrderTop α] [inst : DecidableEq α] (a : α) :
@[simp]
theorem Finset.Ioi_insert {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrderTop α] [inst : DecidableEq α] (a : α) :
theorem Finset.not_mem_Ioi_self {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrderTop α] {b : α} :
@[simp]
theorem Finset.Iic_erase {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrderBot α] [inst : DecidableEq α] (b : α) :
@[simp]
theorem Finset.Iio_insert {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrderBot α] [inst : DecidableEq α] (b : α) :
theorem Finset.not_mem_Iio_self {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrderBot α] {b : α} :
theorem Finset.Ico_subset_Ico_iff {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrder α] {a₁ : α} {b₁ : α} {a₂ : α} {b₂ : α} (h : a₁ < b₁) :
Finset.Ico a₁ b₁ Finset.Ico a₂ b₂ a₂ a₁ b₁ b₂
theorem Finset.Ico_union_Ico_eq_Ico {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} (hab : a b) (hbc : b c) :
@[simp]
theorem Finset.Ioc_union_Ioc_eq_Ioc {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} (h₁ : a b) (h₂ : b c) :
theorem Finset.Ico_subset_Ico_union_Ico {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} :
theorem Finset.Ico_union_Ico' {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} {d : α} (hcb : c b) (had : a d) :
theorem Finset.Ico_union_Ico {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} {d : α} (h₁ : min a b max c d) (h₂ : min c d max a b) :
theorem Finset.Ico_inter_Ico {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} {d : α} :
@[simp]
theorem Finset.Ico_filter_lt {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) (c : α) :
Finset.filter (fun x => x < c) (Finset.Ico a b) = Finset.Ico a (min b c)
@[simp]
theorem Finset.Ico_filter_le {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) (c : α) :
Finset.filter (fun x => c x) (Finset.Ico a b) = Finset.Ico (max a c) b
@[simp]
theorem Finset.Ioo_filter_lt {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) (c : α) :
Finset.filter (fun x => x < c) (Finset.Ioo a b) = Finset.Ioo a (min b c)
@[simp]
theorem Finset.Iio_filter_lt {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrderBot α] (a : α) (b : α) :
Finset.filter (fun x => x < b) (Finset.Iio a) = Finset.Iio (min a b)
@[simp]
theorem Finset.Ico_diff_Ico_left {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) (c : α) :
@[simp]
theorem Finset.Ico_diff_Ico_right {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) (c : α) :
theorem Finset.Ioi_disjUnion_Iio {α : Type u_1} [inst : LinearOrder α] [inst : Fintype α] [inst : LocallyFiniteOrderTop α] [inst : LocallyFiniteOrderBot α] (a : α) :
theorem Finset.uIcc_toDual {α : Type u_1} [inst : Lattice α] [inst : LocallyFiniteOrder α] (a : α) (b : α) :
Finset.uIcc (OrderDual.toDual a) (OrderDual.toDual b) = Finset.map (Equiv.toEmbedding OrderDual.toDual) (Finset.uIcc a b)
@[simp]
theorem Finset.uIcc_of_le {α : Type u_1} [inst : Lattice α] [inst : LocallyFiniteOrder α] {a : α} {b : α} (h : a b) :
@[simp]
theorem Finset.uIcc_of_ge {α : Type u_1} [inst : Lattice α] [inst : LocallyFiniteOrder α] {a : α} {b : α} (h : b a) :
theorem Finset.uIcc_comm {α : Type u_1} [inst : Lattice α] [inst : LocallyFiniteOrder α] (a : α) (b : α) :
theorem Finset.uIcc_self {α : Type u_1} [inst : Lattice α] [inst : LocallyFiniteOrder α] {a : α} :
Finset.uIcc a a = {a}
@[simp]
theorem Finset.nonempty_uIcc {α : Type u_1} [inst : Lattice α] [inst : LocallyFiniteOrder α] {a : α} {b : α} :
theorem Finset.Icc_subset_uIcc {α : Type u_1} [inst : Lattice α] [inst : LocallyFiniteOrder α] {a : α} {b : α} :
theorem Finset.Icc_subset_uIcc' {α : Type u_1} [inst : Lattice α] [inst : LocallyFiniteOrder α] {a : α} {b : α} :
theorem Finset.left_mem_uIcc {α : Type u_1} [inst : Lattice α] [inst : LocallyFiniteOrder α] {a : α} {b : α} :
theorem Finset.right_mem_uIcc {α : Type u_1} [inst : Lattice α] [inst : LocallyFiniteOrder α] {a : α} {b : α} :
theorem Finset.mem_uIcc_of_le {α : Type u_1} [inst : Lattice α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {x : α} (ha : a x) (hb : x b) :
theorem Finset.mem_uIcc_of_ge {α : Type u_1} [inst : Lattice α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {x : α} (hb : b x) (ha : x a) :
theorem Finset.uIcc_subset_uIcc {α : Type u_1} [inst : Lattice α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (h₁ : a₁ Finset.uIcc a₂ b₂) (h₂ : b₁ Finset.uIcc a₂ b₂) :
Finset.uIcc a₁ b₁ Finset.uIcc a₂ b₂
theorem Finset.uIcc_subset_Icc {α : Type u_1} [inst : Lattice α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (ha : a₁ Finset.Icc a₂ b₂) (hb : b₁ Finset.Icc a₂ b₂) :
Finset.uIcc a₁ b₁ Finset.Icc a₂ b₂
theorem Finset.uIcc_subset_uIcc_iff_mem {α : Type u_1} [inst : Lattice α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} :
Finset.uIcc a₁ b₁ Finset.uIcc a₂ b₂ a₁ Finset.uIcc a₂ b₂ b₁ Finset.uIcc a₂ b₂
theorem Finset.uIcc_subset_uIcc_iff_le' {α : Type u_1} [inst : Lattice α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} :
Finset.uIcc a₁ b₁ Finset.uIcc a₂ b₂ a₂ b₂ a₁ b₁ a₁ b₁ a₂ b₂
theorem Finset.uIcc_subset_uIcc_right {α : Type u_1} [inst : Lattice α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {x : α} (h : x Finset.uIcc a b) :
theorem Finset.uIcc_subset_uIcc_left {α : Type u_1} [inst : Lattice α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {x : α} (h : x Finset.uIcc a b) :
theorem Finset.eq_of_mem_uIcc_of_mem_uIcc {α : Type u_1} [inst : DistribLattice α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} :
a Finset.uIcc b cb Finset.uIcc a ca = b
theorem Finset.eq_of_mem_uIcc_of_mem_uIcc' {α : Type u_1} [inst : DistribLattice α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} :
b Finset.uIcc a cc Finset.uIcc a bb = c
theorem Finset.uIcc_injective_right {α : Type u_1} [inst : DistribLattice α] [inst : LocallyFiniteOrder α] (a : α) :
theorem Finset.Icc_min_max {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} :
Finset.Icc (min a b) (max a b) = Finset.uIcc a b
theorem Finset.uIcc_of_not_le {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} (h : ¬a b) :
theorem Finset.uIcc_of_not_ge {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} (h : ¬b a) :
theorem Finset.uIcc_eq_union {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} :
theorem Finset.mem_uIcc' {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} :
a Finset.uIcc b c b a a c c a a b
theorem Finset.not_mem_uIcc_of_lt {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} :
c < ac < b¬c Finset.uIcc a b
theorem Finset.not_mem_uIcc_of_gt {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} :
a < cb < c¬c Finset.uIcc a b
theorem Finset.uIcc_subset_uIcc_iff_le {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} :
Finset.uIcc a₁ b₁ Finset.uIcc a₂ b₂ min a₂ b₂ min a₁ b₁ max a₁ b₁ max a₂ b₂
theorem Finset.uIcc_subset_uIcc_union_uIcc {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} :

A sort of triangle inequality.

@[simp]
theorem Finset.map_add_left_Icc {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] (a : α) (b : α) (c : α) :
@[simp]
theorem Finset.map_add_right_Icc {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] (a : α) (b : α) (c : α) :
@[simp]
theorem Finset.map_add_left_Ico {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] (a : α) (b : α) (c : α) :
@[simp]
theorem Finset.map_add_right_Ico {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] (a : α) (b : α) (c : α) :
@[simp]
theorem Finset.map_add_left_Ioc {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] (a : α) (b : α) (c : α) :
@[simp]
theorem Finset.map_add_right_Ioc {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] (a : α) (b : α) (c : α) :
@[simp]
theorem Finset.map_add_left_Ioo {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] (a : α) (b : α) (c : α) :
@[simp]
theorem Finset.map_add_right_Ioo {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] (a : α) (b : α) (c : α) :
@[simp]
theorem Finset.image_add_left_Icc {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] [inst : DecidableEq α] (a : α) (b : α) (c : α) :
Finset.image ((fun x x_1 => x + x_1) c) (Finset.Icc a b) = Finset.Icc (c + a) (c + b)
@[simp]
theorem Finset.image_add_left_Ico {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] [inst : DecidableEq α] (a : α) (b : α) (c : α) :
Finset.image ((fun x x_1 => x + x_1) c) (Finset.Ico a b) = Finset.Ico (c + a) (c + b)
@[simp]
theorem Finset.image_add_left_Ioc {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] [inst : DecidableEq α] (a : α) (b : α) (c : α) :
Finset.image ((fun x x_1 => x + x_1) c) (Finset.Ioc a b) = Finset.Ioc (c + a) (c + b)
@[simp]
theorem Finset.image_add_left_Ioo {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] [inst : DecidableEq α] (a : α) (b : α) (c : α) :
Finset.image ((fun x x_1 => x + x_1) c) (Finset.Ioo a b) = Finset.Ioo (c + a) (c + b)
@[simp]
theorem Finset.image_add_right_Icc {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] [inst : DecidableEq α] (a : α) (b : α) (c : α) :
Finset.image (fun x => x + c) (Finset.Icc a b) = Finset.Icc (a + c) (b + c)
theorem Finset.image_add_right_Ico {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] [inst : DecidableEq α] (a : α) (b : α) (c : α) :
Finset.image (fun x => x + c) (Finset.Ico a b) = Finset.Ico (a + c) (b + c)
theorem Finset.image_add_right_Ioc {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] [inst : DecidableEq α] (a : α) (b : α) (c : α) :
Finset.image (fun x => x + c) (Finset.Ioc a b) = Finset.Ioc (a + c) (b + c)
theorem Finset.image_add_right_Ioo {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] [inst : DecidableEq α] (a : α) (b : α) (c : α) :
Finset.image (fun x => x + c) (Finset.Ioo a b) = Finset.Ioo (a + c) (b + c)
theorem Finset.sum_sum_Ioi_add_eq_sum_sum_off_diag {ι : Type u_1} {α : Type u_2} [inst : Fintype ι] [inst : LinearOrder ι] [inst : LocallyFiniteOrderTop ι] [inst : LocallyFiniteOrderBot ι] [inst : AddCommMonoid α] (f : ιια) :
(Finset.sum Finset.univ fun i => Finset.sum (Finset.Ioi i) fun j => f j i + f i j) = Finset.sum Finset.univ fun i => Finset.sum ({i}) fun j => f j i
theorem Finset.prod_prod_Ioi_mul_eq_prod_prod_off_diag {ι : Type u_1} {α : Type u_2} [inst : Fintype ι] [inst : LinearOrder ι] [inst : LocallyFiniteOrderTop ι] [inst : LocallyFiniteOrderBot ι] [inst : CommMonoid α] (f : ιια) :
(Finset.prod Finset.univ fun i => Finset.prod (Finset.Ioi i) fun j => f j i * f i j) = Finset.prod Finset.univ fun i => Finset.prod ({i}) fun j => f j i