# Finite intervals of naturals #

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

## TODO #

Some lemmas can be generalized using OrderedGroup, CanonicallyOrderedCommMonoid or SuccOrder and subsequently be moved upstream to Data.Finset.LocallyFinite.

Equations
• One or more equations did not get rendered due to their size.
theorem Nat.Icc_eq_range' (a : ) (b : ) :
= { val := (List.range' a (b + 1 - a)), nodup := }
theorem Nat.Ico_eq_range' (a : ) (b : ) :
= { val := (List.range' a (b - a)), nodup := }
theorem Nat.Ioc_eq_range' (a : ) (b : ) :
= { val := (List.range' (a + 1) (b - a)), nodup := }
theorem Nat.Ioo_eq_range' (a : ) (b : ) :
= { val := (List.range' (a + 1) (b - a - 1)), nodup := }
theorem Nat.uIcc_eq_range' (a : ) (b : ) :
= { val := (List.range' (min a b) (max a b + 1 - min a b)), nodup := }
@[simp]
@[simp]
theorem Nat.card_Icc (a : ) (b : ) :
().card = b + 1 - a
@[simp]
theorem Nat.card_Ico (a : ) (b : ) :
().card = b - a
@[simp]
theorem Nat.card_Ioc (a : ) (b : ) :
().card = b - a
@[simp]
theorem Nat.card_Ioo (a : ) (b : ) :
().card = b - a - 1
@[simp]
theorem Nat.card_uIcc (a : ) (b : ) :
().card = Int.natAbs (b - a) + 1
@[simp]
theorem Nat.card_Iic (b : ) :
().card = b + 1
@[simp]
theorem Nat.card_Iio (b : ) :
().card = b
theorem Nat.card_fintypeIcc (a : ) (b : ) :
Fintype.card (Set.Icc a b) = b + 1 - a
theorem Nat.card_fintypeIco (a : ) (b : ) :
Fintype.card (Set.Ico a b) = b - a
theorem Nat.card_fintypeIoc (a : ) (b : ) :
Fintype.card (Set.Ioc a b) = b - a
theorem Nat.card_fintypeIoo (a : ) (b : ) :
Fintype.card (Set.Ioo a b) = b - a - 1
theorem Nat.card_fintypeIic (b : ) :
Fintype.card () = b + 1
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) =
theorem Nat.Ico_succ_succ (a : ) (b : ) :
Finset.Ico () () =
@[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_succ_right_eq_insert_Ico {a : } {b : } (h : a b) :
Finset.Ico a (b + 1) = insert b ()
theorem Nat.Ico_insert_succ_left {a : } {b : } (h : a < b) :
insert a (Finset.Ico () b) =
theorem Nat.image_sub_const_Ico {a : } {b : } {c : } (h : c a) :
Finset.image (fun (x : ) => x - c) () = Finset.Ico (a - c) (b - c)
theorem Nat.Ico_image_const_sub_eq_Ico {a : } {b : } {c : } (hac : a c) :
Finset.image (fun (x : ) => c - x) () = Finset.Ico (c + 1 - b) (c + 1 - a)
theorem Nat.mod_injOn_Ico (n : ) (a : ) :
Set.InjOn (fun (x : ) => x % a) (Finset.Ico n (n + a))
theorem Nat.image_Ico_mod (n : ) (a : ) :
Finset.image (fun (x : ) => x % a) (Finset.Ico n (n + a)) =

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

theorem Nat.multiset_Ico_map_mod (n : ) (a : ) :
Multiset.map (fun (x : ) => x % a) (Multiset.Ico n (n + a)) =
theorem Finset.range_image_pred_top_sub (n : ) :
Finset.image (fun (j : ) => n - 1 - j) () =
theorem Nat.decreasing_induction_of_not_bddAbove {P : } (h : ∀ (n : ), P (n + 1)P n) (hP : ¬BddAbove {x : | P x}) (n : ) :
P n
theorem Nat.decreasing_induction_of_infinite {P : } (h : ∀ (n : ), P (n + 1)P n) (hP : Set.Infinite {x : | P x}) (n : ) :
P n
theorem Nat.cauchy_induction' {P : } (h : ∀ (n : ), P (n + 1)P n) (seed : ) (hs : P seed) (hi : ∀ (x : ), seed xP x∃ (y : ), x < y P y) (n : ) :
P n
theorem Nat.cauchy_induction {P : } (h : ∀ (n : ), P (n + 1)P n) (seed : ) (hs : P seed) (f : ) (hf : ∀ (x : ), seed xP xx < f x P (f x)) (n : ) :
P n
theorem Nat.cauchy_induction_mul {P : } (h : ∀ (n : ), P (n + 1)P n) (k : ) (seed : ) (hk : 1 < k) (hs : P (Nat.succ seed)) (hm : ∀ (x : ), seed < xP xP (k * x)) (n : ) :
P n
theorem Nat.cauchy_induction_two_mul {P : } (h : ∀ (n : ), P (n + 1)P n) (seed : ) (hs : P (Nat.succ seed)) (hm : ∀ (x : ), seed < xP xP (2 * x)) (n : ) :
P n
theorem Nat.pow_imp_self_of_one_lt {M : Type u_1} [] (k : ) (hk : 1 < k) (P : MProp) (hmul : ∀ (x y : M), P xP (x * y) P (y * x)) (hpow : ∀ (x : M), P (x ^ k)P x) (n : ) (x : M) :
P (x ^ n)P x