let G be _Graph; :: thesis: for S being non empty Subset of (the_Vertices_of G)
for H being inducedSubgraph of G,S
for W1 being Walk of G
for W2 being Walk of H st W1 = W2 holds
( W2 is chordal iff W1 is chordal )
let S be non empty Subset of (the_Vertices_of G); :: thesis: for H being inducedSubgraph of G,S
for W1 being Walk of G
for W2 being Walk of H st W1 = W2 holds
( W2 is chordal iff W1 is chordal )
let H be inducedSubgraph of G,S; :: thesis: for W1 being Walk of G
for W2 being Walk of H st W1 = W2 holds
( W2 is chordal iff W1 is chordal )
let W1 be Walk of G; :: thesis: for W2 being Walk of H st W1 = W2 holds
( W2 is chordal iff W1 is chordal )
let W2 be Walk of H; :: thesis: ( W1 = W2 implies ( W2 is chordal iff W1 is chordal ) )
assume A1:
W1 = W2
; :: thesis: ( W2 is chordal iff W1 is chordal )
A2:
S = the_Vertices_of H
by GLIB_000:def 39;
thus
( W2 is chordal implies W1 is chordal )
:: thesis: ( W1 is chordal implies W2 is chordal )proof
given m,
n being
odd Nat such that A3:
(
m + 2
< n &
n <= len W2 &
W2 . m <> W2 . n )
and A4:
ex
e being
set st
e Joins W2 . m,
W2 . n,
H
and A5:
for
f being
set st
f in W2 .edges() holds
not
f Joins W2 . m,
W2 . n,
H
;
:: according to CHORD:def 10 :: thesis: W1 is chordal
take
m
;
:: according to CHORD:def 10 :: thesis: ex n being natural odd number st
( m + 2 < n & n <= len W1 & W1 . m <> W1 . n & ex e being set st e Joins W1 . m,W1 . n,G & ( for f being set st f in W1 .edges() holds
not f Joins W1 . m,W1 . n,G ) )
take
n
;
:: thesis: ( m + 2 < n & n <= len W1 & W1 . m <> W1 . n & ex e being set st e Joins W1 . m,W1 . n,G & ( for f being set st f in W1 .edges() holds
not f Joins W1 . m,W1 . n,G ) )
thus
(
m + 2
< n &
n <= len W1 &
W1 . m <> W1 . n )
by A1, A3;
:: thesis: ( ex e being set st e Joins W1 . m,W1 . n,G & ( for f being set st f in W1 .edges() holds
not f Joins W1 . m,W1 . n,G ) )
consider e being
set such that A6:
e Joins W2 . m,
W2 . n,
H
by A4;
e Joins W1 . m,
W1 . n,
G
by A1, A6, GLIB_000:75;
hence
ex
e being
set st
e Joins W1 . m,
W1 . n,
G
;
:: thesis: for f being set st f in W1 .edges() holds
not f Joins W1 . m,W1 . n,G
let f be
set ;
:: thesis: ( f in W1 .edges() implies not f Joins W1 . m,W1 . n,G )
assume
f in W1 .edges()
;
:: thesis: not f Joins W1 . m,W1 . n,G
then A7:
f in W2 .edges()
by A1, GLIB_001:111;
then
not
f Joins W1 . m,
W1 . n,
H
by A1, A5;
hence
not
f Joins W1 . m,
W1 . n,
G
by A7, GLIB_000:76;
:: thesis: verum
end;
thus
( W1 is chordal implies W2 is chordal )
:: thesis: verumproof
given m,
n being
odd Nat such that A8:
(
m + 2
< n &
n <= len W1 &
W1 . m <> W1 . n )
and A9:
ex
e being
set st
e Joins W1 . m,
W1 . n,
G
and A10:
for
f being
set st
f in W1 .edges() holds
not
f Joins W1 . m,
W1 . n,
G
;
:: according to CHORD:def 10 :: thesis: W2 is chordal
take
m
;
:: according to CHORD:def 10 :: thesis: ex n being natural odd number st
( m + 2 < n & n <= len W2 & W2 . m <> W2 . n & ex e being set st e Joins W2 . m,W2 . n,H & ( for f being set st f in W2 .edges() holds
not f Joins W2 . m,W2 . n,H ) )
take
n
;
:: thesis: ( m + 2 < n & n <= len W2 & W2 . m <> W2 . n & ex e being set st e Joins W2 . m,W2 . n,H & ( for f being set st f in W2 .edges() holds
not f Joins W2 . m,W2 . n,H ) )
A11:
(
m in NAT &
n in NAT )
by ORDINAL1:def 13;
thus
(
m + 2
< n &
n <= len W2 &
W2 . m <> W2 . n )
by A1, A8;
:: thesis: ( ex e being set st e Joins W2 . m,W2 . n,H & ( for f being set st f in W2 .edges() holds
not f Joins W2 . m,W2 . n,H ) )
consider e being
set such that A12:
e Joins W1 . m,
W1 . n,
G
by A9;
m < n
by A8, NAT_1:12;
then
(
W1 . m in the_Vertices_of H &
W1 . n in the_Vertices_of H )
by A1, A8, A11, GLIB_001:8, XXREAL_0:2;
hence
ex
e being
set st
e Joins W2 . m,
W2 . n,
H
by A1, A2, A12, Th19;
:: thesis: for f being set st f in W2 .edges() holds
not f Joins W2 . m,W2 . n,H
let f be
set ;
:: thesis: ( f in W2 .edges() implies not f Joins W2 . m,W2 . n,H )
assume
f in W2 .edges()
;
:: thesis: not f Joins W2 . m,W2 . n,H
then
f in W1 .edges()
by A1, GLIB_001:111;
then
not
f Joins W2 . m,
W2 . n,
G
by A1, A10;
hence
not
f Joins W2 . m,
W2 . n,
H
by GLIB_000:75;
:: thesis: verum
end;