mathlib documentation

data.int.range

def int.range (m n : ℤ) :

List enumerating [m, n).

Equations

m.range n = list.map (λ (r : ℕ), m + ↑r) (list.range (n - m).to_nat)

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 ≤ r → r < n → P r)

Equations

int.decidable_le_lt P m n = decidable_of_iff (∀ (r : ℤ), r ∈ m.range n → P r) _

@[instance]

def int.decidable_le_le (P : ℤ → Prop) [decidable_pred P] (m n : ℤ) :

decidable (∀ (r : ℤ), m ≤ r → r ≤ n → P r)

Equations

int.decidable_le_le P m n = decidable_of_iff (∀ (r : ℤ), r ∈ m.range (n + 1) → P r) _

@[instance]

def int.decidable_lt_lt (P : ℤ → Prop) [decidable_pred P] (m n : ℤ) :

decidable (∀ (r : ℤ), m < r → r < n → P r)

Equations

int.decidable_lt_lt P m n = int.decidable_le_lt P (m + 1) n

@[instance]

def int.decidable_lt_le (P : ℤ → Prop) [decidable_pred P] (m n : ℤ) :

decidable (∀ (r : ℤ), m < r → r ≤ n → P r)

Equations

int.decidable_lt_le P m n = int.decidable_le_le P (m + 1) n