# mathlib3documentation

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.

@[protected, instance]
Equations
theorem nat.Icc_eq_range' (a b : ) :
b = {val := (b + 1 - a)), nodup := _}
theorem nat.Ico_eq_range' (a b : ) :
b = {val := (b - a)), nodup := _}
theorem nat.Ioc_eq_range' (a b : ) :
b = {val := (list.range' (a + 1) (b - a)), nodup := _}
theorem nat.Ioo_eq_range' (a b : ) :
b = {val := (list.range' (a + 1) (b - a - 1)), nodup := _}
theorem nat.uIcc_eq_range' (a b : ) :
b = {val := (list.range' b) b + 1 - b)), nodup := _}
theorem nat.Iio_eq_range  :
@[simp]
theorem nat.Ico_zero_eq_range  :
@[simp]
theorem nat.card_Icc (a b : ) :
b).card = b + 1 - a
@[simp]
theorem nat.card_Ico (a b : ) :
b).card = b - a
@[simp]
theorem nat.card_Ioc (a b : ) :
b).card = b - a
@[simp]
theorem nat.card_Ioo (a b : ) :
b).card = b - a - 1
@[simp]
theorem nat.card_uIcc (a b : ) :
b).card = (b - a).nat_abs + 1
@[simp]
theorem nat.card_Iic (b : ) :
(finset.Iic b).card = b + 1
@[simp]
theorem nat.card_Iio (b : ) :
@[simp]
theorem nat.card_fintype_Icc (a b : ) :
@[simp]
theorem nat.card_fintype_Ico (a b : ) :
@[simp]
theorem nat.card_fintype_Ioc (a b : ) :
@[simp]
theorem nat.card_fintype_Ioo (a b : ) :
@[simp]
theorem nat.card_fintype_Iic (b : ) :
= b + 1
@[simp]
theorem nat.card_fintype_Iio (b : ) :
= b
theorem nat.Icc_succ_left (a b : ) :
b = b
theorem nat.Ico_succ_right (a b : ) :
b.succ = b
theorem nat.Ico_succ_left (a b : ) :
b = b
theorem nat.Icc_pred_right (a : ) {b : } (h : 0 < b) :
(b - 1) = b
theorem nat.Ico_succ_succ (a b : ) :
b.succ = b
@[simp]
theorem nat.Ico_succ_singleton (a : ) :
(a + 1) = {a}
@[simp]
theorem nat.Ico_pred_singleton {a : } (h : 0 < a) :
finset.Ico (a - 1) a = {a - 1}
@[simp]
theorem nat.Ioc_succ_singleton (b : ) :
(b + 1) = {b + 1}
theorem nat.Ico_succ_right_eq_insert_Ico {a b : } (h : a b) :
(b + 1) = b)
theorem nat.Ico_insert_succ_left {a b : } (h : a < b) :
b) = b
theorem nat.image_sub_const_Ico {a b c : } (h : c a) :
finset.image (λ (x : ), x - c) b) = finset.Ico (a - c) (b - c)
theorem nat.Ico_image_const_sub_eq_Ico {a b c : } (hac : a c) :
finset.image (λ (x : ), c - x) b) = finset.Ico (c + 1 - b) (c + 1 - a)
theorem nat.Ico_succ_left_eq_erase_Ico {a b : } :
b = b).erase a
theorem nat.mod_inj_on_Ico (n a : ) :
set.inj_on (λ (_x : ), _x % a) (n + a))
theorem nat.image_Ico_mod (n a : ) :
finset.image (λ (_x : ), _x % a) (n + 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.

theorem nat.multiset_Ico_map_mod (n a : ) :
multiset.map (λ (_x : ), _x % a) (n + a)) =
theorem finset.range_image_pred_top_sub (n : ) :
finset.image (λ (j : ), n - 1 - j) (finset.range n) =
theorem finset.range_add_eq_union (a b : ) :
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
theorem nat.decreasing_induction_of_infinite {P : Prop} (h : (n : ), P (n + 1) P n) (hP : {x : | P x}.infinite) (n : ) :
P n
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
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
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
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