zigzag_obj_of_zigzag — Mathlib

English

If there is a Zigzag between j1 and j2, then applying a functor F yields a Zigzag between F(j1) and F(j2).

Русский

Если существует Zigzag между j1 и j2, применение к ним функторa F сохраняет Zigzag между F(j1) и F(j2).

LaTeX

$$$\forall F : J \to K,\forall j_1 j_2:\ J,\ Zigzag\ j_1 j_2 \Rightarrow Zigzag\ (F(j_1))\ (F(j_2))$$$

Lean4

/-- If there is a zigzag from `j₁` to `j₂`, then there is a zigzag from `F j₁` to
`F j₂` as long as `F` is a functor.
-/
theorem zigzag_obj_of_zigzag (F : J ⥤ K) {j₁ j₂ : J} (h : Zigzag j₁ j₂) : Zigzag (F.obj j₁) (F.obj j₂) :=
  zigzag_prefunctor_obj_of_zigzag F.toPrefunctor h

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