Commit 2023-08-25 22:21 467c358f

View on Github →

feat(Logic/Relation): add missing relation material and show ⩿ = ReflGen (· ⋖ ·) (#6711)

Estimated changes

Modified Mathlib/Logic/Relation.lean

added theorem Relation.reflGen_eq_self

added theorem Relation.reflGen_minimal

added theorem Relation.reflGen_transGen

added theorem Relation.reflTransGen_eq_reflGen

added theorem Relation.reflTransGen_eq_transGen

added theorem Relation.reflTransGen_idem

added theorem Relation.reflTransGen_minimal

added theorem Relation.reflTransGen_reflGen

added theorem Relation.reflTransGen_transGen

deleted theorem Relation.refl_trans_gen_idem

added theorem Relation.reflexive_reflGen

added theorem Relation.transGen_minimal

added theorem Relation.transGen_reflGen

Modified Mathlib/Order/Cover.lean

added theorem reflTransGen_wcovby_eq_reflTransGen_covby

added theorem transGen_wcovby_eq_reflTransGen_covby

added theorem wcovby_eq_reflGen_covby