yonedaCollectionPresheafToA_val_fst

English

The fst component of p.val matches s when p comes from YonedaCollection presheaf to A.

Русский

Первая компонента p.val совпадает с s, когда p исходит из отображения YonedaCollection presheaf to A.

LaTeX

$$$$ p.\text{val}.\text{fst} = s $$$$

Lean4

@[simp]
theorem yonedaCollectionPresheafToA_val_fst (s : yoneda.obj X ⟶ A) (p : OverArrows (yonedaCollectionPresheafToA F) s) :
    p.val.fst = s := by simpa [YonedaCollection.yonedaEquivFst_eq] using p.app_val

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