let G1, G2 be non-multi _Graph; for f being PVertexMapping of G1,G2 st f is continuous & f is one-to-one holds
PVM2PGM f is semi-continuous
let f be PVertexMapping of G1,G2; ( f is continuous & f is one-to-one implies PVM2PGM f is semi-continuous )
assume A1:
( f is continuous & f is one-to-one )
; PVM2PGM f is semi-continuous
set g = (PVM2PGM f) _E ;
now for e, v, w being object st e in dom ((PVM2PGM f) _E) & v in dom ((PVM2PGM f) _V) & w in dom ((PVM2PGM f) _V) & ((PVM2PGM f) _E) . e Joins ((PVM2PGM f) _V) . v,((PVM2PGM f) _V) . w,G2 holds
e Joins v,w,G1let e,
v,
w be
object ;
( e in dom ((PVM2PGM f) _E) & v in dom ((PVM2PGM f) _V) & w in dom ((PVM2PGM f) _V) & ((PVM2PGM f) _E) . e Joins ((PVM2PGM f) _V) . v,((PVM2PGM f) _V) . w,G2 implies e Joins v,w,G1 )assume A2:
(
e in dom ((PVM2PGM f) _E) &
v in dom ((PVM2PGM f) _V) &
w in dom ((PVM2PGM f) _V) )
;
( ((PVM2PGM f) _E) . e Joins ((PVM2PGM f) _V) . v,((PVM2PGM f) _V) . w,G2 implies e Joins v,w,G1 )assume A3:
((PVM2PGM f) _E) . e Joins ((PVM2PGM f) _V) . v,
((PVM2PGM f) _V) . w,
G2
;
e Joins v,w,G1then
((PVM2PGM f) _E) . e Joins f . v,
f . w,
G2
;
then consider e0 being
object such that A4:
e0 Joins v,
w,
G1
by A1, A2, Th2;
e0 in G1 .edgesBetween (dom f)
by A2, A4, GLIB_000:32;
then A5:
e0 in dom ((PVM2PGM f) _E)
by Def10;
then
((PVM2PGM f) _E) . e0 Joins ((PVM2PGM f) _V) . v,
((PVM2PGM f) _V) . w,
G2
by A2, A4, GLIB_010:4;
then A6:
((PVM2PGM f) _E) . e0 = ((PVM2PGM f) _E) . e
by A3, GLIB_000:def 20;
PVM2PGM f is
one-to-one
by A1, Th34;
hence
e Joins v,
w,
G1
by A2, A4, A5, A6, FUNCT_1:def 4;
verum end;
hence
PVM2PGM f is semi-continuous
by GLIB_010:def 15; verum