proposition: Lemma isubgraph_induced (F G : sgraph) (i : F ⇀ G) : F ≃ induced [set x in codom i].
proof: Proof. set A := [set _ in _]. have jP (x : induced A) : val x \in codom i. abstract by move: (valP x); rewrite inE. pose j (x : induced A) : F := iinv (jP x). have iP (x : F) : i x \in A by abstract by rewrite inE codom_f. pose i' (x : F) : induced A := Sub (i x) (iP x). have can_i : cancel i' j. abstract by move=> x; apply: (isubgraph_inj i); rewrite f_iinv. have can_j : cancel j i'. abstract by move => [x xA]; apply: val_inj; rewrite /j/=f_iinv. apply: Diso' can_i can_j _. abstract by move => x y; rewrite induced_edge /= isubgraph_mono. Defined.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)