covariant_swap_iff_contravariant_swap

English

In a group with LT and MulLeftStrictMono, MulLeftReflectLT N holds; left translation reflects strict order.

Русский

В группе с LT и строгой левой монотонностью выполняется MulLeftReflectLT.

LaTeX

$$Group N ⟹ MulLeftReflectLT N$$

Lean4

@[to_additive]
theorem covariant_swap_iff_contravariant_swap [Group N] :
    Covariant N N (swap (· * ·)) r ↔ Contravariant N N (swap (· * ·)) r :=
  by
  refine ⟨fun h a b c bc ↦ ?_, fun h a b c bc ↦ ?_⟩
  · rw [← mul_inv_cancel_right b a, ← mul_inv_cancel_right c a]
    exact h a⁻¹ bc
  · rw [← mul_inv_cancel_right b a, ← mul_inv_cancel_right c a] at bc
    exact h a⁻¹ bc

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