hom_inv_id_app_apply — Mathlib

English

Two sections x,y of F are equal if and only if their components agree at every object j: x = y iff ∀ j, x.val j = y.val j.

Русский

Две секции x,y функторa F равны тогда и только тогда, когда их компоненты совпадают для каждого объекта j: x = y ⇔ ∀ j, x.val j = y.val j.

LaTeX

$$$$ x = y \iff \forall j, x.\text{val}(j) = y.\text{val}(j). $$$$

Lean4

@[simp]
theorem hom_inv_id_app_apply (α : F ≅ G) (X) (x) : α.inv.app X (α.hom.app X x) = x :=
  congr_fun (α.hom_inv_id_app X) x

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