let n be Nat; for Affn being affinely-independent Subset of (TOP-REAL n) st card Affn = n + 1 holds
Int Affn is open
let Affn be affinely-independent Subset of (TOP-REAL n); ( 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
; Int Affn is open
per cases
( n <> 0 or n = 0 )
;
suppose A2:
n <> 0
;
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
(TOP-REAL n) =
(|-- (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 FINSEQ_1:sch 2();
A5:
dom f = Seg (len f)
by FINSEQ_1:def 3;
then A6:
not
rng f is
empty
by A3, RELAT_1:42;
rng f c= bool the
carrier of
(TOP-REAL n)
then reconsider f =
f as
FinSequence of
bool the
carrier of
(TOP-REAL n) 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 ;
TARSKI:def 3 ( not x in meet (rng f) or x in Int Affn )
dim (TOP-REAL n) = n
by Th4;
then A12:
[#] (TOP-REAL n) = Affin Affn
by A1, Th6;
assume A13:
x in meet (rng f)
;
x in Int Affn
A14:
now for v being Element of (TOP-REAL n) st v in Affn holds
(x |-- Affn) . v > 0 let v be
Element of
(TOP-REAL n);
( v in Affn implies (x |-- Affn) . v > 0 )assume
v in Affn
;
(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 A9, FUNCT_1:def 3;
A17:
k in dom f
by A1, A3, A10, A5, A15, FINSEQ_1:def 3;
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 A13, Def3;
f . k = (|-- (Affn,v)) " L
by A4, A16, A17;
then
(x |-- Affn) . v in L
by A13, A19, A18, FUNCT_1:def 7;
hence
(x |-- Affn) . v > 0
by XXREAL_1:4;
verum end;
A20:
Affn c= Carrier (x |-- Affn)
Carrier (x |-- Affn) c= Affn
by RLVECT_2:def 6;
then A22:
Carrier (x |-- Affn) = Affn
by A20;
for
v being
Element of
(TOP-REAL n) st
v in Affn holds
(x |-- Affn) . v >= 0
by A14;
then A23:
x in conv Affn
by A13, A12, RLAFFIN1:73;
Sum (x |-- Affn) = x
by A13, A12, RLAFFIN1:def 7;
hence
x in Int Affn
by A23, A22, RLAFFIN1:71, RLAFFIN2:12;
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 ;
TARSKI:def 3 ( not x in Int Affn or x in meet (rng f) )
assume A28:
x in Int Affn
;
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 A25, A28;
sum K = 1
by A29, RLAFFIN1:62;
then A32:
K = x |-- Affn
by A24, A30, A31, RLAFFIN1:def 7;
A33:
Carrier K = Affn
by A28, A29, A30, RLAFFIN2:11;
now for Y being set st Y in rng f holds
x in Ylet Y be
set ;
( Y in rng f implies x in Y )assume
Y in rng f
;
x in Ythen 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 A1, A3, A9, A10, A5, A26, A34, FUNCT_1:def 3;
then reconsider Ek = the
Enumeration of
Affn . k as
Element of
(TOP-REAL n) ;
(x |-- Affn) . Ek <> 0
by A32, A33, A36, RLVECT_2:19;
then A37:
0 < (x |-- Affn) . Ek
by A29, A32, RLAFFIN1:62;
A38:
(x |-- Affn) . Ek < 1
(x |-- Affn) . Ek = (|-- (Affn,Ek)) . x
by A30, Def3;
then A40:
(|-- (Affn,Ek)) . x in L
by A38, A37, XXREAL_1:4;
A41:
dom (|-- (Affn,Ek)) = [#] (TOP-REAL n)
by FUNCT_2:def 1;
Y = (|-- (Affn,( the Enumeration of Affn . k))) " L
by A4, A34, A35;
hence
x in Y
by A28, A40, A41, FUNCT_1:def 7;
verum end;
hence
x in meet (rng f)
by A6, SETFAM_1:def 1;
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 A27, A11, XBOOLE_0:def 10;
verum end;