covariant_flip_iff — Mathlib

English

If μ is commutative, Covariant for μ is equivalent to Covariant for flip μ.

Русский

Если μ коммутирует, ковариантность по μ эквивалентна ковариантности по flip μ.

LaTeX

$$$[Std.Commutative(μ)] \Rightarrow (Covariant(N,N,flip μ,r) \iff Covariant(N,N,μ,r))$$$

Lean4

theorem covariant_flip_iff [h : Std.Commutative mu] : Covariant N N (flip mu) r ↔ Covariant N N mu r := by unfold flip;
  simp_rw [h.comm]

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