toProd_injective

Mathlib.Combinatorics.SimpleGraph.Dart

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

English

The map sending a dart to its endpoints (toProd) is injective.

Русский

Отображение стрелы в её концы (toProd) инъективно.

LaTeX

$$$ \forall d_1,d_2,\ d_1.toProd = d_2.toProd \Rightarrow d_1 = d_2 $$$

Lean4

theorem toProd_injective : Function.Injective (Dart.toProd : G.Dart → V × V) :=
  Dart.ext

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

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

Разделы

Аффилиация

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