ne_snd

Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

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

English

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

Русский

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

LaTeX

$$h2.ne_snd$$

Lean4

@[grind]
theorem ne_snd (h2 : G.IsPathGraph3Compl v w₁ w₂) : v ≠ w₂ := fun h ↦ h2.not_adj_fst (h ▸ h2.adj.symm)

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

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

Разделы

Аффилиация

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