copy_eq

Mathlib.Combinatorics.SimpleGraph.Subgraph

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Subgraph.copy_eq

← MathLib Explorer

English

Two copies of a subgraph are equal when their vertex sets and adjacencies match.

Русский

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

LaTeX

$$G'.copy(V'',hV,adj',hadj) = G'$$

Lean4

theorem copy_eq (G' : Subgraph G) (V'' : Set V) (hV : V'' = G'.verts) (adj' : V → V → Prop) (hadj : adj' = G'.Adj) :
    G'.copy V'' hV adj' hadj = G' :=
  Subgraph.ext hV hadj

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

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

Разделы

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

Аффилиация

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