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.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)))
@[simp]
@[simp]
@[simp]
@[simp]
theorem
Int.card_Icc_of_le
(a : ℤ)
(b : ℤ)
(h : a ≤ b + 1)
:
↑(Finset.card (Finset.Icc a b)) = b + 1 - 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_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.image_Ico_emod
(n : ℤ)
(a : ℤ)
(h : 0 ≤ a)
:
Finset.image (fun x => x % a) (Finset.Ico n (n + a)) = Finset.Ico 0 a