Documentation

Mathlib.Data.Multiset.Lattice

Lattice operations on multisets #

sup #

def Multiset.sup {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] (s : Multiset α) :
α

Supremum of a multiset: sup {a, b, c} = a ⊔ b ⊔ c

Equations
@[simp]
theorem Multiset.sup_coe {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] (l : List α) :
Multiset.sup l = List.foldr (fun x x_1 => x x_1) l
@[simp]
theorem Multiset.sup_zero {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] :
@[simp]
theorem Multiset.sup_cons {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] (a : α) (s : Multiset α) :
@[simp]
theorem Multiset.sup_singleton {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] {a : α} :
@[simp]
theorem Multiset.sup_add {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] (s₁ : Multiset α) (s₂ : Multiset α) :
theorem Multiset.sup_le {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] {s : Multiset α} {a : α} :
Multiset.sup s a ∀ (b : α), b sb a
theorem Multiset.le_sup {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] {s : Multiset α} {a : α} (h : a s) :
theorem Multiset.sup_mono {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] {s₁ : Multiset α} {s₂ : Multiset α} (h : s₁ s₂) :
@[simp]
theorem Multiset.sup_dedup {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] [inst : DecidableEq α] (s : Multiset α) :
@[simp]
theorem Multiset.sup_ndunion {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] [inst : DecidableEq α] (s₁ : Multiset α) (s₂ : Multiset α) :
@[simp]
theorem Multiset.sup_union {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] [inst : DecidableEq α] (s₁ : Multiset α) (s₂ : Multiset α) :
@[simp]
theorem Multiset.sup_ndinsert {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] [inst : DecidableEq α] (a : α) (s : Multiset α) :
theorem Multiset.nodup_sup_iff {α : Type u_1} [inst : DecidableEq α] {m : Multiset (Multiset α)} :

inf #

def Multiset.inf {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] (s : Multiset α) :
α

Infimum of a multiset: inf {a, b, c} = a ⊓ b ⊓ c

Equations
@[simp]
theorem Multiset.inf_coe {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] (l : List α) :
Multiset.inf l = List.foldr (fun x x_1 => x x_1) l
@[simp]
theorem Multiset.inf_zero {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] :
@[simp]
theorem Multiset.inf_cons {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] (a : α) (s : Multiset α) :
@[simp]
theorem Multiset.inf_singleton {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] {a : α} :
@[simp]
theorem Multiset.inf_add {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] (s₁ : Multiset α) (s₂ : Multiset α) :
theorem Multiset.le_inf {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] {s : Multiset α} {a : α} :
a Multiset.inf s ∀ (b : α), b sa b
theorem Multiset.inf_le {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] {s : Multiset α} {a : α} (h : a s) :
theorem Multiset.inf_mono {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] {s₁ : Multiset α} {s₂ : Multiset α} (h : s₁ s₂) :
@[simp]
theorem Multiset.inf_dedup {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] [inst : DecidableEq α] (s : Multiset α) :
@[simp]
theorem Multiset.inf_ndunion {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] [inst : DecidableEq α] (s₁ : Multiset α) (s₂ : Multiset α) :
@[simp]
theorem Multiset.inf_union {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] [inst : DecidableEq α] (s₁ : Multiset α) (s₂ : Multiset α) :
@[simp]
theorem Multiset.inf_ndinsert {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] [inst : DecidableEq α] (a : α) (s : Multiset α) :