induce — Mathlib

English

If G is acyclic, then the induced subgraph on any subset is acyclic.

Русский

Если граф G ацикличен, то индуцированный подграф на любую подмножество вершин также ацикличен.

LaTeX

$$$G.IsAcyclic \Rightarrow \forall s: Set V, (G.induce s).IsAcyclic$$$

Lean4

/-- A graph induced from an acyclic graph is acyclic. -/
theorem induce (h : G.IsAcyclic) (s : Set V) : G.induce s |>.IsAcyclic :=
  h.of_comap _

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