let FT be non empty RelStr ; :: thesis: for g being FinSequence of FT
for A being Subset of FT
for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is symmetric holds
g is inv_continuous
let g be FinSequence of FT; :: thesis: for A being Subset of FT
for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is symmetric holds
g is inv_continuous
let A be Subset of FT; :: thesis: for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is symmetric holds
g is inv_continuous
let x1, x2 be Element of FT; :: thesis: ( g is_minimum_path_in A,x1,x2 & FT is symmetric implies g is inv_continuous )
assume A1:
( g is_minimum_path_in A,x1,x2 & FT is symmetric )
; :: thesis: g is inv_continuous
then A2:
( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 )
by Def8;
hence
1 <= len g
by Def6; :: according to FINTOPO6:def 9 :: thesis: for i, j being Nat
for y being Element of FT st 1 <= i & i <= len g & 1 <= j & j <= len g & y = g . i & i <> j & g . j in U_FT y & not i = j + 1 holds
j = i + 1
let i2, j2 be Nat; :: thesis: for y being Element of FT st 1 <= i2 & i2 <= len g & 1 <= j2 & j2 <= len g & y = g . i2 & i2 <> j2 & g . j2 in U_FT y & not i2 = j2 + 1 holds
j2 = i2 + 1
let y be Element of FT; :: thesis: ( 1 <= i2 & i2 <= len g & 1 <= j2 & j2 <= len g & y = g . i2 & i2 <> j2 & g . j2 in U_FT y & not i2 = j2 + 1 implies j2 = i2 + 1 )
assume A3:
( 1 <= i2 & i2 <= len g & 1 <= j2 & j2 <= len g & y = g . i2 & i2 <> j2 & g . j2 in U_FT y )
; :: thesis: ( i2 = j2 + 1 or j2 = i2 + 1 )
hereby :: thesis: verum
assume A4:
(
i2 <> j2 + 1 &
j2 <> i2 + 1 )
;
:: thesis: contradictionper cases
( i2 < j2 or j2 < i2 )
by A3, XXREAL_0:1;
suppose A5:
i2 < j2
;
:: thesis: contradictionset n1 =
j2 -' 1;
set n2 =
i2;
reconsider n1 =
j2 -' 1,
n2 =
i2 as
Element of
NAT by ORDINAL1:def 13;
i2 + 1
<= j2
by A5, NAT_1:13;
then
i2 + 1
< j2
by A4, XXREAL_0:1;
then
i2 < j2 - 1
by XREAL_1:22;
then A6:
n1 > n2
by A3, XREAL_1:235;
reconsider g2 =
(g | n2) ^ (g /^ n1) as
FinSequence of
FT ;
1
< j2
by A3, A5, XXREAL_0:2;
then
1
+ 1
<= j2
by NAT_1:13;
then A7:
1
<= j2 - 1
by XREAL_1:21;
A8:
j2 -' 1
<= j2
by NAT_D:35;
then A9:
( 1
<= n1 &
n1 <= len g )
by A3, A7, XREAL_1:235, XXREAL_0:2;
A10:
len (g | n2) = n2
by A3, FINSEQ_1:80;
then A11:
g2 . 1 =
(g | n2) . 1
by A3, FINSEQ_1:85
.=
x1
by A2, A3, FINSEQ_3:121
;
A12:
len g2 =
(len (g | n2)) + (len (g /^ n1))
by FINSEQ_1:35
.=
n2 + ((len g) - n1)
by A9, A10, RFINSEQ:def 2
;
A13:
(len g) - n1 >= 0
by A9, XREAL_1:50;
then A14:
(len g) -' n1 = (len g) - n1
by XREAL_0:def 2;
set k =
(len g) -' n1;
A15:
len (g /^ n1) = (len g) - n1
by A9, RFINSEQ:def 2;
now per cases
( n1 < len g or n1 = len g )
by A9, XXREAL_0:1;
suppose
n1 < len g
;
:: thesis: contradictionthen
n1 + 1
<= len g
by NAT_1:13;
then A16:
(n1 + 1) - n1 <= (len g) - n1
by XREAL_1:15;
then A17:
(len g) -' n1 in dom (g /^ n1)
by A14, A15, FINSEQ_3:27;
A18:
((len g) -' n1) + n1 = len g
by A14;
A19:
0 + 1
<= n2 + ((len g) - n1)
by A16, XREAL_1:9;
g2 . ((len (g | n2)) + ((len g) -' n1)) =
(g /^ n1) . ((len g) -' n1)
by A17, FINSEQ_1:def 7
.=
x2
by A2, A9, A17, A18, RFINSEQ:def 2
;
then A20:
g2 . (len g2) = x2
by A10, A12, A13, XREAL_0:def 2;
A21:
rng g2 = (rng (g | n2)) \/ (rng (g /^ n1))
by FINSEQ_1:44;
A22:
rng (g | n2) c= rng g
by FINSEQ_5:21;
rng (g /^ n1) c= rng g
by FINSEQ_5:36;
then
rng g2 c= rng g
by A21, A22, XBOOLE_1:8;
then A23:
rng g2 c= A
by A2, XBOOLE_1:1;
g2 is
continuous
proof
thus
len g2 >= 1
by A12, A19;
:: according to FINTOPO6:def 6 :: thesis: for i being Nat
for x1 being Element of FT st 1 <= i & i < len g2 & x1 = g2 . i holds
g2 . (i + 1) in U_FT x1
let i be
Nat;
:: thesis: for x1 being Element of FT st 1 <= i & i < len g2 & x1 = g2 . i holds
g2 . (i + 1) in U_FT x1let z1 be
Element of
FT;
:: thesis: ( 1 <= i & i < len g2 & z1 = g2 . i implies g2 . (i + 1) in U_FT z1 )
assume A24:
( 1
<= i &
i < len g2 &
z1 = g2 . i )
;
:: thesis: g2 . (i + 1) in U_FT z1
then A25:
i + 1
<= len g2
by NAT_1:13;
reconsider i =
i as
Element of
NAT by ORDINAL1:def 13;
1
< i + 1
by A24, NAT_1:13;
then
i + 1
in dom g2
by A25, FINSEQ_3:27;
then
g2 . (i + 1) = g2 /. (i + 1)
by PARTFUN1:def 8;
then reconsider z2 =
g2 . (i + 1) as
Element of
FT ;
per cases
( i < n2 or i >= n2 )
;
suppose A26:
i < n2
;
:: thesis: g2 . (i + 1) in U_FT z1then A27:
i + 1
<= n2
by NAT_1:13;
A28:
i < len g
by A3, A26, XXREAL_0:2;
A29:
z1 =
(g | n2) . i
by A10, A24, A26, FINSEQ_1:85
.=
g . i
by A26, FINSEQ_3:121
;
i + 1
<= len (g | n2)
by A10, A26, NAT_1:13;
then z2 =
(g | n2) . (i + 1)
by FINSEQ_1:85, NAT_1:12
.=
g . (i + 1)
by A27, FINSEQ_3:121
;
hence
g2 . (i + 1) in U_FT z1
by A2, A24, A28, A29, Def6;
:: thesis: verum end; suppose A30:
i >= n2
;
:: thesis: g2 . (i + 1) in U_FT z1
i - n2 < (n2 + ((len g) - n1)) - n2
by A12, A24, XREAL_1:11;
then A31:
i -' n2 < (len g) - n1
by A30, XREAL_1:235;
then
i -' n2 < (len g) -' n1
by A3, A8, XREAL_1:235, XXREAL_0:2;
then
(i -' n2) + 1
<= (len g) -' n1
by NAT_1:13;
then A32:
( 1
<= (i -' n2) + 1 &
(i -' n2) + 1
<= len (g /^ n1) )
by A9, A15, NAT_1:12, XREAL_1:235;
then A33:
(i -' n2) + 1
in dom (g /^ n1)
by FINSEQ_3:27;
A34:
(len (g | n2)) + (i -' n2) =
n2 + (i - n2)
by A10, A30, XREAL_1:235
.=
i
;
A35:
(len (g | n2)) + ((i -' n2) + 1) =
((i - n2) + 1) + n2
by A10, A30, XREAL_1:235
.=
i + 1
;
per cases
( i > n2 or i = n2 )
by A30, XXREAL_0:1;
suppose
i > n2
;
:: thesis: g2 . (i + 1) in U_FT z1then A36:
i - n2 > 0
by XREAL_1:52;
then
i -' n2 = i - n2
by XREAL_0:def 2;
then A37:
0 + 1
<= i -' n2
by A36, NAT_1:13;
then A38:
i -' n2 in dom (g /^ n1)
by A15, A31, FINSEQ_3:27;
A39:
z1 =
(g /^ n1) . (i -' n2)
by A15, A24, A31, A34, A37, FINSEQ_1:86
.=
g . ((i -' n2) + n1)
by A9, A38, RFINSEQ:def 2
;
A40:
z2 =
(g /^ n1) . ((i -' n2) + 1)
by A32, A35, FINSEQ_1:86
.=
g . (((i -' n2) + 1) + n1)
by A9, A33, RFINSEQ:def 2
.=
g . (((i -' n2) + n1) + 1)
;
A41:
1
<= (i -' n2) + n1
by A9, NAT_1:12;
(i -' n2) + n1 < ((len g) - n1) + n1
by A31, XREAL_1:8;
hence
g2 . (i + 1) in U_FT z1
by A2, A39, A40, A41, Def6;
:: thesis: verum end; suppose A42:
i = n2
;
:: thesis: g2 . (i + 1) in U_FT z1then A43:
z1 =
(g | n2) . n2
by A10, A24, FINSEQ_1:85
.=
y
by A3, FINSEQ_3:121
;
z2 =
(g /^ n1) . ((i -' n2) + 1)
by A32, A35, FINSEQ_1:86
.=
g . (((i -' n2) + 1) + n1)
by A9, A33, RFINSEQ:def 2
.=
g . (((i -' n2) + n1) + 1)
.=
g . ((0 + (j2 -' 1)) + 1)
by A42, XREAL_1:234
.=
g . ((j2 - 1) + 1)
by A3, XREAL_1:235
;
hence
g2 . (i + 1) in U_FT z1
by A3, A43;
:: thesis: verum end; end;
end; then
len g <= len g2
by A1, A11, A20, A23, Def8;
then
(len g) - n2 <= (n2 + ((len g) - n1)) - n2
by A12, XREAL_1:15;
hence
contradiction
by A6, XREAL_1:12;
:: thesis: verum end; hence
contradiction
;
:: thesis: verum end; suppose A44:
j2 < i2
;
:: thesis: contradictionreconsider n1 =
i2 -' 1,
n2 =
j2 as
Element of
NAT by ORDINAL1:def 13;
j2 + 1
<= i2
by A44, NAT_1:13;
then
j2 + 1
< i2
by A4, XXREAL_0:1;
then
j2 < i2 - 1
by XREAL_1:22;
then A45:
n1 > n2
by A3, XREAL_1:235;
reconsider g2 =
(g | n2) ^ (g /^ n1) as
FinSequence of
FT ;
1
< i2
by A3, A44, XXREAL_0:2;
then
1
+ 1
<= i2
by NAT_1:13;
then A46:
1
<= i2 - 1
by XREAL_1:21;
A47:
i2 -' 1
<= i2
by NAT_D:35;
then A48:
( 1
<= n1 &
n1 <= len g )
by A3, A46, XREAL_1:235, XXREAL_0:2;
A49:
len (g | n2) = n2
by A3, FINSEQ_1:80;
then A50:
g2 . 1 =
(g | n2) . 1
by A3, FINSEQ_1:85
.=
x1
by A2, A3, FINSEQ_3:121
;
A51:
len g2 =
(len (g | n2)) + (len (g /^ n1))
by FINSEQ_1:35
.=
n2 + ((len g) - n1)
by A48, A49, RFINSEQ:def 2
;
A52:
(len g) - n1 >= 0
by A48, XREAL_1:50;
then A53:
(len g) -' n1 = (len g) - n1
by XREAL_0:def 2;
set k =
(len g) -' n1;
A54:
len (g /^ n1) = (len g) - n1
by A48, RFINSEQ:def 2;
now per cases
( n1 < len g or n1 = len g )
by A48, XXREAL_0:1;
suppose
n1 < len g
;
:: thesis: contradictionthen
n1 + 1
<= len g
by NAT_1:13;
then A55:
(n1 + 1) - n1 <= (len g) - n1
by XREAL_1:15;
then A56:
(len g) -' n1 in dom (g /^ n1)
by A53, A54, FINSEQ_3:27;
A57:
((len g) -' n1) + n1 = len g
by A53;
A58:
0 + 1
<= n2 + ((len g) - n1)
by A55, XREAL_1:9;
g2 . ((len (g | n2)) + ((len g) -' n1)) =
(g /^ n1) . ((len g) -' n1)
by A56, FINSEQ_1:def 7
.=
x2
by A2, A48, A56, A57, RFINSEQ:def 2
;
then A59:
g2 . (len g2) = x2
by A49, A51, A52, XREAL_0:def 2;
A60:
rng g2 = (rng (g | n2)) \/ (rng (g /^ n1))
by FINSEQ_1:44;
A61:
rng (g | n2) c= rng g
by FINSEQ_5:21;
rng (g /^ n1) c= rng g
by FINSEQ_5:36;
then
rng g2 c= rng g
by A60, A61, XBOOLE_1:8;
then A62:
rng g2 c= A
by A2, XBOOLE_1:1;
g2 is
continuous
proof
thus
len g2 >= 1
by A51, A58;
:: according to FINTOPO6:def 6 :: thesis: for i being Nat
for x1 being Element of FT st 1 <= i & i < len g2 & x1 = g2 . i holds
g2 . (i + 1) in U_FT x1
let i be
Nat;
:: thesis: for x1 being Element of FT st 1 <= i & i < len g2 & x1 = g2 . i holds
g2 . (i + 1) in U_FT x1let z1 be
Element of
FT;
:: thesis: ( 1 <= i & i < len g2 & z1 = g2 . i implies g2 . (i + 1) in U_FT z1 )
assume A63:
( 1
<= i &
i < len g2 &
z1 = g2 . i )
;
:: thesis: g2 . (i + 1) in U_FT z1
then A64:
i + 1
<= len g2
by NAT_1:13;
reconsider i =
i as
Element of
NAT by ORDINAL1:def 13;
1
< i + 1
by A63, NAT_1:13;
then
i + 1
in dom g2
by A64, FINSEQ_3:27;
then
g2 . (i + 1) = g2 /. (i + 1)
by PARTFUN1:def 8;
then reconsider z2 =
g2 . (i + 1) as
Element of
FT ;
per cases
( i < n2 or i >= n2 )
;
suppose A65:
i < n2
;
:: thesis: g2 . (i + 1) in U_FT z1then A66:
i + 1
<= n2
by NAT_1:13;
A67:
i < len g
by A3, A65, XXREAL_0:2;
A68:
z1 =
(g | n2) . i
by A49, A63, A65, FINSEQ_1:85
.=
g . i
by A65, FINSEQ_3:121
;
i + 1
<= len (g | n2)
by A49, A65, NAT_1:13;
then z2 =
(g | n2) . (i + 1)
by FINSEQ_1:85, NAT_1:12
.=
g . (i + 1)
by A66, FINSEQ_3:121
;
hence
g2 . (i + 1) in U_FT z1
by A2, A63, A67, A68, Def6;
:: thesis: verum end; suppose A69:
i >= n2
;
:: thesis: g2 . (i + 1) in U_FT z1
i - n2 < (n2 + ((len g) - n1)) - n2
by A51, A63, XREAL_1:11;
then A70:
i -' n2 < (len g) - n1
by A69, XREAL_1:235;
then
i -' n2 < (len g) -' n1
by A3, A47, XREAL_1:235, XXREAL_0:2;
then
(i -' n2) + 1
<= (len g) -' n1
by NAT_1:13;
then A71:
( 1
<= (i -' n2) + 1 &
(i -' n2) + 1
<= len (g /^ n1) )
by A48, A54, NAT_1:12, XREAL_1:235;
then A72:
(i -' n2) + 1
in dom (g /^ n1)
by FINSEQ_3:27;
A73:
(len (g | n2)) + (i -' n2) =
n2 + (i - n2)
by A49, A69, XREAL_1:235
.=
i
;
A74:
(len (g | n2)) + ((i -' n2) + 1) =
((i - n2) + 1) + n2
by A49, A69, XREAL_1:235
.=
i + 1
;
per cases
( i > n2 or i = n2 )
by A69, XXREAL_0:1;
suppose
i > n2
;
:: thesis: g2 . (i + 1) in U_FT z1then A75:
i - n2 > 0
by XREAL_1:52;
then
i -' n2 = i - n2
by XREAL_0:def 2;
then A76:
0 + 1
<= i -' n2
by A75, NAT_1:13;
then A77:
i -' n2 in dom (g /^ n1)
by A54, A70, FINSEQ_3:27;
A78:
z1 =
(g /^ n1) . (i -' n2)
by A54, A63, A70, A73, A76, FINSEQ_1:86
.=
g . ((i -' n2) + n1)
by A48, A77, RFINSEQ:def 2
;
A79:
z2 =
(g /^ n1) . ((i -' n2) + 1)
by A71, A74, FINSEQ_1:86
.=
g . (((i -' n2) + 1) + n1)
by A48, A72, RFINSEQ:def 2
.=
g . (((i -' n2) + n1) + 1)
;
A80:
1
<= (i -' n2) + n1
by A48, NAT_1:12;
(i -' n2) + n1 < ((len g) - n1) + n1
by A70, XREAL_1:8;
hence
g2 . (i + 1) in U_FT z1
by A2, A78, A79, A80, Def6;
:: thesis: verum end; suppose A81:
i = n2
;
:: thesis: g2 . (i + 1) in U_FT z1then A82:
z1 =
(g | n2) . n2
by A49, A63, FINSEQ_1:85
.=
g . j2
by FINSEQ_3:121
;
z2 =
(g /^ n1) . ((i -' n2) + 1)
by A71, A74, FINSEQ_1:86
.=
g . (((i -' n2) + 1) + n1)
by A48, A72, RFINSEQ:def 2
.=
g . (((i -' n2) + n1) + 1)
.=
g . ((0 + (i2 -' 1)) + 1)
by A81, XREAL_1:234
.=
g . ((i2 - 1) + 1)
by A3, XREAL_1:235
.=
y
by A3
;
hence
g2 . (i + 1) in U_FT z1
by A1, A3, A82, FIN_TOPO:def 15;
:: thesis: verum end; end;
end; then
len g <= len g2
by A1, A50, A59, A62, Def8;
then
(len g) - n2 <= (n2 + ((len g) - n1)) - n2
by A51, XREAL_1:15;
hence
contradiction
by A45, XREAL_1:12;
:: thesis: verum end; hence
contradiction
;
:: thesis: verum end;
end;