Commit 2024-10-14 12:17 c8c6a5f1

View on Github →

feat(Order/SuccPred): add instances for OrdConnected subtypes (#16766)

Estimated changes

added theorem le_total_of_codirected
added theorem le_total_of_directed
added theorem lt_or_le_of_codirected
added theorem lt_or_le_of_directed
added theorem coe_pred_of_mem
added theorem coe_succ_of_mem
added theorem isMax_of_not_succ_mem
added theorem isMin_of_not_pred_mem
added theorem not_pred_mem_iff_isMin
added theorem not_succ_mem_iff_isMax