dartOfNeighborSet_injective

Mathlib.Combinatorics.SimpleGraph.Dart

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

← MathLib Explorer

English

For each vertex v, the map G.dartOfNeighborSet v is injective.

Русский

Для каждой вершины v отображение G.dartOfNeighborSet v инъективно.

LaTeX

$$$ \forall v, \mathrm{Injective}(G.dartOfNeighborSet v) $$$

Lean4

theorem dartOfNeighborSet_injective (v : V) : Function.Injective (G.dartOfNeighborSet v) := fun e₁ e₂ h =>
  Subtype.ext <| by
    injection h with h'
    convert congr_arg Prod.snd h'

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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