hom_inv_id_app_app_app — Mathlib

English

For every j in J, h.incl.app j is an isomorphism.

Русский

Для каждого j ∈ J отображение h.incl.app j является изоморфизмом.

LaTeX

$$$ \forall j:\, J,\ IsIso\big( h.incl.app j \big)$$$

Lean4

@[reassoc (attr := simp)]
theorem hom_inv_id_app_app_app {F G : C ⥤ D ⥤ E ⥤ E'} (e : F ≅ G) (X₁ : C) (X₂ : D) (X₃ : E) :
    ((e.hom.app X₁).app X₂).app X₃ ≫ ((e.inv.app X₁).app X₂).app X₃ = 𝟙 _ := by cat_disch

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