Documentation

Mathlib.Data.Multiset.LocallyFinite

Intervals as multisets #

This file provides basic results about all the Multiset.Ixx, which are defined in Order.LocallyFinite.

Note that intervals of multisets themselves (Multiset.LocallyFiniteOrder) are defined elsewhere.

theorem Multiset.nodup_Icc {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} :
theorem Multiset.nodup_Ico {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} :
theorem Multiset.nodup_Ioc {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} :
theorem Multiset.nodup_Ioo {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} :
@[simp]
theorem Multiset.Icc_eq_zero_iff {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} :
@[simp]
theorem Multiset.Ico_eq_zero_iff {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} :
Multiset.Ico a b = 0 ¬a < b
@[simp]
theorem Multiset.Ioc_eq_zero_iff {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} :
Multiset.Ioc a b = 0 ¬a < b
@[simp]
theorem Multiset.Ioo_eq_zero_iff {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} [DenselyOrdered α] :
Multiset.Ioo a b = 0 ¬a < b
theorem Multiset.Icc_eq_zero {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} :
¬a bMultiset.Icc a b = 0

Alias of the reverse direction of Multiset.Icc_eq_zero_iff.

theorem Multiset.Ico_eq_zero {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} :
¬a < bMultiset.Ico a b = 0

Alias of the reverse direction of Multiset.Ico_eq_zero_iff.

theorem Multiset.Ioc_eq_zero {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} :
¬a < bMultiset.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 α] [LocallyFiniteOrder α] {a : α} {b : α} (h : ¬a < b) :
@[simp]
theorem Multiset.Icc_eq_zero_of_lt {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} (h : b < a) :
@[simp]
theorem Multiset.Ico_eq_zero_of_le {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} (h : b a) :
@[simp]
theorem Multiset.Ioc_eq_zero_of_le {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} (h : b a) :
@[simp]
theorem Multiset.Ioo_eq_zero_of_le {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} (h : b a) :
theorem Multiset.Ico_self {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a : α) :
theorem Multiset.Ioc_self {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a : α) :
theorem Multiset.Ioo_self {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a : α) :
theorem Multiset.left_mem_Icc {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} :
theorem Multiset.left_mem_Ico {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} :
a Multiset.Ico a b a < b
theorem Multiset.right_mem_Icc {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} :
theorem Multiset.right_mem_Ioc {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} :
b Multiset.Ioc a b a < b
theorem Multiset.left_not_mem_Ioc {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} :
aMultiset.Ioc a b
theorem Multiset.left_not_mem_Ioo {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} :
aMultiset.Ioo a b
theorem Multiset.right_not_mem_Ico {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} :
bMultiset.Ico a b
theorem Multiset.right_not_mem_Ioo {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} :
bMultiset.Ioo a b
theorem Multiset.Ico_filter_lt_of_le_left {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} {c : α} [DecidablePred fun (x : α) => x < c] (hca : c a) :
Multiset.filter (fun (x : α) => x < c) (Multiset.Ico a b) =
theorem Multiset.Ico_filter_lt_of_right_le {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} {c : α} [DecidablePred fun (x : α) => x < c] (hbc : b c) :
Multiset.filter (fun (x : α) => x < c) (Multiset.Ico a b) = Multiset.Ico a b
theorem Multiset.Ico_filter_lt_of_le_right {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} {c : α} [DecidablePred fun (x : α) => x < c] (hcb : c b) :
Multiset.filter (fun (x : α) => x < c) (Multiset.Ico a b) = Multiset.Ico a c
theorem Multiset.Ico_filter_le_of_le_left {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} {c : α} [DecidablePred fun (x : α) => c x] (hca : c a) :
Multiset.filter (fun (x : α) => c x) (Multiset.Ico a b) = Multiset.Ico a b
theorem Multiset.Ico_filter_le_of_right_le {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} [DecidablePred fun (x : α) => b x] :
Multiset.filter (fun (x : α) => b x) (Multiset.Ico a b) =
theorem Multiset.Ico_filter_le_of_left_le {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} {c : α} [DecidablePred fun (x : α) => c x] (hac : a c) :
Multiset.filter (fun (x : α) => c x) (Multiset.Ico a b) = Multiset.Ico c b
@[simp]
theorem Multiset.Icc_self {α : Type u_1} [PartialOrder α] [LocallyFiniteOrder α] (a : α) :
Multiset.Icc a a = {a}
theorem Multiset.Ico_cons_right {α : Type u_1} [PartialOrder α] [LocallyFiniteOrder α] {a : α} {b : α} (h : a b) :
theorem Multiset.Ioo_cons_left {α : Type u_1} [PartialOrder α] [LocallyFiniteOrder α] {a : α} {b : α} (h : a < b) :
theorem Multiset.Ico_disjoint_Ico {α : Type u_1} [PartialOrder α] [LocallyFiniteOrder α] {a : α} {b : α} {c : α} {d : α} (h : b c) :
@[simp]
theorem Multiset.Ico_inter_Ico_of_le {α : Type u_1} [PartialOrder α] [LocallyFiniteOrder α] [DecidableEq α] {a : α} {b : α} {c : α} {d : α} (h : b c) :
theorem Multiset.Ico_filter_le_left {α : Type u_1} [PartialOrder α] [LocallyFiniteOrder α] {a : α} {b : α} [DecidablePred fun (x : α) => x a] (hab : a < b) :
Multiset.filter (fun (x : α) => x a) (Multiset.Ico a b) = {a}
theorem Multiset.card_Ico_eq_card_Icc_sub_one {α : Type u_1} [PartialOrder α] [LocallyFiniteOrder α] (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} [PartialOrder α] [LocallyFiniteOrder α] (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} [PartialOrder α] [LocallyFiniteOrder α] (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} [PartialOrder α] [LocallyFiniteOrder α] (a : α) (b : α) :
Multiset.card (Multiset.Ioo a b) = Multiset.card (Multiset.Icc a b) - 2
theorem Multiset.Ico_subset_Ico_iff {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] {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} [LinearOrder α] [LocallyFiniteOrder α] {a : α} {b : α} {c : α} (hab : a b) (hbc : b c) :
theorem Multiset.Ico_inter_Ico {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] {a : α} {b : α} {c : α} {d : α} :
@[simp]
theorem Multiset.Ico_filter_lt {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] (a : α) (b : α) (c : α) :
Multiset.filter (fun (x : α) => x < c) (Multiset.Ico a b) = Multiset.Ico a (min b c)
@[simp]
theorem Multiset.Ico_filter_le {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] (a : α) (b : α) (c : α) :
Multiset.filter (fun (x : α) => c x) (Multiset.Ico a b) = Multiset.Ico (max a c) b
@[simp]
theorem Multiset.Ico_sub_Ico_left {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] (a : α) (b : α) (c : α) :
@[simp]
theorem Multiset.Ico_sub_Ico_right {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] (a : α) (b : α) (c : α) :
theorem Multiset.map_add_left_Icc {α : Type u_1} [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a : α) (b : α) (c : α) :
Multiset.map (fun (x : α) => c + x) (Multiset.Icc a b) = Multiset.Icc (c + a) (c + b)
theorem Multiset.map_add_left_Ico {α : Type u_1} [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a : α) (b : α) (c : α) :
Multiset.map (fun (x : α) => c + x) (Multiset.Ico a b) = Multiset.Ico (c + a) (c + b)
theorem Multiset.map_add_left_Ioc {α : Type u_1} [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a : α) (b : α) (c : α) :
Multiset.map (fun (x : α) => c + x) (Multiset.Ioc a b) = Multiset.Ioc (c + a) (c + b)
theorem Multiset.map_add_left_Ioo {α : Type u_1} [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a : α) (b : α) (c : α) :
Multiset.map (fun (x : α) => c + x) (Multiset.Ioo a b) = Multiset.Ioo (c + a) (c + b)
theorem Multiset.map_add_right_Icc {α : Type u_1} [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a : α) (b : α) (c : α) :
Multiset.map (fun (x : α) => x + c) (Multiset.Icc a b) = Multiset.Icc (a + c) (b + c)
theorem Multiset.map_add_right_Ico {α : Type u_1} [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a : α) (b : α) (c : α) :
Multiset.map (fun (x : α) => x + c) (Multiset.Ico a b) = Multiset.Ico (a + c) (b + c)
theorem Multiset.map_add_right_Ioc {α : Type u_1} [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a : α) (b : α) (c : α) :
Multiset.map (fun (x : α) => x + c) (Multiset.Ioc a b) = Multiset.Ioc (a + c) (b + c)
theorem Multiset.map_add_right_Ioo {α : Type u_1} [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a : α) (b : α) (c : α) :
Multiset.map (fun (x : α) => x + c) (Multiset.Ioo a b) = Multiset.Ioo (a + c) (b + c)