Theorem le_total_of_directed

Modification history

2026-02-22 13:15
Mathlib/Order/SuccPred/Archimedean.lean
chore(Order/SuccPred/Archimedean): use `to_dual` (#34882)
Deleted le_total_of_directedView on Github →
2024-10-14 12:17
Mathlib/Order/SuccPred/Archimedean.lean
feat(Order/SuccPred): add instances for OrdConnected subtypes (#16766)
Added le_total_of_directedView on Github →