mathlib3 documentation

data.multiset.locally_finite

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 : α} :
theorem multiset.nodup_Ico {α : Type u_1} [preorder α] [locally_finite_order α] {a b : α} :
theorem multiset.nodup_Ioc {α : Type u_1} [preorder α] [locally_finite_order α] {a b : α} :
theorem multiset.nodup_Ioo {α : Type u_1} [preorder α] [locally_finite_order α] {a b : α} :
@[simp]
theorem multiset.Icc_eq_zero_iff {α : Type u_1} [preorder α] [locally_finite_order α] {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 : α} :

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) :
@[simp]
theorem multiset.Icc_eq_zero_of_lt {α : Type u_1} [preorder α] [locally_finite_order α] {a b : α} (h : b < a) :
@[simp]
theorem multiset.Ico_eq_zero_of_le {α : Type u_1} [preorder α] [locally_finite_order α] {a b : α} (h : b a) :
@[simp]
theorem multiset.Ioc_eq_zero_of_le {α : Type u_1} [preorder α] [locally_finite_order α] {a b : α} (h : b a) :
@[simp]
theorem multiset.Ioo_eq_zero_of_le {α : Type u_1} [preorder α] [locally_finite_order α] {a b : α} (h : b a) :
@[simp]
theorem multiset.Ico_self {α : Type u_1} [preorder α] [locally_finite_order α] (a : α) :
@[simp]
theorem multiset.Ioc_self {α : Type u_1} [preorder α] [locally_finite_order α] (a : α) :
@[simp]
theorem multiset.Ioo_self {α : Type u_1} [preorder α] [locally_finite_order α] (a : α) :
theorem multiset.left_mem_Icc {α : Type u_1} [preorder α] [locally_finite_order α] {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 : α} :
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 : α} :
@[simp]
theorem multiset.left_not_mem_Ioo {α : Type u_1} [preorder α] [locally_finite_order α] {a b : α} :
@[simp]
theorem multiset.right_not_mem_Ico {α : Type u_1} [preorder α] [locally_finite_order α] {a b : α} :
@[simp]
theorem multiset.right_not_mem_Ioo {α : Type u_1} [preorder α] [locally_finite_order α] {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) :
theorem multiset.Ioo_cons_left {α : Type u_1} [partial_order α] [locally_finite_order α] {a b : α} (h : a < b) :
theorem multiset.Ico_disjoint_Ico {α : Type u_1} [partial_order α] [locally_finite_order α] {a b c d : α} (h : b c) :
@[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) :
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.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) :
@[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 : α) :
@[simp]
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)