Commit 2023-07-14 19:11 8d3c56c0

View on Github →

chore: re-port Init.Function (#5859) Notably this fixes the naming of comp_left and comp_right.

Estimated changes

modified def Function.Bijective
modified def Function.Injective
modified def Function.LeftInverse
modified def Function.RightInverse
modified def Function.Surjective
modified def Function.app
modified theorem Function.bijective_id
modified def Function.combine
modified theorem Function.comp.assoc
modified theorem Function.comp.left_id
modified theorem Function.comp.right_id
modified theorem Function.comp_const_right
deleted def Function.comp_left
deleted def Function.comp_right
modified def Function.curry
modified theorem Function.curry_uncurry
added def Function.dcomp
modified theorem Function.injective_id
modified theorem Function.left_id
modified def Function.onFun
modified theorem Function.right_id
modified theorem Function.surjective_id
modified def Function.swap
modified def Function.uncurry
modified theorem Function.uncurry_curry