mathlib3 documentation

data.nat.set

Recursion on the natural numbers and set.range #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
theorem nat.zero_union_range_succ  :
{0} ∪ set.range nat.succ = set.univ
source
@[protected, simp]
theorem nat.range_succ  :
set.range nat.succ = {i : ℕ | 0 < i}
source
theorem nat.range_of_succ {α : Type u_1} (f : ℕ → α) :
{f 0} ∪ set.range (f ∘ nat.succ) = set.range f
source
theorem nat.range_rec {α : Type u_1} (x : α) (f : ℕ → α → α) :
set.range (λ (n : ℕ), nat.rec x f n) = {x} ∪ set.range (λ (n : ℕ), nat.rec (f 0 x) (f ∘ nat.succ) n)
source
theorem nat.range_cases_on {α : Type u_1} (x : α) (f : ℕ → α) :
set.range (λ (n : ℕ), n.cases_on x f) = {x} ∪ set.range f