adj_inj

Mathlib.Combinatorics.Digraph.Basic

URI: https://scilib.ai/kg/mathlib#Digraph.adj_inj

English

Two digraphs have the same adjacency relation if and only if they are equal.

Русский

Два ориентированых графа имеют тождество отношения смежности тогда и только тогда, когда графы совпадают.

LaTeX

$$$G.Adj = H.Adj \\iff G = H$$$

Lean4

@[simp]
theorem adj_inj {G H : Digraph V} : G.Adj = H.Adj ↔ G = H :=
  Digraph.ext_iff.symm

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

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

Разделы

Аффилиация

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