mk — Mathlib · SciLib

English

Given a pair s and x, construct an element of YonedaCollection F X by pairing yonedaEquiv s with the transformed x.

Русский

Для пары s и x построить элемент YonedaCollection F X, сопоставив yonedaEquiv s с преобразованным x.

LaTeX

$$$\\forall s:\\ yoneda.obj X \\to A \\; \\forall x:\\ F.obj (op (CostructuredArrow.mk s)),\\; YonedaCollection.mk s x$$

Lean4

/-- Given a costructured arrow `s : yoneda.obj X ⟶ A` and an element `x : F.obj s`, construct
an element of `YonedaCollection F X`. -/
def mk (s : yoneda.obj X ⟶ A) (x : F.obj (op (CostructuredArrow.mk s))) : YonedaCollection F X :=
  ⟨yonedaEquiv s, F.map (eqToHom <| by rw [Equiv.symm_apply_apply]) x⟩

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