adj_injective

Mathlib.Combinatorics.SimpleGraph.Basic

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

English

The map Adj from SimpleGraph V to V → V → Prop is injective: if Adj G = Adj H then G = H.

Русский

Отображение Adj: SimpleGraph V → V → V → Prop инъективно: если Adj(G) = Adj(H), то G = H.

LaTeX

$$$ \forall G,H : SimpleGraph V, Adj(G) = Adj(H) \Rightarrow G = H $$$

Lean4

theorem adj_injective : Injective (Adj : SimpleGraph V → V → V → Prop) := fun _ _ => SimpleGraph.ext

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

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

Разделы

Аффилиация

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