Commit 2024-02-01 16:22 a55d1223

View on Github →

feat(Data/Fin/Basic): Improvement and extension of order results (#10156) Refines and extends results relating to the monotonicity of succ, castSucc, and related functions

Estimated changes

Modified Mathlib/Algebra/BigOperators/Fin.lean

Modified Mathlib/Combinatorics/SimpleGraph/Clique.lean

Modified Mathlib/Data/Fin/Basic.lean

added theorem Fin.castPred_le_pred_iff

added theorem Fin.castSucc_pred_lt_iff

added theorem Fin.castpred_succ_le_iff

deleted theorem Fin.le_castPred_succ_iff

added theorem Fin.lt_castPred_succ_iff

added theorem Fin.lt_succ_castPred_iff

added theorem Fin.monotone_castPred_comp

added theorem Fin.monotone_pred_comp

added theorem Fin.pred_castSucc_lt_iff

modified theorem Fin.pred_lt_castPred

added theorem Fin.pred_lt_castPred_iff

added theorem Fin.strictMono_castPred_comp

added theorem Fin.strictMono_pred_comp

added theorem Fin.strictMono_succ

added theorem Fin.succAbove_le_succAbove_iff

added theorem Fin.succAbove_lt_succAbove_iff

added def Fin.succEmb

deleted def Fin.succEmbedding

modified theorem Fin.succ_injective

added theorem Fin.val_succEmb

deleted theorem Fin.val_succEmbedding

Modified Mathlib/Data/Fintype/Fin.lean

modified theorem Fin.Ioi_succ

modified theorem Fin.Ioi_zero_eq_map