Documentation

Mathlib.Data.Multiset.Lattice

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
Instances For
    @[simp]
    theorem Multiset.sup_coe {α : Type u_1} [SemilatticeSup α] [OrderBot α] (l : List α) :
    (↑l).sup = List.foldr (fun (x1 x2 : α) => x1 x2) l
    @[simp]
    @[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 bs, 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 am, 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
    Instances For
      @[simp]
      theorem Multiset.inf_coe {α : Type u_1} [SemilatticeInf α] [OrderTop α] (l : List α) :
      (↑l).inf = List.foldr (fun (x1 x2 : α) => x1 x2) l
      @[simp]
      @[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 bs, 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