induce — Mathlib

English

The copy from an induced subgraph to the original graph is given by the induced-subgraph copy construction: induce(G, s) is a Copy (G.induce s) G, i.e. an embedding from the induced subgraph back into G.

Русский

Копия от индуцированного подграфа к исходному графу задаётся конструкцией копирования индуцированного подграфа: induce(G, s) — это Copy (G.induce s) G, то есть вложение из индуцированного подграфа обратно в G.

LaTeX

$$$\text{induce}(G,s) : \text{Copy}(G\induce s, G)$$$

Lean4

/-- The copy from an induced subgraph to the initial simple graph. -/
def induce (G : SimpleGraph V) (s : Set V) : Copy (G.induce s) G :=
  (Embedding.induce s).toCopy

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