symm

Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

URI: https://scilib.ai/kg/mathlib#SimpleGraph.IsPathGraph3Compl.symm

English

If h is IsPathGraph3Compl v w1 w2, then G.IsPathGraph3Compl v w2 w1.

Русский

Если h: G.IsPathGraph3Compl v w1 w2, то G.IsPathGraph3Compl v w2 w1.

LaTeX

$$h.symm$$

Lean4

@[symm]
theorem symm (h : G.IsPathGraph3Compl v w₁ w₂) : G.IsPathGraph3Compl v w₂ w₁ :=
  by
  obtain ⟨h1, h2, h3⟩ := h
  exact ⟨h1.symm, h3, h2⟩

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

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

Разделы

Аффилиация

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