rel_symm

Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

URI: https://scilib.ai/kg/mathlib#SimpleGraph.TripartiteFromTriangles.rel_symm

English

The relation Rel t is symmetric: if x is related to y then y is related to x.

Русский

Отношение Rel t симметрично: если x связано с y, то y связано с x.

LaTeX

$$$\\forall x,y,\\; \\mathrm{Rel}(t)(x,y) \\Rightarrow \\mathrm{Rel}(t)(y,x).$$$

Lean4

theorem rel_symm : Symmetric (Rel t) := fun x y h ↦ by cases h <;> constructor <;> assumption

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

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

Разделы

Аффилиация

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