let kc, km be Element of NAT ; for n being non zero Element of NAT
for f being Function of (FTSL1 n),(FTSL1 n) st f is_continuous kc & km = [/(kc / 2)\] holds
ex p being Element of (FTSL1 n) st f . p in U_FT p,km
let n be non zero Element of NAT ; for f being Function of (FTSL1 n),(FTSL1 n) st f is_continuous kc & km = [/(kc / 2)\] holds
ex p being Element of (FTSL1 n) st f . p in U_FT p,km
let f be Function of (FTSL1 n),(FTSL1 n); ( f is_continuous kc & km = [/(kc / 2)\] implies ex p being Element of (FTSL1 n) st f . p in U_FT p,km )
assume that
A1:
f is_continuous kc
and
A2:
km = [/(kc / 2)\]
; ex p being Element of (FTSL1 n) st f . p in U_FT p,km
assume A3:
for p being Element of (FTSL1 n) holds not f . p in U_FT p,km
; contradiction
defpred S1[ Nat] means ( $1 > 0 & ( for j being Nat st $1 <= n & j = f . $1 holds
$1 > j ) );
A4:
n >= 0 + 1
by NAT_1:13;
A5:
RelStr(# (Seg n),(Nbdl1 n) #) = FTSL1 n
by FINTOPO4:def 4;
A6:
FTSL1 n is filled
by FINTOPO4:18;
now A7:
n in the
carrier of
(FTSL1 n)
by A4, A5;
then reconsider p2 =
n as
Element of
(FTSL1 n) ;
given j being
Nat such that A8:
j = f . n
and A9:
n <= j
;
contradiction
f . n in the
carrier of
(FTSL1 n)
by A7, FUNCT_2:7;
then
j <= n
by A5, A8, FINSEQ_1:3;
then A10:
n = j
by A9, XXREAL_0:1;
p2 in U_FT p2
by A6, FIN_TOPO:def 4;
then A11:
p2 in U_FT p2,
0
by FINTOPO3:47;
U_FT p2,
0 c= U_FT p2,
km
by Th8, FINTOPO4:18;
hence
contradiction
by A3, A8, A10, A11;
verum end;
then A12:
for j being Nat st n <= n & j = f . n holds
n > j
;
then A13:
ex k being Nat st S1[k]
;
ex k being Nat st
( S1[k] & ( for m being Nat st S1[m] holds
k <= m ) )
from NAT_1:sch 5(A13);
then consider k being Nat such that
A14:
S1[k]
and
A15:
for m being Nat st S1[m] holds
k <= m
;
A16:
0 + 1 <= k
by A14, NAT_1:13;
then A17:
k - 1 >= 0
by XREAL_1:50;
then A18:
k - 1 = k -' 1
by XREAL_0:def 2;
k < k + 1
by NAT_1:13;
then A19:
k - 1 < (k + 1) - 1
by XREAL_1:11;
A20:
k <= n
by A12, A15;
then reconsider pk = k as Element of (FTSL1 n) by A5, A16, FINSEQ_1:3;
per cases
( k -' 1 <= 0 or ( k -' 1 > 0 & ex j being Nat st
( k -' 1 <= n & j = f . (k -' 1) & k -' 1 <= j ) ) )
by A15, A18, A19;
suppose A23:
(
k -' 1
> 0 & ex
j being
Nat st
(
k -' 1
<= n &
j = f . (k -' 1) &
k -' 1
<= j ) )
;
contradiction
k in NAT
by ORDINAL1:def 13;
then A24:
k in the
carrier of
(FTSL1 n)
by A5, A20, A16;
then
f . k in Seg n
by A5, FUNCT_2:7;
then reconsider jn =
f . k as
Element of
NAT ;
A25:
not
jn in U_FT pk,
km
by A3;
A26:
jn < k
by A14, A20;
then A27:
k - jn > 0
by XREAL_1:52;
jn in Seg n
by A5, A24, FUNCT_2:7;
then
not
abs (k - jn) <= km + 1
by A25, Th9;
then A28:
k - jn > km + 1
by A27, ABSVALUE:def 1;
k - jn = k -' jn
by A27, XREAL_0:def 2;
then A29:
k - jn >= (km + 1) + 1
by A28, NAT_1:13;
reconsider pfk =
jn as
Element of
(FTSL1 n) by A24, FUNCT_2:7;
A30:
kc < kc + 2
by XREAL_1:31;
A31:
k -' 1
>= 0 + 1
by A23, NAT_1:13;
then A32:
k -' 1
= max (k -' 1),1
by XXREAL_0:def 10;
Im (Nbdl1 n),
k = {k,(max (k -' 1),1),(min (k + 1),n)}
by A5, A24, FINTOPO4:def 3;
then
k -' 1
in U_FT pk
by A5, A32, ENUMSET1:def 1;
then A33:
k -' 1
in U_FT pk,
0
by FINTOPO3:47;
consider j being
Nat such that A34:
k -' 1
<= n
and A35:
j = f . (k -' 1)
and A36:
k -' 1
<= j
by A23;
reconsider pkm =
k -' 1 as
Element of
(FTSL1 n) by A5, A34, A31, FINSEQ_1:3;
A37:
not
j in U_FT pkm,
km
by A3, A35;
A38:
k -' 1
in the
carrier of
(FTSL1 n)
by A5, A34, A31;
then
k -' 1
in dom f
by FUNCT_2:def 1;
then A39:
f . (k -' 1) in f .: (U_FT pk,0 )
by A33, FUNCT_1:def 12;
then
k -' 1
< j
by A36, XXREAL_0:1;
then A42:
(k -' 1) + 1
<= j
by NAT_1:13;
then
j - k >= 0
by A18, XREAL_1:50;
then A43:
j - k = j -' k
by XREAL_0:def 2;
j in the
carrier of
(FTSL1 n)
by A35, A38, FUNCT_2:7;
then
not
abs ((k -' 1) - j) <= km + 1
by A5, A37, Th9;
then
abs (j - (k -' 1)) > km + 1
by UNIFORM1:13;
then
(j -' k) + 1
> km + 1
by A18, A43, ABSVALUE:def 1;
then
(j - k) + 1
>= (km + 1) + 1
by A43, NAT_1:13;
then
(k - jn) + ((j - k) + 1) >= ((km + 1) + 1) + ((km + 1) + 1)
by A29, XREAL_1:9;
then
(j - jn) + 1
>= (((km + 1) + 1) + (km + 1)) + 1
;
then
j - jn >= ((km + 1) + 1) + (km + 1)
by XREAL_1:8;
then
(j - jn) - 1
>= ((((km + 1) + 1) + km) + 1) - 1
by XREAL_1:11;
then A44:
((j - jn) - 1) / 2
>= ((2 * km) + 2) / 2
by XREAL_1:74;
[/(kc / 2)\] >= kc / 2
by INT_1:def 5;
then
[/(kc / 2)\] + (2 / 2) >= (kc / 2) + (2 / 2)
by XREAL_1:9;
then
((j - jn) - 1) / 2
>= (kc / 2) + (2 / 2)
by A2, A44, XXREAL_0:2;
then
(((j - jn) - 1) / 2) * 2
>= ((kc / 2) + (2 / 2)) * 2
by XREAL_1:66;
then
(j - jn) - 1
> kc
by A30, XXREAL_0:2;
then A45:
((j - jn) - 1) + 1
> kc + 1
by XREAL_1:8;
jn < j
by A18, A42, A26, XXREAL_0:2;
then
j - jn >= 0
by XREAL_1:50;
then A46:
abs (j - jn) = j - jn
by ABSVALUE:def 1;
(
f .: (U_FT pk,0 ) c= U_FT pfk,
kc &
abs (jn - j) = abs (j - jn) )
by A1, FINTOPO4:def 2, UNIFORM1:13;
hence
contradiction
by A35, A39, A46, A45, Th9;
verum end;