Theorem lt_or_le_of_codirected

Modification history

2024-10-14 12:17

Mathlib/Order/SuccPred/Archimedean.lean

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

Added lt_or_le_of_codirected View on Github →