Theorems · Theorem · combinatorics

SimpleGraph.Embedding.sum_comp_sumComm

∀ {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'),
  (g.sum f).comp SimpleGraph.Iso.sumComm.toEmbedding = SimpleGraph.Iso.sumComm.toEmbedding.comp (f.sum g)

Defined in

Mathlib.Combinatorics.SimpleGraph.Sum

Cited by

0 results in Mathlib

Foundations

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