proposition: Lemma separation_no_isolated (G: sgraph) (V1 V2 : {set G}) : proper_separation V1 V2 -> smallest vseparator (V1 :&: V2) -> no_isolated G -> no_isolated (induced V1) /\ no_isolated (induced V2).
proof: Proof. move=> sepV smallV no_iso. wlog suff I : V1 V2 sepV smallV / no_isolated (induced V1). { move: (sepV) (smallV) => /proper_separation_symmetry ?; rewrite setIC => ?. by split; apply: I; eassumption. } move=> x; have [xV2|xNV2] := boolP (val x \in V2). - have xV : val x \in V1 :&: V2 by rewrite inE xV2 (valP x). have [y [? [yNV2 _ xy _]]] := svseparator_neighbours sepV smallV xV. have yV1 : y \in V1 by apply: sep_inL (sepV.1) yNV2. by exists (Sub y yV1). - have [y xy] := no_iso (val x). suff yV1 : y \in V1 by exists (Sub y yV1). by apply: contraTT xy => ?; rewrite sepV.1. Qed.
imports: HB(structures) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(sgraph connectivity minor excluded) fourcolor(hypermap geometry walkup color coloring combinatorial4ct) GraphTheory(set_tac) GraphTheory(hmap_ops smerge embedding arc K4plane)