ne_of_adj_of_not_adj

Mathlib.Combinatorics.SimpleGraph.Basic

URI: https://scilib.ai/kg/mathlib#SimpleGraph.ne_of_adj_of_not_adj

English

If v is adjacent to x and hn states that w is not adjacent to x, then v ≠ w.

Русский

Если v смежен с x, и h не смежен с x для w, то v ≠ w.

LaTeX

$$$ G.Adj v x \land \neg G.Adj w x \rightarrow v \neq w $$$

Lean4

theorem ne_of_adj_of_not_adj {v w x : V} (h : G.Adj v x) (hn : ¬G.Adj w x) : v ≠ w := fun h' => hn (h' ▸ h)

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

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

Разделы

Аффилиация

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