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} [] {a : α} {b : α} :
theorem Multiset.nodup_Ico {α : Type u_1} [] {a : α} {b : α} :
theorem Multiset.nodup_Ioc {α : Type u_1} [] {a : α} {b : α} :
theorem Multiset.nodup_Ioo {α : Type u_1} [] {a : α} {b : α} :
@[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 : α} :
theorem Multiset.left_not_mem_Ioo {α : Type u_1} [] {a : α} {b : α} :
theorem Multiset.right_not_mem_Ico {α : Type u_1} [] {a : α} {b : α} :
theorem Multiset.right_not_mem_Ioo {α : Type u_1} [] {a : α} {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 x_1 => x x_1) c)] (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 x_1 => x x_1) b)] :
Multiset.filter (fun x => b x) () =
theorem Multiset.Ico_filter_le_of_left_le {α : Type u_1} [] {a : α} {b : α} {c : α} [DecidablePred ((fun x x_1 => x x_1) c)] (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) :
@[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)
theorem Multiset.map_add_left_Icc {α : Type u_1} [] (a : α) (b : α) (c : α) :
Multiset.map ((fun x x_1 => x + x_1) c) () = Multiset.Icc (c + a) (c + b)
theorem Multiset.map_add_left_Ico {α : Type u_1} [] (a : α) (b : α) (c : α) :
Multiset.map ((fun x x_1 => x + x_1) c) () = Multiset.Ico (c + a) (c + b)
theorem Multiset.map_add_left_Ioc {α : Type u_1} [] (a : α) (b : α) (c : α) :
Multiset.map ((fun x x_1 => x + x_1) c) () = Multiset.Ioc (c + a) (c + b)
theorem Multiset.map_add_left_Ioo {α : Type u_1} [] (a : α) (b : α) (c : α) :
Multiset.map ((fun x x_1 => x + x_1) c) () = Multiset.Ioo (c + a) (c + b)
theorem Multiset.map_add_right_Icc {α : Type u_1} [] (a : α) (b : α) (c : α) :
Multiset.map (fun x => x + c) () = Multiset.Icc (a + c) (b + c)
theorem Multiset.map_add_right_Ico {α : Type u_1} [] (a : α) (b : α) (c : α) :
Multiset.map (fun x => x + c) () = Multiset.Ico (a + c) (b + c)
theorem Multiset.map_add_right_Ioc {α : Type u_1} [] (a : α) (b : α) (c : α) :
Multiset.map (fun x => x + c) () = Multiset.Ioc (a + c) (b + c)
theorem Multiset.map_add_right_Ioo {α : Type u_1} [] (a : α) (b : α) (c : α) :
Multiset.map (fun x => x + c) () = Multiset.Ioo (a + c) (b + c)