embedding — Mathlib

English

If there is an injective graph homomorphism (embedding) from G to G' and G' is acyclic, then G is acyclic.

Русский

Если существует внедрение (инъективный гомоморфизм) от G к G' и G' ацикличесен, то G также ацикличесен.

LaTeX

$$$f : G \\hookrightarrow G' \\;\\text{embedding} \\; \\text{and } G'.IsAcyclic \\Rightarrow G.IsAcyclic$$$

Lean4

theorem embedding (f : G ↪g G') (h : G'.IsAcyclic) : G.IsAcyclic :=
  h.comap f f.injective

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