of_arrow — Mathlib

English

Given a morphism h: f ⟶ g in Arrow C, there is an induced commutative square with arrows f.hom, h.left, h.right, g.hom.

Русский

Для морфизма h: f ⟶ g в Arrow C существует индуцированный коммутативный квадрат со стрелками f.hom, h.left, h.right, g.hom.

LaTeX

$$theorem of_arrow {f g : Arrow C} (h : f ⟶ g) : CommSq f.hom h.left h.right g.hom$$

Lean4

theorem of_arrow {f g : Arrow C} (h : f ⟶ g) : CommSq f.hom h.left h.right g.hom :=
  ⟨h.w.symm⟩

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