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

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

theorem Int.mem_range_iff {m : ℤ} {n : ℤ} {r : ℤ} : r ∈ Int.range m 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 : ℤ) → r ∈ Int.range m n → P r) (_ : ((a : ℤ) → a ∈ Int.range m n → P a) ↔ (r : ℤ) → m ≤ r → r < 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 : ℤ) → r ∈ Int.range m (n + 1) → P r) (_ : ((r : ℤ) → r ∈ Int.range m (n + 1) → P r) ↔ (r : ℤ) → m ≤ r → r ≤ n → 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