let n be Nat; :: thesis: for Affn being affinely-independent Subset of () st card Affn = n + 1 holds
Int Affn is open

let Affn be affinely-independent Subset of (); :: thesis: ( card Affn = n + 1 implies Int Affn is open )
set L = ].0,1.[;
set TRn = TOP-REAL n;
set A = Affn;
assume A1: card Affn = n + 1 ; :: thesis: Int Affn is open
per cases ( n <> 0 or n = 0 ) ;
suppose A2: n <> 0 ; :: thesis: Int Affn is open
reconsider L = ].0,1.[ as Subset of R^1 by TOPMETR:17;
set E = the Enumeration of Affn;
deffunc H1( object ) -> Element of bool the carrier of () = (|-- (Affn,( the Enumeration of Affn . \$1))) " L;
consider f being FinSequence such that
A3: len f = n + 1 and
A4: for k being Nat st k in dom f holds
f . k = H1(k) from A5: dom f = Seg (len f) by FINSEQ_1:def 3;
then A6: not rng f is empty by ;
rng f c= bool the carrier of ()
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in bool the carrier of () )
assume y in rng f ; :: thesis: y in bool the carrier of ()
then consider x being object such that
A7: x in dom f and
A8: f . x = y by FUNCT_1:def 3;
f . x = H1(x) by A4, A7;
hence y in bool the carrier of () by A8; :: thesis: verum
end;
then reconsider f = f as FinSequence of bool the carrier of () by FINSEQ_1:def 4;
A9: rng the Enumeration of Affn = Affn by Def1;
then A10: len the Enumeration of Affn = card Affn by FINSEQ_4:62;
A11: meet (rng f) c= Int Affn
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in meet (rng f) or x in Int Affn )
dim () = n by Th4;
then A12: [#] () = Affin Affn by ;
assume A13: x in meet (rng f) ; :: thesis: x in Int Affn
A14: now :: thesis: for v being Element of () st v in Affn holds
(x |-- Affn) . v > 0
let v be Element of (); :: thesis: ( v in Affn implies (x |-- Affn) . v > 0 )
assume v in Affn ; :: thesis: (x |-- Affn) . v > 0
then consider k being object such that
A15: k in dom the Enumeration of Affn and
A16: the Enumeration of Affn . k = v by ;
A17: k in dom f by ;
then f . k in rng f by FUNCT_1:def 3;
then A18: meet (rng f) c= f . k by SETFAM_1:3;
A19: (x |-- Affn) . v = (|-- (Affn,v)) . x by ;
f . k = (|-- (Affn,v)) " L by A4, A16, A17;
then (x |-- Affn) . v in L by ;
hence (x |-- Affn) . v > 0 by XXREAL_1:4; :: thesis: verum
end;
A20: Affn c= Carrier (x |-- Affn)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Affn or y in Carrier (x |-- Affn) )
assume A21: y in Affn ; :: thesis: y in Carrier (x |-- Affn)
then (x |-- Affn) . y > 0 by A14;
hence y in Carrier (x |-- Affn) by ; :: thesis: verum
end;
Carrier (x |-- Affn) c= Affn by RLVECT_2:def 6;
then A22: Carrier (x |-- Affn) = Affn by A20;
for v being Element of () st v in Affn holds
(x |-- Affn) . v >= 0 by A14;
then A23: x in conv Affn by ;
Sum (x |-- Affn) = x by ;
hence x in Int Affn by ; :: thesis: verum
end;
A24: conv Affn c= Affin Affn by RLAFFIN1:65;
A25: Int Affn c= conv Affn by RLAFFIN2:5;
A26: dom the Enumeration of Affn = Seg (len the Enumeration of Affn) by FINSEQ_1:def 3;
A27: Int Affn c= meet (rng f)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Int Affn or x in meet (rng f) )
assume A28: x in Int Affn ; :: thesis: x in meet (rng f)
then consider K being Linear_Combination of Affn such that
A29: K is convex and
A30: x = Sum K by RLAFFIN2:10;
A31: x in conv Affn by ;
sum K = 1 by ;
then A32: K = x |-- Affn by ;
A33: Carrier K = Affn by ;
now :: thesis: for Y being set st Y in rng f holds
x 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
A34: k in dom f and
A35: f . k = Y by FUNCT_1:def 3;
A36: the Enumeration of Affn . k in Affn by ;
then reconsider Ek = the Enumeration of Affn . k as Element of () ;
(x |-- Affn) . Ek <> 0 by ;
then A37: 0 < (x |-- Affn) . Ek by ;
A38: (x |-- Affn) . Ek < 1
proof
assume A39: (x |-- Affn) . Ek >= 1 ; :: thesis: contradiction
(x |-- Affn) . Ek <= 1 by ;
then Affn = {Ek} by ;
then card Affn = 1 by CARD_2:42;
hence contradiction by A1, A2; :: thesis: verum
end;
(x |-- Affn) . Ek = (|-- (Affn,Ek)) . x by ;
then A40: (|-- (Affn,Ek)) . x in L by ;
A41: dom (|-- (Affn,Ek)) = [#] () by FUNCT_2:def 1;
Y = (|-- (Affn,( the Enumeration of Affn . k))) " L by A4, A34, A35;
hence x in Y by ; :: thesis: verum
end;
hence x in meet (rng f) by ; :: thesis: verum
end;
now :: thesis: for B being Subset of () st B in rng f holds
B is open
let B be Subset of (); :: thesis: ( B in rng f implies B is open )
A42: not [#] R^1 is empty ;
assume B in rng f ; :: thesis: B is open
then consider k being object such that
A43: ( k in dom f & f . k = B ) by FUNCT_1:def 3;
( |-- (Affn,( the Enumeration of Affn . k)) is continuous & L is open ) by ;
then (|-- (Affn,( the Enumeration of Affn . k))) " L is open by ;
hence B is open by ; :: thesis: verum
end;
then rng f is open by TOPS_2:def 1;
then meet (rng f) is open by TOPS_2:20;
hence Int Affn is open by ; :: thesis: verum
end;
suppose A44: n = 0 ; :: thesis: Int Affn is open
not Affn is empty by A1;
then A45: not Int Affn is empty by RLAFFIN2:20;
the carrier of () = {(0. ())} by ;
then Int Affn = [#] () by ;
hence Int Affn is open ; :: thesis: verum
end;
end;