adj_inj

Mathlib.Combinatorics.SimpleGraph.Basic

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

English

Adj is injective, equivalently Adj G = Adj H if and only if G = H.

Русский

Adj инъективно, то есть Adj G = Adj H тогда и только тогда G = H.

LaTeX

$$$ Adj(G) = Adj(H) \iff G = H $$$

Lean4

@[simp]
theorem adj_inj {G H : SimpleGraph V} : G.Adj = H.Adj ↔ G = H :=
  adj_injective.eq_iff

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

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

Разделы

Аффилиация

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