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 ℤ

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

theorem Int.mem_range_iff {m n r : ℤ} : r ∈ m.range n ↔ m ≤ r ∧ r < n

instance Int.decidableLELT (P : ℤ → Prop) [DecidablePred P] (m n : ℤ) : Decidable (∀ (r : ℤ), m ≤ r → r < n → P r)

instance Int.decidableLELE (P : ℤ → Prop) [DecidablePred P] (m n : ℤ) : Decidable (∀ (r : ℤ), m ≤ r → r ≤ n → P r)

instance Int.decidableLTLT (P : ℤ → Prop) [DecidablePred P] (m n : ℤ) : Decidable (∀ (r : ℤ), m < r → r < n → P r)

instance Int.decidableLTLE (P : ℤ → Prop) [DecidablePred P] (m n : ℤ) : Decidable (∀ (r : ℤ), m < r → r ≤ n → P r)