hom_ext — Mathlib

English

A standard extensionality principle for morphisms in an equivalence: equality of the underlying natural transformations forces equality of the morphisms.

Русский

Стандартное свойство экстенсивности для морфизмов между эквивалентностями: равенство базовых натурализующих преобразований влечет равенство самих морфизмов.

LaTeX

$$$\\text{asNatTrans}(\\alpha) = \\text{asNatTrans}(\\beta) \\Rightarrow \\alpha = \\beta$$$

Lean4

@[ext]
theorem hom_ext {e f : C ≌ D} {α β : e ⟶ f} (h : asNatTrans α = asNatTrans β) : α = β :=
  h

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