Commit 2022-08-24 11:42 2629553c

View on Github →

feat: port 'section relation' in Init/Logic (#379) #34 left section relation as a TODO. This PR fills it in. Compare to the Lean 3 version: https://github.com/leanprover-community/lean/blob/741670c439f1ca266bc7fe61ef7212cc9afd9dd8/library/init/logic.lean#L1027-L1062

Estimated changes

added def anti_symmetric
added def empty_relation
added def equivalence
added theorem inv_image.irreflexive
added theorem inv_image.trans
added def inv_image
added def irreflexive
added theorem mk_equivalence
added def reflexive
added def subrelation
added def symmetric
added def total
added def transitive