fst_ne_snd

Mathlib.Combinatorics.SimpleGraph.Dart

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Dart.fst_ne_snd

English

For every dart, the first endpoint is different from the second.

Русский

У каждой стрелы первый и второй концы различны.

LaTeX

$$$ d.fst \neq d.snd $$$

Lean4

@[simp]
theorem fst_ne_snd (d : G.Dart) : d.fst ≠ d.snd := fun h ↦ G.irrefl (h ▸ d.adj)

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

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

Разделы

Аффилиация

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