spanningCoe — Mathlib

English

SpanningCoe extends a graph on a subset to a graph on the full vertex set by including the remaining vertices with no new edges.

Русский

SpanningCoe добавляет граф на оставшиеся вершины, не добавляя новых ребер, получая граф на всем множества вершин.

LaTeX

$$$ \\mathrm{spanningCoe}_{s}(G) = G.\\mathrm{map}(\\mathrm{Embedding.subtype}) $$$

Lean4

/-- Given a graph on a set of vertices, we can make it be a `SimpleGraph V` by
adding in the remaining vertices without adding in any additional edges.
This is a wrapper around `SimpleGraph.map`. -/
abbrev spanningCoe {s : Set V} (G : SimpleGraph s) : SimpleGraph V :=
  G.map (Function.Embedding.subtype _)

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