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 : α} : Multiset.Nodup (Multiset.Icc a b)

theorem Multiset.nodup_Ico {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} : Multiset.Nodup (Multiset.Ico a b)

theorem Multiset.nodup_Ioc {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} : Multiset.Nodup (Multiset.Ioc a b)

theorem Multiset.nodup_Ioo {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} : Multiset.Nodup (Multiset.Ioo a b)

@[simp]

theorem Multiset.Icc_eq_zero_iff {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} : Multiset.Icc a b = 0 ↔ ¬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 ≤ 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 α] [LocallyFiniteOrder α] {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 α] [LocallyFiniteOrder α] {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 α] [LocallyFiniteOrder α] {a : α} {b : α} (h : ¬a < b) : Multiset.Ioo a b = 0

@[simp]

theorem Multiset.Icc_eq_zero_of_lt {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} (h : b < a) : Multiset.Icc a b = 0

@[simp]

theorem Multiset.Ico_eq_zero_of_le {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} (h : b ≤ a) : Multiset.Ico a b = 0

@[simp]

theorem Multiset.Ioc_eq_zero_of_le {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} (h : b ≤ a) : Multiset.Ioc a b = 0

@[simp]

theorem Multiset.Ioo_eq_zero_of_le {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} (h : b ≤ a) : Multiset.Ioo a b = 0

theorem Multiset.Ico_self {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a : α) : Multiset.Ico a a = 0

theorem Multiset.Ioc_self {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a : α) : Multiset.Ioc a a = 0

theorem Multiset.Ioo_self {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a : α) : Multiset.Ioo a a = 0

theorem Multiset.left_mem_Icc {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} : a ∈ Multiset.Icc a b ↔ 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 : α} : b ∈ Multiset.Icc a b ↔ 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 : α} : a ∉ Multiset.Ioc a b

theorem Multiset.left_not_mem_Ioo {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} : a ∉ Multiset.Ioo a b

theorem Multiset.right_not_mem_Ico {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} : b ∉ Multiset.Ico a b

theorem Multiset.right_not_mem_Ioo {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} : b ∉ Multiset.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) : b ::ₘ Multiset.Ico a b = Multiset.Icc a b

theorem Multiset.Ioo_cons_left {α : Type u_1} [PartialOrder α] [LocallyFiniteOrder α] {a : α} {b : α} (h : a < b) : a ::ₘ Multiset.Ioo a b = Multiset.Ico a b

theorem Multiset.Ico_disjoint_Ico {α : Type u_1} [PartialOrder α] [LocallyFiniteOrder α] {a : α} {b : α} {c : α} {d : α} (h : b ≤ c) : Multiset.Disjoint (Multiset.Ico a b) (Multiset.Ico c d)

@[simp]

theorem Multiset.Ico_inter_Ico_of_le {α : Type u_1} [PartialOrder α] [LocallyFiniteOrder α] [DecidableEq α] {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} [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) : Multiset.Ico a b + Multiset.Ico b c = Multiset.Ico a c

theorem Multiset.Ico_inter_Ico {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] {a : α} {b : α} {c : α} {d : α} : Multiset.Ico a b ∩ Multiset.Ico c d = Multiset.Ico (max a c) (min b 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 : α) : Multiset.Ico a b - Multiset.Ico a c = Multiset.Ico (max a c) b

@[simp]

theorem Multiset.Ico_sub_Ico_right {α : Type u_1} [LinearOrder α] [LocallyFiniteOrder α] (a : α) (b : α) (c : α) : Multiset.Ico a b - Multiset.Ico c b = Multiset.Ico a (min 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)