Commit 2023-02-03 06:59 cc3de2a9

View on Github →

feat: port Order.SuccPred.LinearLocallyFinite (#2033)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/SuccPred/LinearLocallyFinite.lean

added theorem LinearLocallyFiniteOrder.isGLB_Ioc_of_isGLB_Ioi

added theorem LinearLocallyFiniteOrder.isMax_of_succFn_le

added theorem LinearLocallyFiniteOrder.le_of_lt_succFn

added theorem LinearLocallyFiniteOrder.le_succFn

added theorem LinearLocallyFiniteOrder.succFn_le_of_lt

added theorem LinearLocallyFiniteOrder.succFn_spec

added theorem injective_toZ

added theorem iterate_pred_toZ

added theorem iterate_succ_toZ

added theorem le_of_toZ_le

added def orderIsoNatOfLinearSuccPredArch

added def orderIsoRangeOfLinearSuccPredArch

added def toZ

added theorem toZ_iterate_pred

added theorem toZ_iterate_pred_ge

added theorem toZ_iterate_pred_of_not_isMin

added theorem toZ_iterate_succ

added theorem toZ_iterate_succ_le

added theorem toZ_iterate_succ_of_not_isMax

added theorem toZ_le_iff

added theorem toZ_mono

added theorem toZ_neg

added theorem toZ_nonneg

added theorem toZ_of_eq

added theorem toZ_of_ge

added theorem toZ_of_lt