Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-12 21:42 55534c4f

View on Github →

feat(data/nat/basic): recursion for set nat (#10273) Adding a special case of nat.le_rec_on where the predicate is membership of a subset.

Estimated changes

added theorem nat.set_eq_univ
added theorem nat.set_induction