Theorems · Theorem · order theory

Multiset.inf_ndinsert

∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderTop α] [inst_2 : DecidableEq α] (a : α) (s : Multiset α),
  (Multiset.ndinsert a s).inf = a ⊓ s.inf

Defined in

Mathlib.Data.Multiset.Lattice

Cited by

0 results in Mathlib

Foundations

Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemilatticeInfOrderTopDecidableEq