Commit 2023-01-02 20:39 cdfaca59

View on Github →

feat: port Order.SuccPred.Relation (#1295) Port Order.SuccPred.Relation. This is my first port, but there were very few things that I needed to change from the file Mathport generated in order to get things to compile.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/SuccPred/Relation.lean

added theorem reflTransGen_of_pred

added theorem reflTransGen_of_pred_of_ge

added theorem reflTransGen_of_pred_of_le

added theorem reflTransGen_of_succ

added theorem reflTransGen_of_succ_of_ge

added theorem reflTransGen_of_succ_of_le

added theorem transGen_of_pred_of_gt

added theorem transGen_of_pred_of_lt

added theorem transGen_of_pred_of_ne

added theorem transGen_of_pred_of_reflexive

added theorem transGen_of_succ_of_gt

added theorem transGen_of_succ_of_lt

added theorem transGen_of_succ_of_ne

added theorem transGen_of_succ_of_reflexive