Finite intervals of integers

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

@[implicit_reducible]

instance Int.instLocallyFiniteOrder : LocallyFiniteOrder ℤ

Equations

• One or more equations did not get rendered due to their size.

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

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

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

theorem Int.Ioo_eq_finset_map (a b : ℤ) : Finset.Ioo 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.uIcc 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 : ℤ) : (Finset.Icc a b).card = (b + 1 - a).toNat

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

theorem Int.Icc_eq_pair (a : ℤ) : Finset.Icc a (a + 1) = {a, 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

theorem Finset.Icc_succ_succ (m n : ℕ) : Icc (-(↑m + 1)) (↑n + 1) = Icc (-↑m) ↑n ∪ {-(↑m + 1), ↑n + 1}

theorem Finset.Ico_succ_succ (m n : ℕ) : Ico (-(↑m + 1)) (↑n + 1) = Ico (-↑m) ↑n ∪ {-(↑m + 1), ↑n}

theorem Finset.Ioc_succ_succ (m n : ℕ) : Ioc (-(↑m + 1)) (↑n + 1) = Ioc (-↑m) ↑n ∪ {-↑m, ↑n + 1}

theorem Finset.Ioo_succ_succ (m n : ℕ) : Ioo (-(↑m + 1)) (↑n + 1) = Ioo (-↑m) ↑n ∪ {-↑m, ↑n}