mathlib documentation

data.multiset.lattice

Lattice operations on multisets

sup

def multiset.sup {α : Type u_1} [semilattice_sup_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_zero {α : Type u_1} [semilattice_sup_bot α] :

@[simp]

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

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

@[simp]

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

(a :: 0).sup = a

@[simp]

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

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

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

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

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

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

s₁.sup ≤ s₂.sup

@[simp]

theorem multiset.sup_erase_dup {α : Type u_1} [semilattice_sup_bot α] [decidable_eq α] (s : multiset α) :

s.erase_dup.sup = s.sup

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

inf

def multiset.inf {α : Type u_1} [semilattice_inf_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_zero {α : Type u_1} [semilattice_inf_top α] :

@[simp]

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

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

@[simp]

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

(a :: 0).inf = a

@[simp]

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

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

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

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

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

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

s₂.inf ≤ s₁.inf

@[simp]

theorem multiset.inf_erase_dup {α : Type u_1} [semilattice_inf_top α] [decidable_eq α] (s : multiset α) :

s.erase_dup.inf = s.inf

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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