Theorems · Theorem · combinatorics

SimpleGraph.Embedding.sum_sum_comp_sumAssoc

∀ {U : Type u_1} {U' : Type u_2} {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} {G : SimpleGraph V}
  {H : SimpleGraph W} {I : SimpleGraph U} {G' : SimpleGraph V'} {H' : SimpleGraph W'} {I' : SimpleGraph U'}
  (f : G ↪g G') (g : H ↪g H') (h : I ↪g I'),
  (f.sum (g.sum h)).comp SimpleGraph.Iso.sumAssoc.toEmbedding =
    SimpleGraph.Iso.sumAssoc.toEmbedding.comp ((f.sum g).sum h)

Defined in

Mathlib.Combinatorics.SimpleGraph.Sum

Cited by

0 results in Mathlib

Foundations

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