inv_right — Mathlib

English

For an isomorphism e in the comma category, the right component of its inverse equals the inverse of the right component: (inv e).right = inv(e.right).

Русский

Для изоморфизма e в комма‑категории правая компонента обращения равна обратной правой компоненте: (inv e).right = inv(e.right).

LaTeX

$$$ (inv\ e).right = inv(e.right). $$$

Lean4

@[simp]
theorem inv_right [IsIso e] : (inv e).right = inv e.right :=
  by
  apply IsIso.eq_inv_of_hom_inv_id
  rw [← Comma.comp_right, IsIso.hom_inv_id, id_right]

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