hom_ext — Mathlib

English

Two morphisms of presheaves are equal if they agree on every object X: f.app X = g.app X for all X implies f = g.

Русский

Два морфизма прешефов равны тогда и только тогда, когда они совпадают на каждом объекте: f.app X = g.app X для всех X тогда и только тогда, что f = g.

LaTeX

$$$\forall X,\ f.app X = g.app X \Rightarrow f = g.$$$

Lean4

@[ext]
theorem hom_ext {f g : M₁ ⟶ M₂} (h : ∀ (X : Cᵒᵖ), f.app X = g.app X) : f = g :=
  Hom.ext (by ext1; apply h)

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