Commit 2022-11-16 23:18 99333e89

View on Github →

feat: port Logic.Relation (#565) mathlib3 sha: 5ca6e9d2bb25feeebdefe9bd9de163897bdecd05 Relatively straightforward. Depends on #559 (EqvGen) and #561 (mk-iffs attribute)

Estimated changes

added theorem Equivalence.reflexive
added theorem Equivalence.symmetric
added theorem Equivalence.transitive
added theorem Acc.TransGen
added theorem Acc.of_downward_closed
added theorem Acc.of_fibration
added theorem Equivalence.comap
added theorem Equivalence.eqvGen_eq
added theorem Equivalence.eqvGen_iff
added theorem EqvGen.mono
added theorem IsRefl.reflexive
added theorem Reflexive.comap
added theorem Reflexive.ne_imp_iff
added def Relation.Comp
added def Relation.Join
added theorem Relation.ReflGen.mono
added inductive Relation.ReflGen
added inductive Relation.ReflTransGen
added theorem Relation.TransGen.head
added theorem Relation.TransGen.lift
added theorem Relation.TransGen.mono
added theorem Relation.TransGen.swap
added inductive Relation.TransGen
added theorem Relation.church_rosser
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
added theorem Relation.transGen_idem
added theorem Relation.transGen_swap
added theorem Symmetric.comap
added theorem Symmetric.flip_eq
added theorem Symmetric.swap_eq
added theorem Transitive.comap
added theorem WellFounded.transGen
added theorem acc_transGen_iff
added theorem flip_eq_iff
added theorem reflexive_ne_imp_iff
added theorem swap_eq_iff