yonedaEquivFst — Mathlib

English

YonedaCollection elements are determined by their first component and a compatible second component up to equality.

Русский

Элементы YonedaCollection определяются по первому компоненту и совместимому второму компоненту до равенства.

LaTeX

$$$\\forall p\\ q : YonedaCollection F X, \\; (p.fst = q.fst) \\Rightarrow p = q$$$

Lean4

/-- This is a definition because it will be helpful to be able to control precisely when this
definition is unfolded. -/
def yonedaEquivFst (p : YonedaCollection F X) : A.obj (op X) :=
  yonedaEquiv p.fst

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