deleteVerts — Mathlib

English

DeleteVerts G' s is defined as the induced subgraph on the vertex set of G' with the vertices s removed; equivalently, G'.deleteVerts s = G'.induce (G'.verts \ s).

Русский

DeleteVerts G' s определяется как индуцированный подграф на вершинах G' после удаления вершин из s; то есть G'.deleteVerts s = G'.induce (G'.verts \ s).

LaTeX

$$$ (G'.deleteVerts s) = G'.induce (G'.verts \ s) $$$

Lean4

/-- Given a subgraph and a set of vertices, delete all the vertices from the subgraph,
if present. Any edges incident to the deleted vertices are deleted as well. -/
abbrev deleteVerts (G' : G.Subgraph) (s : Set V) : G.Subgraph :=
  G'.induce (G'.verts \ s)

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