contravariant_lt_of_covariant_le — Mathlib

English

If a linear order and Covariant with ≤ exist, then there is a contravariant with <.

Русский

Если существует линейный порядок и ковариантность по ≤, то существует противоречивость по <.

LaTeX

$$$[LinearOrder\ N]\; Contravariant(M,N,μ,<) \leftarrow Covariant(M,N,μ,\le)$$$

Lean4

instance contravariant_lt_of_covariant_le [LinearOrder N] [CovariantClass N N mu (· ≤ ·)] :
    ContravariantClass N N mu (· < ·) where elim := (covariant_le_iff_contravariant_lt N N mu).mp CovariantClass.elim

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