mathlib

e6fab1dc - refactor(order/directed): Make `is_directed` a Prop mixin (#11238)

refactor(order/directed): Make `is_directed` a Prop mixin (#11238) This turns `directed_order` into a Prop-valued mixin `is_directed`. The design follows the unbundled relation classes found in core Lean. The current design created obscure problems when showing that a `semilattice_sup` is directed and we couldn't even state that `semilattice_inf` is codirected. Further, it was kind of already used as a mixin, because there was no point inserting it in the hierarchy.