Commit 2023-01-14 04:12 3d0594fc

View on Github →

feat: port Data.Multiset.Lattice (#1556)

Estimated changes

added def Multiset.inf
added theorem Multiset.inf_add
added theorem Multiset.inf_coe
added theorem Multiset.inf_cons
added theorem Multiset.inf_dedup
added theorem Multiset.inf_le
added theorem Multiset.inf_mono
added theorem Multiset.inf_ndinsert
added theorem Multiset.inf_ndunion
added theorem Multiset.inf_singleton
added theorem Multiset.inf_union
added theorem Multiset.inf_zero
added theorem Multiset.le_inf
added theorem Multiset.le_sup
added theorem Multiset.nodup_sup_iff
added def Multiset.sup
added theorem Multiset.sup_add
added theorem Multiset.sup_coe
added theorem Multiset.sup_cons
added theorem Multiset.sup_dedup
added theorem Multiset.sup_le
added theorem Multiset.sup_mono
added theorem Multiset.sup_ndinsert
added theorem Multiset.sup_ndunion
added theorem Multiset.sup_singleton
added theorem Multiset.sup_union
added theorem Multiset.sup_zero