contravariant_flip_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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