Finite intervals of naturals

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

TODO

Some lemmas can be generalized using OrderedGroup, CanonicallyOrderedMul or SuccOrder and subsequently be moved upstream to Order.Interval.Finset.

instance Nat.instLocallyFiniteOrder : LocallyFiniteOrder ℕ

Equations

• One or more equations did not get rendered due to their size.

theorem Nat.Icc_eq_range' (a b : ℕ) : Finset.Icc a b = { val := ↑(List.range' a (b + 1 - a)), nodup := ⋯ }

theorem Nat.Ico_eq_range' (a b : ℕ) : Finset.Ico a b = { val := ↑(List.range' a (b - a)), nodup := ⋯ }

theorem Nat.Ioc_eq_range' (a b : ℕ) : Finset.Ioc a b = { val := ↑(List.range' (a + 1) (b - a)), nodup := ⋯ }

theorem Nat.Ioo_eq_range' (a b : ℕ) : Finset.Ioo a b = { val := ↑(List.range' (a + 1) (b - a - 1)), nodup := ⋯ }

theorem Nat.uIcc_eq_range' (a b : ℕ) : Finset.uIcc a b = { val := ↑(List.range' (a ⊓ b) (a ⊔ b + 1 - a ⊓ b)), nodup := ⋯ }

theorem Nat.Iio_eq_range : Finset.Iio = Finset.range

@[simp]

theorem Nat.Ico_zero_eq_range : Finset.Ico 0 = Finset.range

theorem Nat.range_eq_Icc_zero_sub_one (n : ℕ) (hn : n ≠ 0) : Finset.range n = Finset.Icc 0 (n - 1)

theorem Finset.range_eq_Ico : range = Ico 0

theorem Nat.range_succ_eq_Icc_zero (n : ℕ) : Finset.range (n + 1) = Finset.Icc 0 n

@[simp]

theorem Nat.card_Icc (a b : ℕ) : (Finset.Icc a b).card = b + 1 - a

@[simp]

theorem Nat.card_Ico (a b : ℕ) : (Finset.Ico a b).card = b - a

@[simp]

theorem Nat.card_Ioc (a b : ℕ) : (Finset.Ioc a b).card = b - a

@[simp]

theorem Nat.card_Ioo (a b : ℕ) : (Finset.Ioo a b).card = b - a - 1

@[simp]

theorem Nat.card_uIcc (a b : ℕ) : (Finset.uIcc a b).card = (↑b - ↑a).natAbs + 1

@[simp]

theorem Nat.card_Iic (b : ℕ) : (Finset.Iic b).card = b + 1

@[simp]

theorem Nat.card_Iio (b : ℕ) : (Finset.Iio b).card = b

theorem Nat.card_fintypeIcc (a b : ℕ) : Fintype.card ↑(Set.Icc a b) = b + 1 - a

theorem Nat.card_fintypeIco (a b : ℕ) : Fintype.card ↑(Set.Ico a b) = b - a

theorem Nat.card_fintypeIoc (a b : ℕ) : Fintype.card ↑(Set.Ioc a b) = b - a

theorem Nat.card_fintypeIoo (a b : ℕ) : Fintype.card ↑(Set.Ioo a b) = b - a - 1

theorem Nat.card_fintypeIic (b : ℕ) : Fintype.card ↑(Set.Iic b) = b + 1

theorem Nat.card_fintypeIio (b : ℕ) : Fintype.card ↑(Set.Iio b) = b

theorem Nat.Icc_succ_left (a b : ℕ) : Finset.Icc a.succ b = Finset.Ioc a b

theorem Nat.Ico_succ_right (a b : ℕ) : Finset.Ico a b.succ = Finset.Icc a b

theorem Nat.Ico_succ_left (a b : ℕ) : Finset.Ico a.succ b = Finset.Ioo a b

theorem Nat.Icc_pred_right (a : ℕ) {b : ℕ} (h : 0 < b) : Finset.Icc a (b - 1) = Finset.Ico a b

theorem Nat.Ico_succ_succ (a b : ℕ) : Finset.Ico a.succ b.succ = Finset.Ioc a b

@[simp]

theorem Nat.Ico_succ_singleton (a : ℕ) : Finset.Ico 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 : ℕ) : Finset.Ioc b (b + 1) = {b + 1}

theorem Nat.mem_Ioc_succ {a b : ℕ} : a ∈ Finset.Ioc b (b + 1) ↔ a = b + 1

theorem Nat.mem_Ioc_succ' {b : ℕ} (a : { x : ℕ // x ∈ Finset.Ioc b (b + 1) }) : a = ⟨b + 1, ⋯⟩

theorem Nat.Ico_succ_right_eq_insert_Ico {a b : ℕ} (h : a ≤ b) : Finset.Ico a (b + 1) = insert b (Finset.Ico a b)

theorem Nat.Ico_insert_succ_left {a b : ℕ} (h : a < b) : insert a (Finset.Ico a.succ b) = Finset.Ico a b

theorem Nat.Icc_insert_succ_left {a b : ℕ} (h : a ≤ b) : insert a (Finset.Icc (a + 1) b) = Finset.Icc a b

theorem Nat.Icc_insert_succ_right {a b : ℕ} (h : a ≤ b + 1) : insert (b + 1) (Finset.Icc a b) = Finset.Icc a (b + 1)

theorem Nat.image_sub_const_Ico {a b c : ℕ} (h : c ≤ a) : Finset.image (fun (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 (fun (x : ℕ) => c - x) (Finset.Ico a b) = Finset.Ico (c + 1 - b) (c + 1 - a)

theorem Nat.Ico_succ_left_eq_erase_Ico {a b : ℕ} : Finset.Ico a.succ b = (Finset.Ico a b).erase a

theorem Nat.mod_injOn_Ico (n a : ℕ) : Set.InjOn (fun (x : ℕ) => x % a) ↑(Finset.Ico n (n + a))

theorem Nat.image_Ico_mod (n a : ℕ) : Finset.image (fun (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_emod for the ℤ version.

theorem Nat.multiset_Ico_map_mod (n a : ℕ) : Multiset.map (fun (x : ℕ) => x % a) (Multiset.Ico n (n + a)) = Multiset.range a

theorem Finset.range_image_pred_top_sub (n : ℕ) : image (fun (j : ℕ) => n - 1 - j) (range n) = range n

theorem Finset.range_add_eq_union (a b : ℕ) : range (a + b) = range a ∪ map (addLeftEmbedding a) (range b)

theorem Nat.decreasing_induction_of_not_bddAbove {P : ℕ → Prop} (h : ∀ (n : ℕ), P (n + 1) → P n) (hP : ¬BddAbove {x : ℕ | P x}) (n : ℕ) : P n

theorem Nat.strong_decreasing_induction {P : ℕ → Prop} (base : ∃ (n : ℕ), ∀ m > n, P m) (step : ∀ (n : ℕ), (∀ m > n, P m) → P n) (n : ℕ) : P n

theorem Nat.decreasing_induction_of_infinite {P : ℕ → Prop} (h : ∀ (n : ℕ), P (n + 1) → P n) (hP : {x : ℕ | P x}.Infinite) (n : ℕ) : P n

theorem Nat.cauchy_induction' {P : ℕ → Prop} (seed : ℕ) (h : ∀ (n : ℕ), P (n + 1) → P n) (hs : P seed) (hi : ∀ (x : ℕ), seed ≤ x → P x → ∃ (y : ℕ), x < y ∧ P y) (n : ℕ) : P n

theorem Nat.cauchy_induction {P : ℕ → Prop} (h : ∀ (n : ℕ), P (n + 1) → P n) (seed : ℕ) (hs : P seed) (f : ℕ → ℕ) (hf : ∀ (x : ℕ), seed ≤ x → P x → x < f x ∧ P (f x)) (n : ℕ) : P n

theorem Nat.cauchy_induction_mul {P : ℕ → Prop} (h : ∀ (n : ℕ), P (n + 1) → P n) (k seed : ℕ) (hk : 1 < k) (hs : P seed.succ) (hm : ∀ (x : ℕ), seed < x → P x → P (k * x)) (n : ℕ) : P n

theorem Nat.cauchy_induction_two_mul {P : ℕ → Prop} (h : ∀ (n : ℕ), P (n + 1) → P n) (seed : ℕ) (hs : P seed.succ) (hm : ∀ (x : ℕ), seed < x → P x → P (2 * x)) (n : ℕ) : P n

theorem Nat.pow_imp_self_of_one_lt {M : Type u_1} [Monoid M] (k : ℕ) (hk : 1 < k) (P : M → Prop) (hmul : ∀ (x y : M), P x → P (x * y) ∨ P (y * x)) (hpow : ∀ (x : M), P (x ^ k) → P x) (n : ℕ) (x : M) : P (x ^ n) → P x