# mathlibdocumentation

data.nat.interval

# Finite intervals of naturals #

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

## TODO #

Some lemmas can be generalized using ordered_group, canonically_ordered_monoid or succ_order and subsequently be moved upstream to data.finset.locally_finite.

@[protected, instance]
Equations
theorem nat.Icc_eq_range' (a b : ) :
b = (b + 1 - a)).to_finset
theorem nat.Ico_eq_range' (a b : ) :
b = (b - a)).to_finset
theorem nat.Ioc_eq_range' (a b : ) :
b = (list.range' (a + 1) (b - a)).to_finset
theorem nat.Ioo_eq_range' (a b : ) :
b = (list.range' (a + 1) (b - a - 1)).to_finset
theorem nat.Iio_eq_range  :
@[simp]
theorem nat.Ico_zero_eq_range  :
@[simp]
theorem nat.card_Icc (a b : ) :
b).card = b + 1 - a
@[simp]
theorem nat.card_Ico (a b : ) :
b).card = b - a
@[simp]
theorem nat.card_Ioc (a b : ) :
b).card = b - a
@[simp]
theorem nat.card_Ioo (a b : ) :
b).card = b - a - 1
@[simp]
theorem nat.card_Iic (b : ) :
(finset.Iic b).card = b + 1
@[simp]
theorem nat.card_Iio (b : ) :
@[simp]
theorem nat.card_fintype_Icc (a b : ) :
@[simp]
theorem nat.card_fintype_Ico (a b : ) :
@[simp]
theorem nat.card_fintype_Ioc (a b : ) :
@[simp]
theorem nat.card_fintype_Ioo (a b : ) :
@[simp]
theorem nat.card_fintype_Iic (b : ) :
= b + 1
@[simp]
theorem nat.card_fintype_Iio (b : ) :
= b
theorem nat.Icc_succ_left (a b : ) :
b = b
theorem nat.Ico_succ_right (a b : ) :
b.succ = b
theorem nat.Ico_succ_left (a b : ) :
b = b
theorem nat.Icc_pred_right (a : ) {b : } (h : 0 < b) :
(b - 1) = b
theorem nat.Ico_succ_succ (a b : ) :
b.succ = b
@[simp]
theorem nat.Ico_succ_singleton (a : ) :
(a + 1) = {a}
@[simp]
theorem nat.Ico_pred_singleton {a : } (h : 0 < a) :
finset.Ico (a - 1) a = {a - 1}
@[simp]
theorem nat.Ioc_succ_singleton (b : ) :
(b + 1) = {b + 1}
theorem nat.Ico_succ_right_eq_insert_Ico {a b : } (h : a b) :
(b + 1) = b)
theorem nat.Ico_insert_succ_left {a b : } (h : a < b) :
b) = b
theorem nat.image_sub_const_Ico {a b c : } (h : c a) :
finset.image (λ (x : ), x - c) b) = finset.Ico (a - c) (b - c)
theorem nat.Ico_image_const_sub_eq_Ico {a b c : } (hac : a c) :
finset.image (λ (x : ), c - x) b) = finset.Ico (c + 1 - b) (c + 1 - a)
theorem nat.Ico_succ_left_eq_erase_Ico {a b : } :
b = b).erase a
theorem nat.mod_inj_on_Ico (n a : ) :
set.inj_on (λ (_x : ), _x % a) (n + a))
theorem nat.image_Ico_mod (n a : ) :
finset.image (λ (_x : ), _x % a) (n + a)) =

Note that while this lemma cannot be easily generalized to a type class, it holds for ℤ as well. See int.image_Ico_mod for the ℤ version.

theorem nat.multiset_Ico_map_mod (n a : ) :
multiset.map (λ (_x : ), _x % a) (n + a)) =
theorem finset.range_image_pred_top_sub (n : ) :
finset.image (λ (j : ), n - 1 - j) (finset.range n) =
theorem finset.range_add_eq_union (a b : ) :