symm_apply_apply — Mathlib

English

The map toEquiv : r ≃r s → α ≃ β is injective: two RelIso’s with the same underlying Equiv are equal.

Русский

Отображение toEquiv : r ≃r s → α ≃ β инъективно: если два RelIso имеют одинаковый базовый эквиваленс, то они равны.

LaTeX

$$$$ \\text{toEquiv} : (r \\simeq_r s) \\to (\\alpha \\simeq \\beta) \\quad \\text{injective}. $$$$

Lean4

@[simp]
theorem symm_apply_apply (e : r ≃r s) (x : α) : e.symm (e x) = x :=
  e.left_inv x

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