ext — Mathlib

English

Two morphisms α, β: F ⟶ G in Cat are equal if their components are equal at every object.

Русский

Две морфизмы α, β: F ⟶ G в Cat равны, если их компоненты равны для каждого объекта.

LaTeX

$$$$\\forall {C,D}, \\forall α,β:\\, C\\to D, \\; α.app = β.app \\Rightarrow α=β.$$$$

Lean4

@[ext]
theorem ext {C D : Cat} {F G : C ⟶ D} {α β : F ⟶ G} (w : α.app = β.app) : α = β :=
  NatTrans.ext w

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