Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-07-19 09:29 1e0c38b0

View on Github →

feat(data/multiset): sup and inf for multisets

Estimated changes

added theorem finset.inf_val
added theorem finset.sup_val
added def multiset.inf
added theorem multiset.inf_add
added theorem multiset.inf_cons
added theorem multiset.inf_erase_dup
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 def multiset.sup
added theorem multiset.sup_add
added theorem multiset.sup_cons
added theorem multiset.sup_erase_dup
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