covariant_lt_of_covariant_le_of_contravariant_eq

English

Covariance with respect to the strict order transfers under suitable hypotheses.

Русский

Ковариантность относительно строгого порядка сохраняется при соответствующих условиях.

LaTeX

$$$\operatorname{Covariant}_{<}$ holds under suitable hypotheses.$$

Lean4

theorem covariant_lt_of_covariant_le_of_contravariant_eq [ContravariantClass M N μ (· = ·)] [PartialOrder N]
    [CovariantClass M N μ (· ≤ ·)] : CovariantClass M N μ (· < ·) where
  elim a _ _ bc := (CovariantClass.elim a bc.le).lt_of_ne (bc.ne ∘ ContravariantClass.elim _)

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