of_zag

Mathlib.CategoryTheory.IsConnected

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

English

A Zag between j1 and j2 yields a Zigzag between them.

Русский

Заг между j1 и j2 образует Zigzag между ними.

LaTeX

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

Lean4

theorem of_zag {j₁ j₂ : J} (h : Zag j₁ j₂) : Zigzag j₁ j₂ :=
  Relation.ReflTransGen.single h

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

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

Разделы

Аффилиация

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