let n be Nat; :: thesis: 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); :: thesis: ( 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 ; :: thesis: 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)); :: thesis: 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)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng F or y in bool the carrier of ((TOP-REAL n) | cA) )
assume y in rng F ; :: thesis: y in bool the carrier of ((TOP-REAL n) | cA)
then consider x being object such that
A4: x in dom F and
A5: F . x = y by FUNCT_1:def 3;
A6: H1(x) c= the carrier of ((TOP-REAL n) | cA)
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in H1(x) or z in the carrier of ((TOP-REAL n) | cA) )
assume z in H1(x) ; :: thesis: z in the carrier of ((TOP-REAL n) | cA)
then ex v being Element of ((TOP-REAL n) | cA) st
( z = v & (|-- (A,( the Enumeration of A . x))) . (f . v) <= (|-- (A,( the Enumeration of A . x))) . v ) ;
hence z in the carrier of ((TOP-REAL n) | cA) ; :: thesis: verum
end;
F . x = H1(x) by A3, A4;
hence y in bool the carrier of ((TOP-REAL n) | cA) by A5, A6; :: thesis: verum
end;
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 :: thesis: 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); :: thesis: ( 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 ; :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( not x in AfT " L or x in H1(i) )
reconsider xx = x as set by TARSKI:1;
assume A16: x in AfT " L ; :: thesis: 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; :: thesis: verum
end;
A20: H1(i) c= AfT " L
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H1(i) or x in AfT " L )
assume x in H1(i) ; :: thesis: 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; :: thesis: 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; :: thesis: 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); :: thesis: 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 S is empty ; :: thesis: conv ( the Enumeration of A .: S) c= union (F .: S)
then conv ( the Enumeration of A .: S) is empty ;
hence conv ( the Enumeration of A .: S) c= union (F .: S) ; :: thesis: verum
end;
suppose A30: not S is empty ; :: thesis: conv ( the Enumeration of A .: S) c= union (F .: S)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( 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) ; :: thesis: 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 ) ; :: thesis: 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; :: thesis: verum
end;
suppose A55: for j being Nat st j in Seg (len the Enumeration of A) holds
fxAE . j <= xESE . j ; :: thesis: 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; :: thesis: verum
end;
end;
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; :: thesis: ( j in Seg (len the Enumeration of A) implies fvAE . j <= vAE . j )
assume A70: j in Seg (len the Enumeration of A) ; :: thesis: 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; :: thesis: 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;
A76: now :: thesis: for w being Element of (TOP-REAL n) holds (v |-- A) . w = ((f . v) |-- A) . w
let w be Element of (TOP-REAL n); :: thesis: (v |-- A) . b1 = ((f . v) |-- A) . b1
per cases ( w in A or not w in A ) ;
suppose w in A ; :: thesis: (v |-- A) . b1 = ((f . v) |-- A) . b1
then consider j being object such that
A77: j in dom the Enumeration of A and
A78: the Enumeration of A . j = w by A28, FUNCT_1:def 3;
A79: ( fvAE . j = ((f . v) |-- A) . w & vAE . j = (v |-- A) . w ) by A77, A78, FUNCT_1:13;
( fvAE . j <= vAE . j & fvAE . j >= vAE . j ) by A26, A74, A69, A77, RVSUM_1:83;
hence (v |-- A) . w = ((f . v) |-- A) . w by A79, XXREAL_0:1; :: thesis: verum
end;
suppose A80: not w in A ; :: thesis: (v |-- A) . b1 = ((f . v) |-- A) . b1
then not w in Carrier (v |-- A) by A73;
then A81: (v |-- A) . w = 0 by RLVECT_2:19;
not w in Carrier ((f . v) |-- A) by A75, A80;
hence (v |-- A) . w = ((f . v) |-- A) . w by A81, RLVECT_2:19; :: thesis: verum
end;
end;
end;
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; :: thesis: verum