Commit 2022-10-19 04:27 10fdf3b3

View on Github →

feat: port Logic/Relator (#385) Port logic/relator.lean and add comments in the places where the linter demands them. Compare to the mathlib3 version: https://github.com/leanprover-community/mathlib/blob/7362d50a80c3e7f7a1fb5adb1c0b6ba593db103d/src/logic/relator.lean

Estimated changes

Modified Mathlib.lean

Created Mathlib/Logic/Relator.lean

added theorem Relator.BiTotal.rel_exists

added theorem Relator.BiTotal.rel_forall

added def Relator.BiTotal

added def Relator.BiUnique

added theorem Relator.LeftTotal.rel_exists

added def Relator.LeftTotal

added theorem Relator.LeftUnique.flip

added def Relator.LeftUnique

added def Relator.LiftFun

added theorem Relator.RightTotal.rel_forall

added def Relator.RightTotal

added def Relator.RightUnique

added theorem Relator.bi_total_eq

added theorem Relator.left_unique_of_rel_eq

added theorem Relator.rel_and

added theorem Relator.rel_eq

added theorem Relator.rel_iff

added theorem Relator.rel_imp

added theorem Relator.rel_not

added theorem Relator.rel_or