English
For G' : G.Subgraph, G'' : G'.coe.Subgraph, and v,w ∈ V, (G'.coeSubgraph G'').Adj v w is equivalent to the existence of vertex witnesses in G'.verts with G'' adjacency between their lifted points.
Русский
Для G' : G.Subgraph, G'' : G'.coe.Subgraph, и вершин v,w ∈ V, (G'.coeSubgraph G'').Adj v w эквивалентно существованию доказательств принадлежности вершин в G'.verts с смежностью между их подънятыми точками в G''.Adj.
LaTeX
$$$\\forall G' : G.Subgraph, \\forall G'' : G'.\\mathrm{coe.Subgraph}, \\forall v,w,\\ (G'.\\mathrm{coeSubgraph} G'').\\mathrm{Adj} \\, v \\, w \\iff \\exists hv\\exists hw\\, G''.\\mathrm{Adj}\\langle v, hv\\rangle \\langle w, hw\\rangle$$$
Lean4
/-- Given a subgraph of `G`, restrict it to being a subgraph of another subgraph `G'` by
taking the portion of `G` that intersects `G'`. -/
protected abbrev restrict {G' : G.Subgraph} : G.Subgraph → G'.coe.Subgraph :=
Subgraph.comap G'.hom
