Finite intervals of integers

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

instance instLocallyFiniteOrderIntToPreorderToPartialOrderToStrictOrderedRingToLinearOrderedRingLinearOrderedCommRing : LocallyFiniteOrder ℤ

theorem Int.Icc_eq_finset_map (a : ℤ) (b : ℤ) : Finset.Icc a b = Finset.map (Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding a)) (Finset.range (Int.toNat (b + 1 - a)))

theorem Int.Ico_eq_finset_map (a : ℤ) (b : ℤ) : Finset.Ico a b = Finset.map (Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding a)) (Finset.range (Int.toNat (b - a)))

theorem Int.Ioc_eq_finset_map (a : ℤ) (b : ℤ) : Finset.Ioc a b = Finset.map (Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (a + 1))) (Finset.range (Int.toNat (b - a)))

theorem Int.Ioo_eq_finset_map (a : ℤ) (b : ℤ) : Finset.Ioo a b = Finset.map (Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (a + 1))) (Finset.range (Int.toNat (b - a - 1)))

theorem Int.uIcc_eq_finset_map (a : ℤ) (b : ℤ) : Finset.uIcc a b = Finset.map (Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding (min a b))) (Finset.range (Int.toNat (max a b + 1 - min a b)))

@[simp]

theorem Int.card_Icc (a : ℤ) (b : ℤ) : Finset.card (Finset.Icc a b) = Int.toNat (b + 1 - a)

@[simp]

theorem Int.card_Ico (a : ℤ) (b : ℤ) : Finset.card (Finset.Ico a b) = Int.toNat (b - a)

@[simp]

theorem Int.card_Ioc (a : ℤ) (b : ℤ) : Finset.card (Finset.Ioc a b) = Int.toNat (b - a)

@[simp]

theorem Int.card_Ioo (a : ℤ) (b : ℤ) : Finset.card (Finset.Ioo a b) = Int.toNat (b - a - 1)

@[simp]

theorem Int.card_uIcc (a : ℤ) (b : ℤ) : Finset.card (Finset.uIcc a b) = Int.natAbs (b - a) + 1

theorem Int.card_Icc_of_le (a : ℤ) (b : ℤ) (h : a ≤ b + 1) : ↑(Finset.card (Finset.Icc a b)) = b + 1 - a

theorem Int.card_Ico_of_le (a : ℤ) (b : ℤ) (h : a ≤ b) : ↑(Finset.card (Finset.Ico a b)) = b - a

theorem Int.card_Ioc_of_le (a : ℤ) (b : ℤ) (h : a ≤ b) : ↑(Finset.card (Finset.Ioc a b)) = b - a

theorem Int.card_Ioo_of_lt (a : ℤ) (b : ℤ) (h : a < b) : ↑(Finset.card (Finset.Ioo a b)) = b - a - 1

theorem Int.card_fintype_Icc (a : ℤ) (b : ℤ) : Fintype.card ↑(Set.Icc a b) = Int.toNat (b + 1 - a)

theorem Int.card_fintype_Ico (a : ℤ) (b : ℤ) : Fintype.card ↑(Set.Ico a b) = Int.toNat (b - a)

theorem Int.card_fintype_Ioc (a : ℤ) (b : ℤ) : Fintype.card ↑(Set.Ioc a b) = Int.toNat (b - a)

theorem Int.card_fintype_Ioo (a : ℤ) (b : ℤ) : Fintype.card ↑(Set.Ioo a b) = Int.toNat (b - a - 1)

theorem Int.card_fintype_uIcc (a : ℤ) (b : ℤ) : Fintype.card ↑(Set.uIcc a b) = Int.natAbs (b - a) + 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)) = Finset.Ico 0 a