fst_ne_snd

Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

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

English

If h2 is IsPathGraph3Compl v w1 w2, then w1 ≠ w2.

Русский

Если h2: G.IsPathGraph3Compl v w1 w2, то w1 не равно w2.

LaTeX

$$h2.fst_ne_snd$$

Lean4

@[grind]
theorem fst_ne_snd (h2 : G.IsPathGraph3Compl v w₁ w₂) : w₁ ≠ w₂ :=
  h2.adj.ne

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

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

Разделы

Аффилиация

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