Lattice operations on multisets #

sup #

source

ink

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

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

Equations

Multiset.sup s = Multiset.fold (fun x x_1 => x ⊔ x_1) ⊥ s

source

ink

@[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

source

ink

@[simp]

theorem Multiset.sup_zero {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] :

Multiset.sup 0 = ⊥

source

ink

@[simp]

theorem Multiset.sup_cons {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] (a : α) (s : Multiset α) :

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

source

ink

@[simp]

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

Multiset.sup {a} = a

source

ink

@[simp]

theorem Multiset.sup_add {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] (s₁ : Multiset α) (s₂ : Multiset α) :

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

source

ink

theorem Multiset.sup_le {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] {s : Multiset α} {a : α} :

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

source

ink

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

a ≤ Multiset.sup s

source

ink

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

Multiset.sup s₁ ≤ Multiset.sup s₂

source

ink

@[simp]

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

Multiset.sup (Multiset.dedup s) = Multiset.sup s

source

ink

@[simp]

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

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

source

ink

@[simp]

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

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

source

ink

@[simp]

theorem Multiset.sup_ndinsert {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderBot α] [inst : DecidableEq α] (a : α) (s : Multiset α) :

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

source

ink

theorem Multiset.nodup_sup_iff {α : Type u_1} [inst : DecidableEq α] {m : Multiset (Multiset α)} :

Multiset.Nodup (Multiset.sup m) ↔ ∀ (a : Multiset α), a ∈ m → Multiset.Nodup a

inf #

source

ink

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

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

Equations

Multiset.inf s = Multiset.fold (fun x x_1 => x ⊓ x_1) ⊤ s

source

ink

@[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

source

ink

@[simp]

theorem Multiset.inf_zero {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] :

Multiset.inf 0 = ⊤

source

ink

@[simp]

theorem Multiset.inf_cons {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] (a : α) (s : Multiset α) :

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

source

ink

@[simp]

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

Multiset.inf {a} = a

source

ink

@[simp]

theorem Multiset.inf_add {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] (s₁ : Multiset α) (s₂ : Multiset α) :

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

source

ink

theorem Multiset.le_inf {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] {s : Multiset α} {a : α} :

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

source

ink

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

Multiset.inf s ≤ a

source

ink

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

Multiset.inf s₂ ≤ Multiset.inf s₁

source

ink

@[simp]

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

Multiset.inf (Multiset.dedup s) = Multiset.inf s

source

ink

@[simp]

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

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

source

ink

@[simp]

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

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

source

ink

@[simp]

theorem Multiset.inf_ndinsert {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderTop α] [inst : DecidableEq α] (a : α) (s : Multiset α) :

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