mathlib3 documentation

data.nat.interval

Finite intervals of naturals #

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

This file proves that ℕ is a locally_finite_order and calculates the cardinality of its intervals as finsets and fintypes.

TODO #

Some lemmas can be generalized using ordered_group, canonically_ordered_monoid or succ_order and subsequently be moved upstream to data.finset.locally_finite.

source
@[protected, instance]
def nat.locally_finite_order  :
locally_finite_order ℕ
Equations
source
theorem nat.Icc_eq_range' (a b : ℕ) :
finset.Icc a b = {val := ↑(list.range' a (b + 1 - a)), nodup := _}
source
theorem nat.Ico_eq_range' (a b : ℕ) :
finset.Ico a b = {val := ↑(list.range' a (b - a)), nodup := _}
source
theorem nat.Ioc_eq_range' (a b : ℕ) :
finset.Ioc a b = {val := ↑(list.range' (a + 1) (b - a)), nodup := _}
source
theorem nat.Ioo_eq_range' (a b : ℕ) :
finset.Ioo a b = {val := ↑(list.range' (a + 1) (b - a - 1)), nodup := _}
source
theorem nat.uIcc_eq_range' (a b : ℕ) :
finset.uIcc a b = {val := ↑(list.range' (linear_order.min a b) (linear_order.max a b + 1 - linear_order.min a b)), nodup := _}
source
theorem nat.Iio_eq_range  :
finset.Iio = finset.range
source
@[simp]
theorem nat.Ico_zero_eq_range  :
finset.Ico 0 = finset.range
source
theorem finset.range_eq_Ico  :
finset.range = finset.Ico 0
source
@[simp]
theorem nat.card_Icc (a b : ℕ) :
(finset.Icc a b).card = b + 1 - a
source
@[simp]
theorem nat.card_Ico (a b : ℕ) :
(finset.Ico a b).card = b - a
source
@[simp]
theorem nat.card_Ioc (a b : ℕ) :
(finset.Ioc a b).card = b - a
source
@[simp]
theorem nat.card_Ioo (a b : ℕ) :
(finset.Ioo a b).card = b - a - 1
source
@[simp]
theorem nat.card_uIcc (a b : ℕ) :
(finset.uIcc a b).card = (↑b - ↑a).nat_abs + 1
source
@[simp]
theorem nat.card_Iic (b : ℕ) :
(finset.Iic b).card = b + 1
source
@[simp]
theorem nat.card_Iio (b : ℕ) :
(finset.Iio b).card = b
source
@[simp]
theorem nat.card_fintype_Icc (a b : ℕ) :
fintype.card ↥(set.Icc a b) = b + 1 - a
source
@[simp]
theorem nat.card_fintype_Ico (a b : ℕ) :
fintype.card ↥(set.Ico a b) = b - a
source
@[simp]
theorem nat.card_fintype_Ioc (a b : ℕ) :
fintype.card ↥(set.Ioc a b) = b - a
source
@[simp]
theorem nat.card_fintype_Ioo (a b : ℕ) :
fintype.card ↥(set.Ioo a b) = b - a - 1
source
@[simp]
theorem nat.card_fintype_Iic (b : ℕ) :
fintype.card ↥(set.Iic b) = b + 1
source
@[simp]
theorem nat.card_fintype_Iio (b : ℕ) :
fintype.card ↥(set.Iio b) = b
source
theorem nat.Icc_succ_left (a b : ℕ) :
finset.Icc a.succ b = finset.Ioc a b
source
theorem nat.Ico_succ_right (a b : ℕ) :
finset.Ico a b.succ = finset.Icc a b
source
theorem nat.Ico_succ_left (a b : ℕ) :
finset.Ico a.succ b = finset.Ioo a b
source
theorem nat.Icc_pred_right (a : ℕ) {b : ℕ} (h : 0 < b) :
finset.Icc a (b - 1) = finset.Ico a b
source
theorem nat.Ico_succ_succ (a b : ℕ) :
finset.Ico a.succ b.succ = finset.Ioc a b
source
@[simp]
theorem nat.Ico_succ_singleton (a : ℕ) :
finset.Ico a (a + 1) = {a}
source
@[simp]
theorem nat.Ico_pred_singleton {a : ℕ} (h : 0 < a) :
finset.Ico (a - 1) a = {a - 1}
source
@[simp]
theorem nat.Ioc_succ_singleton (b : ℕ) :
finset.Ioc b (b + 1) = {b + 1}
source
theorem nat.Ico_succ_right_eq_insert_Ico {a b : ℕ} (h : a ≤ b) :
finset.Ico a (b + 1) = has_insert.insert b (finset.Ico a b)
source
theorem nat.Ico_insert_succ_left {a b : ℕ} (h : a < b) :
has_insert.insert a (finset.Ico a.succ b) = finset.Ico a b
source
theorem nat.image_sub_const_Ico {a b c : ℕ} (h : c ≤ a) :
finset.image (λ (x : ℕ), x - c) (finset.Ico a b) = finset.Ico (a - c) (b - c)
source
theorem nat.Ico_image_const_sub_eq_Ico {a b c : ℕ} (hac : a ≤ c) :
finset.image (λ (x : ℕ), c - x) (finset.Ico a b) = finset.Ico (c + 1 - b) (c + 1 - a)
source
theorem nat.Ico_succ_left_eq_erase_Ico {a b : ℕ} :
finset.Ico a.succ b = (finset.Ico a b).erase a
source
theorem nat.mod_inj_on_Ico (n a : ℕ) :
set.inj_on (λ (_x : ℕ), _x % a) ↑(finset.Ico n (n + a))
source
theorem nat.image_Ico_mod (n a : ℕ) :
finset.image (λ (_x : ℕ), _x % a) (finset.Ico n (n + a)) = finset.range a

Note that while this lemma cannot be easily generalized to a type class, it holds for ℤ as well. See int.image_Ico_mod for the ℤ version.

source
theorem nat.multiset_Ico_map_mod (n a : ℕ) :
multiset.map (λ (_x : ℕ), _x % a) (multiset.Ico n (n + a)) = multiset.range a
source
theorem finset.range_image_pred_top_sub (n : ℕ) :
finset.image (λ (j : ℕ), n - 1 - j) (finset.range n) = finset.range n
source
theorem finset.range_add_eq_union (a b : ℕ) :
finset.range (a + b) = finset.range a ∪ finset.map (add_left_embedding a) (finset.range b)
source
theorem nat.decreasing_induction_of_not_bdd_above {P : ℕ → Prop} (h : ∀ (n : ℕ), P (n + 1) → P n) (hP : ¬bdd_above {x : ℕ | P x}) (n : ℕ) :
P n
source
theorem nat.decreasing_induction_of_infinite {P : ℕ → Prop} (h : ∀ (n : ℕ), P (n + 1) → P n) (hP : {x : ℕ | P x}.infinite) (n : ℕ) :
P n
source
theorem nat.cauchy_induction' {P : ℕ → Prop} (h : ∀ (n : ℕ), P (n + 1) → P n) (seed : ℕ) (hs : P seed) (hi : ∀ (x : ℕ), seed ≤ x → P x → (∃ (y : ℕ), x < y ∧ P y)) (n : ℕ) :
P n
source
theorem nat.cauchy_induction {P : ℕ → Prop} (h : ∀ (n : ℕ), P (n + 1) → P n) (seed : ℕ) (hs : P seed) (f : ℕ → ℕ) (hf : ∀ (x : ℕ), seed ≤ x → P x → x < f x ∧ P (f x)) (n : ℕ) :
P n
source
theorem nat.cauchy_induction_mul {P : ℕ → Prop} (h : ∀ (n : ℕ), P (n + 1) → P n) (k seed : ℕ) (hk : 1 < k) (hs : P seed.succ) (hm : ∀ (x : ℕ), seed < x → P x → P (k * x)) (n : ℕ) :
P n
source
theorem nat.cauchy_induction_two_mul {P : ℕ → Prop} (h : ∀ (n : ℕ), P (n + 1) → P n) (seed : ℕ) (hs : P seed.succ) (hm : ∀ (x : ℕ), seed < x → P x → P (2 * x)) (n : ℕ) :
P n