hom_ext — Mathlib

English

Two morphisms between FunctorsInverting objects are equal if their components agree on each object,” a standard extensionality lemma.

Русский

Два морфизма между объектами FunctorsInverting равны, если их компоненты согласованы по каждому объекту.

LaTeX

$$$ \forall {\alpha, \beta : F \to G}, \alpha.app = \beta.app \Rightarrow \alpha = \beta $$$

Lean4

@[ext]
theorem hom_ext {W : MorphismProperty C} {F₁ F₂ : FunctorsInverting W D} {α β : F₁ ⟶ F₂} (h : α.app = β.app) : α = β :=
  NatTrans.ext h

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