Documentation

Mathlib.Data.Nat.Set

Recursion on the natural numbers and Set.range #

@[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_2} (x : α) (f : αα) :
(Set.range fun n => Nat.rec x f n) = {x} Set.range fun n => Nat.rec (f 0 x) (f Nat.succ) n
theorem Nat.range_casesOn {α : Type u_2} (x : α) (f : α) :
(Set.range fun n => Nat.casesOn n x f) = {x} Set.range f