hom_ext — Mathlib

English

Morphisms in Dial are determined by their components: equality of the first component and the second component implies equality of whole morphisms.

Русский

Морфизмы в Dial определяются компонентами: равенство первых и вторых компонентов означает равенство самих морфизмов.

LaTeX

$$∀ {x y : X ⟶ Y}, x.f = y.f ∧ x.F = y.F ⇒ x = y$$

Lean4

@[ext]
theorem hom_ext {X Y : Dial C} {x y : X ⟶ Y} (hf : x.f = y.f) (hF : x.F = y.F) : x = y :=
  Hom.ext hf hF

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