coyonedaPairingExt — Mathlib

English

Two elements x,y of (coyonedaPairing C).obj X are equal if they agree componentwise on every target Y, i.e., x.app Y = y.app Y for all Y ∈ C.

Русский

Два элемента x,y из (coyonedaPairing C).obj X равны, если они совпадают на каждом компоненте; то есть x.app Y = y.app Y для всех Y ∈ C.

LaTeX

$$$$ \forall Y, \; x.app Y = y.app Y \; \Rightarrow \; x = y $$$$

Lean4

@[ext]
theorem coyonedaPairingExt {X : C × (C ⥤ Type v₁)} {x y : (coyonedaPairing C).obj X} (w : ∀ Y, x.app Y = y.app Y) :
    x = y :=
  NatTrans.ext (funext w)

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