let n be Nat; for A being affinely-independent Subset of (TOP-REAL n) st card A = n + 1 holds
for f being continuous Function of ((TOP-REAL n) | (conv A)),((TOP-REAL n) | (conv A)) ex p being Point of (TOP-REAL n) st
( p in dom f & f . p = p )
set TRn = TOP-REAL n;
let A be affinely-independent Subset of (TOP-REAL n); ( card A = n + 1 implies for f being continuous Function of ((TOP-REAL n) | (conv A)),((TOP-REAL n) | (conv A)) ex p being Point of (TOP-REAL n) st
( p in dom f & f . p = p ) )
assume A1:
card A = n + 1
; for f being continuous Function of ((TOP-REAL n) | (conv A)),((TOP-REAL n) | (conv A)) ex p being Point of (TOP-REAL n) st
( p in dom f & f . p = p )
A2:
not A is empty
by A1;
set cA = conv A;
let f be continuous Function of ((TOP-REAL n) | (conv A)),((TOP-REAL n) | (conv A)); ex p being Point of (TOP-REAL n) st
( p in dom f & f . p = p )
reconsider cA = conv A as non empty Subset of (TOP-REAL n) by A2;
set T = (TOP-REAL n) | cA;
reconsider ff = f as continuous Function of ((TOP-REAL n) | cA),((TOP-REAL n) | cA) ;
set E = the Enumeration of A;
deffunc H1( object ) -> set = { v where v is Element of ((TOP-REAL n) | cA) : (|-- (A,( the Enumeration of A . $1))) . (f . v) <= (|-- (A,( the Enumeration of A . $1))) . v } ;
consider F being FinSequence such that
A3:
( len F = card A & ( for k being Nat st k in dom F holds
F . k = H1(k) ) )
from FINSEQ_1:sch 2();
rng F c= bool the carrier of ((TOP-REAL n) | cA)
then reconsider F = F as FinSequence of bool the carrier of ((TOP-REAL n) | cA) by FINSEQ_1:def 4;
A7:
[#] ((TOP-REAL n) | cA) = cA
by PRE_TOPC:def 5;
A8:
dom f = the carrier of ((TOP-REAL n) | cA)
by FUNCT_2:def 1;
now for W being Subset of ((TOP-REAL n) | cA) st W in rng F holds
W is closed let W be
Subset of
((TOP-REAL n) | cA);
( W in rng F implies W is closed )reconsider Z =
0 as
Real ;
reconsider L =
].-infty,Z.] as
Subset of
R^1 by TOPMETR:17;
assume
W in rng F
;
W is closed then consider i being
object such that A9:
i in dom F
and A10:
F . i = W
by FUNCT_1:def 3;
reconsider AEi =
|-- (
A,
( the Enumeration of A . i)) as
continuous Function of
(TOP-REAL n),
R^1 by A1, RLAFFIN3:32;
set AT =
AEi | ((TOP-REAL n) | cA);
set Af =
(AEi | ((TOP-REAL n) | cA)) * ff;
set AfT =
((AEi | ((TOP-REAL n) | cA)) * ff) - (AEi | ((TOP-REAL n) | cA));
A11:
dom (((AEi | ((TOP-REAL n) | cA)) * ff) - (AEi | ((TOP-REAL n) | cA))) = the
carrier of
((TOP-REAL n) | cA)
by FUNCT_2:def 1;
reconsider AfT =
((AEi | ((TOP-REAL n) | cA)) * ff) - (AEi | ((TOP-REAL n) | cA)) as
Function of
((TOP-REAL n) | cA),
R^1 by TOPMETR:17;
A12:
dom (AEi | ((TOP-REAL n) | cA)) = the
carrier of
((TOP-REAL n) | cA)
by FUNCT_2:def 1;
A13:
AEi | ((TOP-REAL n) | cA) = AEi | the
carrier of
((TOP-REAL n) | cA)
by A7, TMAP_1:def 3;
A14:
dom ((AEi | ((TOP-REAL n) | cA)) * ff) = the
carrier of
((TOP-REAL n) | cA)
by FUNCT_2:def 1;
A15:
AfT " L c= H1(
i)
proof
let x be
object ;
TARSKI:def 3 ( not x in AfT " L or x in H1(i) )
reconsider xx =
x as
set by TARSKI:1;
assume A16:
x in AfT " L
;
x in H1(i)
then reconsider v =
x as
Point of
((TOP-REAL n) | cA) ;
x in dom AfT
by A16, FUNCT_1:def 7;
then A17:
AfT . x = (((AEi | ((TOP-REAL n) | cA)) * ff) . xx) - ((AEi | ((TOP-REAL n) | cA)) . xx)
by VALUED_1:13;
(
AfT . x in L &
((AEi | ((TOP-REAL n) | cA)) * ff) . x = (AEi | ((TOP-REAL n) | cA)) . (f . x) )
by A14, A16, FUNCT_1:12, FUNCT_1:def 7;
then
((AEi | ((TOP-REAL n) | cA)) . (f . xx)) - ((AEi | ((TOP-REAL n) | cA)) . xx) <= 0
by A17, XXREAL_1:2;
then A18:
(AEi | ((TOP-REAL n) | cA)) . (f . x) <= (AEi | ((TOP-REAL n) | cA)) . xx
by XREAL_1:50;
f . x in dom (AEi | ((TOP-REAL n) | cA))
by A14, A16, FUNCT_1:11;
then A19:
(AEi | ((TOP-REAL n) | cA)) . (f . x) = AEi . (f . v)
by A13, FUNCT_1:47;
(AEi | ((TOP-REAL n) | cA)) . x = AEi . v
by A12, A13, FUNCT_1:47;
hence
x in H1(
i)
by A18, A19;
verum
end; A20:
H1(
i)
c= AfT " L
proof
let x be
object ;
TARSKI:def 3 ( not x in H1(i) or x in AfT " L )
assume
x in H1(
i)
;
x in AfT " L
then consider v being
Element of
((TOP-REAL n) | cA) such that A21:
x = v
and A22:
AEi . (f . v) <= AEi . v
;
f . v in rng f
by A8, FUNCT_1:def 3;
then A23:
AEi . (f . v) = (AEi | ((TOP-REAL n) | cA)) . (f . v)
by A12, A13, FUNCT_1:47;
AEi . v = (AEi | ((TOP-REAL n) | cA)) . v
by A12, A13, FUNCT_1:47;
then
((AEi | ((TOP-REAL n) | cA)) * ff) . v <= (AEi | ((TOP-REAL n) | cA)) . v
by A14, A22, A23, FUNCT_1:12;
then
(((AEi | ((TOP-REAL n) | cA)) * ff) . v) - ((AEi | ((TOP-REAL n) | cA)) . v) <= 0
by XREAL_1:47;
then
AfT . v <= 0
by A11, VALUED_1:13;
then
AfT . v in L
by XXREAL_1:234;
hence
x in AfT " L
by A11, A21, FUNCT_1:def 7;
verum
end;
L is
closed
by BORSUK_5:41;
then A24:
AfT " L is
closed
by PRE_TOPC:def 6;
F . i = H1(
i)
by A3, A9;
hence
W is
closed
by A10, A15, A20, A24, XBOOLE_0:def 10;
verum end;
then A25:
rng F is closed
by TOPS_2:def 2;
A26:
dom the Enumeration of A = Seg (len the Enumeration of A)
by FINSEQ_1:def 3;
A27:
conv A c= Affin A
by RLAFFIN1:65;
A28:
rng the Enumeration of A = A
by RLAFFIN3:def 1;
then
len the Enumeration of A = card A
by FINSEQ_4:62;
then A29:
dom F = dom the Enumeration of A
by A3, FINSEQ_3:29;
for S being Subset of (dom F) holds conv ( the Enumeration of A .: S) c= union (F .: S)
proof
let S be
Subset of
(dom F);
conv ( the Enumeration of A .: S) c= union (F .: S)
set ES = the
Enumeration of
A .: S;
per cases
( S is empty or not S is empty )
;
suppose A30:
not
S is
empty
;
conv ( the Enumeration of A .: S) c= union (F .: S)let x be
object ;
TARSKI:def 3 ( not x in conv ( the Enumeration of A .: S) or x in union (F .: S) )set fx =
f . x;
set xES =
x |-- ( the Enumeration of A .: S);
set fxA =
(f . x) |-- A;
set xA =
x |-- A;
assume A31:
x in conv ( the Enumeration of A .: S)
;
x in union (F .: S)A32:
conv ( the Enumeration of A .: S) c= conv A
by A28, RELAT_1:111, RLAFFIN1:3;
then reconsider v =
x as
Point of
((TOP-REAL n) | cA) by A7, A31;
A33:
len (((f . x) |-- A) * the Enumeration of A) = len the
Enumeration of
A
by FINSEQ_2:33;
A34:
len the
Enumeration of
A = len ((x |-- ( the Enumeration of A .: S)) * the Enumeration of A)
by FINSEQ_2:33;
then reconsider fxAE =
((f . x) |-- A) * the
Enumeration of
A,
xESE =
(x |-- ( the Enumeration of A .: S)) * the
Enumeration of
A as
Element of
(len the Enumeration of A) -tuples_on REAL by A33, FINSEQ_2:92;
A35:
dom fxAE = Seg (len the Enumeration of A)
by A33, FINSEQ_1:def 3;
A36:
conv ( the Enumeration of A .: S) c= Affin ( the Enumeration of A .: S)
by RLAFFIN1:65;
then A37:
x |-- A = x |-- ( the Enumeration of A .: S)
by A28, A31, RELAT_1:111, RLAFFIN1:77;
A38:
the
Enumeration of
A .: S c= A
by A28, RELAT_1:111;
A39:
Carrier (x |-- ( the Enumeration of A .: S)) c= the
Enumeration of
A .: S
by RLVECT_2:def 6;
the
Enumeration of
A .: S is
affinely-independent
by A28, RELAT_1:111, RLAFFIN1:43;
then
(
sum (x |-- ( the Enumeration of A .: S)) = 1 &
Carrier (x |-- ( the Enumeration of A .: S)) c= A )
by A31, A36, A38, A39, RLAFFIN1:def 7;
then A40:
(
Carrier ((f . x) |-- A) c= A & 1
= Sum ((x |-- ( the Enumeration of A .: S)) * the Enumeration of A) )
by A28, RLAFFIN1:30, RLVECT_2:def 6;
A41:
f . x in rng f
by A7, A8, A31, A32, FUNCT_1:def 3;
then A42:
f . x in conv A
by A7;
then
sum ((f . x) |-- A) = 1
by A27, RLAFFIN1:def 7;
then A43:
Sum fxAE = Sum xESE
by A28, A40, RLAFFIN1:30;
A44:
dom xESE = Seg (len the Enumeration of A)
by A34, FINSEQ_1:def 3;
per cases
( ex j being Nat st
( j in Seg (len the Enumeration of A) & fxAE . j < xESE . j ) or for j being Nat st j in Seg (len the Enumeration of A) holds
fxAE . j <= xESE . j )
by A43, RVSUM_1:83;
suppose
ex
j being
Nat st
(
j in Seg (len the Enumeration of A) &
fxAE . j < xESE . j )
;
x in union (F .: S)then consider j being
Nat such that A45:
j in Seg (len the Enumeration of A)
and A46:
fxAE . j < xESE . j
;
A47:
fxAE . j = ((f . x) |-- A) . ( the Enumeration of A . j)
by A35, A45, FUNCT_1:12;
A48:
xESE . j = (x |-- ( the Enumeration of A .: S)) . ( the Enumeration of A . j)
by A44, A45, FUNCT_1:12;
then
xESE . j = (|-- (A,( the Enumeration of A . j))) . x
by A31, A37, RLAFFIN3:def 3;
then A49:
(|-- (A,( the Enumeration of A . j))) . (f . v) <= (|-- (A,( the Enumeration of A . j))) . v
by A42, A46, A47, RLAFFIN3:def 3;
A50:
the
Enumeration of
A . j in dom ((f . x) |-- A)
by A35, A45, FUNCT_1:11;
then
0 < (x |-- ( the Enumeration of A .: S)) . ( the Enumeration of A . j)
by A7, A41, A46, A47, A48, RLAFFIN1:71;
then
the
Enumeration of
A . j in Carrier (x |-- ( the Enumeration of A .: S))
by A50, RLVECT_2:19;
then consider i being
object such that A51:
i in dom the
Enumeration of
A
and A52:
i in S
and A53:
the
Enumeration of
A . i = the
Enumeration of
A . j
by A39, FUNCT_1:def 6;
i = j
by A26, A45, A51, A53, FUNCT_1:def 4;
then A54:
F . j in F .: S
by A52, FUNCT_1:def 6;
H1(
j)
= F . j
by A3, A26, A29, A45;
then
x in F . j
by A49;
hence
x in union (F .: S)
by A54, TARSKI:def 4;
verum end; suppose A55:
for
j being
Nat st
j in Seg (len the Enumeration of A) holds
fxAE . j <= xESE . j
;
x in union (F .: S)consider j being
object such that A56:
j in S
by A30, XBOOLE_0:def 1;
reconsider j =
j as
Nat by A56;
A57:
fxAE . j <= xESE . j
by A26, A29, A55, A56;
A58:
H1(
j)
= F . j
by A3, A56;
xESE . j = (x |-- ( the Enumeration of A .: S)) . ( the Enumeration of A . j)
by A26, A29, A44, A56, FUNCT_1:12;
then A59:
xESE . j = (|-- (A,( the Enumeration of A . j))) . x
by A31, A37, RLAFFIN3:def 3;
fxAE . j = ((f . x) |-- A) . ( the Enumeration of A . j)
by A26, A29, A35, A56, FUNCT_1:12;
then
(|-- (A,( the Enumeration of A . j))) . (f . v) <= (|-- (A,( the Enumeration of A . j))) . v
by A42, A59, A57, RLAFFIN3:def 3;
then A60:
x in F . j
by A58;
F . j in F .: S
by A56, FUNCT_1:def 6;
hence
x in union (F .: S)
by A60, TARSKI:def 4;
verum end; end;
end;
then
not meet (rng F) is empty
by A2, A3, A25, Th22;
then consider v being object such that
A61:
v in meet (rng F)
by XBOOLE_0:def 1;
A62:
v in cA
by A7, A61;
then reconsider v = v as Element of (TOP-REAL n) ;
set fv = f . v;
set vA = v |-- A;
set fvA = (f . v) |-- A;
A63:
len (((f . v) |-- A) * the Enumeration of A) = len the Enumeration of A
by FINSEQ_2:33;
f . v in rng f
by A8, A61, FUNCT_1:def 3;
then A64:
f . v in cA
by A7;
then
( Carrier ((f . v) |-- A) c= A & sum ((f . v) |-- A) = 1 )
by A27, RLAFFIN1:def 7, RLVECT_2:def 6;
then A65:
( Carrier (v |-- A) c= A & 1 = Sum (((f . v) |-- A) * the Enumeration of A) )
by A28, RLAFFIN1:30, RLVECT_2:def 6;
A66:
len the Enumeration of A = len ((v |-- A) * the Enumeration of A)
by FINSEQ_2:33;
then reconsider fvAE = ((f . v) |-- A) * the Enumeration of A, vAE = (v |-- A) * the Enumeration of A as Element of (len the Enumeration of A) -tuples_on REAL by A63, FINSEQ_2:92;
A67:
dom fvAE = Seg (len the Enumeration of A)
by A63, FINSEQ_1:def 3;
A68:
dom vAE = Seg (len the Enumeration of A)
by A66, FINSEQ_1:def 3;
A69:
for j being Nat st j in Seg (len the Enumeration of A) holds
fvAE . j <= vAE . j
proof
let j be
Nat;
( j in Seg (len the Enumeration of A) implies fvAE . j <= vAE . j )
assume A70:
j in Seg (len the Enumeration of A)
;
fvAE . j <= vAE . j
then
(
F . j = H1(
j) &
F . j in rng F )
by A3, A26, A29, FUNCT_1:def 3;
then
v in H1(
j)
by A61, SETFAM_1:def 1;
then A71:
ex
w being
Element of
((TOP-REAL n) | cA) st
(
w = v &
(|-- (A,( the Enumeration of A . j))) . (f . w) <= (|-- (A,( the Enumeration of A . j))) . w )
;
A72:
(|-- (A,( the Enumeration of A . j))) . v =
(v |-- A) . ( the Enumeration of A . j)
by RLAFFIN3:def 3
.=
vAE . j
by A68, A70, FUNCT_1:12
;
(|-- (A,( the Enumeration of A . j))) . (f . v) =
((f . v) |-- A) . ( the Enumeration of A . j)
by A64, RLAFFIN3:def 3
.=
fvAE . j
by A67, A70, FUNCT_1:12
;
hence
fvAE . j <= vAE . j
by A71, A72;
verum
end;
A73:
Carrier (v |-- A) c= A
by RLVECT_2:def 6;
sum (v |-- A) = 1
by A27, A62, RLAFFIN1:def 7;
then A74:
Sum fvAE = Sum vAE
by A28, A65, RLAFFIN1:30;
A75:
Carrier ((f . v) |-- A) c= A
by RLVECT_2:def 6;
A82:
Sum (v |-- A) = v
by A27, A62, RLAFFIN1:def 7;
Sum ((f . v) |-- A) = f . v
by A27, A64, RLAFFIN1:def 7;
then
v = f . v
by A76, A82, RLVECT_2:def 9;
hence
ex p being Point of (TOP-REAL n) st
( p in dom f & f . p = p )
by A8, A61; verum