Mathlib.Data.Multiset.Lattice

Multiset.sup definition

(s : Multiset α) : α

Full source

/-- Supremum of a multiset: `sup {a, b, c} = a ⊔ b ⊔ c` -/
def sup (s : Multiset α) : α :=
  s.fold (· ⊔ ·) ⊥

Supremum of a multiset

Informal description

Given a join-semilattice $\alpha$ with a bottom element $\bot$, the supremum of a multiset $s$ of elements in $\alpha$ is defined as the fold of the join operation $\sqcup$ over $s$ starting from $\bot$. More precisely, for a multiset $s = \{a_1, a_2, \dots, a_n\}$, the supremum is computed as $a_1 \sqcup a_2 \sqcup \dots \sqcup a_n$.

Multiset.sup_coe theorem

(l : List α) : sup (l : Multiset α) = l.foldr (· ⊔ ·) ⊥

Full source

@[simp]
theorem sup_coe (l : List α) : sup (l : Multiset α) = l.foldr (· ⊔ ·) ⊥ :=
  rfl

Supremum of a Multiset from a List Equals Right-Fold of Join Operation

Informal description

For any list $l$ of elements in a join-semilattice $\alpha$ with a bottom element $\bot$, the supremum of the multiset obtained from $l$ is equal to the right-fold of the join operation $\sqcup$ over $l$ starting from $\bot$. That is, $\sup(l) = \text{foldr}(\sqcup, \bot, l)$.

Multiset.sup_zero theorem

: (0 : Multiset α).sup = ⊥

Full source

@[simp]
theorem sup_zero : (0 : Multiset α).sup = ⊥ :=
  fold_zero _ _

Supremum of Empty Multiset is Bottom Element

Informal description

The supremum of the empty multiset in a join-semilattice $\alpha$ with a bottom element $\bot$ is equal to $\bot$, i.e., $\sup(\emptyset) = \bot$.

Multiset.sup_cons theorem

(a : α) (s : Multiset α) : (a ::ₘ s).sup = a ⊔ s.sup

Full source

@[simp]
theorem sup_cons (a : α) (s : Multiset α) : (a ::ₘ s).sup = a ⊔ s.sup :=
  fold_cons_left _ _ _ _

Supremum of a Multiset with Added Element: $\sup(a \cdot s) = a \sqcup \sup(s)$

Informal description

For any element $a$ in a join-semilattice $\alpha$ with a bottom element $\bot$, and any multiset $s$ of elements in $\alpha$, the supremum of the multiset obtained by adding $a$ to $s$ is equal to the join of $a$ and the supremum of $s$. That is, $\sup(a \cdot s) = a \sqcup \sup(s)$.

Multiset.sup_singleton theorem

{a : α} : ({ a } : Multiset α).sup = a

Full source

@[simp]
theorem sup_singleton {a : α} : ({a} : Multiset α).sup = a := sup_bot_eq _

Supremum of a Singleton Multiset

Informal description

For any element $a$ in a join-semilattice $\alpha$ with a bottom element $\bot$, the supremum of the singleton multiset $\{a\}$ is equal to $a$, i.e., $\sup(\{a\}) = a$.

Multiset.sup_add theorem

(s₁ s₂ : Multiset α) : (s₁ + s₂).sup = s₁.sup ⊔ s₂.sup

Full source

@[simp]
theorem sup_add (s₁ s₂ : Multiset α) : (s₁ + s₂).sup = s₁.sup ⊔ s₂.sup :=
  Eq.trans (by simp [sup]) (fold_add _ _ _ _ _)

Supremum of Multiset Sum Equals Join of Suprema

Informal description

For any two multisets $s₁$ and $s₂$ in a join-semilattice $\alpha$ with a bottom element, the supremum of their sum is equal to the join of their individual suprema, i.e., \[ (s₁ + s₂).\text{sup} = s₁.\text{sup} \sqcup s₂.\text{sup}. \]

Multiset.sup_le theorem

{s : Multiset α} {a : α} : s.sup ≤ a ↔ ∀ b ∈ s, b ≤ a

Full source

@[simp]
theorem sup_le {s : Multiset α} {a : α} : s.sup ≤ a ↔ ∀ b ∈ s, b ≤ a :=
  Multiset.induction_on s (by simp)
    (by simp +contextual [or_imp, forall_and])

Supremum of Multiset is Least Upper Bound

Informal description

For a multiset $s$ in a join-semilattice $\alpha$ with a bottom element $\bot$, the supremum of $s$ is less than or equal to an element $a \in \alpha$ if and only if every element $b$ in $s$ satisfies $b \leq a$. In other words: \[ \sup(s) \leq a \leftrightarrow \forall b \in s, b \leq a. \]

Multiset.le_sup theorem

{s : Multiset α} {a : α} (h : a ∈ s) : a ≤ s.sup

Full source

theorem le_sup {s : Multiset α} {a : α} (h : a ∈ s) : a ≤ s.sup :=
  sup_le.1 le_rfl _ h

Element in Multiset is Less Than or Equal to its Supremum

Informal description

For any multiset $s$ in a join-semilattice $\alpha$ with a bottom element $\bot$, and any element $a \in s$, we have $a \leq \sup(s)$.

Multiset.sup_mono theorem

{s₁ s₂ : Multiset α} (h : s₁ ⊆ s₂) : s₁.sup ≤ s₂.sup

Full source

@[gcongr]
theorem sup_mono {s₁ s₂ : Multiset α} (h : s₁ ⊆ s₂) : s₁.sup ≤ s₂.sup :=
  sup_le.2 fun _ hb => le_sup (h hb)

Monotonicity of Supremum for Multiset Inclusion: $s₁ \subseteq s₂ \implies \sup(s₁) \leq \sup(s₂)$

Informal description

For any two multisets $s₁$ and $s₂$ in a join-semilattice $\alpha$ with a bottom element $\bot$, if $s₁$ is a submultiset of $s₂$, then the supremum of $s₁$ is less than or equal to the supremum of $s₂$, i.e., \[ s₁ \subseteq s₂ \implies \sup(s₁) \leq \sup(s₂). \]

Multiset.sup_dedup theorem

(s : Multiset α) : (dedup s).sup = s.sup

Full source

@[simp]
theorem sup_dedup (s : Multiset α) : (dedup s).sup = s.sup :=
  fold_dedup_idem _ _ _

Supremum Invariance under Deduplication: $\sup(\text{dedup } s) = \sup s$

Informal description

For any multiset $s$ with elements in a join-semilattice $\alpha$ with a bottom element $\bot$, the supremum of the deduplicated version of $s$ is equal to the supremum of $s$ itself. That is, $\sup(\text{dedup } s) = \sup s$.

Multiset.sup_ndunion theorem

(s₁ s₂ : Multiset α) : (ndunion s₁ s₂).sup = s₁.sup ⊔ s₂.sup

Full source

@[simp]
theorem sup_ndunion (s₁ s₂ : Multiset α) : (ndunion s₁ s₂).sup = s₁.sup ⊔ s₂.sup := by
  rw [← sup_dedup, dedup_ext.2, sup_dedup, sup_add]; simp

Supremum of Nondisjoint Union Equals Join of Suprema

Informal description

For any two multisets $s₁$ and $s₂$ in a join-semilattice $\alpha$ with a bottom element, the supremum of their nondisjoint union is equal to the join of their individual suprema, i.e., \[ \text{sup}(\text{ndunion } s₁ s₂) = \text{sup}(s₁) \sqcup \text{sup}(s₂). \]

Multiset.sup_union theorem

(s₁ s₂ : Multiset α) : (s₁ ∪ s₂).sup = s₁.sup ⊔ s₂.sup

Full source

@[simp]
theorem sup_union (s₁ s₂ : Multiset α) : (s₁ ∪ s₂).sup = s₁.sup ⊔ s₂.sup := by
  rw [← sup_dedup, dedup_ext.2, sup_dedup, sup_add]; simp

Supremum of Multiset Union Equals Join of Suprema

Informal description

For any two multisets $s₁$ and $s₂$ with elements in a join-semilattice $\alpha$ with a bottom element $\bot$, the supremum of their union is equal to the join of their individual suprema, i.e., \[ (s₁ \cup s₂).\text{sup} = s₁.\text{sup} \sqcup s₂.\text{sup}. \]

Multiset.sup_ndinsert theorem

(a : α) (s : Multiset α) : (ndinsert a s).sup = a ⊔ s.sup

Full source

@[simp]
theorem sup_ndinsert (a : α) (s : Multiset α) : (ndinsert a s).sup = a ⊔ s.sup := by
  rw [← sup_dedup, dedup_ext.2, sup_dedup, sup_cons]; simp

Supremum of Multiset Insertion: $\sup(\text{ndinsert}(a, s)) = a \sqcup \sup(s)$

Informal description

For any element $a$ in a join-semilattice $\alpha$ with a bottom element $\bot$, and any multiset $s$ of elements in $\alpha$, the supremum of the multiset obtained by inserting $a$ into $s$ (without duplicates) is equal to the join of $a$ and the supremum of $s$. That is, $\sup(\text{ndinsert}(a, s)) = a \sqcup \sup(s)$.

Multiset.nodup_sup_iff theorem

{α : Type*} [DecidableEq α] {m : Multiset (Multiset α)} : m.sup.Nodup ↔ ∀ a : Multiset α, a ∈ m → a.Nodup

Full source

theorem nodup_sup_iff {α : Type*} [DecidableEq α] {m : Multiset (Multiset α)} :
    m.sup.Nodup ↔ ∀ a : Multiset α, a ∈ m → a.Nodup := by
  induction m using Multiset.induction_on with
  | empty => simp
  | cons _ _ h => simp [h]

Supremum of a Multiset of Multisets Has No Duplicates if and only if All Constituent Multisets Have No Duplicates

Informal description

For a multiset $m$ of multisets over a type $\alpha$ with decidable equality, the supremum of $m$ has no duplicate elements if and only if every multiset $a$ in $m$ has no duplicate elements.

Multiset.inf definition

(s : Multiset α) : α

Full source

/-- Infimum of a multiset: `inf {a, b, c} = a ⊓ b ⊓ c` -/
def inf (s : Multiset α) : α :=
  s.fold (· ⊓ ·) ⊤

Infimum of a multiset

Informal description

Given a meet-semilattice $\alpha$ with a top element $\top$, the infimum of a multiset $s$ is defined by folding the meet operation $\sqcap$ over $s$ starting from $\top$. For example, $\text{inf} \{a, b, c\} = a \sqcap b \sqcap c$.

Multiset.inf_coe theorem

(l : List α) : inf (l : Multiset α) = l.foldr (· ⊓ ·) ⊤

Full source

@[simp]
theorem inf_coe (l : List α) : inf (l : Multiset α) = l.foldr (· ⊓ ·) ⊤ :=
  rfl

Infimum of Multiset from List Equals Right-Fold of Meet Operation

Informal description

For any list $l$ of elements in a meet-semilattice $\alpha$ with a top element $\top$, the infimum of the multiset obtained from $l$ is equal to the right-fold of the meet operation $\sqcap$ over $l$ starting from $\top$. That is, $\text{inf}(l) = \text{foldr}(\sqcap, \top, l)$.

Multiset.inf_zero theorem

: (0 : Multiset α).inf = ⊤

Full source

@[simp]
theorem inf_zero : (0 : Multiset α).inf = ⊤ :=
  fold_zero _ _

Infimum of Empty Multiset is Top Element

Informal description

The infimum of the empty multiset in a meet-semilattice $\alpha$ with a top element $\top$ is equal to $\top$, i.e., $\inf(\emptyset) = \top$.

Multiset.inf_cons theorem

(a : α) (s : Multiset α) : (a ::ₘ s).inf = a ⊓ s.inf

Full source

@[simp]
theorem inf_cons (a : α) (s : Multiset α) : (a ::ₘ s).inf = a ⊓ s.inf :=
  fold_cons_left _ _ _ _

Infimum of a Multiset After Insertion: $\text{inf}(a \cdot s) = a \sqcap \text{inf}(s)$

Informal description

For any element $a$ in a meet-semilattice $\alpha$ with a top element $\top$, and any multiset $s$ over $\alpha$, the infimum of the multiset obtained by adding $a$ to $s$ is equal to the meet of $a$ and the infimum of $s$, i.e., $\text{inf}(a \cdot s) = a \sqcap \text{inf}(s)$.

Multiset.inf_singleton theorem

{a : α} : ({ a } : Multiset α).inf = a

Full source

@[simp]
theorem inf_singleton {a : α} : ({a} : Multiset α).inf = a := inf_top_eq _

Infimum of Singleton Multiset is the Element Itself

Informal description

For any element $a$ in a meet-semilattice $\alpha$ with a top element $\top$, the infimum of the singleton multiset $\{a\}$ is equal to $a$, i.e., $\inf(\{a\}) = a$.

Multiset.inf_add theorem

(s₁ s₂ : Multiset α) : (s₁ + s₂).inf = s₁.inf ⊓ s₂.inf

Full source

@[simp]
theorem inf_add (s₁ s₂ : Multiset α) : (s₁ + s₂).inf = s₁.inf ⊓ s₂.inf :=
  Eq.trans (by simp [inf]) (fold_add _ _ _ _ _)

Infimum of Multiset Sum Equals Meet of Infima

Informal description

For any two multisets $s₁$ and $s₂$ in a meet-semilattice $\alpha$ with a top element, the infimum of their sum equals the meet of their individual infima, i.e., \[ \inf(s₁ + s₂) = \inf(s₁) \sqcap \inf(s₂). \]

Multiset.le_inf theorem

{s : Multiset α} {a : α} : a ≤ s.inf ↔ ∀ b ∈ s, a ≤ b

Full source

@[simp]
theorem le_inf {s : Multiset α} {a : α} : a ≤ s.inf ↔ ∀ b ∈ s, a ≤ b :=
  Multiset.induction_on s (by simp)
    (by simp +contextual [or_imp, forall_and])

Characterization of Infimum in Multisets: $a \leq \inf(s) \leftrightarrow \forall b \in s, a \leq b$

Informal description

For any multiset $s$ over a meet-semilattice $\alpha$ with a top element $\top$, and any element $a \in \alpha$, the inequality $a \leq \inf(s)$ holds if and only if $a \leq b$ for every element $b$ in $s$.

Multiset.inf_le theorem

{s : Multiset α} {a : α} (h : a ∈ s) : s.inf ≤ a

Full source

theorem inf_le {s : Multiset α} {a : α} (h : a ∈ s) : s.inf ≤ a :=
  le_inf.1 le_rfl _ h

Infimum of a Multiset is a Lower Bound

Informal description

For any multiset $s$ over a meet-semilattice $\alpha$ with a top element, and any element $a \in s$, the infimum of $s$ is less than or equal to $a$, i.e., $\inf(s) \leq a$.

Multiset.inf_mono theorem

{s₁ s₂ : Multiset α} (h : s₁ ⊆ s₂) : s₂.inf ≤ s₁.inf

Full source

@[gcongr]
theorem inf_mono {s₁ s₂ : Multiset α} (h : s₁ ⊆ s₂) : s₂.inf ≤ s₁.inf :=
  le_inf.2 fun _ hb => inf_le (h hb)

Monotonicity of Infimum under Subset Inclusion: $\inf(s_2) \leq \inf(s_1)$ when $s_1 \subseteq s_2$

Informal description

For any two multisets $s_1$ and $s_2$ in a meet-semilattice $\alpha$ with a top element, if $s_1$ is a subset of $s_2$, then the infimum of $s_2$ is less than or equal to the infimum of $s_1$, i.e., $\inf(s_2) \leq \inf(s_1)$.

Multiset.inf_dedup theorem

(s : Multiset α) : (dedup s).inf = s.inf

Full source

@[simp]
theorem inf_dedup (s : Multiset α) : (dedup s).inf = s.inf :=
  fold_dedup_idem _ _ _

Infimum Invariance under Deduplication

Informal description

For any multiset $s$ with elements in a meet-semilattice $\alpha$, the infimum of the deduplicated version of $s$ is equal to the infimum of $s$ itself, i.e., $\inf(\text{dedup } s) = \inf s$.

Multiset.inf_ndunion theorem

(s₁ s₂ : Multiset α) : (ndunion s₁ s₂).inf = s₁.inf ⊓ s₂.inf

Full source

@[simp]
theorem inf_ndunion (s₁ s₂ : Multiset α) : (ndunion s₁ s₂).inf = s₁.inf ⊓ s₂.inf := by
  rw [← inf_dedup, dedup_ext.2, inf_dedup, inf_add]; simp

Infimum of Nondisjoint Union Equals Meet of Infima

Informal description

For any two multisets $s₁$ and $s₂$ in a meet-semilattice $\alpha$ with a top element, the infimum of their nondisjoint union equals the meet of their individual infima, i.e., \[ \inf(\text{ndunion } s₁ s₂) = \inf s₁ \sqcap \inf s₂. \]

Multiset.inf_union theorem

(s₁ s₂ : Multiset α) : (s₁ ∪ s₂).inf = s₁.inf ⊓ s₂.inf

Full source

@[simp]
theorem inf_union (s₁ s₂ : Multiset α) : (s₁ ∪ s₂).inf = s₁.inf ⊓ s₂.inf := by
  rw [← inf_dedup, dedup_ext.2, inf_dedup, inf_add]; simp

Infimum of Multiset Union Equals Meet of Infima

Informal description

For any two multisets $s₁$ and $s₂$ with elements in a meet-semilattice $\alpha$, the infimum of their union equals the meet of their individual infima, i.e., \[ \inf(s₁ \cup s₂) = \inf(s₁) \sqcap \inf(s₂). \]

Multiset.inf_ndinsert theorem

(a : α) (s : Multiset α) : (ndinsert a s).inf = a ⊓ s.inf

Full source

@[simp]
theorem inf_ndinsert (a : α) (s : Multiset α) : (ndinsert a s).inf = a ⊓ s.inf := by
  rw [← inf_dedup, dedup_ext.2, inf_dedup, inf_cons]; simp

Infimum of Nondependent Insertion in Multiset: $\inf(\text{ndinsert}(a, s)) = a \sqcap \inf(s)$

Informal description

Let $\alpha$ be a meet-semilattice with a top element $\top$. For any element $a \in \alpha$ and any multiset $s$ over $\alpha$, the infimum of the multiset obtained by inserting $a$ into $s$ (without duplicates) equals the meet of $a$ and the infimum of $s$, i.e., \[ \inf(\text{ndinsert}(a, s)) = a \sqcap \inf(s) \] where $\text{ndinsert}(a, s)$ denotes the insertion of $a$ into $s$ while maintaining no duplicates, and $\sqcap$ is the meet operation.