of_zag_trans

Mathlib.CategoryTheory.IsConnected

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Zigzag.of_zag_trans

English

If Zag j1 j2 holds, then Zigzag j1 j2 holds.

Русский

Если Zag j1 j2 верно, то Zigzag j1 j2 верно.

LaTeX

$$$\forall j_1 j_2,\ Zag(j_1,j_2) \Rightarrow Zigzag\ j_1 j_2$$$

Lean4

theorem of_zag_trans {j₁ j₂ j₃ : J} (h₁ : Zag j₁ j₂) (h₂ : Zag j₂ j₃) : Zigzag j₁ j₃ :=
  trans (of_zag h₁) (of_zag h₂)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru