mathlib3
71e9f90d - feat(order/basic): Slightly generalized `densely_ordered` (#10664)

Commit

4 years ago

feat(order/basic): Slightly generalized `densely_ordered` (#10664) Changed `[preorder α]` to `[has_lt α]`.

Author

vihdzp

Parents