Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-10 23:42 13bc7a20

View on Github →

feat(data/pfun): review APIs, add some lemmas about fix_induction (#17004)

Estimated changes

Modified src/data/pfun.lean

modified theorem pfun.fix_fwd

added theorem pfun.fix_fwd_eq

modified def pfun.fix_induction'

added theorem pfun.fix_induction'_fwd

added theorem pfun.fix_induction'_stop

modified def pfun.fix_induction

added theorem pfun.fix_induction_spec

modified theorem pfun.fix_stop