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.
@[simp]
theorem
finset.nonempty_Icc
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α} :
(finset.Icc a b).nonempty ↔ a ≤ b
@[simp]
theorem
finset.nonempty_Ico
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α} :
(finset.Ico a b).nonempty ↔ a < b
@[simp]
theorem
finset.nonempty_Ioc
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α} :
(finset.Ioc a b).nonempty ↔ a < b
@[simp]
theorem
finset.nonempty_Ioo
{α : Type u_1}
[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_1}
[preorder α]
[locally_finite_order α]
{a b : α}
[densely_ordered α] :
theorem
finset.Icc_eq_empty
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α} :
¬a ≤ b → finset.Icc a b = ∅
Alias of Icc_eq_empty_iff.
theorem
finset.Ico_eq_empty
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α} :
¬a < b → finset.Ico a b = ∅
Alias of Ico_eq_empty_iff.
theorem
finset.Ioc_eq_empty
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α} :
¬a < b → finset.Ioc a b = ∅
Alias of Ioc_eq_empty_iff.
@[simp]
theorem
finset.Ioo_eq_empty
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α}
(h : ¬a < b) :
finset.Ioo a b = ∅
@[simp]
theorem
finset.Icc_eq_empty_of_lt
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α}
(h : b < a) :
finset.Icc a b = ∅
@[simp]
theorem
finset.Ico_eq_empty_of_le
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α}
(h : b ≤ a) :
finset.Ico a b = ∅
@[simp]
theorem
finset.Ioc_eq_empty_of_le
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α}
(h : b ≤ a) :
finset.Ioc a b = ∅
@[simp]
theorem
finset.Ioo_eq_empty_of_le
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α}
(h : b ≤ a) :
finset.Ioo a b = ∅
@[simp]
theorem
finset.Ico_self
{α : Type u_1}
[preorder α]
[locally_finite_order α]
(a : α) :
finset.Ico a a = ∅
@[simp]
theorem
finset.Ioc_self
{α : Type u_1}
[preorder α]
[locally_finite_order α]
(a : α) :
finset.Ioc a a = ∅
@[simp]
theorem
finset.Ioo_self
{α : Type u_1}
[preorder α]
[locally_finite_order α]
(a : α) :
finset.Ioo a a = ∅
theorem
finset.left_mem_Icc
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α} :
a ∈ finset.Icc a b ↔ a ≤ b
theorem
finset.left_mem_Ico
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α} :
a ∈ finset.Ico a b ↔ a < b
theorem
finset.right_mem_Icc
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α} :
b ∈ finset.Icc a b ↔ a ≤ b
theorem
finset.right_mem_Ioc
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α} :
b ∈ finset.Ioc a b ↔ a < b
@[simp]
theorem
finset.left_not_mem_Ioc
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α} :
a ∉ finset.Ioc a b
@[simp]
theorem
finset.left_not_mem_Ioo
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α} :
a ∉ finset.Ioo a b
@[simp]
theorem
finset.right_not_mem_Ico
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α} :
b ∉ finset.Ico a b
@[simp]
theorem
finset.right_not_mem_Ioo
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α} :
b ∉ finset.Ioo a b
theorem
finset.Ico_filter_lt_of_le_left
{α : Type u_1}
[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_1}
[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_1}
[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_1}
[preorder α]
[locally_finite_order α]
{a b c : α}
[decidable_pred (has_le.le c)]
(hca : c ≤ a) :
finset.filter (λ (x : α), c ≤ x) (finset.Ico a b) = finset.Ico a b
theorem
finset.Ico_filter_le_of_right_le
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α}
[decidable_pred (has_le.le b)] :
finset.filter (λ (x : α), b ≤ x) (finset.Ico a b) = ∅
theorem
finset.Ico_filter_le_of_left_le
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b c : α}
[decidable_pred (has_le.le c)]
(hac : a ≤ c) :
finset.filter (λ (x : α), c ≤ x) (finset.Ico a b) = finset.Ico c b
def
set.fintype_of_mem_bounds
{α : Type u_1}
[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_1}
[preorder α]
[locally_finite_order α]
{s : set α}
(h₀ : bdd_below s)
(h₁ : bdd_above s) :
s.finite
@[simp]
theorem
finset.Icc_self
{α : Type u_1}
[partial_order α]
[locally_finite_order α]
(a : α) :
finset.Icc a a = {a}
@[simp]
theorem
finset.Icc_eq_singleton_iff
{α : Type u_1}
[partial_order α]
[locally_finite_order α]
{a b c : α} :
theorem
finset.Icc_erase_left
{α : Type u_1}
[partial_order α]
[locally_finite_order α]
{a b : α}
[decidable_eq α] :
(finset.Icc a b).erase a = finset.Ioc a b
theorem
finset.Icc_erase_right
{α : Type u_1}
[partial_order α]
[locally_finite_order α]
{a b : α}
[decidable_eq α] :
(finset.Icc a b).erase b = finset.Ico a b
theorem
finset.Ico_insert_right
{α : Type u_1}
[partial_order α]
[locally_finite_order α]
{a b : α}
[decidable_eq α]
(h : a ≤ b) :
insert b (finset.Ico a b) = finset.Icc a b
theorem
finset.Ioo_insert_left
{α : Type u_1}
[partial_order α]
[locally_finite_order α]
{a b : α}
[decidable_eq α]
(h : a < b) :
insert a (finset.Ioo a b) = finset.Ico a b
@[simp]
theorem
finset.Ico_inter_Ico_consecutive
{α : Type u_1}
[partial_order α]
[locally_finite_order α]
[decidable_eq α]
(a b c : α) :
finset.Ico a b ∩ finset.Ico b c = ∅
theorem
finset.Ico_disjoint_Ico_consecutive
{α : Type u_1}
[partial_order α]
[locally_finite_order α]
[decidable_eq α]
(a b c : α) :
disjoint (finset.Ico a b) (finset.Ico b c)
theorem
finset.Ico_filter_le_left
{α : Type u_1}
[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_1}
[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_1}
[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_1}
[partial_order α]
[locally_finite_order α]
(a b : α) :
(finset.Ioo a b).card = (finset.Ico a b).card - 1
theorem
finset.card_Ioo_eq_card_Icc_sub_two
{α : Type u_1}
[partial_order α]
[locally_finite_order α]
(a b : α) :
(finset.Ioo a b).card = (finset.Icc a b).card - 2
theorem
finset.Ico_subset_Ico_iff
{α : Type u_1}
[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_1}
[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
theorem
finset.Ico_union_Ico'
{α : Type u_1}
[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 (min a c) (max b d)
theorem
finset.Ico_union_Ico
{α : Type u_1}
[linear_order α]
[locally_finite_order α]
{a b c d : α}
(h₁ : min a b ≤ max c d)
(h₂ : min c d ≤ max a b) :
finset.Ico a b ∪ finset.Ico c d = finset.Ico (min a c) (max b d)
theorem
finset.Ico_inter_Ico
{α : Type u_1}
[linear_order α]
[locally_finite_order α]
{a b c d : α} :
finset.Ico a b ∩ finset.Ico c d = finset.Ico (max a c) (min b d)
@[simp]
theorem
finset.Ico_filter_lt
{α : Type u_1}
[linear_order α]
[locally_finite_order α]
(a b c : α) :
finset.filter (λ (x : α), x < c) (finset.Ico a b) = finset.Ico a (min b c)
@[simp]
theorem
finset.Ico_filter_le
{α : Type u_1}
[linear_order α]
[locally_finite_order α]
(a b c : α) :
finset.filter (λ (x : α), c ≤ x) (finset.Ico a b) = finset.Ico (max a c) b
@[simp]
theorem
finset.Ico_diff_Ico_left
{α : Type u_1}
[linear_order α]
[locally_finite_order α]
(a b c : α) :
finset.Ico a b \ finset.Ico a c = finset.Ico (max a c) b
@[simp]
theorem
finset.Ico_diff_Ico_right
{α : Type u_1}
[linear_order α]
[locally_finite_order α]
(a b c : α) :
finset.Ico a b \ finset.Ico c b = finset.Ico a (min b c)
theorem
bdd_below.finite
{α : Type u_1}
[preorder α]
[order_top α]
[locally_finite_order α]
{s : set α}
(hs : bdd_below s) :
s.finite
theorem
bdd_above.finite
{α : Type u_1}
[preorder α]
[order_bot α]
[locally_finite_order α]
{s : set α}
(hs : bdd_above s) :
s.finite
theorem
finset.image_add_left_Icc
{α : Type u_1}
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[decidable_eq α]
[locally_finite_order α]
(a b c : α) :
finset.image (has_add.add c) (finset.Icc a b) = finset.Icc (c + a) (c + b)
theorem
finset.image_add_left_Ico
{α : Type u_1}
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[decidable_eq α]
[locally_finite_order α]
(a b c : α) :
finset.image (has_add.add c) (finset.Ico a b) = finset.Ico (c + a) (c + b)
theorem
finset.image_add_left_Ioc
{α : Type u_1}
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[decidable_eq α]
[locally_finite_order α]
(a b c : α) :
finset.image (has_add.add c) (finset.Ioc a b) = finset.Ioc (c + a) (c + b)
theorem
finset.image_add_left_Ioo
{α : Type u_1}
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[decidable_eq α]
[locally_finite_order α]
(a b c : α) :
finset.image (has_add.add c) (finset.Ioo a b) = finset.Ioo (c + a) (c + b)
theorem
finset.image_add_right_Icc
{α : Type u_1}
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[decidable_eq α]
[locally_finite_order α]
(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_1}
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[decidable_eq α]
[locally_finite_order α]
(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_1}
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[decidable_eq α]
[locally_finite_order α]
(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_1}
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[decidable_eq α]
[locally_finite_order α]
(a b c : α) :
finset.image (λ (x : α), x + c) (finset.Ioo a b) = finset.Ioo (a + c) (b + c)