let n be Nat; :: thesis: for A being affinely-independent Subset of (TOP-REAL n) st card A = n + 1 holds

conv A is closed

set L = [.0,1.];

set TRn = TOP-REAL n;

let A be affinely-independent Subset of (TOP-REAL n); :: thesis: ( card A = n + 1 implies conv A is closed )

assume A1: card A = n + 1 ; :: thesis: conv A is closed

reconsider L = [.0,1.] as Subset of R^1 by TOPMETR:17;

set E = the Enumeration of A;

deffunc H_{1}( object ) -> Element of bool the carrier of (TOP-REAL n) = (|-- (A,( the Enumeration of A . $1))) " L;

consider f being FinSequence such that

A2: len f = n + 1 and

A3: for k being Nat st k in dom f holds

f . k = H_{1}(k)
from FINSEQ_1:sch 2();

A4: dom f = Seg (len f) by FINSEQ_1:def 3;

then A5: not rng f is empty by A2, RELAT_1:42;

rng f c= bool the carrier of (TOP-REAL n)

A8: rng the Enumeration of A = A by Def1;

then A9: len the Enumeration of A = card A by FINSEQ_4:62;

A10: meet (rng f) c= conv A

A19: conv A c= meet (rng f)

then meet (rng f) is closed by TOPS_2:22;

hence conv A is closed by A19, A10, XBOOLE_0:def 10; :: thesis: verum

conv A is closed

set L = [.0,1.];

set TRn = TOP-REAL n;

let A be affinely-independent Subset of (TOP-REAL n); :: thesis: ( card A = n + 1 implies conv A is closed )

assume A1: card A = n + 1 ; :: thesis: conv A is closed

reconsider L = [.0,1.] as Subset of R^1 by TOPMETR:17;

set E = the Enumeration of A;

deffunc H

consider f being FinSequence such that

A2: len f = n + 1 and

A3: for k being Nat st k in dom f holds

f . k = H

A4: dom f = Seg (len f) by FINSEQ_1:def 3;

then A5: not rng f is empty by A2, RELAT_1:42;

rng f c= bool the carrier of (TOP-REAL n)

proof

then reconsider f = f as FinSequence of bool the carrier of (TOP-REAL n) by FINSEQ_1:def 4;
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) )

assume y in rng f ; :: thesis: y in bool the carrier of (TOP-REAL n)

then consider x being object such that

A6: x in dom f and

A7: f . x = y by FUNCT_1:def 3;

f . x = H_{1}(x)
by A3, A6;

hence y in bool the carrier of (TOP-REAL n) by A7; :: thesis: verum

end;assume y in rng f ; :: thesis: y in bool the carrier of (TOP-REAL n)

then consider x being object such that

A6: x in dom f and

A7: f . x = y by FUNCT_1:def 3;

f . x = H

hence y in bool the carrier of (TOP-REAL n) by A7; :: thesis: verum

A8: rng the Enumeration of A = A by Def1;

then A9: len the Enumeration of A = card A by FINSEQ_4:62;

A10: meet (rng f) c= conv A

proof

A18:
dom the Enumeration of A = Seg (len the Enumeration of A)
by FINSEQ_1:def 3;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in meet (rng f) or x in conv A )

assume A11: x in meet (rng f) ; :: thesis: x in conv A

then [#] (TOP-REAL n) = Affin A by A1, Th6;

hence x in conv A by A11, A12, RLAFFIN1:73; :: thesis: verum

end;assume A11: x in meet (rng f) ; :: thesis: x in conv A

A12: now :: thesis: for v being Element of (TOP-REAL n) st v in A holds

(x |-- A) . v >= 0

dim (TOP-REAL n) = n
by Th4;(x |-- A) . v >= 0

let v be Element of (TOP-REAL n); :: thesis: ( v in A implies (x |-- A) . v >= 0 )

assume v in A ; :: thesis: (x |-- A) . v >= 0

then consider k being object such that

A13: k in dom the Enumeration of A and

A14: the Enumeration of A . k = v by A8, FUNCT_1:def 3;

A15: k in dom f by A1, A2, A9, A4, A13, FINSEQ_1:def 3;

then f . k in rng f by FUNCT_1:def 3;

then A16: meet (rng f) c= f . k by SETFAM_1:3;

A17: (x |-- A) . v = (|-- (A,v)) . x by A11, Def3;

f . k = (|-- (A,v)) " L by A3, A14, A15;

then (x |-- A) . v in L by A11, A17, A16, FUNCT_1:def 7;

hence (x |-- A) . v >= 0 by XXREAL_1:1; :: thesis: verum

end;assume v in A ; :: thesis: (x |-- A) . v >= 0

then consider k being object such that

A13: k in dom the Enumeration of A and

A14: the Enumeration of A . k = v by A8, FUNCT_1:def 3;

A15: k in dom f by A1, A2, A9, A4, A13, FINSEQ_1:def 3;

then f . k in rng f by FUNCT_1:def 3;

then A16: meet (rng f) c= f . k by SETFAM_1:3;

A17: (x |-- A) . v = (|-- (A,v)) . x by A11, Def3;

f . k = (|-- (A,v)) " L by A3, A14, A15;

then (x |-- A) . v in L by A11, A17, A16, FUNCT_1:def 7;

hence (x |-- A) . v >= 0 by XXREAL_1:1; :: thesis: verum

then [#] (TOP-REAL n) = Affin A by A1, Th6;

hence x in conv A by A11, A12, RLAFFIN1:73; :: thesis: verum

A19: conv A c= meet (rng f)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in conv A or x in meet (rng f) )

assume A20: x in conv A ; :: thesis: x in meet (rng f)

end;assume A20: x in conv A ; :: thesis: x in meet (rng f)

now :: thesis: for Y being set st Y in rng f holds

x in Y

hence
x in meet (rng f)
by A5, SETFAM_1:def 1; :: thesis: verumx in Y

let Y be set ; :: thesis: ( Y in rng f implies x in Y )

assume Y in rng f ; :: thesis: x in Y

then consider k being object such that

A21: k in dom f and

A22: f . k = Y by FUNCT_1:def 3;

the Enumeration of A . k in A by A1, A2, A8, A9, A4, A18, A21, FUNCT_1:def 3;

then reconsider Ek = the Enumeration of A . k as Element of (TOP-REAL n) ;

A23: dom (|-- (A,Ek)) = [#] (TOP-REAL n) by FUNCT_2:def 1;

A24: ( 0 <= (x |-- A) . Ek & (x |-- A) . Ek <= 1 ) by A20, RLAFFIN1:71;

(x |-- A) . Ek = (|-- (A,Ek)) . x by A20, Def3;

then A25: (|-- (A,Ek)) . x in L by A24, XXREAL_1:1;

Y = (|-- (A,( the Enumeration of A . k))) " L by A3, A21, A22;

hence x in Y by A20, A25, A23, FUNCT_1:def 7; :: thesis: verum

end;assume Y in rng f ; :: thesis: x in Y

then consider k being object such that

A21: k in dom f and

A22: f . k = Y by FUNCT_1:def 3;

the Enumeration of A . k in A by A1, A2, A8, A9, A4, A18, A21, FUNCT_1:def 3;

then reconsider Ek = the Enumeration of A . k as Element of (TOP-REAL n) ;

A23: dom (|-- (A,Ek)) = [#] (TOP-REAL n) by FUNCT_2:def 1;

A24: ( 0 <= (x |-- A) . Ek & (x |-- A) . Ek <= 1 ) by A20, RLAFFIN1:71;

(x |-- A) . Ek = (|-- (A,Ek)) . x by A20, Def3;

then A25: (|-- (A,Ek)) . x in L by A24, XXREAL_1:1;

Y = (|-- (A,( the Enumeration of A . k))) " L by A3, A21, A22;

hence x in Y by A20, A25, A23, FUNCT_1:def 7; :: thesis: verum

now :: thesis: for B being Subset of (TOP-REAL n) st B in rng f holds

B is closed

then
rng f is closed
by TOPS_2:def 2;B is closed

let B be Subset of (TOP-REAL n); :: thesis: ( B in rng f implies B is closed )

assume B in rng f ; :: thesis: B is closed

then consider k being object such that

A26: ( k in dom f & f . k = B ) by FUNCT_1:def 3;

( |-- (A,( the Enumeration of A . k)) is continuous & L is closed ) by A1, Th32, TREAL_1:1;

then (|-- (A,( the Enumeration of A . k))) " L is closed by PRE_TOPC:def 6;

hence B is closed by A3, A26; :: thesis: verum

end;assume B in rng f ; :: thesis: B is closed

then consider k being object such that

A26: ( k in dom f & f . k = B ) by FUNCT_1:def 3;

( |-- (A,( the Enumeration of A . k)) is continuous & L is closed ) by A1, Th32, TREAL_1:1;

then (|-- (A,( the Enumeration of A . k))) " L is closed by PRE_TOPC:def 6;

hence B is closed by A3, A26; :: thesis: verum

then meet (rng f) is closed by TOPS_2:22;

hence conv A is closed by A19, A10, XBOOLE_0:def 10; :: thesis: verum