ofEq_symm — Mathlib

English

The inverse of the equality-based isometry between p and q is the equality-based isometry from q to p with the symmetric equality hpq.symm.

Русский

Обратная изометрия между p и q, заданная равенством, равна изометрии от q к p, задаваемой симметричным равенством.

LaTeX

$$$ofEq(p,q,h).symm = ofEq(q,p,h.symm)$$$

Lean4

@[simp]
theorem ofEq_symm (h : p = q) : (ofEq p q h).symm = ofEq q p h.symm :=
  rfl

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