covariant_lt_of_contravariant_le — Mathlib

English

Let N be a linearly ordered set and μ: N × N → N be contravariant with respect to ≤. Then μ is covariant with respect to <.

Русский

Пусть N упорядочено линейно и μ: N × N → N контравариантна относительно ⩽. Тогда μ ковариантна относительно <.

LaTeX

$$$\operatorname{Covariant}_{<}(\mu) \quad\text{given}\quad \operatorname{Contravariant}_{\le}(\mu).$$$

Lean4

instance covariant_lt_of_contravariant_le [LinearOrder N] [ContravariantClass N N mu (· ≤ ·)] :
    CovariantClass N N mu (· < ·) where elim := (covariant_lt_iff_contravariant_le N N mu).mpr ContravariantClass.elim

Похожие утверждения