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.

Equations

• m.range n = List.map (fun (r : ℕ) => m + ↑r) (List.range (n - m).toNat)

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)

Equations

• Int.decidableLELT P m n = decidable_of_iff (∀ r ∈ m.range n, P r) ⋯

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

Equations

• Int.decidableLELE P m n = decidable_of_iff (∀ r ∈ m.range (n + 1), P r) ⋯

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

Equations

• Int.decidableLTLT P m n = Int.decidableLELT P (m + 1) n

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

Equations

• Int.decidableLTLE P m n = Int.decidableLELE P (m + 1) n