mathlib3 documentation

data.int.range

Intervals in ℤ #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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