ne'

Mathlib.Combinatorics.SimpleGraph.Basic

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

English

If a is adjacent to b, then b ≠ a.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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