map₁_fst — Mathlib

English

Applying map₁ to a morphism η preserves the yonedaEquivFst component.

Русский

Применение map₁ к гомоморфизму η сохраняет компонент yonedaEquivFst.

LaTeX

$$$\\forall {G} (\\eta : F ⟶ G) (p : YonedaCollection F X), (YonedaCollection.map₁ η p).yonedaEquivFst = p.yonedaEquivFst$$$

Lean4

@[simp]
theorem map₁_fst {G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v} (η : F ⟶ G) (p : YonedaCollection F X) :
    (YonedaCollection.map₁ η p).fst = p.fst := by simp [map₁]

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