# 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
theorem Int.mem_range_iff {m : } {n : } {r : } :
r m r r < n
instance Int.decidableLELT (P : ) [inst : ] (m : ) (n : ) :
Decidable ((r : ) → m rr < nP r)
Equations
instance Int.decidableLELE (P : ) [inst : ] (m : ) (n : ) :
Decidable ((r : ) → m rr nP r)
Equations
instance Int.decidableLTLT (P : ) [inst : ] (m : ) (n : ) :
Decidable ((r : ) → m < rr < nP r)
Equations
instance Int.decidableLTLE (P : ) [inst : ] (m : ) (n : ) :
Decidable ((r : ) → m < rr nP r)
Equations