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.

@[protected, simp]
theorem nat.range_succ  :
set.range nat.succ = {i : | 0 < i}
theorem nat.range_of_succ {α : Type u_1} (f : α) :
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)
theorem nat.range_cases_on {α : Type u_1} (x : α) (f : α) :
set.range (λ (n : ), n.cases_on x f) = {x} set.range f