Documentation

Mathlib.Data.Int.Interval

Finite intervals of integers #

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

@[simp]
theorem Int.card_Icc (a : ) (b : ) :
(Finset.Icc a b).card = Int.toNat (b + 1 - a)
@[simp]
theorem Int.card_Ico (a : ) (b : ) :
(Finset.Ico a b).card = Int.toNat (b - a)
@[simp]
theorem Int.card_Ioc (a : ) (b : ) :
(Finset.Ioc a b).card = Int.toNat (b - a)
@[simp]
theorem Int.card_Ioo (a : ) (b : ) :
(Finset.Ioo a b).card = Int.toNat (b - a - 1)
@[simp]
theorem Int.card_uIcc (a : ) (b : ) :
(Finset.uIcc a b).card = Int.natAbs (b - a) + 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.card_fintype_Icc (a : ) (b : ) :
Fintype.card (Set.Icc a b) = Int.toNat (b + 1 - a)
theorem Int.card_fintype_Ico (a : ) (b : ) :
theorem Int.card_fintype_Ioc (a : ) (b : ) :
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