[Merged by Bors] - refactor(order/directed): use (≥) instead of swap (≤)

[urkud]

---

[eric-wieser]

My slight worry here is that all the covariant_class stuff is stated with swap, and while they likely don't interact directly, this makes thing inconsistent.

On the other hand, maybe we're fine to use (≥) in those places too if swap is reducible enough.

[urkud]

My slight worry here is that all the covariant_class stuff is stated with swap, and while they likely don't interact directly, this makes thing inconsistent.

On the other hand, maybe we're fine to use (≥) in those places too if swap is reducible enough.

I can see swap on the operation but not on the relation. OTOH, filter.is_bounded uses (≤) and (≥) (I'm going to reformulate some theorems there using is_directed).

[fpvandoorn]

This seems like a clear improvement. If there are any swap (≤) in the co[ntra]variant classes, then I think those should be changed too. But as Yury said, I think those are also applied to the operation.

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests