# mathlib3documentation

data.finset.locally_finite

# Intervals as finsets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 set.infinite.not_bdd_below {α : Type u_2} [preorder α] {s : set α} :
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 set.infinite.not_bdd_above {α : Type u_2} [preorder α] {s : set α} :
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 α] (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
theorem finset.Ico_disjoint_Ico_consecutive {α : Type u_2} (a b c : α) :
disjoint 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.Icc_eq_cons_Ico {α : Type u_2} {a b : α} (h : a b) :
b =

`finset.cons` version of `finset.Ico_insert_right`.

theorem finset.Icc_eq_cons_Ioc {α : Type u_2} {a b : α} (h : a b) :
b =

`finset.cons` version of `finset.Ioc_insert_left`.

theorem finset.Ioc_eq_cons_Ioo {α : Type u_2} {a b : α} (h : a < b) :
b =

`finset.cons` version of `finset.Ioo_insert_right`.

theorem finset.Ico_eq_cons_Ioo {α : Type u_2} {a b : α} (h : a < b) :
b =

`finset.cons` version of `finset.Ioo_insert_left`.

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} [decidable_eq α] (a : α) :
@[simp]
theorem finset.Ioi_insert {α : Type u_2} [decidable_eq α] (a : α) :
@[simp]
theorem finset.not_mem_Ioi_self {α : Type u_2} {b : α} :
b
theorem finset.Ici_eq_cons_Ioi {α : Type u_2} (a : α) :

`finset.cons` version of `finset.Ioi_insert`.

theorem finset.card_Ioi_eq_card_Ici_sub_one {α : Type u_2} (a : α) :
@[simp]
theorem finset.Iic_erase {α : Type u_2} [decidable_eq α] (b : α) :
@[simp]
theorem finset.Iio_insert {α : Type u_2} [decidable_eq α] (b : α) :
@[simp]
theorem finset.not_mem_Iio_self {α : Type u_2} {b : α} :
b
theorem finset.Iic_eq_cons_Iio {α : Type u_2} (b : α) :

`finset.cons` version of `finset.Iio_insert`.

theorem finset.card_Iio_eq_card_Iic_sub_one {α : Type u_2} (a : α) :
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 set.infinite.exists_gt {α : Type u_2} [linear_order α] {s : set α} (hs : s.infinite) (a : α) :
(b : α) (H : b s), a < b
theorem set.infinite_iff_exists_gt {α : Type u_2} [linear_order α] {s : set α} [nonempty α] :
s.infinite (a : α), (b : α) (H : b s), a < b
theorem set.infinite.exists_lt {α : Type u_2} [linear_order α] {s : set α} (hs : s.infinite) (a : α) :
(b : α) (H : b s), b < a
theorem set.infinite_iff_exists_lt {α : Type u_2} [linear_order α] {s : set α} [nonempty α] :
s.infinite (a : α), (b : α) (H : b s), b < a
theorem finset.Ioi_disj_union_Iio {α : Type u_2} [linear_order α] [fintype α] (a : α) :
theorem finset.uIcc_to_dual {α : Type u_2} [lattice α] (a b : α) :
@[simp]
theorem finset.uIcc_of_le {α : Type u_2} [lattice α] {a b : α} (h : a b) :
b = b
@[simp]
theorem finset.uIcc_of_ge {α : Type u_2} [lattice α] {a b : α} (h : b a) :
b = a
theorem finset.uIcc_comm {α : Type u_2} [lattice α] (a b : α) :
b = a
@[simp]
theorem finset.uIcc_self {α : Type u_2} [lattice α] {a : α} :
a = {a}
@[simp]
theorem finset.nonempty_uIcc {α : Type u_2} [lattice α] {a b : α} :
theorem finset.Icc_subset_uIcc {α : Type u_2} [lattice α] {a b : α} :
b b
theorem finset.Icc_subset_uIcc' {α : Type u_2} [lattice α] {a b : α} :
a b
@[simp]
theorem finset.left_mem_uIcc {α : Type u_2} [lattice α] {a b : α} :
a b
@[simp]
theorem finset.right_mem_uIcc {α : Type u_2} [lattice α] {a b : α} :
b b
theorem finset.mem_uIcc_of_le {α : Type u_2} [lattice α] {a b x : α} (ha : a x) (hb : x b) :
x b
theorem finset.mem_uIcc_of_ge {α : Type u_2} [lattice α] {a b x : α} (hb : b x) (ha : x a) :
x b
theorem finset.uIcc_subset_uIcc {α : Type u_2} [lattice α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₁ b₂) (h₂ : b₁ b₂) :
b₁ b₂
theorem finset.uIcc_subset_Icc {α : Type u_2} [lattice α] {a₁ a₂ b₁ b₂ : α} (ha : a₁ b₂) (hb : b₁ b₂) :
b₁ b₂
theorem finset.uIcc_subset_uIcc_iff_mem {α : Type u_2} [lattice α] {a₁ a₂ b₁ b₂ : α} :
b₁ b₂ a₁ b₂ b₁ b₂
theorem finset.uIcc_subset_uIcc_iff_le' {α : Type u_2} [lattice α] {a₁ a₂ b₁ b₂ : α} :
b₁ b₂ a₂ b₂ a₁ b₁ a₁ b₁ a₂ b₂
theorem finset.uIcc_subset_uIcc_right {α : Type u_2} [lattice α] {a b x : α} (h : x b) :
b b
theorem finset.uIcc_subset_uIcc_left {α : Type u_2} [lattice α] {a b x : α} (h : x b) :
x b
theorem finset.eq_of_mem_uIcc_of_mem_uIcc {α : Type u_2} {a b c : α} :
a c b c a = b
theorem finset.eq_of_mem_uIcc_of_mem_uIcc' {α : Type u_2} {a b c : α} :
b c c b b = c
theorem finset.uIcc_injective_right {α : Type u_2} (a : α) :
function.injective (λ (b : α), a)
theorem finset.uIcc_injective_left {α : Type u_2} (a : α) :
theorem finset.Icc_min_max {α : Type u_2} [linear_order α] {a b : α} :
b) = b
theorem finset.uIcc_of_not_le {α : Type u_2} [linear_order α] {a b : α} (h : ¬a b) :
b = a
theorem finset.uIcc_of_not_ge {α : Type u_2} [linear_order α] {a b : α} (h : ¬b a) :
b = b
theorem finset.uIcc_eq_union {α : Type u_2} [linear_order α] {a b : α} :
b = b a
theorem finset.mem_uIcc' {α : Type u_2} [linear_order α] {a b c : α} :
a c b a a c c a a b
theorem finset.not_mem_uIcc_of_lt {α : Type u_2} [linear_order α] {a b c : α} :
c < a c < b c b
theorem finset.not_mem_uIcc_of_gt {α : Type u_2} [linear_order α] {a b c : α} :
a < c b < c c b
theorem finset.uIcc_subset_uIcc_iff_le {α : Type u_2} [linear_order α] {a₁ a₂ b₁ b₂ : α} :
b₁ b₂ b₂ b₁ b₁ b₂
theorem finset.uIcc_subset_uIcc_union_uIcc {α : Type u_2} [linear_order α] {a b c : α} :
c b c

A sort of triangle inequality.

@[simp]
theorem finset.map_add_left_Icc {α : Type u_2} (a b c : α) :
b) = finset.Icc (c + a) (c + b)
@[simp]
theorem finset.map_add_right_Icc {α : Type u_2} (a b c : α) :
b) = finset.Icc (a + c) (b + c)
@[simp]
theorem finset.map_add_left_Ico {α : Type u_2} (a b c : α) :
b) = finset.Ico (c + a) (c + b)
@[simp]
theorem finset.map_add_right_Ico {α : Type u_2} (a b c : α) :
b) = finset.Ico (a + c) (b + c)
@[simp]
theorem finset.map_add_left_Ioc {α : Type u_2} (a b c : α) :
b) = finset.Ioc (c + a) (c + b)
@[simp]
theorem finset.map_add_right_Ioc {α : Type u_2} (a b c : α) :
b) = finset.Ioc (a + c) (b + c)
@[simp]
theorem finset.map_add_left_Ioo {α : Type u_2} (a b c : α) :
b) = finset.Ioo (c + a) (c + b)
@[simp]
theorem finset.map_add_right_Ioo {α : Type u_2} (a b c : α) :
b) = finset.Ioo (a + c) (b + c)
@[simp]
theorem finset.image_add_left_Icc {α : Type u_2} [decidable_eq α] (a b c : α) :
b) = finset.Icc (c + a) (c + b)
@[simp]
theorem finset.image_add_left_Ico {α : Type u_2} [decidable_eq α] (a b c : α) :
b) = finset.Ico (c + a) (c + b)
@[simp]
theorem finset.image_add_left_Ioc {α : Type u_2} [decidable_eq α] (a b c : α) :
b) = finset.Ioc (c + a) (c + b)
@[simp]
theorem finset.image_add_left_Ioo {α : Type u_2} [decidable_eq α] (a b c : α) :
b) = finset.Ioo (c + a) (c + b)
@[simp]
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))