Theorems · Theorem · combinatorics

SimpleGraph.Iso.connectedComponentEquiv_trans

∀ {V : Type u} {V' : Type v} {V'' : Type w} {G : SimpleGraph V} {G' : SimpleGraph V'} {G'' : SimpleGraph V''}
  (φ : G ≃g G') (φ' : G' ≃g G''),
  SimpleGraph.Iso.connectedComponentEquiv (RelIso.trans φ φ') =
    φ.connectedComponentEquiv.trans φ'.connectedComponentEquiv

Defined in

Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Cited by

0 results in Mathlib

Foundations

Depth 35 from the axioms · uses propext, Classical.choice, Quot.sound