English
If μ is contravariant with respect to equality and strict order, it is contravariant with respect to ≤.
Русский
Если μ контравариантна относительно = и <, тогда она контравариантна относительно ≤.
LaTeX
$$$\operatorname{Contravariant}_{\le}(\mu)$ follows from $\operatorname{Contravariant}_{=}(\mu)$ and $\operatorname{Contravariant}_{<}(\mu)$.$$
Lean4
theorem contravariant_le_of_contravariant_eq_and_lt [PartialOrder N] [ContravariantClass M N μ (· = ·)]
[ContravariantClass M N μ (· < ·)] : ContravariantClass M N μ (· ≤ ·) where
elim :=
(contravariant_le_iff_contravariant_lt_and_eq M N μ).mpr
⟨ContravariantClass.elim, ContravariantClass.elim⟩
/- TODO:
redefine `IsLeftCancel N mu` as abbrev of `ContravariantClass N N mu (· = ·)`,
redefine `IsRightCancel N mu` as abbrev of `ContravariantClass N N (flip mu) (· = ·)`,
redefine `IsLeftCancelMul` as abbrev of `IsLeftCancel`,
then the following four instances (actually eight) can be removed in favor of the above two. -/
