# Finite intervals of integers #

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

Equations
• One or more equations did not get rendered due to their size.
theorem Int.Icc_eq_finset_map (a : ) (b : ) :
= Finset.map (Nat.castEmbedding.trans ()) (Finset.range (b + 1 - a).toNat)
theorem Int.Ico_eq_finset_map (a : ) (b : ) :
= Finset.map (Nat.castEmbedding.trans ()) (Finset.range (b - a).toNat)
theorem Int.Ioc_eq_finset_map (a : ) (b : ) :
= Finset.map (Nat.castEmbedding.trans (addLeftEmbedding (a + 1))) (Finset.range (b - a).toNat)
theorem Int.Ioo_eq_finset_map (a : ) (b : ) :
= Finset.map (Nat.castEmbedding.trans (addLeftEmbedding (a + 1))) (Finset.range (b - a - 1).toNat)
theorem Int.uIcc_eq_finset_map (a : ) (b : ) :
= Finset.map (Nat.castEmbedding.trans (addLeftEmbedding (min a b))) (Finset.range (max a b + 1 - min a b).toNat)
@[simp]
theorem Int.card_Icc (a : ) (b : ) :
().card = (b + 1 - a).toNat
@[simp]
theorem Int.card_Ico (a : ) (b : ) :
().card = (b - a).toNat
@[simp]
theorem Int.card_Ioc (a : ) (b : ) :
().card = (b - a).toNat
@[simp]
theorem Int.card_Ioo (a : ) (b : ) :
().card = (b - a - 1).toNat
@[simp]
theorem Int.card_uIcc (a : ) (b : ) :
().card = (b - a).natAbs + 1
theorem Int.card_Icc_of_le (a : ) (b : ) (h : a b + 1) :
().card = b + 1 - a
theorem Int.card_Ico_of_le (a : ) (b : ) (h : a b) :
().card = b - a
theorem Int.card_Ioc_of_le (a : ) (b : ) (h : a b) :
().card = b - a
theorem Int.card_Ioo_of_lt (a : ) (b : ) (h : a < b) :
().card = b - a - 1
theorem Int.card_fintype_Icc (a : ) (b : ) :
Fintype.card (Set.Icc a b) = (b + 1 - a).toNat
theorem Int.card_fintype_Ico (a : ) (b : ) :
Fintype.card (Set.Ico a b) = (b - a).toNat
theorem Int.card_fintype_Ioc (a : ) (b : ) :
Fintype.card (Set.Ioc a b) = (b - a).toNat
theorem Int.card_fintype_Ioo (a : ) (b : ) :
Fintype.card (Set.Ioo a b) = (b - a - 1).toNat
theorem Int.card_fintype_uIcc (a : ) (b : ) :
Fintype.card (Set.uIcc a b) = (b - a).natAbs + 1
theorem Int.card_fintype_Icc_of_le (a : ) (b : ) (h : a b + 1) :
(Fintype.card (Set.Icc a b)) = b + 1 - a
theorem Int.card_fintype_Ico_of_le (a : ) (b : ) (h : a b) :
(Fintype.card (Set.Ico a b)) = b - a
theorem Int.card_fintype_Ioc_of_le (a : ) (b : ) (h : a b) :
(Fintype.card (Set.Ioc a b)) = b - a
theorem Int.card_fintype_Ioo_of_lt (a : ) (b : ) (h : a < b) :
(Fintype.card (Set.Ioo a b)) = b - a - 1
theorem Int.image_Ico_emod (n : ) (a : ) (h : 0 a) :
Finset.image (fun (x : ) => x % a) (Finset.Ico n (n + a)) =