Theorems · Theorem · combinatorics

SimpleGraph.Iso.sumComm_comp_sumCongr

∀ {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} {G : SimpleGraph V} {H : SimpleGraph W}
  {G' : SimpleGraph V'} {H' : SimpleGraph W'} (f : G ≃g G') (g : H ≃g H'),
  SimpleGraph.Iso.sumComm.comp (f.sumCongr g) = (g.sumCongr f).comp SimpleGraph.Iso.sumComm

Defined in

Mathlib.Combinatorics.SimpleGraph.Sum

Cited by

0 results in Mathlib

Foundations

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