mathlib documentation

data.int.range

def int.range  :
list

List enumerating [m, n).

Equations
theorem int.mem_range_iff {m n r : } :
r m.range n m r r < n

@[instance]
def int.decidable_le_lt (P : → Prop) [decidable_pred P] (m n : ) :
decidable (∀ (r : ), m rr < nP r)

Equations
@[instance]
def int.decidable_le_le (P : → Prop) [decidable_pred P] (m n : ) :
decidable (∀ (r : ), m rr nP r)

Equations
@[instance]
def int.decidable_lt_lt (P : → Prop) [decidable_pred P] (m n : ) :
decidable (∀ (r : ), m < rr < nP r)

Equations
@[instance]
def int.decidable_lt_le (P : → Prop) [decidable_pred P] (m n : ) :
decidable (∀ (r : ), m < rr nP r)

Equations