English
The induced subgraph of a subgraph G' on a set s is the subgraph with vertex set s and edges inherited from G' restricted to s.
Русский
ИНДуцируемый подграф подграфа G' на множестве s имеет вершины s и ребра, которых достаточно в G' на s.
LaTeX
$$$ \\operatorname{induce}(G', s) = G'\\_\\!\\!{\\text{on}}\\, s \\;\\text{ with }\\; \\operatorname{verts}=s,\\; \\operatorname{Adj}(u,v)=u\\in s\\land v\\in s\\land G'.\\Adj(u,v). $$$
Lean4
/-- The induced subgraph of a subgraph. The expectation is that `s ⊆ G'.verts` for the usual
notion of an induced subgraph, but, in general, `s` is taken to be the new vertex set and edges
are induced from the subgraph `G'`. -/
@[simps]
def induce (G' : G.Subgraph) (s : Set V) : G.Subgraph
where
verts := s
Adj u v := u ∈ s ∧ v ∈ s ∧ G'.Adj u v
adj_sub h := G'.adj_sub h.2.2
edge_vert h := h.1
symm _ _ h := ⟨h.2.1, h.1, G'.symm h.2.2⟩
