symm

Mathlib.CategoryTheory.IsConnected

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Zag.symm

English

If there is a Zag from j1 to j2, there is a Zag from j2 to j1.

Русский

Если существует Zag от j1 к j2, тогда существует Zag от j2 к j1.

LaTeX

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

Lean4

@[symm]
theorem symm {j₁ j₂ : J} (h : Zag j₁ j₂) : Zag j₂ j₁ :=
  zag_symmetric h

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

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

Разделы

Аффилиация

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