Lattice operations on multisets

sup

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

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

Equations

• s.sup = Multiset.fold (fun (x1 x2 : α) => x1 ⊔ x2) ⊥ s

@[simp]

theorem Multiset.sup_coe {α : Type u_1} [SemilatticeSup α] [OrderBot α] (l : List α) : (↑l).sup = List.foldr (fun (x1 x2 : α) => x1 ⊔ x2) ⊥ l

@[simp]

theorem Multiset.sup_zero {α : Type u_1} [SemilatticeSup α] [OrderBot α] : Multiset.sup 0 = ⊥

@[simp]

theorem Multiset.sup_cons {α : Type u_1} [SemilatticeSup α] [OrderBot α] (a : α) (s : Multiset α) : (a ::ₘ s).sup = a ⊔ s.sup

@[simp]

theorem Multiset.sup_singleton {α : Type u_1} [SemilatticeSup α] [OrderBot α] {a : α} : {a}.sup = a

@[simp]

theorem Multiset.sup_add {α : Type u_1} [SemilatticeSup α] [OrderBot α] (s₁ : Multiset α) (s₂ : Multiset α) : (s₁ + s₂).sup = s₁.sup ⊔ s₂.sup

@[simp]

theorem Multiset.sup_le {α : Type u_1} [SemilatticeSup α] [OrderBot α] {s : Multiset α} {a : α} : s.sup ≤ a ↔ ∀ b ∈ s, b ≤ a

theorem Multiset.le_sup {α : Type u_1} [SemilatticeSup α] [OrderBot α] {s : Multiset α} {a : α} (h : a ∈ s) : a ≤ s.sup

theorem Multiset.sup_mono {α : Type u_1} [SemilatticeSup α] [OrderBot α] {s₁ : Multiset α} {s₂ : Multiset α} (h : s₁ ⊆ s₂) : s₁.sup ≤ s₂.sup

@[simp]

theorem Multiset.sup_dedup {α : Type u_1} [SemilatticeSup α] [OrderBot α] [DecidableEq α] (s : Multiset α) : s.dedup.sup = s.sup

@[simp]

theorem Multiset.sup_ndunion {α : Type u_1} [SemilatticeSup α] [OrderBot α] [DecidableEq α] (s₁ : Multiset α) (s₂ : Multiset α) : (s₁.ndunion s₂).sup = s₁.sup ⊔ s₂.sup

@[simp]

theorem Multiset.sup_union {α : Type u_1} [SemilatticeSup α] [OrderBot α] [DecidableEq α] (s₁ : Multiset α) (s₂ : Multiset α) : (s₁ ∪ s₂).sup = s₁.sup ⊔ s₂.sup

@[simp]

theorem Multiset.sup_ndinsert {α : Type u_1} [SemilatticeSup α] [OrderBot α] [DecidableEq α] (a : α) (s : Multiset α) : (Multiset.ndinsert a s).sup = a ⊔ s.sup

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

inf

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

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

Equations

• s.inf = Multiset.fold (fun (x1 x2 : α) => x1 ⊓ x2) ⊤ s

@[simp]

theorem Multiset.inf_coe {α : Type u_1} [SemilatticeInf α] [OrderTop α] (l : List α) : (↑l).inf = List.foldr (fun (x1 x2 : α) => x1 ⊓ x2) ⊤ l

@[simp]

theorem Multiset.inf_zero {α : Type u_1} [SemilatticeInf α] [OrderTop α] : Multiset.inf 0 = ⊤

@[simp]

theorem Multiset.inf_cons {α : Type u_1} [SemilatticeInf α] [OrderTop α] (a : α) (s : Multiset α) : (a ::ₘ s).inf = a ⊓ s.inf

@[simp]

theorem Multiset.inf_singleton {α : Type u_1} [SemilatticeInf α] [OrderTop α] {a : α} : {a}.inf = a

@[simp]

theorem Multiset.inf_add {α : Type u_1} [SemilatticeInf α] [OrderTop α] (s₁ : Multiset α) (s₂ : Multiset α) : (s₁ + s₂).inf = s₁.inf ⊓ s₂.inf

@[simp]

theorem Multiset.le_inf {α : Type u_1} [SemilatticeInf α] [OrderTop α] {s : Multiset α} {a : α} : a ≤ s.inf ↔ ∀ b ∈ s, a ≤ b

theorem Multiset.inf_le {α : Type u_1} [SemilatticeInf α] [OrderTop α] {s : Multiset α} {a : α} (h : a ∈ s) : s.inf ≤ a

theorem Multiset.inf_mono {α : Type u_1} [SemilatticeInf α] [OrderTop α] {s₁ : Multiset α} {s₂ : Multiset α} (h : s₁ ⊆ s₂) : s₂.inf ≤ s₁.inf

@[simp]

theorem Multiset.inf_dedup {α : Type u_1} [SemilatticeInf α] [OrderTop α] [DecidableEq α] (s : Multiset α) : s.dedup.inf = s.inf

@[simp]

theorem Multiset.inf_ndunion {α : Type u_1} [SemilatticeInf α] [OrderTop α] [DecidableEq α] (s₁ : Multiset α) (s₂ : Multiset α) : (s₁.ndunion s₂).inf = s₁.inf ⊓ s₂.inf

@[simp]

theorem Multiset.inf_union {α : Type u_1} [SemilatticeInf α] [OrderTop α] [DecidableEq α] (s₁ : Multiset α) (s₂ : Multiset α) : (s₁ ∪ s₂).inf = s₁.inf ⊓ s₂.inf

@[simp]

theorem Multiset.inf_ndinsert {α : Type u_1} [SemilatticeInf α] [OrderTop α] [DecidableEq α] (a : α) (s : Multiset α) : (Multiset.ndinsert a s).inf = a ⊓ s.inf