mathlib3

cd1d839a - feat(order/rel_classes): Unbundled typeclass to state that two relations are the non strict and strict versions (#11381)

feat(order/rel_classes): Unbundled typeclass to state that two relations are the non strict and strict versions (#11381) This defines a Prop-valued mixin `is_nonstrict_strict_order α r s` to state `s a b ↔ r a b ∧ ¬ r b a`. The idea is to allow dot notation for lemmas about the interaction of `⊆` and `⊂` (which currently do not have a `preorder`-like typeclass). Dot notation on each of them is already possible thanks to unbundled relation classes (which allow to state lemmas for both `set` and `finset`).