ne

Mathlib.Combinatorics.SimpleGraph.Basic

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Adj.ne

English

If a is adjacent to b, then a and b are distinct.

Русский

Если a смежен с b, то a ≠ b.

LaTeX

$$$ G.Adj a b \rightarrow a \neq b $$$

Lean4

protected theorem ne {G : SimpleGraph V} {a b : V} (h : G.Adj a b) : a ≠ b :=
  G.ne_of_adj h

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

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

Разделы

Аффилиация

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