self_act_eq_iff_eq — Mathlib

English

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 x = y \triangleleft y \Longrightarrow x = y$ and converse$$

Lean4

theorem self_act_eq_iff_eq {x y : R} : x ◃ x = y ◃ y ↔ x = y :=
  by
  constructor; swap
  · rintro rfl; rfl
  intro h
  trans (x ◃ x) ◃⁻¹ x ◃ x
  · rw [← left_cancel (x ◃ x), right_inv, self_act_act_eq]
  · rw [h, ← left_cancel (y ◃ y), right_inv, self_act_act_eq]

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