Intervals as multisets

This file defines intervals as multisets.

Main declarations

In a LocallyFiniteOrder,

• Multiset.Icc: Closed-closed interval as a multiset.
• Multiset.Ico: Closed-open interval as a multiset.
• Multiset.Ioc: Open-closed interval as a multiset.
• Multiset.Ioo: Open-open interval as a multiset.

In a LocallyFiniteOrderTop,

• Multiset.Ici: Closed-infinite interval as a multiset.
• Multiset.Ioi: Open-infinite interval as a multiset.

In a LocallyFiniteOrderBot,

• Multiset.Iic: Infinite-open interval as a multiset.
• Multiset.Iio: Infinite-closed interval as a multiset.

TODO

Do we really need this file at all? (March 2024)

def Multiset.Icc {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a : α) (b : α) : Multiset α

The multiset of elements x such that a ≤ x and x ≤ b. Basically Set.Icc a b as a multiset.

Equations

• Multiset.Icc a b = (Finset.Icc a b).val

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

The multiset of elements x such that a ≤ x and x < b. Basically Set.Ico a b as a multiset.

Equations

• Multiset.Ico a b = (Finset.Ico a b).val

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

The multiset of elements x such that a < x and x ≤ b. Basically Set.Ioc a b as a multiset.

Equations

• Multiset.Ioc a b = (Finset.Ioc a b).val

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

The multiset of elements x such that a < x and x < b. Basically Set.Ioo a b as a multiset.

Equations

• Multiset.Ioo a b = (Finset.Ioo a b).val

@[simp]

theorem Multiset.mem_Icc {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} {x : α} : x ∈ Multiset.Icc a b ↔ a ≤ x ∧ x ≤ b

@[simp]

theorem Multiset.mem_Ico {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} {x : α} : x ∈ Multiset.Ico a b ↔ a ≤ x ∧ x < b

@[simp]

theorem Multiset.mem_Ioc {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} {x : α} : x ∈ Multiset.Ioc a b ↔ a < x ∧ x ≤ b

@[simp]

theorem Multiset.mem_Ioo {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a : α} {b : α} {x : α} : x ∈ Multiset.Ioo a b ↔ a < x ∧ x < b

def Multiset.Ici {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] (a : α) : Multiset α

The multiset of elements x such that a ≤ x. Basically Set.Ici a as a multiset.

Equations

• Multiset.Ici a = (Finset.Ici a).val

def Multiset.Ioi {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] (a : α) : Multiset α

The multiset of elements x such that a < x. Basically Set.Ioi a as a multiset.

Equations

• Multiset.Ioi a = (Finset.Ioi a).val

@[simp]

theorem Multiset.mem_Ici {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] {a : α} {x : α} : x ∈ Multiset.Ici a ↔ a ≤ x

@[simp]

theorem Multiset.mem_Ioi {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] {a : α} {x : α} : x ∈ Multiset.Ioi a ↔ a < x

def Multiset.Iic {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] (b : α) : Multiset α

The multiset of elements x such that x ≤ b. Basically Set.Iic b as a multiset.

Equations

• Multiset.Iic b = (Finset.Iic b).val

def Multiset.Iio {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] (b : α) : Multiset α

The multiset of elements x such that x < b. Basically Set.Iio b as a multiset.

Equations

• Multiset.Iio b = (Finset.Iio b).val

@[simp]

theorem Multiset.mem_Iic {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] {b : α} {x : α} : x ∈ Multiset.Iic b ↔ x ≤ b

@[simp]

theorem Multiset.mem_Iio {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] {b : α} {x : α} : x ∈ Multiset.Iio b ↔ x < b

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

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

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

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

@[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) : 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 (a ⊔ c) (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 (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 (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 (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 (b ⊓ c)