Theorems · Theorem · combinatorics

SimpleGraph.IsAcyclic.comap

∀ {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G'),
  Function.Injective ⇑f → G'.IsAcyclic → G.IsAcyclic

A graph that has an injective homomorphism to an acyclic graph is acyclic.

Defined in

Mathlib.Combinatorics.SimpleGraph.Acyclic

Cited by

4 results in Mathlib

Foundations

Depth 26 from the axioms · uses propext, Quot.sound