Intervals as multisets #
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 multiset.Ixx, which are defined in
order.locally_finite.
Note that intervals of multisets themselves (multiset.locally_finite_order) are defined elsewhere.
theorem
multiset.nodup_Icc
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α} :
(multiset.Icc a b).nodup
theorem
multiset.nodup_Ico
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α} :
(multiset.Ico a b).nodup
theorem
multiset.nodup_Ioc
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α} :
(multiset.Ioc a b).nodup
theorem
multiset.nodup_Ioo
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α} :
(multiset.Ioo a b).nodup
@[simp]
theorem
multiset.Icc_eq_zero_iff
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α} :
multiset.Icc a b = 0 ↔ ¬a ≤ b
@[simp]
theorem
multiset.Ico_eq_zero_iff
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α} :
multiset.Ico a b = 0 ↔ ¬a < b
@[simp]
theorem
multiset.Ioc_eq_zero_iff
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α} :
multiset.Ioc a b = 0 ↔ ¬a < b
@[simp]
theorem
multiset.Ioo_eq_zero_iff
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α}
[densely_ordered α] :
multiset.Ioo a b = 0 ↔ ¬a < b
theorem
multiset.Icc_eq_zero
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α} :
¬a ≤ b → multiset.Icc a b = 0
Alias of the reverse direction of multiset.Icc_eq_zero_iff.
theorem
multiset.Ico_eq_zero
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α} :
¬a < b → multiset.Ico a b = 0
Alias of the reverse direction of multiset.Ico_eq_zero_iff.
theorem
multiset.Ioc_eq_zero
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α} :
¬a < b → multiset.Ioc a b = 0
Alias of the reverse direction of multiset.Ioc_eq_zero_iff.
@[simp]
theorem
multiset.Ioo_eq_zero
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α}
(h : ¬a < b) :
multiset.Ioo a b = 0
@[simp]
theorem
multiset.Icc_eq_zero_of_lt
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α}
(h : b < a) :
multiset.Icc a b = 0
@[simp]
theorem
multiset.Ico_eq_zero_of_le
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α}
(h : b ≤ a) :
multiset.Ico a b = 0
@[simp]
theorem
multiset.Ioc_eq_zero_of_le
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α}
(h : b ≤ a) :
multiset.Ioc a b = 0
@[simp]
theorem
multiset.Ioo_eq_zero_of_le
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α}
(h : b ≤ a) :
multiset.Ioo a b = 0
@[simp]
theorem
multiset.Ico_self
{α : Type u_1}
[preorder α]
[locally_finite_order α]
(a : α) :
multiset.Ico a a = 0
@[simp]
theorem
multiset.Ioc_self
{α : Type u_1}
[preorder α]
[locally_finite_order α]
(a : α) :
multiset.Ioc a a = 0
@[simp]
theorem
multiset.Ioo_self
{α : Type u_1}
[preorder α]
[locally_finite_order α]
(a : α) :
multiset.Ioo a a = 0
theorem
multiset.left_mem_Icc
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α} :
a ∈ multiset.Icc a b ↔ a ≤ b
theorem
multiset.left_mem_Ico
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α} :
a ∈ multiset.Ico a b ↔ a < b
theorem
multiset.right_mem_Icc
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α} :
b ∈ multiset.Icc a b ↔ a ≤ b
theorem
multiset.right_mem_Ioc
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α} :
b ∈ multiset.Ioc a b ↔ a < b
@[simp]
theorem
multiset.left_not_mem_Ioc
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α} :
a ∉ multiset.Ioc a b
@[simp]
theorem
multiset.left_not_mem_Ioo
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α} :
a ∉ multiset.Ioo a b
@[simp]
theorem
multiset.right_not_mem_Ico
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α} :
b ∉ multiset.Ico a b
@[simp]
theorem
multiset.right_not_mem_Ioo
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α} :
b ∉ multiset.Ioo a b
theorem
multiset.Ico_filter_lt_of_le_left
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b c : α}
[decidable_pred (λ (_x : α), _x < c)]
(hca : c ≤ a) :
multiset.filter (λ (x : α), x < c) (multiset.Ico a b) = ∅
theorem
multiset.Ico_filter_lt_of_right_le
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b c : α}
[decidable_pred (λ (_x : α), _x < c)]
(hbc : b ≤ c) :
multiset.filter (λ (x : α), x < c) (multiset.Ico a b) = multiset.Ico a b
theorem
multiset.Ico_filter_lt_of_le_right
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b c : α}
[decidable_pred (λ (_x : α), _x < c)]
(hcb : c ≤ b) :
multiset.filter (λ (x : α), x < c) (multiset.Ico a b) = multiset.Ico a c
theorem
multiset.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) :
multiset.filter (λ (x : α), c ≤ x) (multiset.Ico a b) = multiset.Ico a b
theorem
multiset.Ico_filter_le_of_right_le
{α : Type u_1}
[preorder α]
[locally_finite_order α]
{a b : α}
[decidable_pred (has_le.le b)] :
multiset.filter (λ (x : α), b ≤ x) (multiset.Ico a b) = ∅
theorem
multiset.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) :
multiset.filter (λ (x : α), c ≤ x) (multiset.Ico a b) = multiset.Ico c b
@[simp]
theorem
multiset.Icc_self
{α : Type u_1}
[partial_order α]
[locally_finite_order α]
(a : α) :
multiset.Icc a a = {a}
theorem
multiset.Ico_cons_right
{α : Type u_1}
[partial_order α]
[locally_finite_order α]
{a b : α}
(h : a ≤ b) :
b ::ₘ multiset.Ico a b = multiset.Icc a b
theorem
multiset.Ioo_cons_left
{α : Type u_1}
[partial_order α]
[locally_finite_order α]
{a b : α}
(h : a < b) :
a ::ₘ multiset.Ioo a b = multiset.Ico a b
theorem
multiset.Ico_disjoint_Ico
{α : Type u_1}
[partial_order α]
[locally_finite_order α]
{a b c d : α}
(h : b ≤ c) :
(multiset.Ico a b).disjoint (multiset.Ico c d)
@[simp]
theorem
multiset.Ico_inter_Ico_of_le
{α : Type u_1}
[partial_order α]
[locally_finite_order α]
[decidable_eq α]
{a b c d : α}
(h : b ≤ c) :
multiset.Ico a b ∩ multiset.Ico c d = 0
theorem
multiset.Ico_filter_le_left
{α : Type u_1}
[partial_order α]
[locally_finite_order α]
{a b : α}
[decidable_pred (λ (_x : α), _x ≤ a)]
(hab : a < b) :
multiset.filter (λ (x : α), x ≤ a) (multiset.Ico a b) = {a}
theorem
multiset.card_Ico_eq_card_Icc_sub_one
{α : Type u_1}
[partial_order α]
[locally_finite_order α]
(a b : α) :
⇑multiset.card (multiset.Ico a b) = ⇑multiset.card (multiset.Icc a b) - 1
theorem
multiset.card_Ioc_eq_card_Icc_sub_one
{α : Type u_1}
[partial_order α]
[locally_finite_order α]
(a b : α) :
⇑multiset.card (multiset.Ioc a b) = ⇑multiset.card (multiset.Icc a b) - 1
theorem
multiset.card_Ioo_eq_card_Ico_sub_one
{α : Type u_1}
[partial_order α]
[locally_finite_order α]
(a b : α) :
⇑multiset.card (multiset.Ioo a b) = ⇑multiset.card (multiset.Ico a b) - 1
theorem
multiset.card_Ioo_eq_card_Icc_sub_two
{α : Type u_1}
[partial_order α]
[locally_finite_order α]
(a b : α) :
⇑multiset.card (multiset.Ioo a b) = ⇑multiset.card (multiset.Icc a b) - 2
theorem
multiset.Ico_subset_Ico_iff
{α : Type u_1}
[linear_order α]
[locally_finite_order α]
{a₁ b₁ a₂ b₂ : α}
(h : a₁ < b₁) :
multiset.Ico a₁ b₁ ⊆ multiset.Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
theorem
multiset.Ico_add_Ico_eq_Ico
{α : Type u_1}
[linear_order α]
[locally_finite_order α]
{a b c : α}
(hab : a ≤ b)
(hbc : b ≤ c) :
multiset.Ico a b + multiset.Ico b c = multiset.Ico a c
theorem
multiset.Ico_inter_Ico
{α : Type u_1}
[linear_order α]
[locally_finite_order α]
{a b c d : α} :
multiset.Ico a b ∩ multiset.Ico c d = multiset.Ico (linear_order.max a c) (linear_order.min b d)
@[simp]
theorem
multiset.Ico_filter_lt
{α : Type u_1}
[linear_order α]
[locally_finite_order α]
(a b c : α) :
multiset.filter (λ (x : α), x < c) (multiset.Ico a b) = multiset.Ico a (linear_order.min b c)
@[simp]
theorem
multiset.Ico_filter_le
{α : Type u_1}
[linear_order α]
[locally_finite_order α]
(a b c : α) :
multiset.filter (λ (x : α), c ≤ x) (multiset.Ico a b) = multiset.Ico (linear_order.max a c) b
@[simp]
theorem
multiset.Ico_sub_Ico_left
{α : Type u_1}
[linear_order α]
[locally_finite_order α]
(a b c : α) :
multiset.Ico a b - multiset.Ico a c = multiset.Ico (linear_order.max a c) b
@[simp]
theorem
multiset.Ico_sub_Ico_right
{α : Type u_1}
[linear_order α]
[locally_finite_order α]
(a b c : α) :
multiset.Ico a b - multiset.Ico c b = multiset.Ico a (linear_order.min b c)
theorem
multiset.map_add_left_Icc
{α : Type u_1}
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[locally_finite_order α]
(a b c : α) :
multiset.map (has_add.add c) (multiset.Icc a b) = multiset.Icc (c + a) (c + b)
theorem
multiset.map_add_left_Ico
{α : Type u_1}
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[locally_finite_order α]
(a b c : α) :
multiset.map (has_add.add c) (multiset.Ico a b) = multiset.Ico (c + a) (c + b)
theorem
multiset.map_add_left_Ioc
{α : Type u_1}
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[locally_finite_order α]
(a b c : α) :
multiset.map (has_add.add c) (multiset.Ioc a b) = multiset.Ioc (c + a) (c + b)
theorem
multiset.map_add_left_Ioo
{α : Type u_1}
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[locally_finite_order α]
(a b c : α) :
multiset.map (has_add.add c) (multiset.Ioo a b) = multiset.Ioo (c + a) (c + b)
theorem
multiset.map_add_right_Icc
{α : Type u_1}
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[locally_finite_order α]
(a b c : α) :
multiset.map (λ (x : α), x + c) (multiset.Icc a b) = multiset.Icc (a + c) (b + c)
theorem
multiset.map_add_right_Ico
{α : Type u_1}
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[locally_finite_order α]
(a b c : α) :
multiset.map (λ (x : α), x + c) (multiset.Ico a b) = multiset.Ico (a + c) (b + c)
theorem
multiset.map_add_right_Ioc
{α : Type u_1}
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[locally_finite_order α]
(a b c : α) :
multiset.map (λ (x : α), x + c) (multiset.Ioc a b) = multiset.Ioc (a + c) (b + c)
theorem
multiset.map_add_right_Ioo
{α : Type u_1}
[ordered_cancel_add_comm_monoid α]
[has_exists_add_of_le α]
[locally_finite_order α]
(a b c : α) :
multiset.map (λ (x : α), x + c) (multiset.Ioo a b) = multiset.Ioo (a + c) (b + c)