let kc, km be Nat; for n being non zero 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 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 for j being Nat holds
( not j = f . n or not n <= j )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:5;
then
j <= n
by A5, A8, FINSEQ_1:1;
then A10:
n = j
by A9, XXREAL_0:1;
p2 in U_FT p2
by A6;
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:48;
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:9;
A20:
k <= n
by A12, A15;
then reconsider pk = k as Element of (FTSL1 n) by A5, A16, FINSEQ_1:1;
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 ) )
;
contradictionA24:
k in the
carrier of
(FTSL1 n)
by A5, A20, A16;
then
f . k in Seg n
by A5, FUNCT_2:5;
then reconsider jn =
f . k as
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:50;
jn in Seg n
by A5, A24, FUNCT_2:5;
then
not
|.(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:5;
A30:
kc < kc + 2
by XREAL_1:29;
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:1;
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 6;
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:48;
then A43:
j - k = j -' k
by XREAL_0:def 2;
j in the
carrier of
(FTSL1 n)
by A35, A38, FUNCT_2:5;
then
not
|.((k -' 1) - j).| <= km + 1
by A5, A37, Th9;
then
|.(j - (k -' 1)).| > km + 1
by UNIFORM1:11;
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:7;
then
(j - jn) + 1
>= (((km + 1) + 1) + (km + 1)) + 1
;
then
j - jn >= ((km + 1) + 1) + (km + 1)
by XREAL_1:6;
then
(j - jn) - 1
>= ((((km + 1) + 1) + km) + 1) - 1
by XREAL_1:9;
then A44:
((j - jn) - 1) / 2
>= ((2 * km) + 2) / 2
by XREAL_1:72;
[/(kc / 2)\] >= kc / 2
by INT_1:def 7;
then
[/(kc / 2)\] + (2 / 2) >= (kc / 2) + (2 / 2)
by XREAL_1:7;
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:64;
then
(j - jn) - 1
> kc
by A30, XXREAL_0:2;
then A45:
((j - jn) - 1) + 1
> kc + 1
by XREAL_1:6;
jn < j
by A18, A42, A26, XXREAL_0:2;
then
j - jn >= 0
by XREAL_1:48;
then A46:
|.(j - jn).| = j - jn
by ABSVALUE:def 1;
(
f .: (U_FT (pk,0)) c= U_FT (
pfk,
kc) &
|.(jn - j).| = |.(j - jn).| )
by A1, FINTOPO4:def 2, UNIFORM1:11;
hence
contradiction
by A35, A39, A46, A45, Th9;
verum end;