zag_symmetric

Mathlib.CategoryTheory.IsConnected

URI: https://scilib.ai/kg/mathlib#CategoryTheory.zag_symmetric

English

Let J be a category and Zag a relation on its objects. Then Zag is symmetric: if Zag(j1, j2) holds, then Zag(j2, j1) also holds.

Русский

Пусть J — категория и Zag — отношения между её объектами. Тогда Zag симметрично: если Zag(j1, j2), то Zag(j2, j1).

LaTeX

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

Lean4

theorem zag_symmetric : Symmetric (@Zag J _) := fun _ _ h => h.symm

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

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

Разделы

Аффилиация

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