Theorem coe_pred_of_mem

Modification history

2024-10-14 12:17

Mathlib/Order/SuccPred/Basic.lean

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

Added coe_pred_of_mem View on Github →