doc-next-gen

Mathlib.Order.Interval.Multiset

Module docstring

{"# 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) "}

Multiset.Icc definition
(a b : α) : Multiset α
Full source 
/-- The multiset of elements `x` such that `a ≤ x` and `x ≤ b`. Basically `Set.Icc a b` as a
multiset. -/
def Icc (a b : α) : Multiset α := (Finset.Icc a b).val
Closed interval as a multiset
Informal description
For a locally finite order $\alpha$ and elements $a, b \in \alpha$, the multiset $\text{Icc}(a, b)$ consists of all elements $x$ such that $a \leq x \leq b$. This is the multiset representation of the closed interval $[a, b]$, obtained by converting the corresponding finset to a multiset.
Multiset.Ico definition
(a b : α) : Multiset α
Full source 
/-- The multiset of elements `x` such that `a ≤ x` and `x < b`. Basically `Set.Ico a b` as a
multiset. -/
def Ico (a b : α) : Multiset α := (Finset.Ico a b).val
Closed-open interval as a multiset
Informal description
For a locally finite order $\alpha$ and elements $a, b \in \alpha$, the multiset $\text{Ico}(a, b)$ consists of all elements $x$ such that $a \leq x < b$. This is the multiset representation of the half-open interval $[a, b)$, obtained by converting the corresponding finset to a multiset.
Multiset.Ioc definition
(a b : α) : Multiset α
Full source 
/-- The multiset of elements `x` such that `a < x` and `x ≤ b`. Basically `Set.Ioc a b` as a
multiset. -/
def Ioc (a b : α) : Multiset α := (Finset.Ioc a b).val
Open-closed interval as a multiset
Informal description
For a locally finite order $\alpha$ and elements $a, b \in \alpha$, the multiset $\text{Ioc}(a, b)$ consists of all elements $x$ such that $a < x \leq b$. This is the multiset representation of the half-open interval $(a, b]$, obtained by converting the corresponding finset to a multiset.
Multiset.Ioo definition
(a b : α) : Multiset α
Full source 
/-- The multiset of elements `x` such that `a < x` and `x < b`. Basically `Set.Ioo a b` as a
multiset. -/
def Ioo (a b : α) : Multiset α := (Finset.Ioo a b).val
Open interval as a multiset
Informal description
For a locally finite order $\alpha$ and elements $a, b \in \alpha$, the multiset $\text{Ioo}(a, b)$ consists of all elements $x$ such that $a < x < b$. This is the multiset representation of the open interval $(a, b)$, obtained by converting the corresponding finset to a multiset.
Multiset.Ici definition
(a : α) : Multiset α
Full source 
/-- The multiset of elements `x` such that `a ≤ x`. Basically `Set.Ici a` as a multiset. -/
def Ici (a : α) : Multiset α := (Finset.Ici a).val
Closed-infinite interval as a multiset
Informal description
For an element $a$ in a locally finite order with finite intervals bounded below, the multiset $\text{Ici}(a)$ consists of all elements $x$ such that $a \leq x$. This is the multiset representation of the set $\{x \mid a \leq x\}$.
Multiset.Ioi definition
(a : α) : Multiset α
Full source 
/-- The multiset of elements `x` such that `a < x`. Basically `Set.Ioi a` as a multiset. -/
def Ioi (a : α) : Multiset α := (Finset.Ioi a).val
Open infinite interval as a multiset
Informal description
The multiset of elements $x$ in a locally finite order with finite intervals bounded below such that $a < x$. This is the multiset representation of the open interval $(a, \infty)$.
Multiset.mem_Ici theorem
: x ∈ Ici a ↔ a ≤ x
Full source 
@[simp] lemma mem_Ici : x ∈ Ici ax ∈ Ici a ↔ a ≤ x := by rw [Ici, ← Finset.mem_def, Finset.mem_Ici]
Membership in Closed-Infinite Interval Multiset: $x \in \text{Ici}(a) \leftrightarrow a \leq x$
Informal description
For any element $x$ in a locally finite order with finite intervals bounded below, $x$ belongs to the closed-infinite interval multiset $\text{Ici}(a)$ if and only if $a \leq x$.
Multiset.mem_Ioi theorem
: x ∈ Ioi a ↔ a < x
Full source 
@[simp] lemma mem_Ioi : x ∈ Ioi ax ∈ Ioi a ↔ a < x := by rw [Ioi, ← Finset.mem_def, Finset.mem_Ioi]
Membership in Open-Infinite Interval Multiset: $x \in \text{Ioi}(a) \leftrightarrow a < x$
Informal description
For any elements $x$ and $a$ in a locally finite order with finite intervals bounded below, $x$ belongs to the open-infinite interval multiset $\text{Ioi}(a)$ if and only if $a < x$.
Multiset.Iic definition
(b : α) : Multiset α
Full source 
/-- The multiset of elements `x` such that `x ≤ b`. Basically `Set.Iic b` as a multiset. -/
def Iic (b : α) : Multiset α := (Finset.Iic b).val
Lower-closed interval as a multiset
Informal description
For an element $b$ in a locally finite order with finite lower-bounded intervals, the multiset $\text{Iic}(b)$ consists of all elements $x$ such that $x \leq b$, with each element appearing with multiplicity according to its occurrences in the order. This is the multiset version of the set $\{x \mid x \leq b\}$.
Multiset.Iio definition
(b : α) : Multiset α
Full source 
/-- The multiset of elements `x` such that `x < b`. Basically `Set.Iio b` as a multiset. -/
def Iio (b : α) : Multiset α := (Finset.Iio b).val
Open lower interval as a multiset
Informal description
For an element $b$ in a locally finite order with finite lower-bounded intervals, the multiset $\text{Iio}(b)$ consists of all elements $x$ such that $x < b$, with each element appearing with multiplicity according to its occurrences in the order. This is the multiset version of the set $\{x \mid x < b\}$.
Multiset.mem_Iic theorem
: x ∈ Iic b ↔ x ≤ b
Full source 
@[simp] lemma mem_Iic : x ∈ Iic bx ∈ Iic b ↔ x ≤ b := by rw [Iic, ← Finset.mem_def, Finset.mem_Iic]
Membership in Closed Lower Interval Multiset: $x \in \text{Iic}(b) \leftrightarrow x \leq b$
Informal description
For any elements $x$ and $b$ in a locally finite order with finite lower-bounded intervals, $x$ belongs to the multiset $\text{Iic}(b)$ if and only if $x \leq b$.
Multiset.mem_Iio theorem
: x ∈ Iio b ↔ x < b
Full source 
@[simp] lemma mem_Iio : x ∈ Iio bx ∈ Iio b ↔ x < b := by rw [Iio, ← Finset.mem_def, Finset.mem_Iio]
Membership in Open Lower Interval Multiset: $x \in \text{Iio}(b) \leftrightarrow x < b$
Informal description
For any elements $x$ and $b$ in a locally finite order with finite lower-bounded intervals, $x$ belongs to the multiset $\text{Iio}(b)$ if and only if $x < b$.
Multiset.nodup_Icc theorem
: (Icc a b).Nodup
Full source 
theorem nodup_Icc : (Icc a b).Nodup :=
  Finset.nodup _
No Duplicates in Closed Interval Multiset
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the multiset $\text{Icc}(a, b)$ representing the closed interval $[a, b]$ has no duplicate elements.
Multiset.nodup_Ico theorem
: (Ico a b).Nodup
Full source 
theorem nodup_Ico : (Ico a b).Nodup :=
  Finset.nodup _
No Duplicates in Closed-Open Interval Multiset
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the multiset $\text{Ico}(a, b)$ representing the closed-open interval $[a, b)$ has no duplicate elements.
Multiset.nodup_Ioc theorem
: (Ioc a b).Nodup
Full source 
theorem nodup_Ioc : (Ioc a b).Nodup :=
  Finset.nodup _
No Duplicates in Open-Closed Interval Multiset
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the multiset $\text{Ioc}(a, b)$ representing the open-closed interval $(a, b]$ has no duplicate elements.
Multiset.nodup_Ioo theorem
: (Ioo a b).Nodup
Full source 
theorem nodup_Ioo : (Ioo a b).Nodup :=
  Finset.nodup _
No Duplicates in Open Interval Multiset
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the multiset $\text{Ioo}(a, b)$ representing the open interval $(a, b)$ has no duplicate elements.
Multiset.Icc_eq_zero_iff theorem
: Icc a b = 0 ↔ ¬a ≤ b
Full source 
@[simp]
theorem Icc_eq_zero_iff : IccIcc a b = 0 ↔ ¬a ≤ b := by
  rw [Icc, Finset.val_eq_zero, Finset.Icc_eq_empty_iff]
Empty Closed Interval Criterion: $\text{Icc}(a, b) = \emptyset \leftrightarrow a \nleq b$
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the multiset $\text{Icc}(a, b)$ representing the closed interval $[a, b]$ is empty if and only if $a$ is not less than or equal to $b$, i.e., $\text{Icc}(a, b) = \emptyset \leftrightarrow a \nleq b$.
Multiset.Ico_eq_zero_iff theorem
: Ico a b = 0 ↔ ¬a < b
Full source 
@[simp]
theorem Ico_eq_zero_iff : IcoIco a b = 0 ↔ ¬a < b := by
  rw [Ico, Finset.val_eq_zero, Finset.Ico_eq_empty_iff]
Empty Closed-Open Interval Multiset Criterion: $\text{Ico}(a, b) = \emptyset \leftrightarrow a \geq b$
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the multiset $\text{Ico}(a, b)$ representing the closed-open interval $[a, b)$ is empty if and only if $a \nless b$.
Multiset.Ioc_eq_zero_iff theorem
: Ioc a b = 0 ↔ ¬a < b
Full source 
@[simp]
theorem Ioc_eq_zero_iff : IocIoc a b = 0 ↔ ¬a < b := by
  rw [Ioc, Finset.val_eq_zero, Finset.Ioc_eq_empty_iff]
Empty Open-Closed Interval Multiset Criterion: $\text{Ioc}(a, b) = 0 \leftrightarrow a \geq b$
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the open-closed interval multiset $\text{Ioc}(a, b)$ is empty if and only if $a$ is not less than $b$, i.e., $\text{Ioc}(a, b) = 0 \leftrightarrow \neg (a < b)$.
Multiset.Ioo_eq_zero_iff theorem
[DenselyOrdered α] : Ioo a b = 0 ↔ ¬a < b
Full source 
@[simp]
theorem Ioo_eq_zero_iff [DenselyOrdered α] : IooIoo a b = 0 ↔ ¬a < b := by
  rw [Ioo, Finset.val_eq_zero, Finset.Ioo_eq_empty_iff]
Empty Open Interval Multiset Criterion in Densely Ordered Sets
Informal description
In a densely ordered set $\alpha$, the open interval multiset $\text{Ioo}(a, b)$ is empty if and only if $a$ is not less than $b$, i.e., $\text{Ioo}(a, b) = 0 \leftrightarrow \neg (a < b)$.
Multiset.Ioo_eq_zero theorem
(h : ¬a < b) : Ioo a b = 0
Full source 
@[simp]
theorem Ioo_eq_zero (h : ¬a < b) : Ioo a b = 0 :=
  eq_zero_iff_forall_not_mem.2 fun _x hx => h ((mem_Ioo.1 hx).1.trans (mem_Ioo.1 hx).2)
Empty Open Interval Multiset When Not $a < b$
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, if $a$ is not less than $b$ (i.e., $\neg (a < b)$), then the open interval multiset $\text{Ioo}(a, b)$ is empty (i.e., $\text{Ioo}(a, b) = 0$).
Multiset.Icc_eq_zero_of_lt theorem
(h : b < a) : Icc a b = 0
Full source 
@[simp]
theorem Icc_eq_zero_of_lt (h : b < a) : Icc a b = 0 :=
  Icc_eq_zero h.not_le
Empty Closed Interval Multiset When $b < a$
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, if $b < a$, then the closed interval multiset $\text{Icc}(a, b)$ is empty, i.e., $\text{Icc}(a, b) = 0$.
Multiset.Ico_eq_zero_of_le theorem
(h : b ≤ a) : Ico a b = 0
Full source 
@[simp]
theorem Ico_eq_zero_of_le (h : b ≤ a) : Ico a b = 0 :=
  Ico_eq_zero h.not_lt
Empty Closed-Open Interval Multiset When $b \leq a$
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, if $b \leq a$, then the closed-open interval multiset $\text{Ico}(a, b)$ is empty, i.e., $\text{Ico}(a, b) = 0$.
Multiset.Ioc_eq_zero_of_le theorem
(h : b ≤ a) : Ioc a b = 0
Full source 
@[simp]
theorem Ioc_eq_zero_of_le (h : b ≤ a) : Ioc a b = 0 :=
  Ioc_eq_zero h.not_lt
Empty Open-Closed Interval Multiset When $b \leq a$
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, if $b \leq a$, then the open-closed interval multiset $\text{Ioc}(a, b)$ is empty, i.e., $\text{Ioc}(a, b) = 0$.
Multiset.Ioo_eq_zero_of_le theorem
(h : b ≤ a) : Ioo a b = 0
Full source 
@[simp]
theorem Ioo_eq_zero_of_le (h : b ≤ a) : Ioo a b = 0 :=
  Ioo_eq_zero h.not_lt
Empty Open Interval Multiset When $b \leq a$
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, if $b \leq a$, then the open interval multiset $\text{Ioo}(a, b)$ is empty, i.e., $\text{Ioo}(a, b) = 0$.
Multiset.Ico_self theorem
: Ico a a = 0
Full source 
theorem Ico_self : Ico a a = 0 := by rw [Ico, Finset.Ico_self, Finset.empty_val]
Empty Closed-Open Interval Multiset at a Point: $\text{Ico}(a, a) = 0$
Informal description
For any element $a$ in a locally finite order, the closed-open interval multiset $[a, a)$ is empty, i.e., $\text{Ico}(a, a) = 0$.
Multiset.Ioc_self theorem
: Ioc a a = 0
Full source 
theorem Ioc_self : Ioc a a = 0 := by rw [Ioc, Finset.Ioc_self, Finset.empty_val]
Empty Open-Closed Interval Multiset at a Point: $\text{Ioc}(a, a) = 0$
Informal description
For any element $a$ in a locally finite order, the open-closed interval multiset $\text{Ioc}(a, a)$ is empty, i.e., $(a, a] = \emptyset$.
Multiset.Ioo_self theorem
: Ioo a a = 0
Full source 
theorem Ioo_self : Ioo a a = 0 := by rw [Ioo, Finset.Ioo_self, Finset.empty_val]
Empty Open Interval Multiset at a Point: $\text{Ioo}(a, a) = 0$
Informal description
For any element $a$ in a locally finite order, the open interval multiset $\text{Ioo}(a, a)$ is empty, i.e., $\text{Ioo}(a, a) = 0$.
Multiset.left_mem_Icc theorem
: a ∈ Icc a b ↔ a ≤ b
Full source 
theorem left_mem_Icc : a ∈ Icc a ba ∈ Icc a b ↔ a ≤ b :=
  Finset.left_mem_Icc
Membership of Left Endpoint in Closed Interval Multiset: $a \in [a, b] \leftrightarrow a \leq b$
Informal description
For elements $a$ and $b$ in a locally finite order $\alpha$, the element $a$ belongs to the closed interval $[a, b]$ (represented as a multiset) if and only if $a \leq b$.
Multiset.left_mem_Ico theorem
: a ∈ Ico a b ↔ a < b
Full source 
theorem left_mem_Ico : a ∈ Ico a ba ∈ Ico a b ↔ a < b :=
  Finset.left_mem_Ico
Membership of Left Endpoint in Closed-Open Interval Multiset: $a \in [a, b) \leftrightarrow a < b$
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the left endpoint $a$ belongs to the closed-open interval $[a, b)$ (represented as a multiset) if and only if $a < b$.
Multiset.right_mem_Icc theorem
: b ∈ Icc a b ↔ a ≤ b
Full source 
theorem right_mem_Icc : b ∈ Icc a bb ∈ Icc a b ↔ a ≤ b :=
  Finset.right_mem_Icc
Membership of Right Endpoint in Closed Interval Multiset: $b \in [a, b] \leftrightarrow a \leq b$
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the right endpoint $b$ belongs to the closed interval $[a, b]$ (represented as a multiset) if and only if $a \leq b$.
Multiset.right_mem_Ioc theorem
: b ∈ Ioc a b ↔ a < b
Full source 
theorem right_mem_Ioc : b ∈ Ioc a bb ∈ Ioc a b ↔ a < b :=
  Finset.right_mem_Ioc
Membership of Right Endpoint in Open-Closed Interval Multiset: $b \in (a, b] \leftrightarrow a < b$
Informal description
For elements $a$ and $b$ in a locally finite order $\alpha$, the element $b$ belongs to the open-closed interval $(a, b]$ (represented as a multiset) if and only if $a < b$.
Multiset.left_not_mem_Ioc theorem
: a ∉ Ioc a b
Full source 
theorem left_not_mem_Ioc : a ∉ Ioc a b :=
  Finset.left_not_mem_Ioc
Left Endpoint Exclusion in Open-Closed Interval Multiset: $a \notin (a, b]$
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the left endpoint $a$ does not belong to the open-closed interval multiset $(a, b]$.
Multiset.left_not_mem_Ioo theorem
: a ∉ Ioo a b
Full source 
theorem left_not_mem_Ioo : a ∉ Ioo a b :=
  Finset.left_not_mem_Ioo
Left Endpoint Exclusion in Open Interval Multiset: $a \notin (a, b)$
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the left endpoint $a$ does not belong to the open interval multiset $\text{Ioo}(a, b)$, i.e., $a \notin (a, b)$.
Multiset.right_not_mem_Ico theorem
: b ∉ Ico a b
Full source 
theorem right_not_mem_Ico : b ∉ Ico a b :=
  Finset.right_not_mem_Ico
Exclusion of Right Endpoint from Closed-Open Interval Multiset: $b \notin \text{Ico}(a, b)$
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the element $b$ does not belong to the closed-open interval multiset $\text{Ico}(a, b)$, which consists of all elements $x$ such that $a \leq x < b$.
Multiset.right_not_mem_Ioo theorem
: b ∉ Ioo a b
Full source 
theorem right_not_mem_Ioo : b ∉ Ioo a b :=
  Finset.right_not_mem_Ioo
Right Endpoint Exclusion in Open Interval Multiset: $b \notin \text{Ioo}(a, b)$
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the element $b$ does not belong to the open interval multiset $\text{Ioo}(a, b)$, i.e., $b \notin \text{Ioo}(a, b)$.
Multiset.Ico_filter_lt_of_le_left theorem
[DecidablePred (· < c)] (hca : c ≤ a) : ((Ico a b).filter fun x => x < c) = ∅
Full source 
theorem Ico_filter_lt_of_le_left [DecidablePred (· < c)] (hca : c ≤ a) :
    ((Ico a b).filter fun x => x < c) = ∅ := by
  rw [Ico, ← Finset.filter_val, Finset.Ico_filter_lt_of_le_left hca]
  rfl
Empty Filtered Closed-Open Multiset Interval for Left-Leaning Condition
Informal description
For a locally finite order $\alpha$ and elements $a, b, c \in \alpha$ with $c \leq a$, the multiset obtained by filtering the closed-open interval multiset $\text{Ico}(a, b)$ to include only elements less than $c$ is empty. In other words, $\{x \in [a, b) \mid x < c\} = \emptyset$ as a multiset.
Multiset.Ico_filter_lt_of_right_le theorem
[DecidablePred (· < c)] (hbc : b ≤ c) : ((Ico a b).filter fun x => x < c) = Ico a b
Full source 
theorem Ico_filter_lt_of_right_le [DecidablePred (· < c)] (hbc : b ≤ c) :
    ((Ico a b).filter fun x => x < c) = Ico a b := by
  rw [Ico, ← Finset.filter_val, Finset.Ico_filter_lt_of_right_le hbc]
Filtered Closed-Open Interval Equals Original When Upper Bound is Below Filter Condition
Informal description
For a locally finite order $\alpha$ and elements $a, b, c \in \alpha$ with $b \leq c$, the multiset obtained by filtering the closed-open interval multiset $\text{Ico}(a, b)$ to retain only elements less than $c$ is equal to the original interval multiset $\text{Ico}(a, b)$. In other words, $\{x \in [a, b) \mid x < c\} = [a, b)$ when $b \leq c$.
Multiset.Ico_filter_lt_of_le_right theorem
[DecidablePred (· < c)] (hcb : c ≤ b) : ((Ico a b).filter fun x => x < c) = Ico a c
Full source 
theorem Ico_filter_lt_of_le_right [DecidablePred (· < c)] (hcb : c ≤ b) :
    ((Ico a b).filter fun x => x < c) = Ico a c := by
  rw [Ico, ← Finset.filter_val, Finset.Ico_filter_lt_of_le_right hcb]
  rfl
Filtered Closed-Open Interval Equals Smaller Interval When Filter Condition is Met
Informal description
For a locally finite order $\alpha$ and elements $a, b, c \in \alpha$ with $c \leq b$, the multiset obtained by filtering the closed-open interval multiset $\text{Ico}(a, b)$ to keep only elements less than $c$ is equal to the closed-open interval multiset $\text{Ico}(a, c)$. In other words: $$\{x \in [a, b) \mid x < c\} = [a, c)$$ where both sides are interpreted as multisets.
Multiset.Ico_filter_le_of_le_left theorem
[DecidablePred (c ≤ ·)] (hca : c ≤ a) : ((Ico a b).filter fun x => c ≤ x) = Ico a b
Full source 
theorem Ico_filter_le_of_le_left [DecidablePred (c ≤ ·)] (hca : c ≤ a) :
    ((Ico a b).filter fun x => c ≤ x) = Ico a b := by
  rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_of_le_left hca]
Filtered Closed-Open Interval Equals Original When Lower Bound is Below Interval Start
Informal description
Let $\alpha$ be a locally finite order, and let $a, b, c \in \alpha$ such that $c \leq a$. Then the multiset obtained by filtering the closed-open interval multiset $\text{Ico}(a, b)$ to include only elements $x$ satisfying $c \leq x$ is equal to $\text{Ico}(a, b)$ itself.
Multiset.Ico_filter_le_of_right_le theorem
[DecidablePred (b ≤ ·)] : ((Ico a b).filter fun x => b ≤ x) = ∅
Full source 
theorem Ico_filter_le_of_right_le [DecidablePred (b ≤ ·)] :
    ((Ico a b).filter fun x => b ≤ x) = ∅ := by
  rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_of_right_le]
  rfl
Emptyness of Closed-Open Interval Multiset Filtered by Upper Bound
Informal description
For any elements $a, b$ in a locally finite order $\alpha$, the multiset obtained by filtering the closed-open interval multiset $\text{Ico}(a, b)$ to retain only elements $x$ satisfying $b \leq x$ is empty. In other words, $\{x \in [a, b) \mid b \leq x\} = \emptyset$ as a multiset.
Multiset.Ico_filter_le_of_left_le theorem
[DecidablePred (c ≤ ·)] (hac : a ≤ c) : ((Ico a b).filter fun x => c ≤ x) = Ico c b
Full source 
theorem Ico_filter_le_of_left_le [DecidablePred (c ≤ ·)] (hac : a ≤ c) :
    ((Ico a b).filter fun x => c ≤ x) = Ico c b := by
  rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_of_left_le hac]
  rfl
Filtered Closed-Open Interval Equals Smaller Interval When Filter Bound is Within Original Bounds
Informal description
For any elements $a, b, c$ in a locally finite order $\alpha$ with a decidable predicate for elements greater than or equal to $c$, if $a \leq c$, then filtering the multiset $\text{Ico}(a, b)$ to keep only elements $x$ satisfying $c \leq x$ results in the multiset $\text{Ico}(c, b)$.
Multiset.Icc_self theorem
(a : α) : Icc a a = { a }
Full source 
@[simp]
theorem Icc_self (a : α) : Icc a a = {a} := by rw [Icc, Finset.Icc_self, Finset.singleton_val]
Closed Interval Multiset at a Point is Singleton: $[a, a] = \{a\}$
Informal description
For any element $a$ in a locally finite order $\alpha$, the multiset representing the closed interval $[a, a]$ is equal to the singleton multiset $\{a\}$.
Multiset.Ico_cons_right theorem
(h : a ≤ b) : b ::ₘ Ico a b = Icc a b
Full source 
theorem Ico_cons_right (h : a ≤ b) : b ::ₘ Ico a b = Icc a b := by
  classical
    rw [Ico, ← Finset.insert_val_of_not_mem right_not_mem_Ico, Finset.Ico_insert_right h]
    rfl
Insertion of Right Endpoint into Closed-Open Interval Multiset Yields Closed Interval: $b \cup \text{Ico}(a, b) = \text{Icc}(a, b)$
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$ with $a \leq b$, the multiset obtained by inserting $b$ into the closed-open interval multiset $\text{Ico}(a, b)$ equals the closed interval multiset $\text{Icc}(a, b)$. In other words, $b \cup \text{Ico}(a, b) = \text{Icc}(a, b)$.
Multiset.Ioo_cons_left theorem
(h : a < b) : a ::ₘ Ioo a b = Ico a b
Full source 
theorem Ioo_cons_left (h : a < b) : a ::ₘ Ioo a b = Ico a b := by
  classical
    rw [Ioo, ← Finset.insert_val_of_not_mem left_not_mem_Ioo, Finset.Ioo_insert_left h]
    rfl
Insertion of Left Endpoint into Open Interval Multiset Yields Closed-Open Interval Multiset: $a \cup (a, b) = [a, b)$
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$ with $a < b$, the multiset obtained by inserting $a$ into the open interval multiset $\text{Ioo}(a, b)$ equals the closed-open interval multiset $\text{Ico}(a, b)$. In other words, $a \cup (a, b) = [a, b)$ as multisets.
Multiset.Ico_disjoint_Ico theorem
{a b c d : α} (h : b ≤ c) : Disjoint (Ico a b) (Ico c d)
Full source 
theorem Ico_disjoint_Ico {a b c d : α} (h : b ≤ c) : Disjoint (Ico a b) (Ico c d) :=
  disjoint_left.mpr fun hab hbc => by
    rw [mem_Ico] at hab hbc
    exact hab.2.not_le (h.trans hbc.1)
Disjointness of Closed-Open Intervals When $b \leq c$
Informal description
For any elements $a, b, c, d$ in a locally finite order $\alpha$, if $b \leq c$, then the closed-open interval multisets $[a, b)$ and $[c, d)$ are disjoint.
Multiset.Ico_inter_Ico_of_le theorem
[DecidableEq α] {a b c d : α} (h : b ≤ c) : Ico a b ∩ Ico c d = 0
Full source 
@[simp]
theorem Ico_inter_Ico_of_le [DecidableEq α] {a b c d : α} (h : b ≤ c) : IcoIco a b ∩ Ico c d = 0 :=
  Multiset.inter_eq_zero_iff_disjoint.2 <| Ico_disjoint_Ico h
Empty Intersection of Closed-Open Intervals When $b \leq c$
Informal description
For any elements $a, b, c, d$ in a locally finite order $\alpha$ with decidable equality, if $b \leq c$, then the intersection of the closed-open interval multisets $[a, b)$ and $[c, d)$ is the empty multiset. In symbols: $$ [a, b) \cap [c, d) = \emptyset. $$
Multiset.Ico_filter_le_left theorem
{a b : α} [DecidablePred (· ≤ a)] (hab : a < b) : ((Ico a b).filter fun x => x ≤ a) = { a }
Full source 
theorem Ico_filter_le_left {a b : α} [DecidablePred (· ≤ a)] (hab : a < b) :
    ((Ico a b).filter fun x => x ≤ a) = {a} := by
  rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_left hab]
  rfl
Filtering the Closed-Open Interval for Elements Below Left Endpoint Yields Singleton $\{a\}$
Informal description
Let $\alpha$ be a locally finite order, and let $a, b \in \alpha$ with $a < b$. Then the multiset obtained by filtering the closed-open interval $[a, b)$ (represented as a multiset) for elements $x$ satisfying $x \leq a$ is exactly the singleton multiset $\{a\}$.
Multiset.card_Ico_eq_card_Icc_sub_one theorem
(a b : α) : card (Ico a b) = card (Icc a b) - 1
Full source 
theorem card_Ico_eq_card_Icc_sub_one (a b : α) : card (Ico a b) = card (Icc a b) - 1 :=
  Finset.card_Ico_eq_card_Icc_sub_one _ _
Cardinality relation: $|\text{Ico}(a, b)| = |\text{Icc}(a, b)| - 1$
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the cardinality of the closed-open interval multiset $[a, b)$ is equal to the cardinality of the closed interval multiset $[a, b]$ minus one. That is, $$|\text{Ico}(a, b)| = |\text{Icc}(a, b)| - 1.$$
Multiset.card_Ioc_eq_card_Icc_sub_one theorem
(a b : α) : card (Ioc a b) = card (Icc a b) - 1
Full source 
theorem card_Ioc_eq_card_Icc_sub_one (a b : α) : card (Ioc a b) = card (Icc a b) - 1 :=
  Finset.card_Ioc_eq_card_Icc_sub_one _ _
Cardinality relation: $|\text{Ioc}(a, b)| = |\text{Icc}(a, b)| - 1$
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the cardinality of the open-closed interval multiset $\text{Ioc}(a, b)$ is equal to the cardinality of the closed interval multiset $\text{Icc}(a, b)$ minus one, i.e., $$|\text{Ioc}(a, b)| = |\text{Icc}(a, b)| - 1.$$
Multiset.card_Ioo_eq_card_Ico_sub_one theorem
(a b : α) : card (Ioo a b) = card (Ico a b) - 1
Full source 
theorem card_Ioo_eq_card_Ico_sub_one (a b : α) : card (Ioo a b) = card (Ico a b) - 1 :=
  Finset.card_Ioo_eq_card_Ico_sub_one _ _
Cardinality Relation: $|\text{Ioo}(a, b)| = |\text{Ico}(a, b)| - 1$
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the cardinality of the open interval multiset $\text{Ioo}(a, b)$ is equal to the cardinality of the closed-open interval multiset $\text{Ico}(a, b)$ minus one, i.e., $|\text{Ioo}(a, b)| = |\text{Ico}(a, b)| - 1$.
Multiset.card_Ioo_eq_card_Icc_sub_two theorem
(a b : α) : card (Ioo a b) = card (Icc a b) - 2
Full source 
theorem card_Ioo_eq_card_Icc_sub_two (a b : α) : card (Ioo a b) = card (Icc a b) - 2 :=
  Finset.card_Ioo_eq_card_Icc_sub_two _ _
Cardinality Relation: $|\text{Ioo}(a, b)| = |\text{Icc}(a, b)| - 2$
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the cardinality of the open interval multiset $\text{Ioo}(a, b)$ is equal to the cardinality of the closed interval multiset $\text{Icc}(a, b)$ minus two, i.e., $$|\text{Ioo}(a, b)| = |\text{Icc}(a, b)| - 2.$$
Multiset.Ico_subset_Ico_iff theorem
{a₁ b₁ a₂ b₂ : α} (h : a₁ < b₁) : Ico a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
Full source 
theorem Ico_subset_Ico_iff {a₁ b₁ a₂ b₂ : α} (h : a₁ < b₁) :
    IcoIco a₁ b₁ ⊆ Ico a₂ b₂Ico a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂ :=
  Finset.Ico_subset_Ico_iff h
Subset Condition for Closed-Open Multiset Intervals: $\text{Ico}(a₁, b₁) \subseteq \text{Ico}(a₂, b₂) \leftrightarrow a₂ \leq a₁ \land b₁ \leq b₂$
Informal description
For any elements $a₁, b₁, a₂, b₂$ in a locally finite order $\alpha$ with $a₁ < b₁$, the closed-open interval multiset $\text{Ico}(a₁, b₁)$ is a subset of $\text{Ico}(a₂, b₂)$ if and only if $a₂ \leq a₁$ and $b₁ \leq b₂$.
Multiset.Ico_add_Ico_eq_Ico theorem
{a b c : α} (hab : a ≤ b) (hbc : b ≤ c) : Ico a b + Ico b c = Ico a c
Full source 
theorem Ico_add_Ico_eq_Ico {a b c : α} (hab : a ≤ b) (hbc : b ≤ c) :
    Ico a b + Ico b c = Ico a c := by
  rw [add_eq_union_iff_disjoint.2 (Ico_disjoint_Ico le_rfl), Ico, Ico, Ico, ← Finset.union_val,
    Finset.Ico_union_Ico_eq_Ico hab hbc]
Sum of Adjacent Closed-Open Interval Multisets: $[a, b) + [b, c) = [a, c)$ when $a \leq b \leq c$
Informal description
For any elements $a$, $b$, and $c$ in a locally finite order $\alpha$ such that $a \leq b \leq c$, the sum of the closed-open interval multisets $[a, b)$ and $[b, c)$ is equal to the closed-open interval multiset $[a, c)$. That is, $$ [a, b) + [b, c) = [a, c). $$
Multiset.Ico_inter_Ico theorem
: Ico a b ∩ Ico c d = Ico (max a c) (min b d)
Full source 
theorem Ico_inter_Ico : IcoIco a b ∩ Ico c d = Ico (max a c) (min b d) := by
  rw [Ico, Ico, Ico, ← Finset.inter_val, Finset.Ico_inter_Ico]
Intersection of Closed-Open Interval Multisets: $\text{Ico}(a, b) \cap \text{Ico}(c, d) = \text{Ico}(\max(a, c), \min(b, d))$
Informal description
For any elements $a, b, c, d$ in a locally finite order $\alpha$, the intersection of the closed-open interval multisets $\text{Ico}(a, b)$ and $\text{Ico}(c, d)$ is equal to the closed-open interval multiset $\text{Ico}(\max(a, c), \min(b, d))$. In symbols: \[ \text{Ico}(a, b) \cap \text{Ico}(c, d) = \text{Ico}(\max(a, c), \min(b, d)). \]
Multiset.Ico_filter_lt theorem
(a b c : α) : ((Ico a b).filter fun x => x < c) = Ico a (min b c)
Full source 
@[simp]
theorem Ico_filter_lt (a b c : α) : ((Ico a b).filter fun x => x < c) = Ico a (min b c) := by
  rw [Ico, Ico, ← Finset.filter_val, Finset.Ico_filter_lt]
Filtered Closed-Open Interval Equality: $\{x \in [a,b) \mid x < c\} = [a, \min(b,c))$
Informal description
For any elements $a, b, c$ in a locally finite order $\alpha$, the multiset obtained by filtering the closed-open interval $[a, b)$ to include only elements less than $c$ is equal to the closed-open interval $[a, \min(b, c))$. In other words: $$\{x \in [a, b) \mid x < c\} = [a, \min(b, c))$$
Multiset.Ico_filter_le theorem
(a b c : α) : ((Ico a b).filter fun x => c ≤ x) = Ico (max a c) b
Full source 
@[simp]
theorem Ico_filter_le (a b c : α) : ((Ico a b).filter fun x => c ≤ x) = Ico (max a c) b := by
  rw [Ico, Ico, ← Finset.filter_val, Finset.Ico_filter_le]
Filtered Closed-Open Interval Equality: $\{x \in [a,b) \mid c \leq x\} = [\max(a,c), b)$
Informal description
For any elements $a, b, c$ in a locally finite order $\alpha$, the multiset obtained by filtering the closed-open interval $[a, b)$ to retain only elements $x$ satisfying $c \leq x$ is equal to the closed-open interval $[\max(a, c), b)$. In other words: $$\text{filter} \ (x \mapsto c \leq x) \ [a, b) = [\max(a, c), b)$$
Multiset.Ico_sub_Ico_left theorem
(a b c : α) : Ico a b - Ico a c = Ico (max a c) b
Full source 
@[simp]
theorem Ico_sub_Ico_left (a b c : α) : Ico a b - Ico a c = Ico (max a c) b := by
  rw [Ico, Ico, Ico, ← Finset.sdiff_val, Finset.Ico_diff_Ico_left]
Multiset Difference of Closed-Open Intervals: $[a, b) \setminus [a, c) = [\max(a, c), b)$
Informal description
For any elements $a, b, c$ in a locally finite order $\alpha$, the multiset difference between the closed-open intervals $[a, b)$ and $[a, c)$ is equal to the closed-open interval $[\max(a, c), b)$. In symbols: $$ [a, b) \setminus [a, c) = [\max(a, c), b). $$
Multiset.Ico_sub_Ico_right theorem
(a b c : α) : Ico a b - Ico c b = Ico a (min b c)
Full source 
@[simp]
theorem Ico_sub_Ico_right (a b c : α) : Ico a b - Ico c b = Ico a (min b c) := by
  rw [Ico, Ico, Ico, ← Finset.sdiff_val, Finset.Ico_diff_Ico_right]
Multiset Difference of Closed-Open Intervals: $[a,b) \setminus [c,b) = [a,\min(b,c))$
Informal description
For any elements $a, b, c$ in a locally finite order $\alpha$, the multiset difference between the closed-open interval multisets $[a, b)$ and $[c, b)$ is equal to the closed-open interval multiset $[a, \min(b, c))$. In symbols: $$ [a, b) \setminus [c, b) = [a, \min(b, c)) $$