fact: Definition component (G : graph2) (H : {set G}) : graph2 := @point (induced (input |: (output |: H))) (Sub input (setU11 _ _)) (Sub output (setU1r _ (setU11 _ _))).
imports: Coq(RelationClasses Morphisms Setoid Lia) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries) GraphTheory(digraph sgraph minor checkpoint cp_minor) GraphTheory(setoid_bigop structures pttdom ptt) GraphTheory(mgraph mgraph2 skeleton bounded)