# mathlibdocumentation

data.finset.locally_finite

# Intervals as finsets #

This file provides basic results about all the finset.Ixx, which are defined in order.locally_finite.

## 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_2} [preorder α] {a b : α} :
b).nonempty a b
@[simp]
theorem finset.nonempty_Ico {α : Type u_2} [preorder α] {a b : α} :
b).nonempty a < b
@[simp]
theorem finset.nonempty_Ioc {α : Type u_2} [preorder α] {a b : α} :
b).nonempty a < b
@[simp]
theorem finset.nonempty_Ioo {α : Type u_2} [preorder α] {a b : α}  :
b).nonempty a < b
@[simp]
theorem finset.Icc_eq_empty_iff {α : Type u_2} [preorder α] {a b : α} :
b = ¬a b
@[simp]
theorem finset.Ico_eq_empty_iff {α : Type u_2} [preorder α] {a b : α} :
b = ¬a < b
@[simp]
theorem finset.Ioc_eq_empty_iff {α : Type u_2} [preorder α] {a b : α} :
b = ¬a < b
@[simp]
theorem finset.Ioo_eq_empty_iff {α : Type u_2} [preorder α] {a b : α}  :
b = ¬a < b
theorem finset.Icc_eq_empty {α : Type u_2} [preorder α] {a b : α} :
¬a b b =

Alias of the reverse direction of finset.Icc_eq_empty_iff.

theorem finset.Ico_eq_empty {α : Type u_2} [preorder α] {a b : α} :
¬a < b b =

Alias of the reverse direction of finset.Ico_eq_empty_iff.

theorem finset.Ioc_eq_empty {α : Type u_2} [preorder α] {a b : α} :
¬a < b b =

Alias of the reverse direction of finset.Ioc_eq_empty_iff.

@[simp]
theorem finset.Ioo_eq_empty {α : Type u_2} [preorder α] {a b : α} (h : ¬a < b) :
b =
@[simp]
theorem finset.Icc_eq_empty_of_lt {α : Type u_2} [preorder α] {a b : α} (h : b < a) :
b =
@[simp]
theorem finset.Ico_eq_empty_of_le {α : Type u_2} [preorder α] {a b : α} (h : b a) :
b =
@[simp]
theorem finset.Ioc_eq_empty_of_le {α : Type u_2} [preorder α] {a b : α} (h : b a) :
b =
@[simp]
theorem finset.Ioo_eq_empty_of_le {α : Type u_2} [preorder α] {a b : α} (h : b a) :
b =
@[simp]
theorem finset.left_mem_Icc {α : Type u_2} [preorder α] {a b : α} :
a b a b
@[simp]
theorem finset.left_mem_Ico {α : Type u_2} [preorder α] {a b : α} :
a b a < b
@[simp]
theorem finset.right_mem_Icc {α : Type u_2} [preorder α] {a b : α} :
b b a b
@[simp]
theorem finset.right_mem_Ioc {α : Type u_2} [preorder α] {a b : α} :
b b a < b
@[simp]
theorem finset.left_not_mem_Ioc {α : Type u_2} [preorder α] {a b : α} :
a b
@[simp]
theorem finset.left_not_mem_Ioo {α : Type u_2} [preorder α] {a b : α} :
a b
@[simp]
theorem finset.right_not_mem_Ico {α : Type u_2} [preorder α] {a b : α} :
b b
@[simp]
theorem finset.right_not_mem_Ioo {α : Type u_2} [preorder α] {a b : α} :
b b
theorem finset.Icc_subset_Icc {α : Type u_2} [preorder α] {a₁ a₂ b₁ b₂ : α} (ha : a₂ a₁) (hb : b₁ b₂) :
b₁ b₂
theorem finset.Ico_subset_Ico {α : Type u_2} [preorder α] {a₁ a₂ b₁ b₂ : α} (ha : a₂ a₁) (hb : b₁ b₂) :
b₁ b₂
theorem finset.Ioc_subset_Ioc {α : Type u_2} [preorder α] {a₁ a₂ b₁ b₂ : α} (ha : a₂ a₁) (hb : b₁ b₂) :
b₁ b₂
theorem finset.Ioo_subset_Ioo {α : Type u_2} [preorder α] {a₁ a₂ b₁ b₂ : α} (ha : a₂ a₁) (hb : b₁ b₂) :
b₁ b₂
theorem finset.Icc_subset_Icc_left {α : Type u_2} [preorder α] {a₁ a₂ b : α} (h : a₁ a₂) :
b b
theorem finset.Ico_subset_Ico_left {α : Type u_2} [preorder α] {a₁ a₂ b : α} (h : a₁ a₂) :
b b
theorem finset.Ioc_subset_Ioc_left {α : Type u_2} [preorder α] {a₁ a₂ b : α} (h : a₁ a₂) :
b b
theorem finset.Ioo_subset_Ioo_left {α : Type u_2} [preorder α] {a₁ a₂ b : α} (h : a₁ a₂) :
b b
theorem finset.Icc_subset_Icc_right {α : Type u_2} [preorder α] {a b₁ b₂ : α} (h : b₁ b₂) :
b₁ b₂
theorem finset.Ico_subset_Ico_right {α : Type u_2} [preorder α] {a b₁ b₂ : α} (h : b₁ b₂) :
b₁ b₂
theorem finset.Ioc_subset_Ioc_right {α : Type u_2} [preorder α] {a b₁ b₂ : α} (h : b₁ b₂) :
b₁ b₂
theorem finset.Ioo_subset_Ioo_right {α : Type u_2} [preorder α] {a b₁ b₂ : α} (h : b₁ b₂) :
b₁ b₂
theorem finset.Ico_subset_Ioo_left {α : Type u_2} [preorder α] {a₁ a₂ b : α} (h : a₁ < a₂) :
b b
theorem finset.Ioc_subset_Ioo_right {α : Type u_2} [preorder α] {a b₁ b₂ : α} (h : b₁ < b₂) :
b₁ b₂
theorem finset.Icc_subset_Ico_right {α : Type u_2} [preorder α] {a b₁ b₂ : α} (h : b₁ < b₂) :
b₁ b₂
theorem finset.Ioo_subset_Ico_self {α : Type u_2} [preorder α] {a b : α} :
b b
theorem finset.Ioo_subset_Ioc_self {α : Type u_2} [preorder α] {a b : α} :
b b
theorem finset.Ico_subset_Icc_self {α : Type u_2} [preorder α] {a b : α} :
b b
theorem finset.Ioc_subset_Icc_self {α : Type u_2} [preorder α] {a b : α} :
b b
theorem finset.Ioo_subset_Icc_self {α : Type u_2} [preorder α] {a b : α} :
b b
theorem finset.Icc_subset_Icc_iff {α : Type u_2} [preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₁ b₁) :
b₁ b₂ a₂ a₁ b₁ b₂
theorem finset.Icc_subset_Ioo_iff {α : Type u_2} [preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₁ b₁) :
b₁ b₂ a₂ < a₁ b₁ < b₂
theorem finset.Icc_subset_Ico_iff {α : Type u_2} [preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₁ b₁) :
b₁ b₂ a₂ a₁ b₁ < b₂
theorem finset.Icc_subset_Ioc_iff {α : Type u_2} [preorder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₁ b₁) :
b₁ b₂ a₂ < a₁ b₁ b₂
theorem finset.Icc_ssubset_Icc_left {α : Type u_2} [preorder α] {a₁ a₂ b₁ b₂ : α} (hI : a₂ b₂) (ha : a₂ < a₁) (hb : b₁ b₂) :
b₁ b₂
theorem finset.Icc_ssubset_Icc_right {α : Type u_2} [preorder α] {a₁ a₂ b₁ b₂ : α} (hI : a₂ b₂) (ha : a₂ a₁) (hb : b₁ < b₂) :
b₁ b₂
@[simp]
theorem finset.Ico_self {α : Type u_2} [preorder α] (a : α) :
a =
@[simp]
theorem finset.Ioc_self {α : Type u_2} [preorder α] (a : α) :
a =
@[simp]
theorem finset.Ioo_self {α : Type u_2} [preorder α] (a : α) :
a =
def set.fintype_of_mem_bounds {α : Type u_2} [preorder α] {a b : α} {s : set α} [decidable_pred (λ (_x : α), _x s)] (ha : a ) (hb : b ) :

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

Equations
theorem bdd_below.finite_of_bdd_above {α : Type u_2} [preorder α] {s : set α} (h₀ : bdd_below s) (h₁ : bdd_above s) :
theorem finset.Ico_filter_lt_of_le_left {α : Type u_2} [preorder α] {a b c : α} [decidable_pred (λ (_x : α), _x < c)] (hca : c a) :
finset.filter (λ (_x : α), _x < c) b) =
theorem finset.Ico_filter_lt_of_right_le {α : Type u_2} [preorder α] {a b c : α} [decidable_pred (λ (_x : α), _x < c)] (hbc : b c) :
finset.filter (λ (_x : α), _x < c) b) = b
theorem finset.Ico_filter_lt_of_le_right {α : Type u_2} [preorder α] {a b c : α} [decidable_pred (λ (_x : α), _x < c)] (hcb : c b) :
finset.filter (λ (_x : α), _x < c) b) = c
theorem finset.Ico_filter_le_of_le_left {α : Type u_2} [preorder α] {a b c : α} [decidable_pred (has_le.le c)] (hca : c a) :
b) = b
theorem finset.Ico_filter_le_of_right_le {α : Type u_2} [preorder α] {a b : α} [decidable_pred (has_le.le b)] :
b) =
theorem finset.Ico_filter_le_of_left_le {α : Type u_2} [preorder α] {a b c : α} [decidable_pred (has_le.le c)] (hac : a c) :
b) = b
theorem finset.Icc_filter_lt_of_lt_right {α : Type u_2} [preorder α] {a b c : α} [decidable_pred (λ (_x : α), _x < c)] (h : b < c) :
finset.filter (λ (_x : α), _x < c) b) = b
theorem finset.Ioc_filter_lt_of_lt_right {α : Type u_2} [preorder α] {a b c : α} [decidable_pred (λ (_x : α), _x < c)] (h : b < c) :
finset.filter (λ (_x : α), _x < c) b) = b
theorem finset.Iic_filter_lt_of_lt_right {α : Type u_1} [preorder α] {a c : α} [decidable_pred (λ (_x : α), _x < c)] (h : a < c) :
finset.filter (λ (_x : α), _x < c) (finset.Iic a) =
theorem finset.filter_lt_lt_eq_Ioo {α : Type u_2} [preorder α] (a b : α) [fintype α] [decidable_pred (λ (j : α), a < j j < b)] :
finset.filter (λ (j : α), a < j j < b) finset.univ = b
theorem finset.filter_lt_le_eq_Ioc {α : Type u_2} [preorder α] (a b : α) [fintype α] [decidable_pred (λ (j : α), a < j j b)] :
finset.filter (λ (j : α), a < j j b) finset.univ = b
theorem finset.filter_le_lt_eq_Ico {α : Type u_2} [preorder α] (a b : α) [fintype α] [decidable_pred (λ (j : α), a j j < b)] :
finset.filter (λ (j : α), a j j < b) finset.univ = b
theorem finset.filter_le_le_eq_Icc {α : Type u_2} [preorder α] (a b : α) [fintype α] [decidable_pred (λ (j : α), a j j b)] :
finset.filter (λ (j : α), a j j b) finset.univ = b
theorem finset.Icc_subset_Ici_self {α : Type u_2} [preorder α] {a b : α}  :
b
theorem finset.Ico_subset_Ici_self {α : Type u_2} [preorder α] {a b : α}  :
b
theorem finset.Ioc_subset_Ioi_self {α : Type u_2} [preorder α] {a b : α}  :
b
theorem finset.Ioo_subset_Ioi_self {α : Type u_2} [preorder α] {a b : α}  :
b
theorem finset.Ioc_subset_Ici_self {α : Type u_2} [preorder α] {a b : α}  :
b
theorem finset.Ioo_subset_Ici_self {α : Type u_2} [preorder α] {a b : α}  :
b
theorem finset.Icc_subset_Iic_self {α : Type u_2} [preorder α] {a b : α}  :
b
theorem finset.Ioc_subset_Iic_self {α : Type u_2} [preorder α] {a b : α}  :
b
theorem finset.Ico_subset_Iio_self {α : Type u_2} [preorder α] {a b : α}  :
b
theorem finset.Ioo_subset_Iio_self {α : Type u_2} [preorder α] {a b : α}  :
b
theorem finset.Ico_subset_Iic_self {α : Type u_2} [preorder α] {a b : α}  :
b
theorem finset.Ioo_subset_Iic_self {α : Type u_2} [preorder α] {a b : α}  :
b
theorem finset.Ioi_subset_Ici_self {α : Type u_2} [preorder α] {a : α} :
theorem bdd_below.finite {α : Type u_2} [preorder α] {s : set α} (hs : bdd_below s) :
theorem finset.filter_lt_eq_Ioi {α : Type u_2} [preorder α] {a : α} [fintype α] [decidable_pred (has_lt.lt a)] :
theorem finset.filter_le_eq_Ici {α : Type u_2} [preorder α] {a : α} [fintype α] [decidable_pred (has_le.le a)] :
theorem finset.Iio_subset_Iic_self {α : Type u_2} [preorder α] {a : α} :
theorem bdd_above.finite {α : Type u_2} [preorder α] {s : set α} (hs : bdd_above s) :
theorem finset.filter_gt_eq_Iio {α : Type u_2} [preorder α] {a : α} [fintype α] [decidable_pred (λ (_x : α), _x < a)] :
finset.filter (λ (_x : α), _x < a) finset.univ =
theorem finset.filter_ge_eq_Iic {α : Type u_2} [preorder α] {a : α} [fintype α] [decidable_pred (λ (_x : α), _x a)] :
finset.filter (λ (_x : α), _x a) finset.univ =
theorem finset.disjoint_Ioi_Iio {α : Type u_2} [preorder α] [decidable_eq α] (a : α) :
@[simp]
theorem finset.Icc_self {α : Type u_2} (a : α) :
a = {a}
@[simp]
theorem finset.Icc_eq_singleton_iff {α : Type u_2} {a b c : α} :
b = {c} a = c b = c
@[simp]
theorem finset.Icc_erase_left {α : Type u_2} [decidable_eq α] (a b : α) :
b).erase a = b
@[simp]
theorem finset.Icc_erase_right {α : Type u_2} [decidable_eq α] (a b : α) :
b).erase b = b
@[simp]
theorem finset.Ico_erase_left {α : Type u_2} [decidable_eq α] (a b : α) :
b).erase a = b
@[simp]
theorem finset.Ioc_erase_right {α : Type u_2} [decidable_eq α] (a b : α) :
b).erase b = b
@[simp]
theorem finset.Icc_diff_both {α : Type u_2} [decidable_eq α] (a b : α) :
b \ {a, b} = b
@[simp]
theorem finset.Ico_insert_right {α : Type u_2} {a b : α} [decidable_eq α] (h : a b) :
b) = b
@[simp]
theorem finset.Ioc_insert_left {α : Type u_2} {a b : α} [decidable_eq α] (h : a b) :
b) = b
@[simp]
theorem finset.Ioo_insert_left {α : Type u_2} {a b : α} [decidable_eq α] (h : a < b) :
b) = b
@[simp]
theorem finset.Ioo_insert_right {α : Type u_2} {a b : α} [decidable_eq α] (h : a < b) :
b) = b
@[simp]
theorem finset.Icc_diff_Ico_self {α : Type u_2} {a b : α} [decidable_eq α] (h : a b) :
b \ b = {b}
@[simp]
theorem finset.Icc_diff_Ioc_self {α : Type u_2} {a b : α} [decidable_eq α] (h : a b) :
b \ b = {a}
@[simp]
theorem finset.Icc_diff_Ioo_self {α : Type u_2} {a b : α} [decidable_eq α] (h : a b) :
b \ b = {a, b}
@[simp]
theorem finset.Ico_diff_Ioo_self {α : Type u_2} {a b : α} [decidable_eq α] (h : a < b) :
b \ b = {a}
@[simp]
theorem finset.Ioc_diff_Ioo_self {α : Type u_2} {a b : α} [decidable_eq α] (h : a < b) :
b \ b = {b}
@[simp]
theorem finset.Ico_inter_Ico_consecutive {α : Type u_2} [decidable_eq α] (a b c : α) :
b c =
theorem finset.Ico_disjoint_Ico_consecutive {α : Type u_2} [decidable_eq α] (a b c : α) :
disjoint b) c)
theorem finset.Icc_eq_cons_Ico {α : Type u_2} {a b : α} (h : a b) :
b =
theorem finset.Icc_eq_cons_Ioc {α : Type u_2} {a b : α} (h : a b) :
b =
theorem finset.Ico_filter_le_left {α : Type u_2} {a b : α} [decidable_pred (λ (_x : α), _x a)] (hab : a < b) :
finset.filter (λ (x : α), x a) b) = {a}
theorem finset.card_Ico_eq_card_Icc_sub_one {α : Type u_2} (a b : α) :
b).card = b).card - 1
theorem finset.card_Ioc_eq_card_Icc_sub_one {α : Type u_2} (a b : α) :
b).card = b).card - 1
theorem finset.card_Ioo_eq_card_Ico_sub_one {α : Type u_2} (a b : α) :
b).card = b).card - 1
theorem finset.card_Ioo_eq_card_Ioc_sub_one {α : Type u_2} (a b : α) :
b).card = b).card - 1
theorem finset.card_Ioo_eq_card_Icc_sub_two {α : Type u_2} (a b : α) :
b).card = b).card - 2
@[simp]
theorem finset.Ici_erase {α : Type u_2} [order_top α] [decidable_eq α] (a : α) :
@[simp]
theorem finset.Ioi_insert {α : Type u_2} [order_top α] [decidable_eq α] (a : α) :
theorem finset.Ici_eq_cons_Ioi {α : Type u_2} [order_top α] (a : α) :
@[simp]
theorem finset.Iic_erase {α : Type u_2} [order_bot α] [decidable_eq α] (b : α) :
@[simp]
theorem finset.Iio_insert {α : Type u_2} [order_bot α] [decidable_eq α] (b : α) :
theorem finset.Iic_eq_cons_Iio {α : Type u_2} [order_bot α] (b : α) :
theorem finset.Ico_subset_Ico_iff {α : Type u_2} [linear_order α] {a₁ b₁ a₂ b₂ : α} (h : a₁ < b₁) :
b₁ b₂ a₂ a₁ b₁ b₂
theorem finset.Ico_union_Ico_eq_Ico {α : Type u_2} [linear_order α] {a b c : α} (hab : a b) (hbc : b c) :
b c = c
@[simp]
theorem finset.Ioc_union_Ioc_eq_Ioc {α : Type u_2} [linear_order α] {a b c : α} (h₁ : a b) (h₂ : b c) :
b c = c
theorem finset.Ico_subset_Ico_union_Ico {α : Type u_2} [linear_order α] {a b c : α} :
c b c
theorem finset.Ico_union_Ico' {α : Type u_2} [linear_order α] {a b c d : α} (hcb : c b) (had : a d) :
b d = d)
theorem finset.Ico_union_Ico {α : Type u_2} [linear_order α] {a b c d : α} (h₁ : ) (h₂ : ) :
b d = d)
theorem finset.Ico_inter_Ico {α : Type u_2} [linear_order α] {a b c d : α} :
b d = d)
@[simp]
theorem finset.Ico_filter_lt {α : Type u_2} [linear_order α] (a b c : α) :
finset.filter (λ (x : α), x < c) b) = c)
@[simp]
theorem finset.Ico_filter_le {α : Type u_2} [linear_order α] (a b c : α) :
finset.filter (λ (x : α), c x) b) = b
@[simp]
theorem finset.Ioo_filter_lt {α : Type u_2} [linear_order α] (a b c : α) :
finset.filter (λ (_x : α), _x < c) b) = c)
@[simp]
theorem finset.Iio_filter_lt {α : Type u_1} [linear_order α] (a b : α) :
finset.filter (λ (_x : α), _x < b) (finset.Iio a) =
@[simp]
theorem finset.Ico_diff_Ico_left {α : Type u_2} [linear_order α] (a b c : α) :
b \ c = b
@[simp]
theorem finset.Ico_diff_Ico_right {α : Type u_2} [linear_order α] (a b c : α) :
b \ b = c)
theorem finset.Ioi_disj_union_Iio {α : Type u_2} [linear_order α] [fintype α] (a : α) :
theorem finset.image_add_left_Icc {α : Type u_2} [decidable_eq α] (a b c : α) :
b) = finset.Icc (c + a) (c + b)
theorem finset.image_add_left_Ico {α : Type u_2} [decidable_eq α] (a b c : α) :
b) = finset.Ico (c + a) (c + b)
theorem finset.image_add_left_Ioc {α : Type u_2} [decidable_eq α] (a b c : α) :
b) = finset.Ioc (c + a) (c + b)
theorem finset.image_add_left_Ioo {α : Type u_2} [decidable_eq α] (a b c : α) :
b) = finset.Ioo (c + a) (c + b)
theorem finset.image_add_right_Icc {α : Type u_2} [decidable_eq α] (a b c : α) :
finset.image (λ (_x : α), _x + c) b) = finset.Icc (a + c) (b + c)
theorem finset.image_add_right_Ico {α : Type u_2} [decidable_eq α] (a b c : α) :
finset.image (λ (_x : α), _x + c) b) = finset.Ico (a + c) (b + c)
theorem finset.image_add_right_Ioc {α : Type u_2} [decidable_eq α] (a b c : α) :
finset.image (λ (_x : α), _x + c) b) = finset.Ioc (a + c) (b + c)
theorem finset.image_add_right_Ioo {α : Type u_2} [decidable_eq α] (a b c : α) :
finset.image (λ (_x : α), _x + c) b) = finset.Ioo (a + c) (b + c)
theorem finset.prod_prod_Ioi_mul_eq_prod_prod_off_diag {ι : Type u_1} {α : Type u_2} [fintype ι] [linear_order ι] [comm_monoid α] (f : ι → ι → α) :
finset.univ.prod (λ (i : ι), (finset.Ioi i).prod (λ (j : ι), f j i * f i j)) = finset.univ.prod (λ (i : ι), {i}.prod (λ (j : ι), f j i))
theorem finset.sum_sum_Ioi_add_eq_sum_sum_off_diag {ι : Type u_1} {α : Type u_2} [fintype ι] [linear_order ι] (f : ι → ι → α) :
finset.univ.sum (λ (i : ι), (finset.Ioi i).sum (λ (j : ι), f j i + f i j)) = finset.univ.sum (λ (i : ι), {i}.sum (λ (j : ι), f j i))