self_invAct_eq_iff_eq — Mathlib

English

Similarly, the map x ↦ x ◃⁻¹ x is injective: x ◃⁻¹ x = y ◃⁻¹ y implies x = y.

Русский

Аналогично, отображение x ↦ x ◃⁻¹ x инъективно: x ◃⁻¹ x = y ◃⁻¹ y ⇒ x = y.

LaTeX

$$$x \triangleleft^{-1} x = y \triangleleft^{-1} y \Longrightarrow x = y$$$

Lean4

theorem self_invAct_eq_iff_eq {x y : R} : x ◃⁻¹ x = y ◃⁻¹ y ↔ x = y :=
  by
  have h := @self_act_eq_iff_eq _ _ (op x) (op y)
  simpa using h

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