flip — Mathlib

English

If h is Covariant, then the relation with swapped arguments (flip r) is also Covariant with the same action μ.

Русский

Если выполняется ковариантность относительно r, то ковариантность сохраняется и для relation, у которой аргументы поменяны местами (flip r).

LaTeX

$$Covariant M N μ r → Covariant M N μ (flip r)$$

Lean4

theorem flip (h : Covariant M N μ r) : Covariant M N μ (flip r) := fun a _ _ ↦ h a

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