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.

@[protected, instance]
Equations
theorem nat.Icc_eq_range' (a b : ) :
finset.Icc a b = {val := (list.range' a (b + 1 - a)), nodup := _}
theorem nat.Ico_eq_range' (a b : ) :
finset.Ico a b = {val := (list.range' a (b - a)), nodup := _}
theorem nat.Ioc_eq_range' (a b : ) :
finset.Ioc a b = {val := (list.range' (a + 1) (b - a)), nodup := _}
theorem nat.Ioo_eq_range' (a b : ) :
finset.Ioo a b = {val := (list.range' (a + 1) (b - a - 1)), nodup := _}
@[simp]
theorem nat.card_Icc (a b : ) :
(finset.Icc a b).card = b + 1 - a
@[simp]
theorem nat.card_Ico (a b : ) :
(finset.Ico a b).card = b - a
@[simp]
theorem nat.card_Ioc (a b : ) :
(finset.Ioc a b).card = b - a
@[simp]
theorem nat.card_Ioo (a b : ) :
(finset.Ioo a b).card = b - a - 1
@[simp]
theorem nat.card_uIcc (a b : ) :
@[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 : ) :
@[simp]
theorem nat.Icc_succ_left (a b : ) :
theorem nat.Ico_succ_right (a b : ) :
theorem nat.Ico_succ_left (a b : ) :
theorem nat.Icc_pred_right (a : ) {b : } (h : 0 < b) :
finset.Icc a (b - 1) = finset.Ico a b
@[simp]
theorem nat.Ico_succ_singleton (a : ) :
finset.Ico 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 : ) :
finset.Ioc b (b + 1) = {b + 1}
theorem nat.Ico_insert_succ_left {a b : } (h : a < b) :
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)
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)
theorem nat.mod_inj_on_Ico (n a : ) :
set.inj_on (λ (_x : ), _x % a) (finset.Ico n (n + a))
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.

theorem nat.multiset_Ico_map_mod (n a : ) :
multiset.map (λ (_x : ), _x % a) (multiset.Ico n (n + a)) = multiset.range a
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