Documentation

Mathlib.Data.Multiset.Range

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

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

Equations
    Instances For
      @[simp]
      @[simp]
      @[simp]
      theorem Multiset.card_range (n : ) :
      (range n).card = n
      @[simp]
      theorem Multiset.mem_range {m n : } :
      m range n m < n
      @[deprecated Multiset.notMem_range_self (since := "2025-05-23")]
      theorem Multiset.not_mem_range_self {n : } :
      nrange n

      Alias of Multiset.notMem_range_self.

      theorem Multiset.range_add (a b : ) :
      range (a + b) = range a + map (fun (x : ) => a + x) (range b)
      theorem Multiset.range_disjoint_map_add (a : ) (m : Multiset ) :
      Disjoint (range a) (map (fun (x : ) => a + x) m)
      theorem Multiset.range_add_eq_union (a b : ) :
      range (a + b) = range a map (fun (x : ) => a + x) (range b)
      theorem Multiset.range_le {m n : } :