let G be SimpleGraph; for C being Coloring of G
for S being Subset of (Vertices G) holds C | S is Coloring of (G SubgraphInducedBy S)
let C be Coloring of G; for S being Subset of (Vertices G) holds C | S is Coloring of (G SubgraphInducedBy S)
let S be Subset of (Vertices G); C | S is Coloring of (G SubgraphInducedBy S)
set g = G SubgraphInducedBy S;
A1: Vertices (G SubgraphInducedBy S) =
S /\ (Vertices G)
by Th45
.=
S
by XBOOLE_1:28
;
reconsider CS = C | S as a_partition of Vertices (G SubgraphInducedBy S) by A1;
CS is StableSet-wise
proof
let x be
set ;
SCMYCIEL:def 20 ( x in CS implies x is StableSet of (G SubgraphInducedBy S) )
assume A2:
x in CS
;
x is StableSet of (G SubgraphInducedBy S)
reconsider xx =
x as
Subset of
(Vertices (G SubgraphInducedBy S)) by A2;
consider z being
Element of
C such that A3:
xx = z /\ S
and
z meets S
by A2;
xx is
stable
proof
let x,
y be
set ;
SCMYCIEL:def 19 ( x <> y & x in xx & y in xx implies {x,y} nin G SubgraphInducedBy S )
assume that A4:
x <> y
and A5:
x in xx
and A6:
y in xx
;
{x,y} nin G SubgraphInducedBy S
assume A7:
{x,y} in G SubgraphInducedBy S
;
contradiction
A8:
x in z
by A3, A5, XBOOLE_0:def 4;
A9:
y in z
by A6, A3, XBOOLE_0:def 4;
z is
StableSet of
G
by A3, A5, Def20;
hence
contradiction
by A7, A4, A8, A9, Def19;
verum
end;
hence
x is
StableSet of
(G SubgraphInducedBy S)
;
verum
end;
hence
C | S is Coloring of (G SubgraphInducedBy S)
; verum