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 α]
[locally_finite_order α]
{a b : α} :
(finset.Icc a b).nonempty ↔ a ≤ b
@[simp]
theorem
finset.nonempty_Ico
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α} :
(finset.Ico a b).nonempty ↔ a < b
@[simp]
theorem
finset.nonempty_Ioc
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α} :
(finset.Ioc a b).nonempty ↔ a < b
@[simp]
theorem
finset.nonempty_Ioo
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α}
[densely_ordered α] :
(finset.Ioo a b).nonempty ↔ a < b
@[simp]
@[simp]
@[simp]
@[simp]
theorem
finset.Ioo_eq_empty_iff
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α}
[densely_ordered α] :
theorem
finset.Icc_eq_empty
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α} :
¬a ≤ b → finset.Icc a b = ∅
Alias of the reverse direction of finset.Icc_eq_empty_iff.
theorem
finset.Ico_eq_empty
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α} :
¬a < b → finset.Ico a b = ∅
Alias of the reverse direction of finset.Ico_eq_empty_iff.
theorem
finset.Ioc_eq_empty
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α} :
¬a < b → finset.Ioc a b = ∅
Alias of the reverse direction of finset.Ioc_eq_empty_iff.
@[simp]
theorem
finset.Ioo_eq_empty
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α}
(h : ¬a < b) :
finset.Ioo a b = ∅
@[simp]
theorem
finset.Icc_eq_empty_of_lt
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α}
(h : b < a) :
finset.Icc a b = ∅
@[simp]
theorem
finset.Ico_eq_empty_of_le
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α}
(h : b ≤ a) :
finset.Ico a b = ∅
@[simp]
theorem
finset.Ioc_eq_empty_of_le
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α}
(h : b ≤ a) :
finset.Ioc a b = ∅
@[simp]
theorem
finset.Ioo_eq_empty_of_le
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α}
(h : b ≤ a) :
finset.Ioo a b = ∅
@[simp]
theorem
finset.left_mem_Icc
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α} :
a ∈ finset.Icc a b ↔ a ≤ b
@[simp]
theorem
finset.left_mem_Ico
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α} :
a ∈ finset.Ico a b ↔ a < b
@[simp]
theorem
finset.right_mem_Icc
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α} :
b ∈ finset.Icc a b ↔ a ≤ b
@[simp]
theorem
finset.right_mem_Ioc
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α} :
b ∈ finset.Ioc a b ↔ a < b
@[simp]
theorem
finset.left_not_mem_Ioc
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α} :
a ∉ finset.Ioc a b
@[simp]
theorem
finset.left_not_mem_Ioo
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α} :
a ∉ finset.Ioo a b
@[simp]
theorem
finset.right_not_mem_Ico
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α} :
b ∉ finset.Ico a b
@[simp]
theorem
finset.right_not_mem_Ioo
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α} :
b ∉ finset.Ioo a b
theorem
finset.Icc_subset_Icc
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{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_2}
[preorder α]
[locally_finite_order α]
{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_2}
[preorder α]
[locally_finite_order α]
{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_2}
[preorder α]
[locally_finite_order α]
{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_2}
[preorder α]
[locally_finite_order α]
{a₁ a₂ b : α}
(h : a₁ ≤ a₂) :
finset.Icc a₂ b ⊆ finset.Icc a₁ b
theorem
finset.Ico_subset_Ico_left
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a₁ a₂ b : α}
(h : a₁ ≤ a₂) :
finset.Ico a₂ b ⊆ finset.Ico a₁ b
theorem
finset.Ioc_subset_Ioc_left
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a₁ a₂ b : α}
(h : a₁ ≤ a₂) :
finset.Ioc a₂ b ⊆ finset.Ioc a₁ b
theorem
finset.Ioo_subset_Ioo_left
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a₁ a₂ b : α}
(h : a₁ ≤ a₂) :
finset.Ioo a₂ b ⊆ finset.Ioo a₁ b
theorem
finset.Icc_subset_Icc_right
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b₁ b₂ : α}
(h : b₁ ≤ b₂) :
finset.Icc a b₁ ⊆ finset.Icc a b₂
theorem
finset.Ico_subset_Ico_right
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b₁ b₂ : α}
(h : b₁ ≤ b₂) :
finset.Ico a b₁ ⊆ finset.Ico a b₂
theorem
finset.Ioc_subset_Ioc_right
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b₁ b₂ : α}
(h : b₁ ≤ b₂) :
finset.Ioc a b₁ ⊆ finset.Ioc a b₂
theorem
finset.Ioo_subset_Ioo_right
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b₁ b₂ : α}
(h : b₁ ≤ b₂) :
finset.Ioo a b₁ ⊆ finset.Ioo a b₂
theorem
finset.Ico_subset_Ioo_left
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a₁ a₂ b : α}
(h : a₁ < a₂) :
finset.Ico a₂ b ⊆ finset.Ioo a₁ b
theorem
finset.Ioc_subset_Ioo_right
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b₁ b₂ : α}
(h : b₁ < b₂) :
finset.Ioc a b₁ ⊆ finset.Ioo a b₂
theorem
finset.Icc_subset_Ico_right
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b₁ b₂ : α}
(h : b₁ < b₂) :
finset.Icc a b₁ ⊆ finset.Ico a b₂
theorem
finset.Ioo_subset_Ico_self
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α} :
finset.Ioo a b ⊆ finset.Ico a b
theorem
finset.Ioo_subset_Ioc_self
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α} :
finset.Ioo a b ⊆ finset.Ioc a b
theorem
finset.Ico_subset_Icc_self
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α} :
finset.Ico a b ⊆ finset.Icc a b
theorem
finset.Ioc_subset_Icc_self
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α} :
finset.Ioc a b ⊆ finset.Icc a b
theorem
finset.Ioo_subset_Icc_self
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α} :
finset.Ioo a b ⊆ finset.Icc a b
theorem
finset.Icc_subset_Icc_iff
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{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_2}
[preorder α]
[locally_finite_order α]
{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_2}
[preorder α]
[locally_finite_order α]
{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_2}
[preorder α]
[locally_finite_order α]
{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_2}
[preorder α]
[locally_finite_order α]
{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_2}
[preorder α]
[locally_finite_order α]
{a₁ a₂ b₁ b₂ : α}
(hI : a₂ ≤ b₂)
(ha : a₂ ≤ a₁)
(hb : b₁ < b₂) :
finset.Icc a₁ b₁ ⊂ finset.Icc a₂ b₂
@[simp]
theorem
finset.Ico_self
{α : Type u_2}
[preorder α]
[locally_finite_order α]
(a : α) :
finset.Ico a a = ∅
@[simp]
theorem
finset.Ioc_self
{α : Type u_2}
[preorder α]
[locally_finite_order α]
(a : α) :
finset.Ioc a a = ∅
@[simp]
theorem
finset.Ioo_self
{α : Type u_2}
[preorder α]
[locally_finite_order α]
(a : α) :
finset.Ioo a a = ∅
def
set.fintype_of_mem_bounds
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α}
{s : set α}
[decidable_pred (λ (_x : α), _x ∈ s)]
(ha : a ∈ lower_bounds s)
(hb : b ∈ upper_bounds s) :
A set with upper and lower bounds in a locally finite order is a fintype
Equations
- set.fintype_of_mem_bounds ha hb = (set.Icc a b).fintype_subset _
theorem
bdd_below.finite_of_bdd_above
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{s : set α}
(h₀ : bdd_below s)
(h₁ : bdd_above s) :
s.finite
theorem
finset.Ico_filter_lt_of_le_left
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b c : α}
[decidable_pred (λ (_x : α), _x < c)]
(hca : c ≤ a) :
finset.filter (λ (_x : α), _x < c) (finset.Ico a b) = ∅
theorem
finset.Ico_filter_lt_of_right_le
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b c : α}
[decidable_pred (λ (_x : α), _x < c)]
(hbc : b ≤ c) :
finset.filter (λ (_x : α), _x < c) (finset.Ico a b) = finset.Ico a b
theorem
finset.Ico_filter_lt_of_le_right
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b c : α}
[decidable_pred (λ (_x : α), _x < c)]
(hcb : c ≤ b) :
finset.filter (λ (_x : α), _x < c) (finset.Ico a b) = finset.Ico a c
theorem
finset.Ico_filter_le_of_le_left
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b c : α}
[decidable_pred (has_le.le c)]
(hca : c ≤ a) :
finset.filter (has_le.le c) (finset.Ico a b) = finset.Ico a b
theorem
finset.Ico_filter_le_of_right_le
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α}
[decidable_pred (has_le.le b)] :
finset.filter (has_le.le b) (finset.Ico a b) = ∅
theorem
finset.Ico_filter_le_of_left_le
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b c : α}
[decidable_pred (has_le.le c)]
(hac : a ≤ c) :
finset.filter (has_le.le c) (finset.Ico a b) = finset.Ico c b
theorem
finset.Icc_filter_lt_of_lt_right
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b c : α}
[decidable_pred (λ (_x : α), _x < c)]
(h : b < c) :
finset.filter (λ (_x : α), _x < c) (finset.Icc a b) = finset.Icc a b
theorem
finset.Ioc_filter_lt_of_lt_right
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b c : α}
[decidable_pred (λ (_x : α), _x < c)]
(h : b < c) :
finset.filter (λ (_x : α), _x < c) (finset.Ioc a b) = finset.Ioc a b
theorem
finset.Iic_filter_lt_of_lt_right
{α : Type u_1}
[preorder α]
[locally_finite_order_bot α]
{a c : α}
[decidable_pred (λ (_x : α), _x < c)]
(h : a < c) :
finset.filter (λ (_x : α), _x < c) (finset.Iic a) = finset.Iic a
theorem
finset.filter_lt_lt_eq_Ioo
{α : Type u_2}
[preorder α]
[locally_finite_order α]
(a b : α)
[fintype α]
[decidable_pred (λ (j : α), a < j ∧ j < b)] :
finset.filter (λ (j : α), a < j ∧ j < b) finset.univ = finset.Ioo a b
theorem
finset.filter_lt_le_eq_Ioc
{α : Type u_2}
[preorder α]
[locally_finite_order α]
(a b : α)
[fintype α]
[decidable_pred (λ (j : α), a < j ∧ j ≤ b)] :
finset.filter (λ (j : α), a < j ∧ j ≤ b) finset.univ = finset.Ioc a b
theorem
finset.filter_le_lt_eq_Ico
{α : Type u_2}
[preorder α]
[locally_finite_order α]
(a b : α)
[fintype α]
[decidable_pred (λ (j : α), a ≤ j ∧ j < b)] :
finset.filter (λ (j : α), a ≤ j ∧ j < b) finset.univ = finset.Ico a b
theorem
finset.filter_le_le_eq_Icc
{α : Type u_2}
[preorder α]
[locally_finite_order α]
(a b : α)
[fintype α]
[decidable_pred (λ (j : α), a ≤ j ∧ j ≤ b)] :
finset.filter (λ (j : α), a ≤ j ∧ j ≤ b) finset.univ = finset.Icc a b
theorem
finset.Icc_subset_Ici_self
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α}
[locally_finite_order_top α] :
finset.Icc a b ⊆ finset.Ici a
theorem
finset.Ico_subset_Ici_self
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α}
[locally_finite_order_top α] :
finset.Ico a b ⊆ finset.Ici a
theorem
finset.Ioc_subset_Ioi_self
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α}
[locally_finite_order_top α] :
finset.Ioc a b ⊆ finset.Ioi a
theorem
finset.Ioo_subset_Ioi_self
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α}
[locally_finite_order_top α] :
finset.Ioo a b ⊆ finset.Ioi a
theorem
finset.Ioc_subset_Ici_self
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α}
[locally_finite_order_top α] :
finset.Ioc a b ⊆ finset.Ici a
theorem
finset.Ioo_subset_Ici_self
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α}
[locally_finite_order_top α] :
finset.Ioo a b ⊆ finset.Ici a
theorem
finset.Icc_subset_Iic_self
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α}
[locally_finite_order_bot α] :
finset.Icc a b ⊆ finset.Iic b
theorem
finset.Ioc_subset_Iic_self
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α}
[locally_finite_order_bot α] :
finset.Ioc a b ⊆ finset.Iic b
theorem
finset.Ico_subset_Iio_self
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α}
[locally_finite_order_bot α] :
finset.Ico a b ⊆ finset.Iio b
theorem
finset.Ioo_subset_Iio_self
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α}
[locally_finite_order_bot α] :
finset.Ioo a b ⊆ finset.Iio b
theorem
finset.Ico_subset_Iic_self
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α}
[locally_finite_order_bot α] :
finset.Ico a b ⊆ finset.Iic b
theorem
finset.Ioo_subset_Iic_self
{α : Type u_2}
[preorder α]
[locally_finite_order α]
{a b : α}
[locally_finite_order_bot α] :
finset.Ioo a b ⊆ finset.Iic b
theorem
finset.Ioi_subset_Ici_self
{α : Type u_2}
[preorder α]
[locally_finite_order_top α]
{a : α} :
finset.Ioi a ⊆ finset.Ici a
theorem
bdd_below.finite
{α : Type u_2}
[preorder α]
[locally_finite_order_top α]
{s : set α}
(hs : bdd_below s) :
s.finite
theorem
set.infinite.not_bdd_below
{α : Type u_2}
[preorder α]
[locally_finite_order_top α]
{s : set α} :
theorem
finset.filter_lt_eq_Ioi
{α : Type u_2}
[preorder α]
[locally_finite_order_top α]
{a : α}
[fintype α]
[decidable_pred (has_lt.lt a)] :
theorem
finset.filter_le_eq_Ici
{α : Type u_2}
[preorder α]
[locally_finite_order_top α]
{a : α}
[fintype α]
[decidable_pred (has_le.le a)] :
theorem
finset.Iio_subset_Iic_self
{α : Type u_2}
[preorder α]
[locally_finite_order_bot α]
{a : α} :
finset.Iio a ⊆ finset.Iic a
theorem
bdd_above.finite
{α : Type u_2}
[preorder α]
[locally_finite_order_bot α]
{s : set α}
(hs : bdd_above s) :
s.finite
theorem
set.infinite.not_bdd_above
{α : Type u_2}
[preorder α]
[locally_finite_order_bot α]
{s : set α} :
theorem
finset.filter_gt_eq_Iio
{α : Type u_2}
[preorder α]
[locally_finite_order_bot α]
{a : α}
[fintype α]
[decidable_pred (λ (_x : α), _x < a)] :
finset.filter (λ (_x : α), _x < a) finset.univ = finset.Iio a
theorem
finset.filter_ge_eq_Iic
{α : Type u_2}
[preorder α]
[locally_finite_order_bot α]
{a : α}
[fintype α]
[decidable_pred (λ (_x : α), _x ≤ a)] :
finset.filter (λ (_x : α), _x ≤ a) finset.univ = finset.Iic a
theorem
finset.disjoint_Ioi_Iio
{α : Type u_2}
[preorder α]
[locally_finite_order_top α]
[locally_finite_order_bot α]
(a : α) :
disjoint (finset.Ioi a) (finset.Iio a)
@[simp]
theorem
finset.Icc_self
{α : Type u_2}
[partial_order α]
[locally_finite_order α]
(a : α) :
finset.Icc a a = {a}
@[simp]
theorem
finset.Icc_eq_singleton_iff
{α : Type u_2}
[partial_order α]
[locally_finite_order α]
{a b c : α} :
theorem
finset.Ico_disjoint_Ico_consecutive
{α : Type u_2}
[partial_order α]
[locally_finite_order α]
(a b c : α) :
disjoint (finset.Ico a b) (finset.Ico b c)
@[simp]
theorem
finset.Icc_erase_left
{α : Type u_2}
[partial_order α]
[locally_finite_order α]
[decidable_eq α]
(a b : α) :
(finset.Icc a b).erase a = finset.Ioc a b
@[simp]
theorem
finset.Icc_erase_right
{α : Type u_2}
[partial_order α]
[locally_finite_order α]
[decidable_eq α]
(a b : α) :
(finset.Icc a b).erase b = finset.Ico a b
@[simp]
theorem
finset.Ico_erase_left
{α : Type u_2}
[partial_order α]
[locally_finite_order α]
[decidable_eq α]
(a b : α) :
(finset.Ico a b).erase a = finset.Ioo a b
@[simp]
theorem
finset.Ioc_erase_right
{α : Type u_2}
[partial_order α]
[locally_finite_order α]
[decidable_eq α]
(a b : α) :
(finset.Ioc a b).erase b = finset.Ioo a b
@[simp]
theorem
finset.Icc_diff_both
{α : Type u_2}
[partial_order α]
[locally_finite_order α]
[decidable_eq α]
(a b : α) :
finset.Icc a b \ {a, b} = finset.Ioo a b
@[simp]
theorem
finset.Ico_insert_right
{α : Type u_2}
[partial_order α]
[locally_finite_order α]
{a b : α}
[decidable_eq α]
(h : a ≤ b) :
has_insert.insert b (finset.Ico a b) = finset.Icc a b
@[simp]
theorem
finset.Ioc_insert_left
{α : Type u_2}
[partial_order α]
[locally_finite_order α]
{a b : α}
[decidable_eq α]
(h : a ≤ b) :
has_insert.insert a (finset.Ioc a b) = finset.Icc a b
@[simp]
theorem
finset.Ioo_insert_left
{α : Type u_2}
[partial_order α]
[locally_finite_order α]
{a b : α}
[decidable_eq α]
(h : a < b) :
has_insert.insert a (finset.Ioo a b) = finset.Ico a b
@[simp]
theorem
finset.Ioo_insert_right
{α : Type u_2}
[partial_order α]
[locally_finite_order α]
{a b : α}
[decidable_eq α]
(h : a < b) :
has_insert.insert b (finset.Ioo a b) = finset.Ioc a b
@[simp]
theorem
finset.Icc_diff_Ico_self
{α : Type u_2}
[partial_order α]
[locally_finite_order α]
{a b : α}
[decidable_eq α]
(h : a ≤ b) :
finset.Icc a b \ finset.Ico a b = {b}
@[simp]
theorem
finset.Icc_diff_Ioc_self
{α : Type u_2}
[partial_order α]
[locally_finite_order α]
{a b : α}
[decidable_eq α]
(h : a ≤ b) :
finset.Icc a b \ finset.Ioc a b = {a}
@[simp]
theorem
finset.Icc_diff_Ioo_self
{α : Type u_2}
[partial_order α]
[locally_finite_order α]
{a b : α}
[decidable_eq α]
(h : a ≤ b) :
finset.Icc a b \ finset.Ioo a b = {a, b}
@[simp]
theorem
finset.Ico_diff_Ioo_self
{α : Type u_2}
[partial_order α]
[locally_finite_order α]
{a b : α}
[decidable_eq α]
(h : a < b) :
finset.Ico a b \ finset.Ioo a b = {a}
@[simp]
theorem
finset.Ioc_diff_Ioo_self
{α : Type u_2}
[partial_order α]
[locally_finite_order α]
{a b : α}
[decidable_eq α]
(h : a < b) :
finset.Ioc a b \ finset.Ioo a b = {b}
@[simp]
theorem
finset.Ico_inter_Ico_consecutive
{α : Type u_2}
[partial_order α]
[locally_finite_order α]
[decidable_eq α]
(a b c : α) :
finset.Ico a b ∩ finset.Ico b c = ∅
theorem
finset.Icc_eq_cons_Ico
{α : Type u_2}
[partial_order α]
[locally_finite_order α]
{a b : α}
(h : a ≤ b) :
finset.Icc a b = finset.cons b (finset.Ico a b) finset.right_not_mem_Ico
finset.cons version of finset.Ico_insert_right.
theorem
finset.Icc_eq_cons_Ioc
{α : Type u_2}
[partial_order α]
[locally_finite_order α]
{a b : α}
(h : a ≤ b) :
finset.Icc a b = finset.cons a (finset.Ioc a b) finset.left_not_mem_Ioc
finset.cons version of finset.Ioc_insert_left.
theorem
finset.Ioc_eq_cons_Ioo
{α : Type u_2}
[partial_order α]
[locally_finite_order α]
{a b : α}
(h : a < b) :
finset.Ioc a b = finset.cons b (finset.Ioo a b) finset.right_not_mem_Ioo
finset.cons version of finset.Ioo_insert_right.
theorem
finset.Ico_eq_cons_Ioo
{α : Type u_2}
[partial_order α]
[locally_finite_order α]
{a b : α}
(h : a < b) :
finset.Ico a b = finset.cons a (finset.Ioo a b) finset.left_not_mem_Ioo
finset.cons version of finset.Ioo_insert_left.
theorem
finset.Ico_filter_le_left
{α : Type u_2}
[partial_order α]
[locally_finite_order α]
{a b : α}
[decidable_pred (λ (_x : α), _x ≤ a)]
(hab : a < b) :
finset.filter (λ (x : α), x ≤ a) (finset.Ico a b) = {a}
theorem
finset.card_Ico_eq_card_Icc_sub_one
{α : Type u_2}
[partial_order α]
[locally_finite_order α]
(a b : α) :
(finset.Ico a b).card = (finset.Icc a b).card - 1
theorem
finset.card_Ioc_eq_card_Icc_sub_one
{α : Type u_2}
[partial_order α]
[locally_finite_order α]
(a b : α) :
(finset.Ioc a b).card = (finset.Icc a b).card - 1
theorem
finset.card_Ioo_eq_card_Ico_sub_one
{α : Type u_2}
[partial_order α]
[locally_finite_order α]
(a b : α) :
(finset.Ioo a b).card = (finset.Ico a b).card - 1
theorem
finset.card_Ioo_eq_card_Ioc_sub_one
{α : Type u_2}
[partial_order α]
[locally_finite_order α]
(a b : α) :
(finset.Ioo a b).card = (finset.Ioc a b).card - 1
theorem
finset.card_Ioo_eq_card_Icc_sub_two
{α : Type u_2}
[partial_order α]
[locally_finite_order α]
(a b : α) :
(finset.Ioo a b).card = (finset.Icc a b).card - 2
@[simp]
theorem
finset.Ici_erase
{α : Type u_2}
[partial_order α]
[locally_finite_order_top α]
[decidable_eq α]
(a : α) :
(finset.Ici a).erase a = finset.Ioi a
@[simp]
theorem
finset.Ioi_insert
{α : Type u_2}
[partial_order α]
[locally_finite_order_top α]
[decidable_eq α]
(a : α) :
has_insert.insert a (finset.Ioi a) = finset.Ici a
@[simp]
theorem
finset.not_mem_Ioi_self
{α : Type u_2}
[partial_order α]
[locally_finite_order_top α]
{b : α} :
b ∉ finset.Ioi b
theorem
finset.Ici_eq_cons_Ioi
{α : Type u_2}
[partial_order α]
[locally_finite_order_top α]
(a : α) :
finset.cons version of finset.Ioi_insert.
theorem
finset.card_Ioi_eq_card_Ici_sub_one
{α : Type u_2}
[partial_order α]
[locally_finite_order_top α]
(a : α) :
(finset.Ioi a).card = (finset.Ici a).card - 1
@[simp]
theorem
finset.Iic_erase
{α : Type u_2}
[partial_order α]
[locally_finite_order_bot α]
[decidable_eq α]
(b : α) :
(finset.Iic b).erase b = finset.Iio b
@[simp]
theorem
finset.Iio_insert
{α : Type u_2}
[partial_order α]
[locally_finite_order_bot α]
[decidable_eq α]
(b : α) :
has_insert.insert b (finset.Iio b) = finset.Iic b
@[simp]
theorem
finset.not_mem_Iio_self
{α : Type u_2}
[partial_order α]
[locally_finite_order_bot α]
{b : α} :
b ∉ finset.Iio b
theorem
finset.Iic_eq_cons_Iio
{α : Type u_2}
[partial_order α]
[locally_finite_order_bot α]
(b : α) :
finset.cons version of finset.Iio_insert.
theorem
finset.card_Iio_eq_card_Iic_sub_one
{α : Type u_2}
[partial_order α]
[locally_finite_order_bot α]
(a : α) :
(finset.Iio a).card = (finset.Iic a).card - 1
theorem
finset.Ico_subset_Ico_iff
{α : Type u_2}
[linear_order α]
[locally_finite_order α]
{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_2}
[linear_order α]
[locally_finite_order α]
{a b c : α}
(hab : a ≤ b)
(hbc : b ≤ c) :
finset.Ico a b ∪ finset.Ico b c = finset.Ico a c
@[simp]
theorem
finset.Ioc_union_Ioc_eq_Ioc
{α : Type u_2}
[linear_order α]
[locally_finite_order α]
{a b c : α}
(h₁ : a ≤ b)
(h₂ : b ≤ c) :
finset.Ioc a b ∪ finset.Ioc b c = finset.Ioc a c
theorem
finset.Ico_subset_Ico_union_Ico
{α : Type u_2}
[linear_order α]
[locally_finite_order α]
{a b c : α} :
finset.Ico a c ⊆ finset.Ico a b ∪ finset.Ico b c
theorem
finset.Ico_union_Ico'
{α : Type u_2}
[linear_order α]
[locally_finite_order α]
{a b c d : α}
(hcb : c ≤ b)
(had : a ≤ d) :
finset.Ico a b ∪ finset.Ico c d = finset.Ico (linear_order.min a c) (linear_order.max b d)
theorem
finset.Ico_union_Ico
{α : Type u_2}
[linear_order α]
[locally_finite_order α]
{a b c d : α}
(h₁ : linear_order.min a b ≤ linear_order.max c d)
(h₂ : linear_order.min c d ≤ linear_order.max a b) :
finset.Ico a b ∪ finset.Ico c d = finset.Ico (linear_order.min a c) (linear_order.max b d)
theorem
finset.Ico_inter_Ico
{α : Type u_2}
[linear_order α]
[locally_finite_order α]
{a b c d : α} :
finset.Ico a b ∩ finset.Ico c d = finset.Ico (linear_order.max a c) (linear_order.min b d)
@[simp]
theorem
finset.Ico_filter_lt
{α : Type u_2}
[linear_order α]
[locally_finite_order α]
(a b c : α) :
finset.filter (λ (x : α), x < c) (finset.Ico a b) = finset.Ico a (linear_order.min b c)
@[simp]
theorem
finset.Ico_filter_le
{α : Type u_2}
[linear_order α]
[locally_finite_order α]
(a b c : α) :
finset.filter (λ (x : α), c ≤ x) (finset.Ico a b) = finset.Ico (linear_order.max a c) b
@[simp]
theorem
finset.Ioo_filter_lt
{α : Type u_2}
[linear_order α]
[locally_finite_order α]
(a b c : α) :
finset.filter (λ (_x : α), _x < c) (finset.Ioo a b) = finset.Ioo a (linear_order.min b c)
@[simp]
theorem
finset.Iio_filter_lt
{α : Type u_1}
[linear_order α]
[locally_finite_order_bot α]
(a b : α) :
finset.filter (λ (_x : α), _x < b) (finset.Iio a) = finset.Iio (linear_order.min a b)
@[simp]
theorem
finset.Ico_diff_Ico_left
{α : Type u_2}
[linear_order α]
[locally_finite_order α]
(a b c : α) :
finset.Ico a b \ finset.Ico a c = finset.Ico (linear_order.max a c) b
@[simp]
theorem
finset.Ico_diff_Ico_right
{α : Type u_2}
[linear_order α]
[locally_finite_order α]
(a b c : α) :
finset.Ico a b \ finset.Ico c b = finset.Ico a (linear_order.min b c)
theorem
set.infinite.exists_gt
{α : Type u_2}
[linear_order α]
[locally_finite_order_bot α]
{s : set α}
(hs : s.infinite)
(a : α) :
theorem
set.infinite_iff_exists_gt
{α : Type u_2}
[linear_order α]
[locally_finite_order_bot α]
{s : set α}
[nonempty α] :
theorem
set.infinite.exists_lt
{α : Type u_2}
[linear_order α]
[locally_finite_order_top α]
{s : set α}
(hs : s.infinite)
(a : α) :
theorem
set.infinite_iff_exists_lt
{α : Type u_2}
[linear_order α]
[locally_finite_order_top α]
{s : set α}
[nonempty α] :
theorem
finset.Ioi_disj_union_Iio
{α : Type u_2}
[linear_order α]
[fintype α]
[locally_finite_order_top α]
[locally_finite_order_bot α]
(a : α) :
(finset.Ioi a).disj_union (finset.Iio a) _ = {a}ᶜ
@[simp]
theorem
finset.uIcc_of_le
{α : Type u_2}
[lattice α]
[locally_finite_order α]
{a b : α}
(h : a ≤ b) :
finset.uIcc a b = finset.Icc a b
@[simp]
theorem
finset.uIcc_of_ge
{α : Type u_2}
[lattice α]
[locally_finite_order α]
{a b : α}
(h : b ≤ a) :
finset.uIcc a b = finset.Icc b a
theorem
finset.uIcc_comm
{α : Type u_2}
[lattice α]
[locally_finite_order α]
(a b : α) :
finset.uIcc a b = finset.uIcc b a
@[simp]
theorem
finset.uIcc_self
{α : Type u_2}
[lattice α]
[locally_finite_order α]
{a : α} :
finset.uIcc a a = {a}
@[simp]
theorem
finset.nonempty_uIcc
{α : Type u_2}
[lattice α]
[locally_finite_order α]
{a b : α} :
(finset.uIcc a b).nonempty
theorem
finset.Icc_subset_uIcc
{α : Type u_2}
[lattice α]
[locally_finite_order α]
{a b : α} :
finset.Icc a b ⊆ finset.uIcc a b
theorem
finset.Icc_subset_uIcc'
{α : Type u_2}
[lattice α]
[locally_finite_order α]
{a b : α} :
finset.Icc b a ⊆ finset.uIcc a b
@[simp]
theorem
finset.left_mem_uIcc
{α : Type u_2}
[lattice α]
[locally_finite_order α]
{a b : α} :
a ∈ finset.uIcc a b
@[simp]
theorem
finset.right_mem_uIcc
{α : Type u_2}
[lattice α]
[locally_finite_order α]
{a b : α} :
b ∈ finset.uIcc a b
theorem
finset.mem_uIcc_of_le
{α : Type u_2}
[lattice α]
[locally_finite_order α]
{a b x : α}
(ha : a ≤ x)
(hb : x ≤ b) :
x ∈ finset.uIcc a b
theorem
finset.mem_uIcc_of_ge
{α : Type u_2}
[lattice α]
[locally_finite_order α]
{a b x : α}
(hb : b ≤ x)
(ha : x ≤ a) :
x ∈ finset.uIcc a b
theorem
finset.uIcc_subset_uIcc
{α : Type u_2}
[lattice α]
[locally_finite_order α]
{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_2}
[lattice α]
[locally_finite_order α]
{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_2}
[lattice α]
[locally_finite_order α]
{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_2}
[lattice α]
[locally_finite_order α]
{a₁ a₂ b₁ b₂ : α} :
theorem
finset.uIcc_subset_uIcc_right
{α : Type u_2}
[lattice α]
[locally_finite_order α]
{a b x : α}
(h : x ∈ finset.uIcc a b) :
finset.uIcc x b ⊆ finset.uIcc a b
theorem
finset.uIcc_subset_uIcc_left
{α : Type u_2}
[lattice α]
[locally_finite_order α]
{a b x : α}
(h : x ∈ finset.uIcc a b) :
finset.uIcc a x ⊆ finset.uIcc a b
theorem
finset.eq_of_mem_uIcc_of_mem_uIcc
{α : Type u_2}
[distrib_lattice α]
[locally_finite_order α]
{a b c : α} :
a ∈ finset.uIcc b c → b ∈ finset.uIcc a c → a = b
theorem
finset.eq_of_mem_uIcc_of_mem_uIcc'
{α : Type u_2}
[distrib_lattice α]
[locally_finite_order α]
{a b c : α} :
b ∈ finset.uIcc a c → c ∈ finset.uIcc a b → b = c
theorem
finset.uIcc_injective_right
{α : Type u_2}
[distrib_lattice α]
[locally_finite_order α]
(a : α) :
function.injective (λ (b : α), finset.uIcc b a)
theorem
finset.uIcc_injective_left
{α : Type u_2}
[distrib_lattice α]
[locally_finite_order α]
(a : α) :
theorem
finset.Icc_min_max
{α : Type u_2}
[linear_order α]
[locally_finite_order α]
{a b : α} :
finset.Icc (linear_order.min a b) (linear_order.max a b) = finset.uIcc a b
theorem
finset.uIcc_of_not_le
{α : Type u_2}
[linear_order α]
[locally_finite_order α]
{a b : α}
(h : ¬a ≤ b) :
finset.uIcc a b = finset.Icc b a
theorem
finset.uIcc_of_not_ge
{α : Type u_2}
[linear_order α]
[locally_finite_order α]
{a b : α}
(h : ¬b ≤ a) :
finset.uIcc a b = finset.Icc a b
theorem
finset.uIcc_eq_union
{α : Type u_2}
[linear_order α]
[locally_finite_order α]
{a b : α} :
finset.uIcc a b = finset.Icc a b ∪ finset.Icc b a
theorem
finset.not_mem_uIcc_of_lt
{α : Type u_2}
[linear_order α]
[locally_finite_order α]
{a b c : α} :
c < a → c < b → c ∉ finset.uIcc a b
theorem
finset.not_mem_uIcc_of_gt
{α : Type u_2}
[linear_order α]
[locally_finite_order α]
{a b c : α} :
a < c → b < c → c ∉ finset.uIcc a b
theorem
finset.uIcc_subset_uIcc_iff_le
{α : Type u_2}
[linear_order α]
[locally_finite_order α]
{a₁ a₂ b₁ b₂ : α} :
finset.uIcc a₁ b₁ ⊆ finset.uIcc a₂ b₂ ↔ linear_order.min a₂ b₂ ≤ linear_order.min a₁ b₁ ∧ linear_order.max a₁ b₁ ≤ linear_order.max a₂ b₂
theorem
finset.uIcc_subset_uIcc_union_uIcc
{α : Type u_2}
[linear_order α]
[locally_finite_order α]
{a b c : α} :
finset.uIcc a c ⊆ finset.uIcc a b ∪ finset.uIcc b c
A sort of triangle inequality.
@[simp]
theorem
finset.map_add_left_Icc
{α : Type u_2}
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[locally_finite_order α]
(a b c : α) :
finset.map (add_left_embedding c) (finset.Icc a b) = finset.Icc (c + a) (c + b)
@[simp]
theorem
finset.map_add_right_Icc
{α : Type u_2}
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[locally_finite_order α]
(a b c : α) :
finset.map (add_right_embedding c) (finset.Icc a b) = finset.Icc (a + c) (b + c)
@[simp]
theorem
finset.map_add_left_Ico
{α : Type u_2}
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[locally_finite_order α]
(a b c : α) :
finset.map (add_left_embedding c) (finset.Ico a b) = finset.Ico (c + a) (c + b)
@[simp]
theorem
finset.map_add_right_Ico
{α : Type u_2}
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[locally_finite_order α]
(a b c : α) :
finset.map (add_right_embedding c) (finset.Ico a b) = finset.Ico (a + c) (b + c)
@[simp]
theorem
finset.map_add_left_Ioc
{α : Type u_2}
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[locally_finite_order α]
(a b c : α) :
finset.map (add_left_embedding c) (finset.Ioc a b) = finset.Ioc (c + a) (c + b)
@[simp]
theorem
finset.map_add_right_Ioc
{α : Type u_2}
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[locally_finite_order α]
(a b c : α) :
finset.map (add_right_embedding c) (finset.Ioc a b) = finset.Ioc (a + c) (b + c)
@[simp]
theorem
finset.map_add_left_Ioo
{α : Type u_2}
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[locally_finite_order α]
(a b c : α) :
finset.map (add_left_embedding c) (finset.Ioo a b) = finset.Ioo (c + a) (c + b)
@[simp]
theorem
finset.map_add_right_Ioo
{α : Type u_2}
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[locally_finite_order α]
(a b c : α) :
finset.map (add_right_embedding c) (finset.Ioo a b) = finset.Ioo (a + c) (b + c)
@[simp]
theorem
finset.image_add_left_Icc
{α : Type u_2}
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[locally_finite_order α]
[decidable_eq α]
(a b c : α) :
finset.image (has_add.add c) (finset.Icc a b) = finset.Icc (c + a) (c + b)
@[simp]
theorem
finset.image_add_left_Ico
{α : Type u_2}
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[locally_finite_order α]
[decidable_eq α]
(a b c : α) :
finset.image (has_add.add c) (finset.Ico a b) = finset.Ico (c + a) (c + b)
@[simp]
theorem
finset.image_add_left_Ioc
{α : Type u_2}
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[locally_finite_order α]
[decidable_eq α]
(a b c : α) :
finset.image (has_add.add c) (finset.Ioc a b) = finset.Ioc (c + a) (c + b)
@[simp]
theorem
finset.image_add_left_Ioo
{α : Type u_2}
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[locally_finite_order α]
[decidable_eq α]
(a b c : α) :
finset.image (has_add.add c) (finset.Ioo a b) = finset.Ioo (c + a) (c + b)
@[simp]
theorem
finset.image_add_right_Icc
{α : Type u_2}
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[locally_finite_order α]
[decidable_eq α]
(a b c : α) :
finset.image (λ (_x : α), _x + c) (finset.Icc a b) = finset.Icc (a + c) (b + c)
theorem
finset.image_add_right_Ico
{α : Type u_2}
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[locally_finite_order α]
[decidable_eq α]
(a b c : α) :
finset.image (λ (_x : α), _x + c) (finset.Ico a b) = finset.Ico (a + c) (b + c)
theorem
finset.image_add_right_Ioc
{α : Type u_2}
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[locally_finite_order α]
[decidable_eq α]
(a b c : α) :
finset.image (λ (_x : α), _x + c) (finset.Ioc a b) = finset.Ioc (a + c) (b + c)
theorem
finset.image_add_right_Ioo
{α : Type u_2}
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[locally_finite_order α]
[decidable_eq α]
(a b c : α) :
finset.image (λ (_x : α), _x + c) (finset.Ioo a 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 ι]
[locally_finite_order_top ι]
[locally_finite_order_bot ι]
[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 ι]
[locally_finite_order_top ι]
[locally_finite_order_bot ι]
[add_comm_monoid α]
(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))