mathlib3 documentation

data.multiset.lattice

Lattice operations on multisets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

sup #

def multiset.sup {α : Type u_1} [semilattice_sup α] [order_bot α] (s : multiset α) :

α

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

Equations

s.sup = multiset.fold has_sup.sup ⊥ s

@[simp]

theorem multiset.sup_coe {α : Type u_1} [semilattice_sup α] [order_bot α] (l : list α) :

↑l.sup = list.foldr has_sup.sup ⊥ l

@[simp]

theorem multiset.sup_zero {α : Type u_1} [semilattice_sup α] [order_bot α] :

@[simp]

theorem multiset.sup_cons {α : Type u_1} [semilattice_sup α] [order_bot α] (a : α) (s : multiset α) :

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

@[simp]

theorem multiset.sup_singleton {α : Type u_1} [semilattice_sup α] [order_bot α] {a : α} :

{a}.sup = a

@[simp]

theorem multiset.sup_add {α : Type u_1} [semilattice_sup α] [order_bot α] (s₁ s₂ : multiset α) :

(s₁ + s₂).sup = s₁.sup ⊔ s₂.sup

@[simp]

theorem multiset.sup_le {α : Type u_1} [semilattice_sup α] [order_bot α] {s : multiset α} {a : α} :

s.sup ≤ a ↔ ∀ (b : α), b ∈ s → b ≤ a

theorem multiset.le_sup {α : Type u_1} [semilattice_sup α] [order_bot α] {s : multiset α} {a : α} (h : a ∈ s) :

theorem multiset.sup_mono {α : Type u_1} [semilattice_sup α] [order_bot α] {s₁ s₂ : multiset α} (h : s₁ ⊆ s₂) :

s₁.sup ≤ s₂.sup

@[simp]

theorem multiset.sup_dedup {α : Type u_1} [semilattice_sup α] [order_bot α] [decidable_eq α] (s : multiset α) :

s.dedup.sup = s.sup

@[simp]

theorem multiset.sup_ndunion {α : Type u_1} [semilattice_sup α] [order_bot α] [decidable_eq α] (s₁ s₂ : multiset α) :

(s₁.ndunion s₂).sup = s₁.sup ⊔ s₂.sup

@[simp]

theorem multiset.sup_union {α : Type u_1} [semilattice_sup α] [order_bot α] [decidable_eq α] (s₁ s₂ : multiset α) :

(s₁ ∪ s₂).sup = s₁.sup ⊔ s₂.sup

@[simp]

theorem multiset.sup_ndinsert {α : Type u_1} [semilattice_sup α] [order_bot α] [decidable_eq α] (a : α) (s : multiset α) :

(multiset.ndinsert a s).sup = a ⊔ s.sup

theorem multiset.nodup_sup_iff {α : Type u_1} [decidable_eq α] {m : multiset (multiset α)} :

m.sup.nodup ↔ ∀ (a : multiset α), a ∈ m → a.nodup

inf #

def multiset.inf {α : Type u_1} [semilattice_inf α] [order_top α] (s : multiset α) :

α

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

Equations

s.inf = multiset.fold has_inf.inf ⊤ s

@[simp]

theorem multiset.inf_coe {α : Type u_1} [semilattice_inf α] [order_top α] (l : list α) :

↑l.inf = list.foldr has_inf.inf ⊤ l

@[simp]

theorem multiset.inf_zero {α : Type u_1} [semilattice_inf α] [order_top α] :

@[simp]

theorem multiset.inf_cons {α : Type u_1} [semilattice_inf α] [order_top α] (a : α) (s : multiset α) :

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

@[simp]

theorem multiset.inf_singleton {α : Type u_1} [semilattice_inf α] [order_top α] {a : α} :

{a}.inf = a

@[simp]

theorem multiset.inf_add {α : Type u_1} [semilattice_inf α] [order_top α] (s₁ s₂ : multiset α) :

(s₁ + s₂).inf = s₁.inf ⊓ s₂.inf

theorem multiset.le_inf {α : Type u_1} [semilattice_inf α] [order_top α] {s : multiset α} {a : α} :

a ≤ s.inf ↔ ∀ (b : α), b ∈ s → a ≤ b

theorem multiset.inf_le {α : Type u_1} [semilattice_inf α] [order_top α] {s : multiset α} {a : α} (h : a ∈ s) :

theorem multiset.inf_mono {α : Type u_1} [semilattice_inf α] [order_top α] {s₁ s₂ : multiset α} (h : s₁ ⊆ s₂) :

s₂.inf ≤ s₁.inf

@[simp]

theorem multiset.inf_dedup {α : Type u_1} [semilattice_inf α] [order_top α] [decidable_eq α] (s : multiset α) :

s.dedup.inf = s.inf

@[simp]

theorem multiset.inf_ndunion {α : Type u_1} [semilattice_inf α] [order_top α] [decidable_eq α] (s₁ s₂ : multiset α) :

(s₁.ndunion s₂).inf = s₁.inf ⊓ s₂.inf

@[simp]

theorem multiset.inf_union {α : Type u_1} [semilattice_inf α] [order_top α] [decidable_eq α] (s₁ s₂ : multiset α) :

(s₁ ∪ s₂).inf = s₁.inf ⊓ s₂.inf

@[simp]

theorem multiset.inf_ndinsert {α : Type u_1} [semilattice_inf α] [order_top α] [decidable_eq α] (a : α) (s : multiset α) :

(multiset.ndinsert a s).inf = a ⊓ s.inf