Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-16 02:20 59954c19

View on Github →

docs(data/pfun): add module docstring and def docstrings (#8629)

Estimated changes

modified def pfun.core
modified theorem pfun.core_def
modified theorem pfun.core_res
modified theorem pfun.core_restrict
modified theorem pfun.dom_iff_graph
modified def pfun.image
modified theorem pfun.image_def
modified theorem pfun.mem_core
modified theorem pfun.mem_image
modified theorem pfun.mem_preimage
modified def pfun.preimage
modified theorem pfun.preimage_def
modified theorem pfun.pure_defined
modified def pfun.ran
modified def pfun