ne_fst

Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

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

English

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

Русский

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

LaTeX

$$h2.ne_fst$$

Lean4

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

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

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

Разделы

Аффилиация

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