Commit 2022-01-12 22:49 e6fab1dc

View on Github →

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.

Estimated changes

added theorem directed_id
added theorem directed_of
added theorem exists_ge_ge
added theorem exists_le_le
added theorem is_directed_mono