Mathlib.Order.Interval.Finset.Nat

Nat.instLocallyFiniteOrder instance

: LocallyFiniteOrder ℕ

Full source

instance instLocallyFiniteOrder : LocallyFiniteOrder ℕ where
  finsetIcc a b := ⟨List.range' a (b + 1 - a), List.nodup_range'⟩
  finsetIco a b := ⟨List.range' a (b - a), List.nodup_range'⟩
  finsetIoc a b := ⟨List.range' (a + 1) (b - a), List.nodup_range'⟩
  finsetIoo a b := ⟨List.range' (a + 1) (b - a - 1), List.nodup_range'⟩
  finset_mem_Icc a b x := by rw [Finset.mem_mk, Multiset.mem_coe, List.mem_range'_1]; omega
  finset_mem_Ico a b x := by rw [Finset.mem_mk, Multiset.mem_coe, List.mem_range'_1]; omega
  finset_mem_Ioc a b x := by rw [Finset.mem_mk, Multiset.mem_coe, List.mem_range'_1]; omega
  finset_mem_Ioo a b x := by rw [Finset.mem_mk, Multiset.mem_coe, List.mem_range'_1]; omega

Natural Numbers as a Locally Finite Order

Informal description

The natural numbers $\mathbb{N}$ form a locally finite order, meaning that for any two natural numbers $a \leq b$, the intervals $[a, b]$, $[a, b)$, $(a, b]$, and $(a, b)$ are all finite.

Nat.Icc_eq_range' theorem

: Icc a b = ⟨List.range' a (b + 1 - a), List.nodup_range'⟩

Full source

theorem Icc_eq_range' : Icc a b = ⟨List.range' a (b + 1 - a), List.nodup_range'⟩ :=
  rfl

Closed Interval of Natural Numbers as Range List

Informal description

For any natural numbers $a$ and $b$, the closed interval $\text{Icc}(a, b) = \{x \in \mathbb{N} \mid a \leq x \leq b\}$ is equal to the finset constructed from the list $\text{range'}(a, b + 1 - a)$, where $\text{range'}(n, k)$ generates the list $[n, n+1, \dots, n+k-1]$, and this list has no duplicates.

Nat.Ico_eq_range' theorem

: Ico a b = ⟨List.range' a (b - a), List.nodup_range'⟩

Full source

theorem Ico_eq_range' : Ico a b = ⟨List.range' a (b - a), List.nodup_range'⟩ :=
  rfl

Closed-open interval of natural numbers as a range' list

Informal description

For any natural numbers $a$ and $b$, the half-open interval $\text{Ico}(a, b) = \{x \in \mathbb{N} \mid a \leq x < b\}$ is equal to the finset constructed from the list $\text{range'}(a, b - a)$, where $\text{range'}(n, k)$ generates the list $[n, n+1, \dots, n+k-1]$, and this list has no duplicates.

Nat.Ioc_eq_range' theorem

: Ioc a b = ⟨List.range' (a + 1) (b - a), List.nodup_range'⟩

Full source

theorem Ioc_eq_range' : Ioc a b = ⟨List.range' (a + 1) (b - a), List.nodup_range'⟩ :=
  rfl

Open-closed interval of natural numbers as a range' list

Informal description

For any natural numbers $a$ and $b$, the open-closed interval $\text{Ioc}(a, b) = \{x \in \mathbb{N} \mid a < x \leq b\}$ is equal to the finset constructed from the list $\text{range'}(a+1, b-a)$, where $\text{range'}(n, k)$ generates the list $[n, n+1, \dots, n+k-1]$, and this list is nodup (has no duplicates).

Nat.Ioo_eq_range' theorem

: Ioo a b = ⟨List.range' (a + 1) (b - a - 1), List.nodup_range'⟩

Full source

theorem Ioo_eq_range' : Ioo a b = ⟨List.range' (a + 1) (b - a - 1), List.nodup_range'⟩ :=
  rfl

Open interval of natural numbers as a range' list

Informal description

For any natural numbers $a$ and $b$, the open interval $\text{Ioo}(a, b) = \{x \in \mathbb{N} \mid a < x < b\}$ is equal to the finset constructed from the list $\text{range'}(a+1, b-a-1)$, where $\text{range'}(n, k)$ generates the list $[n, n+1, \dots, n+k-1]$, and this list has no duplicates.

Nat.uIcc_eq_range' theorem

: uIcc a b = ⟨List.range' (min a b) (max a b + 1 - min a b), List.nodup_range'⟩

Full source

theorem uIcc_eq_range' :
    uIcc a b = ⟨List.range' (min a b) (max a b + 1 - min a b), List.nodup_range'⟩ := rfl

Unordered Closed Interval of Natural Numbers as Range' List

Informal description

For any natural numbers $a$ and $b$, the unordered closed interval $\text{uIcc}(a, b) = \{x \in \mathbb{N} \mid \min(a, b) \leq x \leq \max(a, b)\}$ is equal to the finset constructed from the list $\text{range'}(\min(a, b), \max(a, b) + 1 - \min(a, b))$, where $\text{range'}(n, k)$ generates the list $[n, n+1, \dots, n+k-1]$, and this list has no duplicates.

Nat.Iio_eq_range theorem

: Iio = range

Full source

theorem Iio_eq_range : Iio = range := by
  ext b x
  rw [mem_Iio, mem_range]

Open Lower Interval of Natural Numbers Equals Range from Zero

Informal description

For the natural numbers $\mathbb{N}$, the open lower interval finset $\text{Iio}(b) = \{x \in \mathbb{N} \mid x < b\}$ is equal to the finset $\text{range}(b) = \{0, 1, \dots, b-1\}$ for any natural number $b$.

Nat.Ico_zero_eq_range theorem

: Ico 0 = range

Full source

@[simp]
theorem Ico_zero_eq_range : Ico 0 = range := by rw [← Nat.bot_eq_zero, ← Iio_eq_Ico, Iio_eq_range]

Half-open interval from zero equals range of natural numbers

Informal description

For any natural number $b$, the half-open interval $[0, b)$ of natural numbers is equal to the finset $\text{range}(b) = \{0, 1, \dots, b-1\}$.

Nat.range_eq_Icc_zero_sub_one theorem

(n : ℕ) (hn : n ≠ 0) : range n = Icc 0 (n - 1)

Full source

lemma range_eq_Icc_zero_sub_one (n : ℕ) (hn : n ≠ 0) : range n = Icc 0 (n - 1) := by
  ext b
  simp_all only [mem_Icc, zero_le, true_and, mem_range]
  exact lt_iff_le_pred (zero_lt_of_ne_zero hn)

Range of $n$ Natural Numbers Equals Closed Interval $[0, n-1]$ for $n \neq 0$

Informal description

For any nonzero natural number $n$, the range of natural numbers from $0$ to $n-1$ is equal to the closed interval $[0, n-1]$, i.e., $\text{range}(n) = \{x \in \mathbb{N} \mid 0 \leq x \leq n-1\}$.

Finset.range_eq_Ico theorem

: range = Ico 0

Full source

theorem _root_.Finset.range_eq_Ico : range = Ico 0 :=
  Ico_zero_eq_range.symm

Range as Half-Open Interval from Zero: $\text{range}(b) = [0, b)$

Informal description

For any natural number $b$, the finset $\text{range}(b)$ is equal to the half-open interval $[0, b)$ of natural numbers, i.e., $\text{range}(b) = \{x \in \mathbb{N} \mid 0 \leq x < b\}$.

Nat.range_succ_eq_Icc_zero theorem

(n : ℕ) : range (n + 1) = Icc 0 n

Full source

theorem range_succ_eq_Icc_zero (n : ℕ) : range (n + 1) = Icc 0 n := by
  rw [range_eq_Icc_zero_sub_one _ (Nat.add_one_ne_zero _), Nat.add_sub_cancel_right]

Range of Successor Equals Closed Interval from Zero

Informal description

For any natural number $n$, the range of natural numbers from $0$ to $n$ (inclusive) is equal to the closed interval $[0, n]$, i.e., $\text{range}(n + 1) = \{x \in \mathbb{N} \mid 0 \leq x \leq n\}$.

Nat.card_Icc theorem

: #(Icc a b) = b + 1 - a

Full source

@[simp] lemma card_Icc : #(Icc a b) = b + 1 - a := List.length_range' ..

Cardinality of the Closed Interval of Natural Numbers: $\#([a, b]) = b + 1 - a$

Informal description

For any natural numbers $a$ and $b$, the cardinality of the finset $\text{Icc}(a, b)$ (the closed interval $[a, b]$) is equal to $b + 1 - a$.

Nat.card_Ico theorem

: #(Ico a b) = b - a

Full source

@[simp] lemma card_Ico : #(Ico a b) = b - a := List.length_range' ..

Cardinality of the Half-Open Interval of Natural Numbers: $\#([a, b)) = b - a$

Informal description

For any natural numbers $a$ and $b$, the cardinality of the finset $\text{Ico}(a, b)$ (the half-open interval $[a, b)$) is equal to $b - a$.

Nat.card_Ioc theorem

: #(Ioc a b) = b - a

Full source

@[simp] lemma card_Ioc : #(Ioc a b) = b - a := List.length_range' ..

Cardinality of Open-Closed Interval of Natural Numbers: $\#((a, b]) = b - a$

Informal description

For any natural numbers $a$ and $b$, the cardinality of the finset $\text{Ioc}(a, b)$ (the open-closed interval $(a, b]$) is equal to $b - a$.

Nat.card_Ioo theorem

: #(Ioo a b) = b - a - 1

Full source

@[simp] lemma card_Ioo : #(Ioo a b) = b - a - 1 := List.length_range' ..

Cardinality of Open Interval of Natural Numbers: $\#((a, b)) = b - a - 1$

Informal description

For any natural numbers $a$ and $b$, the cardinality of the finset $\text{Ioo}(a, b)$ (the open interval $(a, b)$) is equal to $b - a - 1$.

Nat.card_uIcc theorem

: #(uIcc a b) = (b - a : ℤ).natAbs + 1

Full source

@[simp]
theorem card_uIcc : #(uIcc a b) = (b - a : ℤ).natAbs + 1 :=
  (card_Icc _ _).trans <| by rw [← Int.natCast_inj, Int.ofNat_sub] <;> omega

Cardinality of Unordered Closed Interval in Natural Numbers: $\#(\text{uIcc}(a, b)) = |b - a| + 1$

Informal description

For any natural numbers $a$ and $b$, the cardinality of the unordered closed interval $\text{uIcc}(a, b)$ is equal to the natural number absolute value of $b - a$ plus one, i.e., $\#(\text{uIcc}(a, b)) = |b - a| + 1$.

Nat.card_Iic theorem

: #(Iic b) = b + 1

Full source

@[simp]
lemma card_Iic : #(Iic b) = b + 1 := by rw [Iic_eq_Icc, card_Icc, Nat.bot_eq_zero, Nat.sub_zero]

Cardinality of Lower-Closed Interval of Natural Numbers: $\#((-\infty, b]) = b + 1$

Informal description

For any natural number $b$, the cardinality of the finset $\text{Iic}(b)$ (the lower-closed interval $(-\infty, b]$) is equal to $b + 1$.

Nat.card_Iio theorem

: #(Iio b) = b

Full source

@[simp]
theorem card_Iio : #(Iio b) = b := by rw [Iio_eq_Ico, card_Ico, Nat.bot_eq_zero, Nat.sub_zero]

Cardinality of Open Lower Interval in Natural Numbers: $\#((-\infty, b)) = b$

Informal description

For any natural number $b$, the cardinality of the finset $\text{Iio}(b)$ (the open lower interval $(-\infty, b)$) is equal to $b$.

Nat.card_fintypeIcc theorem

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

Full source

@[deprecated Fintype.card_Icc (since := "2025-03-28")]
theorem card_fintypeIcc : Fintype.card (Set.Icc a b) = b + 1 - a := by simp

Cardinality of Closed Interval of Natural Numbers: $|[a, b]| = b + 1 - a$

Informal description

For any natural numbers $a$ and $b$, the cardinality of the closed interval $[a, b]$ as a fintype is equal to $b + 1 - a$.

Nat.card_fintypeIco theorem

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

Full source

@[deprecated Fintype.card_Ico (since := "2025-03-28")]
theorem card_fintypeIco : Fintype.card (Set.Ico a b) = b - a := by simp

Cardinality of Fintype for Closed-Open Interval of Natural Numbers: $\text{card}([a, b)) = b - a$

Informal description

For any natural numbers $a$ and $b$, the cardinality of the fintype representing the closed-open interval $[a, b)$ is equal to $b - a$.

Nat.card_fintypeIoc theorem

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

Full source

@[deprecated Fintype.card_Ioc (since := "2025-03-28")]
theorem card_fintypeIoc : Fintype.card (Set.Ioc a b) = b - a := by simp

Cardinality of Open-Closed Interval of Natural Numbers: $\text{card}((a, b]) = b - a$

Informal description

For any natural numbers $a$ and $b$, the cardinality of the open-closed interval $(a, b]$ as a fintype is equal to $b - a$.

Nat.card_fintypeIoo theorem

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

Full source

@[deprecated Fintype.card_Ioo (since := "2025-03-28")]
theorem card_fintypeIoo : Fintype.card (Set.Ioo a b) = b - a - 1 := by simp

Cardinality of Open Interval Fintype: $|\text{Ioo}(a, b)| = b - a - 1$

Informal description

For any natural numbers $a$ and $b$, the cardinality of the open interval $(a, b)$ as a fintype is equal to $b - a - 1$.

Nat.card_fintypeIic theorem

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

Full source

@[deprecated Fintype.card_Iic (since := "2025-03-28")]
theorem card_fintypeIic : Fintype.card (Set.Iic b) = b + 1 := by simp

Cardinality of Closed Lower Interval of Natural Numbers: $|(-\infty, b]| = b + 1$

Informal description

For any natural number $b$, the cardinality of the closed lower interval $(-\infty, b]$ (as a fintype) is equal to $b + 1$.

Nat.card_fintypeIio theorem

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

Full source

@[deprecated Fintype.card_Iio (since := "2025-03-28")]
theorem card_fintypeIio : Fintype.card (Set.Iio b) = b := by simp

Cardinality of Open Lower Interval Fintype: $|\text{Iio}(b)| = b$

Informal description

For any natural number $b$, the cardinality of the fintype representing the open lower interval $(-\infty, b)$ is equal to $b$.

Nat.Icc_succ_left theorem

: Icc a.succ b = Ioc a b

Full source

theorem Icc_succ_left : Icc a.succ b = Ioc a b := by
  ext x
  rw [mem_Icc, mem_Ioc, succ_le_iff]

Closed Interval with Successor Left Endpoint Equals Open-Closed Interval in Natural Numbers

Informal description

For any natural numbers $a$ and $b$, the closed interval $[a+1, b]$ is equal to the open-closed interval $(a, b]$.

Nat.Ico_succ_right theorem

: Ico a b.succ = Icc a b

Full source

theorem Ico_succ_right : Ico a b.succ = Icc a b := by
  ext x
  rw [mem_Ico, mem_Icc, Nat.lt_succ_iff]

Closed-Open Interval with Successor Right Endpoint Equals Closed Interval in Natural Numbers

Informal description

For any natural numbers $a$ and $b$, the closed-open interval $[a, b+1)$ is equal to the closed interval $[a, b]$.

Nat.Ico_succ_left theorem

: Ico a.succ b = Ioo a b

Full source

theorem Ico_succ_left : Ico a.succ b = Ioo a b := by
  ext x
  rw [mem_Ico, mem_Ioo, succ_le_iff]

Successor Left Endpoint Converts Closed-Open to Open Interval in Natural Numbers: $[a+1, b) = (a, b)$

Informal description

For any natural numbers $a$ and $b$, the closed-open interval $[a+1, b)$ is equal to the open interval $(a, b)$.

Nat.Icc_pred_right theorem

{b : ℕ} (h : 0 < b) : Icc a (b - 1) = Ico a b

Full source

theorem Icc_pred_right {b : ℕ} (h : 0 < b) : Icc a (b - 1) = Ico a b := by
  ext x
  rw [mem_Icc, mem_Ico, lt_iff_le_pred h]

Closed Interval with Predecessor Right Endpoint Equals Closed-Open Interval in Natural Numbers

Informal description

For any natural numbers $a$ and $b$ with $b > 0$, the closed interval $[a, b-1]$ is equal to the closed-open interval $[a, b)$.

Nat.Ico_succ_succ theorem

: Ico a.succ b.succ = Ioc a b

Full source

theorem Ico_succ_succ : Ico a.succ b.succ = Ioc a b := by
  ext x
  rw [mem_Ico, mem_Ioc, succ_le_iff, Nat.lt_succ_iff]

Successor Interval Equality: $[a+1, b+1) = (a, b]$ for Natural Numbers

Informal description

For any natural numbers $a$ and $b$, the closed-open interval $[a+1, b+1)$ is equal to the open-closed interval $(a, b]$.

Nat.Ico_succ_singleton theorem

: Ico a (a + 1) = { a }

Full source

@[simp]
theorem Ico_succ_singleton : Ico a (a + 1) = {a} := by rw [Ico_succ_right, Icc_self]

Singleton Interval Property: $[a, a+1) = \{a\}$ for Natural Numbers

Informal description

For any natural number $a$, the closed-open interval $[a, a+1)$ is equal to the singleton set $\{a\}$.

Nat.Ico_pred_singleton theorem

{a : ℕ} (h : 0 < a) : Ico (a - 1) a = {a - 1}

Full source

@[simp]
theorem Ico_pred_singleton {a : ℕ} (h : 0 < a) : Ico (a - 1) a = {a - 1} := by
  rw [← Icc_pred_right _ h, Icc_self]

Closed-Open Interval at Predecessor is Singleton: $[a-1, a) = \{a-1\}$ for $a > 0$

Informal description

For any natural number $a > 0$, the closed-open interval $[a-1, a)$ is equal to the singleton set $\{a-1\}$.

Nat.Ioc_succ_singleton theorem

: Ioc b (b + 1) = {b + 1}

Full source

@[simp]
theorem Ioc_succ_singleton : Ioc b (b + 1) = {b + 1} := by rw [← Nat.Icc_succ_left, Icc_self]

Open-Closed Interval at Successor is Singleton: $(b, b+1] = \{b+1\}$

Informal description

For any natural number $b$, the open-closed interval $(b, b+1]$ is equal to the singleton set $\{b+1\}$.

Nat.mem_Ioc_succ theorem

: a ∈ Ioc b (b + 1) ↔ a = b + 1

Full source

lemma mem_Ioc_succ : a ∈ Ioc b (b + 1)a ∈ Ioc b (b + 1) ↔ a = b + 1 := by simp

Membership in Open-Closed Successor Interval: $a \in (b, b+1] \leftrightarrow a = b+1$

Informal description

For any natural numbers $a$ and $b$, the element $a$ belongs to the open-closed interval $(b, b+1]$ if and only if $a = b + 1$.

Nat.mem_Ioc_succ' theorem

(a : Ioc b (b + 1)) : a = ⟨b + 1, mem_Ioc.2 (by omega)⟩

Full source

lemma mem_Ioc_succ' (a : Ioc b (b + 1)) : a = ⟨b + 1, mem_Ioc.2 (by omega)⟩ :=
  Subtype.val_inj.1 (mem_Ioc_succ.1 a.2)

Characterization of Elements in Successor Interval $(b, b+1]$

Informal description

For any natural number $b$, if $a$ is an element of the open-closed interval $(b, b+1]$, then $a$ is equal to $b+1$ and satisfies the membership condition $b < a \leq b+1$.

Nat.Ico_succ_right_eq_insert_Ico theorem

(h : a ≤ b) : Ico a (b + 1) = insert b (Ico a b)

Full source

theorem Ico_succ_right_eq_insert_Ico (h : a ≤ b) : Ico a (b + 1) = insert b (Ico a b) := by
  rw [Ico_succ_right, ← Ico_insert_right h]

Closed-Open Interval with Successor Right Endpoint as Insertion in Natural Numbers

Informal description

For any natural numbers $a$ and $b$ with $a \leq b$, the closed-open interval $[a, b+1)$ is equal to the union of $\{b\}$ and the closed-open interval $[a, b)$. In other words: $$ [a, b+1) = \{b\} \cup [a, b) $$

Nat.Ico_insert_succ_left theorem

(h : a < b) : insert a (Ico a.succ b) = Ico a b

Full source

theorem Ico_insert_succ_left (h : a < b) : insert a (Ico a.succ b) = Ico a b := by
  rw [Ico_succ_left, ← Ioo_insert_left h]

Insertion of Left Endpoint in Closed-Open Interval of Natural Numbers

Informal description

For any natural numbers $a$ and $b$ with $a < b$, the closed-open interval $[a, b)$ is equal to the union of $\{a\}$ and the closed-open interval $[a+1, b)$. That is: $$ \{a\} \cup [a+1, b) = [a, b) $$

Nat.Icc_insert_succ_left theorem

(h : a ≤ b) : insert a (Icc (a + 1) b) = Icc a b

Full source

lemma Icc_insert_succ_left (h : a ≤ b) : insert a (Icc (a + 1) b) = Icc a b := by
  ext x
  simp only [mem_insert, mem_Icc]
  omega

Insertion of Left Endpoint in Closed Interval of Natural Numbers

Informal description

For any natural numbers $a$ and $b$ with $a \leq b$, the closed interval $[a, b]$ is equal to the union of $\{a\}$ and the closed interval $[a+1, b]$. In other words: $$ \{a\} \cup [a+1, b] = [a, b] $$

Nat.Icc_insert_succ_right theorem

(h : a ≤ b + 1) : insert (b + 1) (Icc a b) = Icc a (b + 1)

Full source

lemma Icc_insert_succ_right (h : a ≤ b + 1) : insert (b + 1) (Icc a b) = Icc a (b + 1) := by
  ext x
  simp only [mem_insert, mem_Icc]
  omega

Insertion of Right Endpoint Successor in Closed Interval of Natural Numbers

Informal description

For any natural numbers $a$ and $b$ with $a \leq b + 1$, the closed interval $[a, b + 1]$ is equal to the union of the closed interval $[a, b]$ and the singleton $\{b + 1\}$. In other words: $$ [a, b] \cup \{b + 1\} = [a, b + 1] $$

Nat.image_sub_const_Ico theorem

(h : c ≤ a) : ((Ico a b).image fun x => x - c) = Ico (a - c) (b - c)

Full source

theorem image_sub_const_Ico (h : c ≤ a) :
    ((Ico a b).image fun x => x - c) = Ico (a - c) (b - c) := by
  ext x
  simp_rw [mem_image, mem_Ico]
  refine ⟨?_, fun h ↦ ⟨x + c, by omega⟩⟩
  rintro ⟨x, hx, rfl⟩
  omega

Image of Shifted Subtraction on Closed-Open Interval of Naturals

Informal description

For natural numbers $a, b, c$ with $c \leq a$, the image of the function $x \mapsto x - c$ applied to the interval $[a, b)$ is equal to the interval $[a - c, b - c)$. In other words: $$\{x - c \mid x \in [a, b)\} = [a - c, b - c)$$

Nat.Ico_image_const_sub_eq_Ico theorem

(hac : a ≤ c) : ((Ico a b).image fun x => c - x) = Ico (c + 1 - b) (c + 1 - a)

Full source

theorem Ico_image_const_sub_eq_Ico (hac : a ≤ c) :
    ((Ico a b).image fun x => c - x) = Ico (c + 1 - b) (c + 1 - a) := by
  ext x
  simp_rw [mem_image, mem_Ico]
  refine ⟨?_, fun h ↦ ⟨c - x, by omega⟩⟩
  rintro ⟨x, hx, rfl⟩
  omega

Image of Subtraction under Closed-Open Interval of Naturals

Informal description

For natural numbers $a, b, c$ with $a \leq c$, the image of the function $x \mapsto c - x$ applied to the interval $[a, b)$ is equal to the interval $[c + 1 - b, c + 1 - a)$. In other words: $$\{c - x \mid x \in [a, b)\} = [c + 1 - b, c + 1 - a)$$

Nat.Ico_succ_left_eq_erase_Ico theorem

: Ico a.succ b = erase (Ico a b) a

Full source

theorem Ico_succ_left_eq_erase_Ico : Ico a.succ b = erase (Ico a b) a := by
  ext x
  rw [Ico_succ_left, mem_erase, mem_Ico, mem_Ioo, ← and_assoc, ne_comm,
    and_comm (a := a ≠ x), lt_iff_le_and_ne]

Successor Left Endpoint Converts Closed-Open Interval to Interval Minus Left Endpoint: $[a+1, b) = [a, b) \setminus \{a\}$

Informal description

For any natural numbers $a$ and $b$, the closed-open interval $[a+1, b)$ is equal to the interval $[a, b)$ with the element $a$ removed. In other words: $$ [a+1, b) = [a, b) \setminus \{a\} $$

Nat.mod_injOn_Ico theorem

(n a : ℕ) : Set.InjOn (· % a) (Finset.Ico n (n + a))

Full source

theorem mod_injOn_Ico (n a : ℕ) : Set.InjOn (· % a) (Finset.Ico n (n + a)) := by
  induction' n with n ih
  · simp only [zero_add, Ico_zero_eq_range]
    rintro k hk l hl (hkl : k % a = l % a)
    simp only [Finset.mem_range, Finset.mem_coe] at hk hl
    rwa [mod_eq_of_lt hk, mod_eq_of_lt hl] at hkl
  rw [Ico_succ_left_eq_erase_Ico, succ_add, succ_eq_add_one,
    Ico_succ_right_eq_insert_Ico (by omega)]
  rintro k hk l hl (hkl : k % a = l % a)
  have ha : 0 < a := Nat.pos_iff_ne_zero.2 <| by rintro rfl; simp at hk
  simp only [Finset.mem_coe, Finset.mem_insert, Finset.mem_erase] at hk hl
  rcases hk with ⟨hkn, rfl | hk⟩ <;> rcases hl with ⟨hln, rfl | hl⟩
  · rfl
  · rw [add_mod_right] at hkl
    refine (hln <| ih hl ?_ hkl.symm).elim
    simpa using Nat.lt_add_of_pos_right (n := n) ha
  · rw [add_mod_right] at hkl
    suffices k = n by contradiction
    refine ih hk ?_ hkl
    simpa using Nat.lt_add_of_pos_right (n := n) ha
  · refine ih ?_ ?_ hkl <;> simp only [Finset.mem_coe, hk, hl]

Injectivity of Modulo Operation on Interval $[n, n + a)$ in Natural Numbers

Informal description

For any natural numbers $n$ and $a$, the modulo operation $\cdot \bmod a$ is injective on the closed-open interval $[n, n + a)$ of natural numbers. In other words, for any $x, y \in [n, n + a)$, if $x \bmod a = y \bmod a$, then $x = y$.

Nat.image_Ico_mod theorem

(n a : ℕ) : (Ico n (n + a)).image (· % a) = range a

Full source

/-- 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 image_Ico_mod (n a : ℕ) : (Ico n (n + a)).image (· % a) = range a := by
  obtain rfl | ha := eq_or_ne a 0
  · rw [range_zero, add_zero, Ico_self, image_empty]
  ext i
  simp only [mem_image, exists_prop, mem_range, mem_Ico]
  constructor
  · rintro ⟨i, _, rfl⟩
    exact mod_lt i ha.bot_lt
  intro hia
  have hn := Nat.mod_add_div n a
  obtain hi | hi := lt_or_le i (n % a)
  · refine ⟨i + a * (n / a + 1), ⟨?_, ?_⟩, ?_⟩
    · rw [add_comm (n / a), Nat.mul_add, mul_one, ← add_assoc]
      refine hn.symm.le.trans (Nat.add_le_add_right ?_ _)
      simpa only [zero_add] using add_le_add (zero_le i) (Nat.mod_lt n ha.bot_lt).le
    · refine lt_of_lt_of_le (Nat.add_lt_add_right hi (a * (n / a + 1))) ?_
      rw [Nat.mul_add, mul_one, ← add_assoc, hn]
    · rw [Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt hia]
  · refine ⟨i + a * (n / a), ⟨?_, ?_⟩, ?_⟩
    · omega
    · omega
    · rw [Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt hia]

Modulo Operation Maps Interval to Full Range: $[n, n+a) \bmod a = \{0, \dots, a-1\}$

Informal description

For any natural numbers $n$ and $a$, the image of the modulo operation $\cdot \bmod a$ applied to the half-open interval $[n, n + a)$ is equal to the finite set $\{0, 1, \dots, a-1\}$.

Nat.multiset_Ico_map_mod theorem

(n a : ℕ) : (Multiset.Ico n (n + a)).map (· % a) = Multiset.range a

Full source

theorem multiset_Ico_map_mod (n a : ℕ) :
    (Multiset.Ico n (n + a)).map (· % a) = Multiset.range a := by
  convert congr_arg Finset.val (image_Ico_mod n a)
  refine ((nodup_map_iff_inj_on (Finset.Ico _ _).nodup).2 <| ?_).dedup.symm
  exact mod_injOn_Ico _ _

Modulo Operation Maps Interval Multiset to Full Range Multiset: $[n, n+a) \bmod a = \{0, \dots, a-1\}$

Informal description

For any natural numbers $n$ and $a$, the multiset obtained by applying the modulo operation $\cdot \bmod a$ to each element of the closed-open interval multiset $[n, n + a)$ is equal to the multiset $\{0, 1, \dots, a-1\}$.

List.toFinset_range'_1 theorem

(a b : ℕ) : (List.range' a b).toFinset = Ico a (a + b)

Full source

lemma toFinset_range'_1 (a b : ℕ) : (List.range' a b).toFinset = Ico a (a + b) := by
  ext x
  rw [List.mem_toFinset, List.mem_range'_1, Finset.mem_Ico]

Conversion of Range List to Closed-Open Interval Finset: $\text{toFinset}(\text{range'}\ a\ b) = [a, a + b)$

Informal description

For any natural numbers $a$ and $b$, the finset obtained by converting the list `List.range' a b` to a finset is equal to the closed-open interval finset $\text{Ico}(a, a + b)$. In other words, $\text{toFinset}(\text{range'}\ a\ b) = [a, a + b)$.

List.toFinset_range'_1_1 theorem

(a : ℕ) : (List.range' 1 a).toFinset = Icc 1 a

Full source

lemma toFinset_range'_1_1 (a : ℕ) : (List.range' 1 a).toFinset = Icc 1 a := by
  ext x
  rw [List.mem_toFinset, List.mem_range'_1, add_comm, Nat.lt_succ_iff, Finset.mem_Icc]

Conversion of Range List to Closed Interval Finset: $\text{toFinset}(\text{range'}\ 1\ a) = [1, a]$

Informal description

For any natural number $a$, the finset obtained by converting the list $\text{range'}\ 1\ a$ to a finset is equal to the closed interval finset $[1, a]$, i.e., $\text{toFinset}(\text{range'}\ 1\ a) = [1, a]$.

Finset.range_image_pred_top_sub theorem

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

Full source

theorem range_image_pred_top_sub (n : ℕ) :
    ((Finset.range n).image fun j => n - 1 - j) = Finset.range n := by
  cases n
  · rw [range_zero, image_empty]
  · rw [Finset.range_eq_Ico, Nat.Ico_image_const_sub_eq_Ico (Nat.zero_le _)]
    simp_rw [succ_sub_succ, Nat.sub_zero, Nat.sub_self]

Involution Property of Range Subtraction: $\{n-1-j \mid j \in [0, n)\} = [0, n)$

Informal description

For any natural number $n$, the image of the function $j \mapsto n - 1 - j$ applied to the finset $\text{range}(n) = \{0, 1, \dots, n-1\}$ is equal to $\text{range}(n)$ itself. In other words: $$\{n - 1 - j \mid j \in \{0, 1, \dots, n-1\}\} = \{0, 1, \dots, n-1\}$$

Finset.range_add_eq_union theorem

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

Full source

theorem range_add_eq_union : range (a + b) = rangerange a ∪ (range b).map (addLeftEmbedding a) := by
  rw [Finset.range_eq_Ico, map_eq_image]
  convert (Ico_union_Ico_eq_Ico a.zero_le (a.le_add_right b)).symm
  ext x
  simp only [Ico_zero_eq_range, mem_image, mem_range, addLeftEmbedding_apply, mem_Ico]
  constructor
  · aesop
  · rintro h
    exact ⟨x - a, by omega⟩

Range Addition as Union of Shifted Ranges: $\text{range}(a + b) = \text{range}(a) \cup (a + \text{range}(b))$

Informal description

For any natural numbers $a$ and $b$, the range of $a + b$ is equal to the union of the range of $a$ and the range of $b$ shifted left by $a$. That is, $$\text{range}(a + b) = \text{range}(a) \cup \{a + x \mid x \in \text{range}(b)\}.$$

Nat.decreasing_induction_of_not_bddAbove theorem

(h : ∀ n, P (n + 1) → P n) (hP : ¬BddAbove {x | P x}) (n : ℕ) : P n

Full source

theorem Nat.decreasing_induction_of_not_bddAbove (h : ∀ n, P (n + 1) → P n)
    (hP : ¬BddAbove { x | P x }) (n : ℕ) : P n :=
  let ⟨_, hm, hl⟩ := not_bddAbove_iff.1 hP n
  decreasingInduction (fun _ _ => h _) hm hl.le

Unbounded Decreasing Induction on Natural Numbers

Informal description

Let $P$ be a predicate on natural numbers such that for any $n$, if $P(n+1)$ holds then $P(n)$ holds. If the set $\{x \mid P(x)\}$ is not bounded above, then $P(n)$ holds for all natural numbers $n$.

Nat.strong_decreasing_induction theorem

(base : ∃ n, ∀ m > n, P m) (step : ∀ n, (∀ m > n, P m) → P n) (n : ℕ) : P n

Full source

@[elab_as_elim]
lemma Nat.strong_decreasing_induction (base : ∃ n, ∀ m > n, P m) (step : ∀ n, (∀ m > n, P m) → P n)
    (n : ℕ) : P n := by
  apply Nat.decreasing_induction_of_not_bddAbove (P := fun n ↦ ∀ m ≥ n, P m) _ _ n n le_rfl
  · intro n ih m hm
    rcases hm.eq_or_lt with rfl | hm
    · exact step n ih
    · exact ih m hm
  · rintro ⟨b, hb⟩
    rcases base with ⟨n, hn⟩
    specialize @hb (n + b + 1) (fun m hm ↦ hn _ _)
    all_goals omega

Strong Decreasing Induction Principle for Natural Numbers

Informal description

Let $P$ be a predicate on natural numbers. Suppose there exists a natural number $n$ such that $P(m)$ holds for all $m > n$, and for any natural number $n$, if $P(m)$ holds for all $m > n$, then $P(n)$ holds. Then $P(n)$ holds for all natural numbers $n$.

Nat.decreasing_induction_of_infinite theorem

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

Full source

theorem Nat.decreasing_induction_of_infinite
    (h : ∀ n, P (n + 1) → P n) (hP : { x | P x }.Infinite) (n : ℕ) : P n :=
  Nat.decreasing_induction_of_not_bddAbove h (mt BddAbove.finite hP) n

Infinite Set Decreasing Induction for Natural Numbers

Informal description

Let $P$ be a predicate on natural numbers such that for any $n$, if $P(n+1)$ holds then $P(n)$ holds. If the set $\{x \mid P(x)\}$ is infinite, then $P(n)$ holds for all natural numbers $n$.

Nat.cauchy_induction' theorem

 (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

Full source

theorem Nat.cauchy_induction' (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 := by
  apply Nat.decreasing_induction_of_infinite h fun hf => _
  intro hf
  obtain ⟨m, hP, hm⟩ := hf.exists_maximal_wrt id _ ⟨seed, hs⟩
  obtain ⟨y, hl, hy⟩ := hi m (le_of_not_lt fun hl => hl.ne <| hm seed hs hl.le) hP
  exact hl.ne (hm y hy hl.le)

Cauchy Induction with Seed and Infinite Extension

Informal description

Let $P$ be a predicate on natural numbers and let $\text{seed}$ be a natural number. Suppose that: 1. For any natural number $n$, if $P(n+1)$ holds then $P(n)$ holds. 2. The base case $P(\text{seed})$ holds. 3. For any $x \geq \text{seed}$, if $P(x)$ holds then there exists $y > x$ such that $P(y)$ holds. Then $P(n)$ holds for all natural numbers $n$.

Nat.cauchy_induction theorem

 (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

Full source

theorem Nat.cauchy_induction (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 :=
  seed.cauchy_induction' h hs (fun x hl hx => ⟨f x, hf x hl hx⟩) n

Cauchy Induction with Growth Function

Informal description

Let $P$ be a predicate on natural numbers and let $\text{seed}$ be a natural number. Suppose that: 1. For any natural number $n$, if $P(n+1)$ holds then $P(n)$ holds. 2. The base case $P(\text{seed})$ holds. 3. There exists a function $f : \mathbb{N} \to \mathbb{N}$ such that for any $x \geq \text{seed}$, if $P(x)$ holds then $x < f(x)$ and $P(f(x))$ holds. Then $P(n)$ holds for all natural numbers $n$.

Nat.cauchy_induction_mul theorem

 (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

Full source

theorem Nat.cauchy_induction_mul (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 := by
  apply Nat.cauchy_induction h _ hs (k * ·) fun x hl hP => ⟨_, hm x hl hP⟩
  intro _ hl _
  convert (Nat.mul_lt_mul_right <| seed.succ_pos.trans_le hl).2 hk
  rw [one_mul]

Cauchy Induction with Multiplicative Growth

Informal description

Let $P$ be a predicate on natural numbers, $k$ and $\text{seed}$ be natural numbers with $k > 1$, and suppose that: 1. For any natural number $n$, if $P(n+1)$ holds then $P(n)$ holds. 2. The base case $P(\text{seed}+1)$ holds. 3. For any $x > \text{seed}$, if $P(x)$ holds then $P(k \cdot x)$ holds. Then $P(n)$ holds for all natural numbers $n$.

Nat.cauchy_induction_two_mul theorem

 (h : ∀ n, P (n + 1) → P n) (seed : ℕ) (hs : P seed.succ) (hm : ∀ x, seed < x → P x → P (2 * x)) (n : ℕ) : P n

Full source

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

Cauchy Induction with Doubling Growth

Informal description

Let $P$ be a predicate on natural numbers and let $\text{seed}$ be a natural number. Suppose that: 1. For any natural number $n$, if $P(n+1)$ holds then $P(n)$ holds. 2. The base case $P(\text{seed}+1)$ holds. 3. For any $x > \text{seed}$, if $P(x)$ holds then $P(2 \cdot x)$ holds. Then $P(n)$ holds for all natural numbers $n$.

Nat.pow_imp_self_of_one_lt theorem

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

Full source

theorem Nat.pow_imp_self_of_one_lt {M} [Monoid M] (k : ℕ) (hk : 1 < k)
    (P : M → Prop) (hmul : ∀ x y, P x → P (x * y) ∨ P (y * x))
    (hpow : ∀ x, P (x ^ k) → P x) : ∀ n x, P (x ^ n) → P x :=
  k.cauchy_induction_mul (fun n ih x hx ↦ ih x <| (hmul _ x hx).elim
    (fun h ↦ by rwa [_root_.pow_succ]) fun h ↦ by rwa [_root_.pow_succ']) 0 hk
    (fun x hx ↦ pow_one x ▸ hx) fun n _ hn x hx ↦ hpow x <| hn _ <| (pow_mul x k n).subst hx

Implication of Power Predicate to Element Predicate in Monoids

Informal description

Let $M$ be a monoid, $k$ a natural number with $k > 1$, and $P$ a predicate on $M$. Suppose that: 1. For any $x, y \in M$, if $P(x)$ holds then either $P(x \cdot y)$ or $P(y \cdot x)$ holds. 2. For any $x \in M$, if $P(x^k)$ holds then $P(x)$ holds. Then for any natural number $n$ and any $x \in M$, if $P(x^n)$ holds then $P(x)$ holds.

TODO