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
- nat.locally_finite_order = {finset_Icc := λ (a b : ℕ), (list.range' a (b + 1 - a)).to_finset, finset_Ico := λ (a b : ℕ), (list.range' a (b - a)).to_finset, finset_Ioc := λ (a b : ℕ), (list.range' (a + 1) (b - a)).to_finset, finset_Ioo := λ (a b : ℕ), (list.range' (a + 1) (b - a - 1)).to_finset, finset_mem_Icc := nat.locally_finite_order._proof_1, finset_mem_Ico := nat.locally_finite_order._proof_2, finset_mem_Ioc := nat.locally_finite_order._proof_3, finset_mem_Ioo := nat.locally_finite_order._proof_4}
theorem
nat.Ico_succ_right_eq_insert_Ico
{a b : ℕ}
(h : a ≤ b) :
finset.Ico a (b + 1) = has_insert.insert b (finset.Ico a b)
theorem
nat.Ico_insert_succ_left
{a b : ℕ}
(h : a < b) :
has_insert.insert a (finset.Ico a.succ b) = finset.Ico a b
theorem
nat.image_sub_const_Ico
{a b c : ℕ}
(h : c ≤ a) :
finset.image (λ (x : ℕ), x - c) (finset.Ico a 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) (finset.Ico a b) = finset.Ico (c + 1 - b) (c + 1 - a)
theorem
nat.image_Ico_mod
(n a : ℕ) :
finset.image (λ (_x : ℕ), _x % a) (finset.Ico n (n + a)) = finset.range 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) (multiset.Ico n (n + a)) = multiset.range a
theorem
finset.range_image_pred_top_sub
(n : ℕ) :
finset.image (λ (j : ℕ), n - 1 - j) (finset.range n) = finset.range n
theorem
finset.range_add_eq_union
(a b : ℕ) :
finset.range (a + b) = finset.range a ∪ finset.map (add_left_embedding a) (finset.range b)