mathlib documentation


multiset.range n gives {0, 1, ..., n-1} as a multiset. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

range n is the multiset lifted from the list range n, that is, the set {0, 1, ..., n-1}.

theorem multiset.mem_range {m n : } :
theorem multiset.range_add (a b : ) :