Theorem le_total_of_codirected

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_codirected View on Github →