# mathlib3documentation

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 α] {a b : α} :
b).nodup
theorem multiset.nodup_Ico {α : Type u_1} [preorder α] {a b : α} :
b).nodup
theorem multiset.nodup_Ioc {α : Type u_1} [preorder α] {a b : α} :
b).nodup
theorem multiset.nodup_Ioo {α : Type u_1} [preorder α] {a b : α} :
b).nodup
@[simp]
theorem multiset.Icc_eq_zero_iff {α : Type u_1} [preorder α] {a b : α} :
b = 0 ¬a b
@[simp]
theorem multiset.Ico_eq_zero_iff {α : Type u_1} [preorder α] {a b : α} :
b = 0 ¬a < b
@[simp]
theorem multiset.Ioc_eq_zero_iff {α : Type u_1} [preorder α] {a b : α} :
b = 0 ¬a < b
@[simp]
theorem multiset.Ioo_eq_zero_iff {α : Type u_1} [preorder α] {a b : α}  :
b = 0 ¬a < b
theorem multiset.Icc_eq_zero {α : Type u_1} [preorder α] {a b : α} :
¬a b b = 0

Alias of the reverse direction of multiset.Icc_eq_zero_iff.

theorem multiset.Ico_eq_zero {α : Type u_1} [preorder α] {a b : α} :
¬a < b b = 0

Alias of the reverse direction of multiset.Ico_eq_zero_iff.

theorem multiset.Ioc_eq_zero {α : Type u_1} [preorder α] {a b : α} :
¬a < b b = 0

Alias of the reverse direction of multiset.Ioc_eq_zero_iff.

@[simp]
theorem multiset.Ioo_eq_zero {α : Type u_1} [preorder α] {a b : α} (h : ¬a < b) :
b = 0
@[simp]
theorem multiset.Icc_eq_zero_of_lt {α : Type u_1} [preorder α] {a b : α} (h : b < a) :
b = 0
@[simp]
theorem multiset.Ico_eq_zero_of_le {α : Type u_1} [preorder α] {a b : α} (h : b a) :
b = 0
@[simp]
theorem multiset.Ioc_eq_zero_of_le {α : Type u_1} [preorder α] {a b : α} (h : b a) :
b = 0
@[simp]
theorem multiset.Ioo_eq_zero_of_le {α : Type u_1} [preorder α] {a b : α} (h : b a) :
b = 0
@[simp]
theorem multiset.Ico_self {α : Type u_1} [preorder α] (a : α) :
a = 0
@[simp]
theorem multiset.Ioc_self {α : Type u_1} [preorder α] (a : α) :
a = 0
@[simp]
theorem multiset.Ioo_self {α : Type u_1} [preorder α] (a : α) :
a = 0
theorem multiset.left_mem_Icc {α : Type u_1} [preorder α] {a b : α} :
a b a b
theorem multiset.left_mem_Ico {α : Type u_1} [preorder α] {a b : α} :
a b a < b
theorem multiset.right_mem_Icc {α : Type u_1} [preorder α] {a b : α} :
b b a b
theorem multiset.right_mem_Ioc {α : Type u_1} [preorder α] {a b : α} :
b b a < b
@[simp]
theorem multiset.left_not_mem_Ioc {α : Type u_1} [preorder α] {a b : α} :
a b
@[simp]
theorem multiset.left_not_mem_Ioo {α : Type u_1} [preorder α] {a b : α} :
a b
@[simp]
theorem multiset.right_not_mem_Ico {α : Type u_1} [preorder α] {a b : α} :
b b
@[simp]
theorem multiset.right_not_mem_Ioo {α : Type u_1} [preorder α] {a b : α} :
b b
theorem multiset.Ico_filter_lt_of_le_left {α : Type u_1} [preorder α] {a b c : α} [decidable_pred (λ (_x : α), _x < c)] (hca : c a) :
multiset.filter (λ (x : α), x < c) b) =
theorem multiset.Ico_filter_lt_of_right_le {α : Type u_1} [preorder α] {a b c : α} [decidable_pred (λ (_x : α), _x < c)] (hbc : b c) :
multiset.filter (λ (x : α), x < c) b) = b
theorem multiset.Ico_filter_lt_of_le_right {α : Type u_1} [preorder α] {a b c : α} [decidable_pred (λ (_x : α), _x < c)] (hcb : c b) :
multiset.filter (λ (x : α), x < c) b) = c
theorem multiset.Ico_filter_le_of_le_left {α : Type u_1} [preorder α] {a b c : α} [decidable_pred (has_le.le c)] (hca : c a) :
multiset.filter (λ (x : α), c x) b) = b
theorem multiset.Ico_filter_le_of_right_le {α : Type u_1} [preorder α] {a b : α} [decidable_pred (has_le.le b)] :
multiset.filter (λ (x : α), b x) b) =
theorem multiset.Ico_filter_le_of_left_le {α : Type u_1} [preorder α] {a b c : α} [decidable_pred (has_le.le c)] (hac : a c) :
multiset.filter (λ (x : α), c x) b) = b
@[simp]
theorem multiset.Icc_self {α : Type u_1} (a : α) :
a = {a}
theorem multiset.Ico_cons_right {α : Type u_1} {a b : α} (h : a b) :
b ::ₘ b = b
theorem multiset.Ioo_cons_left {α : Type u_1} {a b : α} (h : a < b) :
a ::ₘ b = b
theorem multiset.Ico_disjoint_Ico {α : Type u_1} {a b c d : α} (h : b c) :
b).disjoint d)
@[simp]
theorem multiset.Ico_inter_Ico_of_le {α : Type u_1} [decidable_eq α] {a b c d : α} (h : b c) :
b d = 0
theorem multiset.Ico_filter_le_left {α : Type u_1} {a b : α} [decidable_pred (λ (_x : α), _x a)] (hab : a < b) :
multiset.filter (λ (x : α), x a) b) = {a}
theorem multiset.card_Ico_eq_card_Icc_sub_one {α : Type u_1} (a b : α) :
= - 1
theorem multiset.card_Ioc_eq_card_Icc_sub_one {α : Type u_1} (a b : α) :
= - 1
theorem multiset.card_Ioo_eq_card_Ico_sub_one {α : Type u_1} (a b : α) :
= - 1
theorem multiset.card_Ioo_eq_card_Icc_sub_two {α : Type u_1} (a b : α) :
= - 2
theorem multiset.Ico_subset_Ico_iff {α : Type u_1} [linear_order α] {a₁ b₁ a₂ b₂ : α} (h : a₁ < b₁) :
b₁ b₂ a₂ a₁ b₁ b₂
theorem multiset.Ico_add_Ico_eq_Ico {α : Type u_1} [linear_order α] {a b c : α} (hab : a b) (hbc : b c) :
b + c = c
theorem multiset.Ico_inter_Ico {α : Type u_1} [linear_order α] {a b c d : α} :
b d = d)
@[simp]
theorem multiset.Ico_filter_lt {α : Type u_1} [linear_order α] (a b c : α) :
multiset.filter (λ (x : α), x < c) b) = c)
@[simp]
theorem multiset.Ico_filter_le {α : Type u_1} [linear_order α] (a b c : α) :
multiset.filter (λ (x : α), c x) b) = b
@[simp]
theorem multiset.Ico_sub_Ico_left {α : Type u_1} [linear_order α] (a b c : α) :
b - c = b
@[simp]
theorem multiset.Ico_sub_Ico_right {α : Type u_1} [linear_order α] (a b c : α) :
b - b = c)
theorem multiset.map_add_left_Icc {α : Type u_1} (a b c : α) :
b) = multiset.Icc (c + a) (c + b)
theorem multiset.map_add_left_Ico {α : Type u_1} (a b c : α) :
b) = multiset.Ico (c + a) (c + b)
theorem multiset.map_add_left_Ioc {α : Type u_1} (a b c : α) :
b) = multiset.Ioc (c + a) (c + b)
theorem multiset.map_add_left_Ioo {α : Type u_1} (a b c : α) :
b) = multiset.Ioo (c + a) (c + b)
theorem multiset.map_add_right_Icc {α : Type u_1} (a b c : α) :
multiset.map (λ (x : α), x + c) b) = multiset.Icc (a + c) (b + c)
theorem multiset.map_add_right_Ico {α : Type u_1} (a b c : α) :
multiset.map (λ (x : α), x + c) b) = multiset.Ico (a + c) (b + c)
theorem multiset.map_add_right_Ioc {α : Type u_1} (a b c : α) :
multiset.map (λ (x : α), x + c) b) = multiset.Ioc (a + c) (b + c)
theorem multiset.map_add_right_Ioo {α : Type u_1} (a b c : α) :
multiset.map (λ (x : α), x + c) b) = multiset.Ioo (a + c) (b + c)