Cut conditions under graph isomorphism

The no-bridge cut condition is a property of the underlying multigraph, so it must be transported across the graph isomorphisms supplied by structural normal forms. Keeping this at the graph-isomorphism layer avoids rebuilding the same finite-cut argument for every presentation theorem.

theorem Utilities.CFGraphIso.cutMultiplicity_image {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) (S : Finset G.V) : cutMultiplicity H (Finset.image (⇑φ.vertexEquiv) S) = cutMultiplicity G S

Cut multiplicity is preserved when a vertex set is carried across a graph isomorphism.

theorem Utilities.CFGraphIso.twoEdgeCutCondition_map_iff {G : CFGraph} {H : CFGraph} (φ : CFGraphIso G H) : TwoEdgeCutCondition H ↔ TwoEdgeCutCondition G

The absence-of-bridges cut condition is invariant under graph isomorphism.