induce — Mathlib

English

For any subset s of V, the induced subgraph G.induce s embeds into G; the embedding is given by the natural inclusion.

Русский

Для любого подмножества s вершин V индуцированный подграф G.induce s встраивается в G; вложение задаётся естественным включением.

LaTeX

$$$ G\!\mathrm{induce}(s) \hookrightarrow G $$$

Lean4

/-- Induced graphs embed in the original graph.

Note that if `G.induce s = ⊤` (i.e., if `s` is a clique) then this gives the embedding of a
complete graph. -/
protected abbrev induce (s : Set V) : G.induce s ↪g G :=
  SimpleGraph.Embedding.comap (Function.Embedding.subtype _) G

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