Theorem le_total_of_directed

Modification history

2024-10-14 12:17

Mathlib/Order/SuccPred/Archimedean.lean

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

Added le_total_of_directed View on Github →