let G1, G2 be _Graph; for H being Subgraph of G2
for F being PGraphMapping of G1,G2 holds
( ( F is empty implies H |` F is empty ) & ( F is one-to-one implies H |` F is one-to-one ) & ( F is onto implies H |` F is onto ) & ( not F is total implies not H |` F is total ) & ( F is directed implies H |` F is directed ) & ( F is semi-continuous implies H |` F is semi-continuous ) & ( F is continuous implies H |` F is continuous ) & ( F is semi-Dcontinuous implies H |` F is semi-Dcontinuous ) & ( F is Dcontinuous implies H |` F is Dcontinuous ) )
let H be Subgraph of G2; for F being PGraphMapping of G1,G2 holds
( ( F is empty implies H |` F is empty ) & ( F is one-to-one implies H |` F is one-to-one ) & ( F is onto implies H |` F is onto ) & ( not F is total implies not H |` F is total ) & ( F is directed implies H |` F is directed ) & ( F is semi-continuous implies H |` F is semi-continuous ) & ( F is continuous implies H |` F is continuous ) & ( F is semi-Dcontinuous implies H |` F is semi-Dcontinuous ) & ( F is Dcontinuous implies H |` F is Dcontinuous ) )
let F be PGraphMapping of G1,G2; ( ( F is empty implies H |` F is empty ) & ( F is one-to-one implies H |` F is one-to-one ) & ( F is onto implies H |` F is onto ) & ( not F is total implies not H |` F is total ) & ( F is directed implies H |` F is directed ) & ( F is semi-continuous implies H |` F is semi-continuous ) & ( F is continuous implies H |` F is continuous ) & ( F is semi-Dcontinuous implies H |` F is semi-Dcontinuous ) & ( F is Dcontinuous implies H |` F is Dcontinuous ) )
reconsider f = (the_Vertices_of H) |` (F _V) as PartFunc of (the_Vertices_of G1),(the_Vertices_of H) by PARTFUN1:12;
reconsider g = (the_Edges_of H) |` (F _E) as PartFunc of (the_Edges_of G1),(the_Edges_of H) by PARTFUN1:12;
thus
( F is one-to-one implies H |` F is one-to-one )
by FUNCT_1:58; ( ( F is onto implies H |` F is onto ) & ( not F is total implies not H |` F is total ) & ( F is directed implies H |` F is directed ) & ( F is semi-continuous implies H |` F is semi-continuous ) & ( F is continuous implies H |` F is continuous ) & ( F is semi-Dcontinuous implies H |` F is semi-Dcontinuous ) & ( F is Dcontinuous implies H |` F is Dcontinuous ) )
thus
( F is onto implies H |` F is onto )
( ( not F is total implies not H |` F is total ) & ( F is directed implies H |` F is directed ) & ( F is semi-continuous implies H |` F is semi-continuous ) & ( F is continuous implies H |` F is continuous ) & ( F is semi-Dcontinuous implies H |` F is semi-Dcontinuous ) & ( F is Dcontinuous implies H |` F is Dcontinuous ) )
hence
( not F is total implies not H |` F is total )
; ( ( F is directed implies H |` F is directed ) & ( F is semi-continuous implies H |` F is semi-continuous ) & ( F is continuous implies H |` F is continuous ) & ( F is semi-Dcontinuous implies H |` F is semi-Dcontinuous ) & ( F is Dcontinuous implies H |` F is Dcontinuous ) )
thus
( F is directed implies H |` F is directed )
( ( F is semi-continuous implies H |` F is semi-continuous ) & ( F is continuous implies H |` F is continuous ) & ( F is semi-Dcontinuous implies H |` F is semi-Dcontinuous ) & ( F is Dcontinuous implies H |` F is Dcontinuous ) )proof
assume A3:
F is
directed
;
H |` F is directed
let e,
v,
w be
object ;
GLIB_010:def 14 ( e in dom ((H |` F) _E) & v in dom ((H |` F) _V) & w in dom ((H |` F) _V) & e DJoins v,w,G1 implies ((H |` F) _E) . e DJoins ((H |` F) _V) . v,((H |` F) _V) . w,H )
assume A4:
(
e in dom ((H |` F) _E) &
v in dom ((H |` F) _V) &
w in dom ((H |` F) _V) )
;
( not e DJoins v,w,G1 or ((H |` F) _E) . e DJoins ((H |` F) _V) . v,((H |` F) _V) . w,H )
then A5:
(
e in dom (F _E) &
(F _E) . e in the_Edges_of H &
v in dom (F _V) &
(F _V) . v in the_Vertices_of H &
w in dom (F _V) &
(F _V) . w in the_Vertices_of H )
by FUNCT_1:54;
then
(
e DJoins v,
w,
G1 implies
(F _E) . e DJoins (F _V) . v,
(F _V) . w,
G2 )
by A3;
then A6:
(
e DJoins v,
w,
G1 implies
(F _E) . e DJoins (F _V) . v,
(F _V) . w,
H )
by A5, GLIB_000:73;
(
((H |` F) _E) . e = (F _E) . e &
((H |` F) _V) . v = (F _V) . v &
((H |` F) _V) . w = (F _V) . w )
by A4, FUNCT_1:53;
hence
(
e DJoins v,
w,
G1 implies
((H |` F) _E) . e DJoins ((H |` F) _V) . v,
((H |` F) _V) . w,
H )
by A6;
verum
end;
thus
( F is semi-continuous implies H |` F is semi-continuous )
( ( F is continuous implies H |` F is continuous ) & ( F is semi-Dcontinuous implies H |` F is semi-Dcontinuous ) & ( F is Dcontinuous implies H |` F is Dcontinuous ) )proof
assume A7:
F is
semi-continuous
;
H |` F is semi-continuous
reconsider f =
(the_Vertices_of H) |` (F _V) as
PartFunc of
(the_Vertices_of G1),
(the_Vertices_of H) by PARTFUN1:12;
reconsider g =
(the_Edges_of H) |` (F _E) as
PartFunc of
(the_Edges_of G1),
(the_Edges_of H) by PARTFUN1:12;
let e,
v,
w be
object ;
GLIB_010:def 15 ( e in dom ((H |` F) _E) & v in dom ((H |` F) _V) & w in dom ((H |` F) _V) & ((H |` F) _E) . e Joins ((H |` F) _V) . v,((H |` F) _V) . w,H implies e Joins v,w,G1 )
assume A8:
(
e in dom ((H |` F) _E) &
v in dom ((H |` F) _V) &
w in dom ((H |` F) _V) )
;
( not ((H |` F) _E) . e Joins ((H |` F) _V) . v,((H |` F) _V) . w,H or e Joins v,w,G1 )
then
(
e in dom (F _E) &
(F _E) . e in the_Edges_of H &
v in dom (F _V) &
(F _V) . v in the_Vertices_of H &
w in dom (F _V) &
(F _V) . w in the_Vertices_of H )
by FUNCT_1:54;
then
(
(F _E) . e Joins (F _V) . v,
(F _V) . w,
G2 implies
e Joins v,
w,
G1 )
by A7;
then A9:
(
(F _E) . e Joins (F _V) . v,
(F _V) . w,
H implies
e Joins v,
w,
G1 )
by GLIB_000:72;
(
g . e = (F _E) . e &
f . v = (F _V) . v &
f . w = (F _V) . w )
by A8, FUNCT_1:53;
hence
( not
((H |` F) _E) . e Joins ((H |` F) _V) . v,
((H |` F) _V) . w,
H or
e Joins v,
w,
G1 )
by A9;
verum
end;
thus
( F is continuous implies H |` F is continuous )
( ( F is semi-Dcontinuous implies H |` F is semi-Dcontinuous ) & ( F is Dcontinuous implies H |` F is Dcontinuous ) )proof
assume A10:
F is
continuous
;
H |` F is continuous
now for e9, v, w being object st v in dom ((H |` F) _V) & w in dom ((H |` F) _V) & e9 Joins ((H |` F) _V) . v,((H |` F) _V) . w,H holds
ex e being object st
( e Joins v,w,G1 & e in dom ((H |` F) _E) & ((H |` F) _E) . e = e9 )let e9,
v,
w be
object ;
( v in dom ((H |` F) _V) & w in dom ((H |` F) _V) & e9 Joins ((H |` F) _V) . v,((H |` F) _V) . w,H implies ex e being object st
( e Joins v,w,G1 & e in dom ((H |` F) _E) & ((H |` F) _E) . e = e9 ) )set f =
(the_Vertices_of H) |` (F _V);
assume A11:
(
v in dom ((H |` F) _V) &
w in dom ((H |` F) _V) &
e9 Joins ((H |` F) _V) . v,
((H |` F) _V) . w,
H )
;
ex e being object st
( e Joins v,w,G1 & e in dom ((H |` F) _E) & ((H |` F) _E) . e = e9 )then A12:
(
v in dom ((the_Vertices_of H) |` (F _V)) &
w in dom ((the_Vertices_of H) |` (F _V)) &
e9 Joins ((the_Vertices_of H) |` (F _V)) . v,
((the_Vertices_of H) |` (F _V)) . w,
H )
;
then A13:
(
((the_Vertices_of H) |` (F _V)) . v = (F _V) . v &
((the_Vertices_of H) |` (F _V)) . w = (F _V) . w )
by FUNCT_1:55;
A14:
(
v in dom (F _V) &
(F _V) . v in the_Vertices_of H &
w in dom (F _V) &
(F _V) . w in the_Vertices_of H &
v is
set &
w is
set )
by A11, FUNCT_1:54;
e9 Joins (F _V) . v,
(F _V) . w,
G2
by A12, A13, GLIB_000:72;
then consider e being
object such that A15:
(
e Joins v,
w,
G1 &
e in dom (F _E) &
(F _E) . e = e9 )
by A10, A14;
take e =
e;
( e Joins v,w,G1 & e in dom ((H |` F) _E) & ((H |` F) _E) . e = e9 )thus
e Joins v,
w,
G1
by A15;
( e in dom ((H |` F) _E) & ((H |` F) _E) . e = e9 )
e9 in the_Edges_of H
by A11, GLIB_000:def 13;
then
e in dom ((the_Edges_of H) |` (F _E))
by A15, FUNCT_1:54;
hence
(
e in dom ((H |` F) _E) &
((H |` F) _E) . e = e9 )
by A15, FUNCT_1:55;
verum end;
hence
H |` F is
continuous
;
verum
end;
thus
( F is semi-Dcontinuous implies H |` F is semi-Dcontinuous )
( F is Dcontinuous implies H |` F is Dcontinuous )proof
assume A16:
F is
semi-Dcontinuous
;
H |` F is semi-Dcontinuous
let e,
v,
w be
object ;
GLIB_010:def 17 ( e in dom ((H |` F) _E) & v in dom ((H |` F) _V) & w in dom ((H |` F) _V) & ((H |` F) _E) . e DJoins ((H |` F) _V) . v,((H |` F) _V) . w,H implies e DJoins v,w,G1 )
assume A17:
(
e in dom ((H |` F) _E) &
v in dom ((H |` F) _V) &
w in dom ((H |` F) _V) )
;
( not ((H |` F) _E) . e DJoins ((H |` F) _V) . v,((H |` F) _V) . w,H or e DJoins v,w,G1 )
then
(
e in dom (F _E) &
(F _E) . e in the_Edges_of H &
v in dom (F _V) &
(F _V) . v in the_Vertices_of H &
w in dom (F _V) &
(F _V) . w in the_Vertices_of H )
by FUNCT_1:54;
then A18:
(
(F _E) . e DJoins (F _V) . v,
(F _V) . w,
H implies
e DJoins v,
w,
G1 )
by A16, GLIB_000:72;
(
((H |` F) _E) . e = (F _E) . e &
((H |` F) _V) . v = (F _V) . v &
((H |` F) _V) . w = (F _V) . w )
by A17, FUNCT_1:53;
hence
(
((H |` F) _E) . e DJoins ((H |` F) _V) . v,
((H |` F) _V) . w,
H implies
e DJoins v,
w,
G1 )
by A18;
verum
end;
thus
( F is Dcontinuous implies H |` F is Dcontinuous )
verumproof
assume A19:
F is
Dcontinuous
;
H |` F is Dcontinuous
now for e9, v, w being object st v in dom ((H |` F) _V) & w in dom ((H |` F) _V) & e9 DJoins ((H |` F) _V) . v,((H |` F) _V) . w,H holds
ex e being object st
( e DJoins v,w,G1 & e in dom ((H |` F) _E) & ((H |` F) _E) . e = e9 )let e9,
v,
w be
object ;
( v in dom ((H |` F) _V) & w in dom ((H |` F) _V) & e9 DJoins ((H |` F) _V) . v,((H |` F) _V) . w,H implies ex e being object st
( e DJoins v,w,G1 & e in dom ((H |` F) _E) & ((H |` F) _E) . e = e9 ) )set f =
(the_Vertices_of H) |` (F _V);
assume A20:
(
v in dom ((H |` F) _V) &
w in dom ((H |` F) _V) &
e9 DJoins ((H |` F) _V) . v,
((H |` F) _V) . w,
H )
;
ex e being object st
( e DJoins v,w,G1 & e in dom ((H |` F) _E) & ((H |` F) _E) . e = e9 )then A21:
(
v in dom ((the_Vertices_of H) |` (F _V)) &
w in dom ((the_Vertices_of H) |` (F _V)) &
e9 DJoins ((the_Vertices_of H) |` (F _V)) . v,
((the_Vertices_of H) |` (F _V)) . w,
H )
;
then A22:
(
((the_Vertices_of H) |` (F _V)) . v = (F _V) . v &
((the_Vertices_of H) |` (F _V)) . w = (F _V) . w )
by FUNCT_1:55;
A23:
(
v in dom (F _V) &
(F _V) . v in the_Vertices_of H &
w in dom (F _V) &
(F _V) . w in the_Vertices_of H &
v is
set &
w is
set )
by A20, FUNCT_1:54;
e9 DJoins (F _V) . v,
(F _V) . w,
G2
by A21, A22, GLIB_000:72;
then consider e being
object such that A24:
(
e DJoins v,
w,
G1 &
e in dom (F _E) &
(F _E) . e = e9 )
by A19, A23;
take e =
e;
( e DJoins v,w,G1 & e in dom ((H |` F) _E) & ((H |` F) _E) . e = e9 )thus
e DJoins v,
w,
G1
by A24;
( e in dom ((H |` F) _E) & ((H |` F) _E) . e = e9 )
e9 in the_Edges_of H
by A20, GLIB_000:def 14;
then
e in dom ((the_Edges_of H) |` (F _E))
by A24, FUNCT_1:54;
hence
(
e in dom ((H |` F) _E) &
((H |` F) _E) . e = e9 )
by A24, FUNCT_1:55;
verum end;
hence
H |` F is
Dcontinuous
;
verum
end;