Mathlib.Data.Nat.Set

Nat.zero_union_range_succ theorem

: {0} ∪ range succ = univ

Full source

theorem zero_union_range_succ : {0}{0} ∪ range succ = univ := by
  ext n
  cases n <;> simp

Universal Set Decomposition via Zero and Successor Range

Informal description

The union of the singleton set $\{0\}$ and the range of the successor function on natural numbers is equal to the universal set of natural numbers, i.e., $\{0\} \cup \text{range}(\text{succ}) = \text{univ}$.

Nat.range_succ theorem

: range succ = {i | 0 < i}

Full source

@[simp]
protected theorem range_succ : range succ = { i | 0 < i } := by
  ext (_ | i) <;> simp [succ_pos, succ_ne_zero, Set.mem_setOf]

Range of Successor Function Equals Positive Natural Numbers

Informal description

The range of the successor function on natural numbers is equal to the set of all positive natural numbers, i.e., $\text{range}(\text{succ}) = \{i \in \mathbb{N} \mid 0 < i\}$.

Nat.range_of_succ theorem

(f : ℕ → α) : {f 0} ∪ range (f ∘ succ) = range f

Full source

theorem range_of_succ (f : ℕ → α) : {f 0}{f 0} ∪ range (f ∘ succ) = range f := by
  rw [← image_singleton, range_comp, ← image_union, zero_union_range_succ, image_univ]

Range Decomposition via Initial Value and Successor Composition

Informal description

For any function $f \colon \mathbb{N} \to \alpha$, the union of the singleton set $\{f(0)\}$ and the range of the composition $f \circ \mathrm{succ}$ is equal to the range of $f$, i.e., $\{f(0)\} \cup \mathrm{range}(f \circ \mathrm{succ}) = \mathrm{range}(f)$.

Nat.range_rec theorem

 {α : Type*} (x : α) (f : ℕ → α → α) :
  (Set.range fun n => Nat.rec x f n : Set α) = { x } ∪ Set.range fun n => Nat.rec (f 0 x) (f ∘ succ) n

Full source

theorem range_rec {α : Type*} (x : α) (f : ℕ → α → α) :
    (Set.range fun n => Nat.rec x f n : Set α) =
      {x}{x} ∪ Set.range fun n => Nat.rec (f 0 x) (f ∘ succ) n := by
  convert (range_of_succ (fun n => Nat.rec x f n : ℕ → α)).symm using 4
  dsimp
  rename_i n
  induction n with
  | zero => rfl
  | succ n ihn => dsimp at ihn ⊢; rw [ihn]

Range Decomposition for Recursive Functions on Natural Numbers

Informal description

For any type $\alpha$, element $x \in \alpha$, and function $f \colon \mathbb{N} \to \alpha \to \alpha$, the range of the function defined by recursion on natural numbers (starting with $x$ and applying $f$ at each step) is equal to the union of the singleton set $\{x\}$ and the range of the function defined by recursion starting with $f(0)(x)$ and applying $f \circ \mathrm{succ}$ at each step. That is, $$\mathrm{range}(\lambda n.\ \mathrm{rec}\ n\ x\ f) = \{x\} \cup \mathrm{range}(\lambda n.\ \mathrm{rec}\ n\ (f(0)(x))\ (f \circ \mathrm{succ})).$$

Nat.range_casesOn theorem

{α : Type*} (x : α) (f : ℕ → α) : (Set.range fun n => Nat.casesOn n x f : Set α) = { x } ∪ Set.range f

Full source

theorem range_casesOn {α : Type*} (x : α) (f : ℕ → α) :
    (Set.range fun n => Nat.casesOn n x f : Set α) = {x}{x} ∪ Set.range f :=
  (range_of_succ _).symm

Range of Cases Function Equals Union of Singleton and Range

Informal description

For any type $\alpha$, element $x \in \alpha$, and function $f \colon \mathbb{N} \to \alpha$, the range of the function defined by cases on natural numbers (returning $x$ at zero and $f(n)$ otherwise) equals the union of $\{x\}$ with the range of $f$, i.e., $$\mathrm{range}(\lambda n.\ \mathrm{casesOn}\ n\ x\ f) = \{x\} \cup \mathrm{range}(f).$$