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} [] (a : α) (b : α) :

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

Equations
• = ().val
Instances For
def Multiset.Ico {α : Type u_1} [] (a : α) (b : α) :

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

Equations
• = ().val
Instances For
def Multiset.Ioc {α : Type u_1} [] (a : α) (b : α) :

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

Equations
• = ().val
Instances For
def Multiset.Ioo {α : Type u_1} [] (a : α) (b : α) :

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

Equations
• = ().val
Instances For
@[simp]
theorem Multiset.mem_Icc {α : Type u_1} [] {a : α} {b : α} {x : α} :
x a x x b
@[simp]
theorem Multiset.mem_Ico {α : Type u_1} [] {a : α} {b : α} {x : α} :
x a x x < b
@[simp]
theorem Multiset.mem_Ioc {α : Type u_1} [] {a : α} {b : α} {x : α} :
x a < x x b
@[simp]
theorem Multiset.mem_Ioo {α : Type u_1} [] {a : α} {b : α} {x : α} :
x a < x x < b
def Multiset.Ici {α : Type u_1} [] (a : α) :

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

Equations
• = ().val
Instances For
def Multiset.Ioi {α : Type u_1} [] (a : α) :

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

Equations
• = ().val
Instances For
@[simp]
theorem Multiset.mem_Ici {α : Type u_1} [] {a : α} {x : α} :
a x
@[simp]
theorem Multiset.mem_Ioi {α : Type u_1} [] {a : α} {x : α} :
a < x
def Multiset.Iic {α : Type u_1} [] (b : α) :

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

Equations
• = ().val
Instances For
def Multiset.Iio {α : Type u_1} [] (b : α) :

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

Equations
• = ().val
Instances For
@[simp]
theorem Multiset.mem_Iic {α : Type u_1} [] {b : α} {x : α} :
x b
@[simp]
theorem Multiset.mem_Iio {α : Type u_1} [] {b : α} {x : α} :
x < b
theorem Multiset.nodup_Icc {α : Type u_1} [] {a : α} {b : α} :
().Nodup
theorem Multiset.nodup_Ico {α : Type u_1} [] {a : α} {b : α} :
().Nodup
theorem Multiset.nodup_Ioc {α : Type u_1} [] {a : α} {b : α} :
().Nodup
theorem Multiset.nodup_Ioo {α : Type u_1} [] {a : α} {b : α} :
().Nodup
@[simp]
theorem Multiset.Icc_eq_zero_iff {α : Type u_1} [] {a : α} {b : α} :
= 0 ¬a b
@[simp]
theorem Multiset.Ico_eq_zero_iff {α : Type u_1} [] {a : α} {b : α} :
= 0 ¬a < b
@[simp]
theorem Multiset.Ioc_eq_zero_iff {α : Type u_1} [] {a : α} {b : α} :
= 0 ¬a < b
@[simp]
theorem Multiset.Ioo_eq_zero_iff {α : Type u_1} [] {a : α} {b : α} [] :
= 0 ¬a < b
theorem Multiset.Icc_eq_zero {α : Type u_1} [] {a : α} {b : α} :
¬a b = 0

Alias of the reverse direction of Multiset.Icc_eq_zero_iff.

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

Alias of the reverse direction of Multiset.Ico_eq_zero_iff.

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

Alias of the reverse direction of Multiset.Ioc_eq_zero_iff.

@[simp]
theorem Multiset.Ioo_eq_zero {α : Type u_1} [] {a : α} {b : α} (h : ¬a < b) :
= 0
@[simp]
theorem Multiset.Icc_eq_zero_of_lt {α : Type u_1} [] {a : α} {b : α} (h : b < a) :
= 0
@[simp]
theorem Multiset.Ico_eq_zero_of_le {α : Type u_1} [] {a : α} {b : α} (h : b a) :
= 0
@[simp]
theorem Multiset.Ioc_eq_zero_of_le {α : Type u_1} [] {a : α} {b : α} (h : b a) :
= 0
@[simp]
theorem Multiset.Ioo_eq_zero_of_le {α : Type u_1} [] {a : α} {b : α} (h : b a) :
= 0
theorem Multiset.Ico_self {α : Type u_1} [] (a : α) :
= 0
theorem Multiset.Ioc_self {α : Type u_1} [] (a : α) :
= 0
theorem Multiset.Ioo_self {α : Type u_1} [] (a : α) :
= 0
theorem Multiset.left_mem_Icc {α : Type u_1} [] {a : α} {b : α} :
a a b
theorem Multiset.left_mem_Ico {α : Type u_1} [] {a : α} {b : α} :
a a < b
theorem Multiset.right_mem_Icc {α : Type u_1} [] {a : α} {b : α} :
b a b
theorem Multiset.right_mem_Ioc {α : Type u_1} [] {a : α} {b : α} :
b a < b
theorem Multiset.left_not_mem_Ioc {α : Type u_1} [] {a : α} {b : α} :
a
theorem Multiset.left_not_mem_Ioo {α : Type u_1} [] {a : α} {b : α} :
a
theorem Multiset.right_not_mem_Ico {α : Type u_1} [] {a : α} {b : α} :
b
theorem Multiset.right_not_mem_Ioo {α : Type u_1} [] {a : α} {b : α} :
b
theorem Multiset.Ico_filter_lt_of_le_left {α : Type u_1} [] {a : α} {b : α} {c : α} [DecidablePred fun (x : α) => x < c] (hca : c a) :
Multiset.filter (fun (x : α) => x < c) () =
theorem Multiset.Ico_filter_lt_of_right_le {α : Type u_1} [] {a : α} {b : α} {c : α} [DecidablePred fun (x : α) => x < c] (hbc : b c) :
Multiset.filter (fun (x : α) => x < c) () =
theorem Multiset.Ico_filter_lt_of_le_right {α : Type u_1} [] {a : α} {b : α} {c : α} [DecidablePred fun (x : α) => x < c] (hcb : c b) :
Multiset.filter (fun (x : α) => x < c) () =
theorem Multiset.Ico_filter_le_of_le_left {α : Type u_1} [] {a : α} {b : α} {c : α} [DecidablePred fun (x : α) => c x] (hca : c a) :
Multiset.filter (fun (x : α) => c x) () =
theorem Multiset.Ico_filter_le_of_right_le {α : Type u_1} [] {a : α} {b : α} [DecidablePred fun (x : α) => b x] :
Multiset.filter (fun (x : α) => b x) () =
theorem Multiset.Ico_filter_le_of_left_le {α : Type u_1} [] {a : α} {b : α} {c : α} [DecidablePred fun (x : α) => c x] (hac : a c) :
Multiset.filter (fun (x : α) => c x) () =
@[simp]
theorem Multiset.Icc_self {α : Type u_1} [] (a : α) :
= {a}
theorem Multiset.Ico_cons_right {α : Type u_1} [] {a : α} {b : α} (h : a b) :
b ::ₘ =
theorem Multiset.Ioo_cons_left {α : Type u_1} [] {a : α} {b : α} (h : a < b) :
a ::ₘ =
theorem Multiset.Ico_disjoint_Ico {α : Type u_1} [] {a : α} {b : α} {c : α} {d : α} (h : b c) :
().Disjoint ()
@[simp]
theorem Multiset.Ico_inter_Ico_of_le {α : Type u_1} [] [] {a : α} {b : α} {c : α} {d : α} (h : b c) :
= 0
theorem Multiset.Ico_filter_le_left {α : Type u_1} [] {a : α} {b : α} [DecidablePred fun (x : α) => x a] (hab : a < b) :
Multiset.filter (fun (x : α) => x a) () = {a}
theorem Multiset.card_Ico_eq_card_Icc_sub_one {α : Type u_1} [] (a : α) (b : α) :
Multiset.card () = Multiset.card () - 1
theorem Multiset.card_Ioc_eq_card_Icc_sub_one {α : Type u_1} [] (a : α) (b : α) :
Multiset.card () = Multiset.card () - 1
theorem Multiset.card_Ioo_eq_card_Ico_sub_one {α : Type u_1} [] (a : α) (b : α) :
Multiset.card () = Multiset.card () - 1
theorem Multiset.card_Ioo_eq_card_Icc_sub_two {α : Type u_1} [] (a : α) (b : α) :
Multiset.card () = Multiset.card () - 2
theorem Multiset.Ico_subset_Ico_iff {α : Type u_1} [] {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} [] {a : α} {b : α} {c : α} (hab : a b) (hbc : b c) :
+ =
theorem Multiset.Ico_inter_Ico {α : Type u_1} [] {a : α} {b : α} {c : α} {d : α} :
= Multiset.Ico (max a c) (min b d)
@[simp]
theorem Multiset.Ico_filter_lt {α : Type u_1} [] (a : α) (b : α) (c : α) :
Multiset.filter (fun (x : α) => x < c) () = Multiset.Ico a (min b c)
@[simp]
theorem Multiset.Ico_filter_le {α : Type u_1} [] (a : α) (b : α) (c : α) :
Multiset.filter (fun (x : α) => c x) () = Multiset.Ico (max a c) b
@[simp]
theorem Multiset.Ico_sub_Ico_left {α : Type u_1} [] (a : α) (b : α) (c : α) :
- = Multiset.Ico (max a c) b
@[simp]
theorem Multiset.Ico_sub_Ico_right {α : Type u_1} [] (a : α) (b : α) (c : α) :
- = Multiset.Ico a (min b c)