Documentation

Mathlib.Data.Int.Range

Intervals in ℤ #

This file defines integer ranges. range m n is the set of integers greater than m and strictly less than n.

Note #

This could be unified with Data.List.Intervals. See the TODOs there.

def Int.range (m : ) (n : ) :

List enumerating [m, n). This is the ℤ variant of List.Ico.

Equations
Instances For
    theorem Int.mem_range_iff {m : } {n : } {r : } :
    r m.range n m r r < n
    instance Int.decidableLELT (P : Prop) [DecidablePred P] (m : ) (n : ) :
    Decidable (∀ (r : ), m rr < nP r)
    Equations
    instance Int.decidableLELE (P : Prop) [DecidablePred P] (m : ) (n : ) :
    Decidable (∀ (r : ), m rr nP r)
    Equations
    instance Int.decidableLTLT (P : Prop) [DecidablePred P] (m : ) (n : ) :
    Decidable (∀ (r : ), m < rr < nP r)
    Equations
    instance Int.decidableLTLE (P : Prop) [DecidablePred P] (m : ) (n : ) :
    Decidable (∀ (r : ), m < rr nP r)
    Equations