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, CanonicallyOrderedMonoid or SuccOrder and subsequently be moved upstream to Data.Finset.LocallyFinite.

source

instance instLocallyFiniteOrderNatToPreorderToPartialOrderStrictOrderedSemiring :

LocallyFiniteOrder ℕ

Equations

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

source

theorem Nat.Icc_eq_range' (a : ℕ) (b : ℕ) :

Finset.Icc a b = { val := ↑(List.range' a (b + 1 - a)), nodup := (_ : List.Nodup (List.range' a (b + 1 - a))) }

source

theorem Nat.Ico_eq_range' (a : ℕ) (b : ℕ) :

Finset.Ico a b = { val := ↑(List.range' a (b - a)), nodup := (_ : List.Nodup (List.range' a (b - a))) }

source

theorem Nat.Ioc_eq_range' (a : ℕ) (b : ℕ) :

Finset.Ioc a b = { val := ↑(List.range' (a + 1) (b - a)), nodup := (_ : List.Nodup (List.range' (a + 1) (b - a))) }

source

theorem Nat.Ioo_eq_range' (a : ℕ) (b : ℕ) :

Finset.Ioo a b = { val := ↑(List.range' (a + 1) (b - a - 1)), nodup := (_ : List.Nodup (List.range' (a + 1) (b - a - 1))) }

source

theorem Nat.uIcc_eq_range' (a : ℕ) (b : ℕ) :

Finset.uIcc a b = { val := ↑(List.range' (min a b) (max a b + 1 - min a b)), nodup := (_ : List.Nodup (List.range' (min a b) (max a b + 1 - min a b))) }

source

theorem Nat.Iio_eq_range :

Finset.Iio = Finset.range

source

@[simp]

theorem Nat.Ico_zero_eq_range :

Finset.Ico 0 = Finset.range

source

theorem Finset.range_eq_Ico :

Finset.range = Finset.Ico 0

source

@[simp]

theorem Nat.card_Icc (a : ℕ) (b : ℕ) :

Finset.card (Finset.Icc a b) = b + 1 - a

source

@[simp]

theorem Nat.card_Ico (a : ℕ) (b : ℕ) :

Finset.card (Finset.Ico a b) = b - a

source

@[simp]

theorem Nat.card_Ioc (a : ℕ) (b : ℕ) :

Finset.card (Finset.Ioc a b) = b - a

source

@[simp]

theorem Nat.card_Ioo (a : ℕ) (b : ℕ) :

Finset.card (Finset.Ioo a b) = b - a - 1

source

@[simp]

theorem Nat.card_uIcc (a : ℕ) (b : ℕ) :

Finset.card (Finset.uIcc a b) = Int.natAbs (↑b - ↑a) + 1

source

@[simp]

theorem Nat.card_Iic (b : ℕ) :

Finset.card (Finset.Iic b) = b + 1

source

@[simp]

theorem Nat.card_Iio (b : ℕ) :

Finset.card (Finset.Iio b) = b

source

theorem Nat.card_fintypeIcc (a : ℕ) (b : ℕ) :

Fintype.card ↑(Set.Icc a b) = b + 1 - a

source

theorem Nat.card_fintypeIco (a : ℕ) (b : ℕ) :

Fintype.card ↑(Set.Ico a b) = b - a

source

theorem Nat.card_fintypeIoc (a : ℕ) (b : ℕ) :

Fintype.card ↑(Set.Ioc a b) = b - a

source

theorem Nat.card_fintypeIoo (a : ℕ) (b : ℕ) :

Fintype.card ↑(Set.Ioo a b) = b - a - 1

source

theorem Nat.card_fintypeIic (b : ℕ) :

Fintype.card ↑(Set.Iic b) = b + 1

source

theorem Nat.card_fintypeIio (b : ℕ) :

Fintype.card ↑(Set.Iio b) = b

source

theorem Nat.Icc_succ_left (a : ℕ) (b : ℕ) :

Finset.Icc (Nat.succ a) b = Finset.Ioc a b

source

theorem Nat.Ico_succ_right (a : ℕ) (b : ℕ) :

Finset.Ico a (Nat.succ b) = Finset.Icc a b

source

theorem Nat.Ico_succ_left (a : ℕ) (b : ℕ) :

Finset.Ico (Nat.succ a) b = Finset.Ioo a b

source

theorem Nat.Icc_pred_right (a : ℕ) {b : ℕ} (h : 0 < b) :

Finset.Icc a (b - 1) = Finset.Ico a b

source

theorem Nat.Ico_succ_succ (a : ℕ) (b : ℕ) :

Finset.Ico (Nat.succ a) (Nat.succ b) = Finset.Ioc a b

source

@[simp]

theorem Nat.Ico_succ_singleton (a : ℕ) :

Finset.Ico a (a + 1) = {a}

source

@[simp]

theorem Nat.Ico_pred_singleton {a : ℕ} (h : 0 < a) :

Finset.Ico (a - 1) a = {a - 1}

source

@[simp]

theorem Nat.Ioc_succ_singleton (b : ℕ) :

Finset.Ioc b (b + 1) = {b + 1}

source

theorem Nat.Ico_succ_right_eq_insert_Ico {a : ℕ} {b : ℕ} (h : a ≤ b) :

Finset.Ico a (b + 1) = insert b (Finset.Ico a b)

source

theorem Nat.Ico_insert_succ_left {a : ℕ} {b : ℕ} (h : a < b) :

insert a (Finset.Ico (Nat.succ a) b) = Finset.Ico a b

source

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)

source

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)

source

theorem Nat.Ico_succ_left_eq_erase_Ico {a : ℕ} {b : ℕ} :

Finset.Ico (Nat.succ a) b = Finset.erase (Finset.Ico a b) a

source

theorem Nat.mod_injOn_Ico (n : ℕ) (a : ℕ) :

Set.InjOn (fun x => x % a) ↑(Finset.Ico n (n + a))

source

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.

source

theorem Nat.multiset_Ico_map_mod (n : ℕ) (a : ℕ) :

Multiset.map (fun x => x % a) (Multiset.Ico n (n + a)) = Multiset.range a

source

theorem Finset.range_image_pred_top_sub (n : ℕ) :

Finset.image (fun j => n - 1 - j) (Finset.range n) = Finset.range n

source

theorem Finset.range_add_eq_union (a : ℕ) (b : ℕ) :

Finset.range (a + b) = Finset.range a ∪ Finset.map (addLeftEmbedding a) (Finset.range b)

source

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

P n

source

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

P n

source

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

P n

source

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

source

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

P n

source

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

P n