mathlib3 documentation

data.list.intervals

Intervals in ℕ #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines intervals of naturals. list.Ico m n is the list of integers greater than m and strictly less than n.

TODO #

source
def list.Ico (n m : ℕ) :
list ℕ

Ico n m is the list of natural numbers n ≤ x < m. (Ico stands for "interval, closed-open".)

See also data/set/intervals.lean for set.Ico, modelling intervals in general preorders, and multiset.Ico and finset.Ico for n ≤ x < m as a multiset or as a finset.

Equations
source
theorem list.Ico.zero_bot (n : ℕ) :
list.Ico 0 n = list.range n
source
@[simp]
theorem list.Ico.length (n m : ℕ) :
(list.Ico n m).length = m - n
source
theorem list.Ico.pairwise_lt (n m : ℕ) :
list.pairwise has_lt.lt (list.Ico n m)
source
theorem list.Ico.nodup (n m : ℕ) :
(list.Ico n m).nodup
source
@[simp]
theorem list.Ico.mem {n m l : ℕ} :
l ∈ list.Ico n m ↔ n ≤ l ∧ l < m
source
theorem list.Ico.eq_nil_of_le {n m : ℕ} (h : m ≤ n) :
list.Ico n m = list.nil
source
theorem list.Ico.map_add (n m k : ℕ) :
list.map (has_add.add k) (list.Ico n m) = list.Ico (n + k) (m + k)
source
theorem list.Ico.map_sub (n m k : ℕ) (h₁ : k ≤ n) :
list.map (λ (x : ℕ), x - k) (list.Ico n m) = list.Ico (n - k) (m - k)
source
@[simp]
theorem list.Ico.self_empty {n : ℕ} :
list.Ico n n = list.nil
source
@[simp]
theorem list.Ico.eq_empty_iff {n m : ℕ} :
list.Ico n m = list.nil ↔ m ≤ n
source
theorem list.Ico.append_consecutive {n m l : ℕ} (hnm : n ≤ m) (hml : m ≤ l) :
list.Ico n m ++ list.Ico m l = list.Ico n l
source
@[simp]
theorem list.Ico.inter_consecutive (n m l : ℕ) :
list.Ico n m ∩ list.Ico m l = list.nil
source
@[simp]
theorem list.Ico.bag_inter_consecutive (n m l : ℕ) :
(list.Ico n m).bag_inter (list.Ico m l) = list.nil
source
@[simp]
theorem list.Ico.succ_singleton {n : ℕ} :
list.Ico n (n + 1) = [n]
source
theorem list.Ico.succ_top {n m : ℕ} (h : n ≤ m) :
list.Ico n (m + 1) = list.Ico n m ++ [m]
source
theorem list.Ico.eq_cons {n m : ℕ} (h : n < m) :
list.Ico n m = n :: list.Ico (n + 1) m
source
@[simp]
theorem list.Ico.pred_singleton {m : ℕ} (h : 0 < m) :
list.Ico (m - 1) m = [m - 1]
source
theorem list.Ico.chain'_succ (n m : ℕ) :
list.chain' (λ (a b : ℕ), b = a.succ) (list.Ico n m)
source
@[simp]
theorem list.Ico.not_mem_top {n m : ℕ} :
m ∉ list.Ico n m
source
theorem list.Ico.filter_lt_of_top_le {n m l : ℕ} (hml : m ≤ l) :
list.filter (λ (x : ℕ), x < l) (list.Ico n m) = list.Ico n m
source
theorem list.Ico.filter_lt_of_le_bot {n m l : ℕ} (hln : l ≤ n) :
list.filter (λ (x : ℕ), x < l) (list.Ico n m) = list.nil
source
theorem list.Ico.filter_lt_of_ge {n m l : ℕ} (hlm : l ≤ m) :
list.filter (λ (x : ℕ), x < l) (list.Ico n m) = list.Ico n l
source
@[simp]
theorem list.Ico.filter_lt (n m l : ℕ) :
list.filter (λ (x : ℕ), x < l) (list.Ico n m) = list.Ico n (linear_order.min m l)
source
theorem list.Ico.filter_le_of_le_bot {n m l : ℕ} (hln : l ≤ n) :
list.filter (λ (x : ℕ), l ≤ x) (list.Ico n m) = list.Ico n m
source
theorem list.Ico.filter_le_of_top_le {n m l : ℕ} (hml : m ≤ l) :
list.filter (λ (x : ℕ), l ≤ x) (list.Ico n m) = list.nil
source
theorem list.Ico.filter_le_of_le {n m l : ℕ} (hnl : n ≤ l) :
list.filter (λ (x : ℕ), l ≤ x) (list.Ico n m) = list.Ico l m
source
@[simp]
theorem list.Ico.filter_le (n m l : ℕ) :
list.filter (λ (x : ℕ), l ≤ x) (list.Ico n m) = list.Ico (linear_order.max n l) m
source
theorem list.Ico.filter_lt_of_succ_bot {n m : ℕ} (hnm : n < m) :
list.filter (λ (x : ℕ), x < n + 1) (list.Ico n m) = [n]
source
@[simp]
theorem list.Ico.filter_le_of_bot {n m : ℕ} (hnm : n < m) :
list.filter (λ (x : ℕ), x ≤ n) (list.Ico n m) = [n]
source
theorem list.Ico.trichotomy (n a b : ℕ) :
n < a ∨ b ≤ n ∨ n ∈ list.Ico a b

For any natural numbers n, a, and b, one of the following holds:

  1. n < a
  2. n ≥ b
  3. n ∈ Ico a b