yonedaEvaluation_map_down — Mathlib

English

For product-like objects P,Q and morphism α: P ⟶ Q, and x in (yonedaEvaluation C).obj P, the down-component of the mapped element is ((yonedaEvaluation C).map α x).down = α.2.app Q.1 (P.2.map α.1 x.down).

Русский

Для произведений P,Q и отображения α: P ⟶ Q, и элемента x ∈ (yonedaEvaluation C).obj P, нижняя компонента отображённого элемента равна ((yonedaEvaluation C).map α x).down = α.2.app Q.1 (P.2.map α.1 x.down).

LaTeX

$$$((\mathrm{yonedaEvaluation}\; C).map \alpha\, x).down = \alpha.2.app Q.1 (P.2.map \alpha.1\, x.down)$$$

Lean4

@[simp]
theorem yonedaEvaluation_map_down (P Q : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)) (α : P ⟶ Q) (x : (yonedaEvaluation C).obj P) :
    ((yonedaEvaluation C).map α x).down = α.2.app Q.1 (P.2.map α.1 x.down) :=
  rfl

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