covconv — Mathlib

English

In a group setting, from Covariant to a relation, there exists a canonical Contravariant instance for the swapped relation.

Русский

В группе существует каноническая инстанция контравариантности для переставленного отношения, базирующаяся на ковариантности.

LaTeX

$$Covariant M N μ r → Contravariant N N (swap (· * ·)) r$$

Lean4

@[to_additive]
instance (priority := 100) covconv [Group N] [CovariantClass N N (· * ·) r] : ContravariantClass N N (· * ·) r :=
  ⟨Group.covariant_iff_contravariant.mp CovariantClass.elim⟩

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