ext — Mathlib

English

CatCenter objects are determined componentwise: two CatCenter C-objects are equal if their components agree on every object X in C.

Русский

Объекты CatCenter определяются по компонентам: два объекта равны, если их компоненты совпадают для каждого X в C.

LaTeX

$$$\text{ext} (x \ n y) (h) : x.app X = y.app X \text{ for all } X \Rightarrow x = y$$$

Lean4

@[ext]
theorem ext (x y : CatCenter C) (h : ∀ (X : C), x.app X = y.app X) : x = y :=
  NatTrans.ext (funext h)

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