mathlib documentation

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.range n m r r < n
@[protected, instance]
def int.decidable_le_lt (P : → Prop) [decidable_pred P] (m n : ) :
decidable (∀ (r : ), m rr < nP r)
Equations
@[protected, instance]
def int.decidable_le_le (P : → Prop) [decidable_pred P] (m n : ) :
decidable (∀ (r : ), m rr nP r)
Equations
@[protected, instance]
def int.decidable_lt_lt (P : → Prop) [decidable_pred P] (m n : ) :
decidable (∀ (r : ), m < rr < nP r)
Equations
@[protected, instance]
def int.decidable_lt_le (P : → Prop) [decidable_pred P] (m n : ) :
decidable (∀ (r : ), m < rr nP r)
Equations