Documentation

Mathlib.Order.Interval.Finset.Nat

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.

source
instance Nat.instLocallyFiniteOrder :
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 := ⋯ }
source
theorem Nat.Ico_eq_range' (a b : ℕ) :
Finset.Ico a b = { val := ↑(List.range' a (b - a)), nodup := ⋯ }
source
theorem Nat.Ioc_eq_range' (a b : ℕ) :
Finset.Ioc a b = { val := ↑(List.range' (a + 1) (b - a)), nodup := ⋯ }
source
theorem Nat.Ioo_eq_range' (a b : ℕ) :
Finset.Ioo a b = { val := ↑(List.range' (a + 1) (b - a - 1)), nodup := ⋯ }
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 := ⋯ }
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 Nat.range_eq_Icc_zero_sub_one (n : ℕ) (hn : n ≠ 0) :
Finset.range n = Finset.Icc 0 (n - 1)
source
theorem Finset.range_eq_Ico :
range = Ico 0
source
theorem Nat.range_succ_eq_Icc_zero (n : ℕ) :
Finset.range (n + 1) = Finset.Icc 0 n
source
@[simp]
theorem Nat.card_Icc (a b : ℕ) :
(Finset.Icc a b).card = b + 1 - a
source
@[simp]
theorem Nat.card_Ico (a b : ℕ) :
(Finset.Ico a b).card = b - a
source
@[simp]
theorem Nat.card_Ioc (a b : ℕ) :
(Finset.Ioc a b).card = b - a
source
@[simp]
theorem Nat.card_Ioo (a b : ℕ) :
(Finset.Ioo a b).card = b - a - 1
source
@[simp]
theorem Nat.card_uIcc (a b : ℕ) :
(Finset.uIcc a b).card = (↑b - ↑a).natAbs + 1
source
@[simp]
theorem Nat.card_Iic (b : ℕ) :
(Finset.Iic b).card = b + 1
source
@[simp]
theorem Nat.card_Iio (b : ℕ) :
(Finset.Iio b).card = b
source
@[deprecated Fintype.card_Icc (since := "2025-03-28")]
theorem Nat.card_fintypeIcc (a b : ℕ) :
Fintype.card ↑(Set.Icc a b) = b + 1 - a
source
@[deprecated Fintype.card_Ico (since := "2025-03-28")]
theorem Nat.card_fintypeIco (a b : ℕ) :
Fintype.card ↑(Set.Ico a b) = b - a
source
@[deprecated Fintype.card_Ioc (since := "2025-03-28")]
theorem Nat.card_fintypeIoc (a b : ℕ) :
Fintype.card ↑(Set.Ioc a b) = b - a
source
@[deprecated Fintype.card_Ioo (since := "2025-03-28")]
theorem Nat.card_fintypeIoo (a b : ℕ) :
Fintype.card ↑(Set.Ioo a b) = b - a - 1
source
@[deprecated Fintype.card_Iic (since := "2025-03-28")]
theorem Nat.card_fintypeIic (b : ℕ) :
Fintype.card ↑(Set.Iic b) = b + 1
source
@[deprecated Fintype.card_Iio (since := "2025-03-28")]
theorem Nat.card_fintypeIio (b : ℕ) :
Fintype.card ↑(Set.Iio b) = b
source
@[deprecated Finset.Icc_succ_left_eq_Ioc (since := "2025-04-24")]
theorem Nat.Icc_succ_left (a b : ℕ) :
Finset.Icc a.succ b = Finset.Ioc a b
source
@[deprecated Finset.Ico_succ_right_eq_Icc (since := "2025-04-24")]
theorem Nat.Ico_succ_right (a b : ℕ) :
Finset.Ico a b.succ = Finset.Icc a b
source
@[deprecated Finset.Ico_succ_left_eq_Ioo (since := "2025-04-24")]
theorem Nat.Ico_succ_left (a b : ℕ) :
Finset.Ico a.succ b = Finset.Ioo a b
source
@[deprecated Finset.Icc_pred_right_eq_Ico (since := "2025-04-24")]
theorem Nat.Icc_pred_right (a : ℕ) {b : ℕ} (h : 0 < b) :
Finset.Icc a (b - 1) = Finset.Ico a b
source
@[deprecated Finset.Ico_succ_succ_eq_Ioc (since := "2025-04-24")]
theorem Nat.Ico_succ_succ (a b : ℕ) :
Finset.Ico a.succ b.succ = 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.mem_Ioc_succ {a b : ℕ} :
a ∈ Finset.Ioc b (b + 1) ↔ a = b + 1
source
theorem Nat.mem_Ioc_succ' {b : ℕ} (a : { x : ℕ // x ∈ Finset.Ioc b (b + 1) }) :
a = ⟨b + 1, ⋯⟩
source
@[deprecated Finset.insert_Ico_right_eq_Ico_succ_right (since := "2025-04-24")]
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
@[deprecated Finset.insert_Ico_succ_left_eq_Ico (since := "2025-04-24")]
theorem Nat.Ico_insert_succ_left {a b : ℕ} (h : a < b) :
insert a (Finset.Ico a.succ b) = Finset.Ico a b
source
@[deprecated Finset.insert_Icc_succ_left_eq_Icc (since := "2025-04-24")]
theorem Nat.Icc_insert_succ_left {a b : ℕ} (h : a ≤ b) :
insert a (Finset.Icc (a + 1) b) = Finset.Icc a b
source
@[deprecated Finset.insert_Icc_eq_Icc_succ_right (since := "2025-04-24")]
theorem Nat.Icc_insert_succ_right {a b : ℕ} (h : a ≤ b + 1) :
insert (b + 1) (Finset.Icc a b) = Finset.Icc a (b + 1)
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 a.succ b = (Finset.Ico a b).erase 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 List.toFinset_range'_1 (a b : ℕ) :
(range' a b).toFinset = Finset.Ico a (a + b)
source
theorem List.toFinset_range'_1_1 (a : ℕ) :
(range' 1 a).toFinset = Finset.Icc 1 a
source
theorem Finset.range_image_pred_top_sub (n : ℕ) :
image (fun (j : ℕ) => n - 1 - j) (range n) = range n
source
theorem Finset.range_add_eq_union (a b : ℕ) :
range (a + b) = range a ∪ map (addLeftEmbedding a) (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.strong_decreasing_induction {P : ℕ → Prop} (base : ∃ (n : ℕ), ∀ m > n, P m) (step : ∀ (n : ℕ), (∀ m > n, P m) → P n) (n : ℕ) :
P n
source
theorem Nat.decreasing_induction_of_infinite {P : ℕ → Prop} (h : ∀ (n : ℕ), P (n + 1) → P n) (hP : {x : ℕ | P x}.Infinite) (n : ℕ) :
P n
source
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
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 seed.succ) (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 seed.succ) (hm : ∀ (x : ℕ), seed < x → P x → P (2 * x)) (n : ℕ) :
P n
source
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