Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-06-11 14:04 205e3b4e

View on Github →

feat(logic/relation): add relation composition, map, and bi_unique

Estimated changes

Modified logic/relation.lean

added def relation.comp

added theorem relation.comp_assoc

added theorem relation.comp_eq

added theorem relation.comp_iff

added theorem relation.eq_comp

added theorem relation.flip_comp

added theorem relation.iff_comp

Created logic/relator.lean

added def relator.bi_unique

added theorem relator.left_unique_flip

added theorem relator.rel_and

added theorem relator.rel_eq

added theorem relator.rel_iff

added theorem relator.rel_or