basic): generalize from `linear_order` to `preorder` (#18876)

Commit

2 years ago

feat(data/set/intervals/basic): generalize from `linear_order` to `preorder` (#18876) The lemma statements are unchanged, but the proofs are rewritten

Author

eric-wieser

Parents

e4bc74cb

mathlib 4367b192 - feat(data/set/intervals/basic): generalize from `linear_order` to `preorder` (#18876)

mathlib
4367b192 - feat(data/set/intervals/basic): generalize from `linear_order` to `preorder` (#18876)