# mathlib3documentation

data.int.interval

# Finite intervals of integers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

@[protected, instance]
Equations
theorem int.Icc_eq_finset_map (a b : ) :
b = (finset.range (b + 1 - a).to_nat)
theorem int.Ico_eq_finset_map (a b : ) :
b = (finset.range (b - a).to_nat)
theorem int.uIcc_eq_finset_map (a b : ) :
b = (finset.range b + 1 - b).to_nat)
@[simp]
theorem int.card_Icc (a b : ) :
b).card = (b + 1 - a).to_nat
@[simp]
theorem int.card_Ico (a b : ) :
b).card = (b - a).to_nat
@[simp]
theorem int.card_Ioc (a b : ) :
b).card = (b - a).to_nat
@[simp]
theorem int.card_Ioo (a b : ) :
b).card = (b - a - 1).to_nat
@[simp]
theorem int.card_uIcc (a b : ) :
b).card = (b - a).nat_abs + 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
@[simp]
theorem int.card_fintype_Icc (a b : ) :
@[simp]
theorem int.card_fintype_Ico (a b : ) :
@[simp]
theorem int.card_fintype_Ioc (a b : ) :
@[simp]
theorem int.card_fintype_Ioo (a b : ) :
@[simp]
theorem int.card_fintype_uIcc (a b : ) :
theorem int.card_fintype_Icc_of_le (a b : ) (h : a b + 1) :
theorem int.card_fintype_Ico_of_le (a b : ) (h : a b) :
theorem int.card_fintype_Ioc_of_le (a b : ) (h : a b) :
theorem int.card_fintype_Ioo_of_lt (a b : ) (h : a < b) :
theorem int.image_Ico_mod (n a : ) (h : 0 a) :
finset.image (λ (_x : ), _x % a) (n + a)) = a