adj_injective — Mathlib

English

The operation Adj, which maps a directed graph to its adjacency predicate, is injective: two digraphs are equal if they have the same adjacency relation.

Русский

Операция Adj, отображающая граф на его отношение смежности, инъективна: два графа совпадают тогда и только тогда, когда совпадают их отношения смежности.

LaTeX

$$$\\text{G.Adj} = \\text{H.Adj} \\Rightarrow G = H$ for all digraphs G,H on the same vertex set.$$

Lean4

theorem adj_injective : Injective (Adj : Digraph V → V → V → Prop) := fun _ _ ↦ Digraph.ext

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