restrict_adj — Mathlib

English

For G,G'': G.Subgraph restricted to G''.verts has adjacency that is the conjunction of adjacencies from G' and G'' on common vertices.

Русский

Для подграфа, ограниченного G'' на вершинном множестве, смежность равна конъюнкции смежностей из G' и G'' на общих вершинах.

LaTeX

$$$\\forall (v,w) : G'.\\mathrm{verts}, (G'.\\mathrm{restrict} G'').\\mathrm{Adj} v w \\iff G'.\\mathrm{Adj} v w \\land G''.\\mathrm{Adj} v w$$$

Lean4

theorem restrict_adj {G' G'' : G.Subgraph} (v w : G'.verts) : (G'.restrict G'').Adj v w ↔ G'.Adj v w ∧ G''.Adj v w :=
  Iff.rfl

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