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.

source
def int.range (m n : ℤ) :
list ℤ

List enumerating [m, n). This is the ℤ variant of list.Ico.

Equations
source
theorem int.mem_range_iff {m n r : ℤ} :
r ∈ m.range n ↔ m ≤ r ∧ r < n
source
@[protected, instance]
def int.decidable_le_lt (P : ℤ → Prop) [decidable_pred P] (m n : ℤ) :
decidable (∀ (r : ℤ), m ≤ r → r < n → P r)
Equations
source
@[protected, instance]
def int.decidable_le_le (P : ℤ → Prop) [decidable_pred P] (m n : ℤ) :
decidable (∀ (r : ℤ), m ≤ r → r ≤ n → P r)
Equations
source
@[protected, instance]
def int.decidable_lt_lt (P : ℤ → Prop) [decidable_pred P] (m n : ℤ) :
decidable (∀ (r : ℤ), m < r → r < n → P r)
Equations
source
@[protected, instance]
def int.decidable_lt_le (P : ℤ → Prop) [decidable_pred P] (m n : ℤ) :
decidable (∀ (r : ℤ), m < r → r ≤ n → P r)
Equations