Theorems · Theorem · combinatorics

SimpleGraph.induceHom_comp

∀ {V : Type u_1} {W : Type u_2} {X : Type u_3} {G : SimpleGraph V} {G' : SimpleGraph W} {G'' : SimpleGraph X}
  {s : Set V} {t : Set W} {r : Set X} (φ : G →g G') (φst : Set.MapsTo (⇑φ) s t) (ψ : G' →g G'')
  (ψtr : Set.MapsTo (⇑ψ) t r),
  (SimpleGraph.induceHom ψ ψtr).comp (SimpleGraph.induceHom φ φst) = SimpleGraph.induceHom (ψ.comp φ) ⋯

Defined in

Mathlib.Combinatorics.SimpleGraph.Maps

Cited by

1 results in Mathlib

Foundations

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