mathlib
b7581040 - feat(order/basic): a symmetric relation implies equality when it implies less-equal (#15149)

Commit

3 years ago

feat(order/basic): a symmetric relation implies equality when it implies less-equal (#15149) Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

Author

vihdzp

Parents