coe_inv_coe' — Mathlib

English

Let p be a morphism in the subgroupoid S; the inverse in S has the same underlying arrow as the inverse in the ambient groupoid C. In symbols, inv_S p = inv_C (val p).

Русский

Пусть p — морфизм в подгруппоида S; обратная к p внутри S имеет ту же базовую стрелку, что и обратная в окружающем группой C: inv_S(p) = inv_C(p).

LaTeX

$$$(\mathrm{inv}_S p).\mathrm{val} = \mathrm{inv}_C(p.\mathrm{val}).$$$

Lean4

@[simp]
theorem coe_inv_coe' {c d : S.objs} (p : c ⟶ d) : (CategoryTheory.inv p).val = CategoryTheory.inv p.val := by
  simp only [← inv_eq_inv, coe_inv_coe]

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