Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-17 20:29 152bf15a

View on Github →

feat(data/fin): pred_above_monotone (#6170)

Estimated changes

Modified src/data/fin.lean

added theorem fin.cast_pred_monotone

added theorem fin.cast_succ_lt_cast_succ_iff

added theorem fin.pred_above_left_monotone

added theorem fin.pred_above_right_monotone

Modified src/order/preorder_hom.lean

added def order_embedding.to_preorder_hom

added theorem order_embedding.to_preorder_hom_coe