Transport of pointed genus-one rigidity

The rigid pointed-cycle predicate is invariant under graph isomorphism. This small transport lemma is useful when nested induced-subgraph cuts introduce extra subtype layers around an already-certified marker cycle.

theorem Utilities.PointedGenusOneRigid.map {G : CFGraph} {H : CFGraph} {root : G.V} (hRigid : PointedGenusOneRigid G root) (equivalence : CFGraphIso G H) : PointedGenusOneRigid H (equivalence.vertexEquiv root)

Transport a pointed rigid genus-one graph along a graph isomorphism.