let n, k be Nat; :: thesis: for An being Subset of (TOP-REAL n)

for Affn being affinely-independent Subset of (TOP-REAL n)

for Ak being Subset of (TOP-REAL k)

for EN being Enumeration of Affn st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds

( Ak is closed iff An is closed )

let An be Subset of (TOP-REAL n); :: thesis: for Affn being affinely-independent Subset of (TOP-REAL n)

for Ak being Subset of (TOP-REAL k)

for EN being Enumeration of Affn st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds

( Ak is closed iff An is closed )

let Affn be affinely-independent Subset of (TOP-REAL n); :: thesis: for Ak being Subset of (TOP-REAL k)

for EN being Enumeration of Affn st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds

( Ak is closed iff An is closed )

let Ak be Subset of (TOP-REAL k); :: thesis: for EN being Enumeration of Affn st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds

( Ak is closed iff An is closed )

set TRn = TOP-REAL n;

set TRk = TOP-REAL k;

set A = Affn;

let E be Enumeration of Affn; :: thesis: ( k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- E) | k in Ak } implies ( Ak is closed iff An is closed ) )

assume that

A1: ( k <= n & card Affn = n + 1 ) and

A2: An = { v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak } ; :: thesis: ( Ak is closed iff An is closed )

set B1 = { v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak ` } ;

A3: k < card Affn by A1, NAT_1:13;

A4: An ` c= { v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak ` }

then ( Ak ` is open iff An ` is open ) by A1, Th25;

hence ( Ak is closed iff An is closed ) by TOPS_1:3; :: thesis: verum

for Affn being affinely-independent Subset of (TOP-REAL n)

for Ak being Subset of (TOP-REAL k)

for EN being Enumeration of Affn st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds

( Ak is closed iff An is closed )

let An be Subset of (TOP-REAL n); :: thesis: for Affn being affinely-independent Subset of (TOP-REAL n)

for Ak being Subset of (TOP-REAL k)

for EN being Enumeration of Affn st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds

( Ak is closed iff An is closed )

let Affn be affinely-independent Subset of (TOP-REAL n); :: thesis: for Ak being Subset of (TOP-REAL k)

for EN being Enumeration of Affn st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds

( Ak is closed iff An is closed )

let Ak be Subset of (TOP-REAL k); :: thesis: for EN being Enumeration of Affn st k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- EN) | k in Ak } holds

( Ak is closed iff An is closed )

set TRn = TOP-REAL n;

set TRk = TOP-REAL k;

set A = Affn;

let E be Enumeration of Affn; :: thesis: ( k <= n & card Affn = n + 1 & An = { pn where pn is Point of (TOP-REAL n) : (pn |-- E) | k in Ak } implies ( Ak is closed iff An is closed ) )

assume that

A1: ( k <= n & card Affn = n + 1 ) and

A2: An = { v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak } ; :: thesis: ( Ak is closed iff An is closed )

set B1 = { v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak ` } ;

A3: k < card Affn by A1, NAT_1:13;

A4: An ` c= { v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak ` }

proof

{ v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak ` } c= An `
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in An ` or x in { v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak ` } )

assume A5: x in An ` ; :: thesis: x in { v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak ` }

then reconsider f = x as Element of (TOP-REAL n) ;

set fE = f |-- E;

len (f |-- E) = card Affn by Th16;

then len ((f |-- E) | k) = k by A3, FINSEQ_1:59;

then A6: (f |-- E) | k is Element of (TOP-REAL k) by TOPREAL3:46;

assume not x in { v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak ` } ; :: thesis: contradiction

then not (f |-- E) | k in Ak ` ;

then (f |-- E) | k in Ak by A6, XBOOLE_0:def 5;

then f in An by A2;

hence contradiction by A5, XBOOLE_0:def 5; :: thesis: verum

end;assume A5: x in An ` ; :: thesis: x in { v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak ` }

then reconsider f = x as Element of (TOP-REAL n) ;

set fE = f |-- E;

len (f |-- E) = card Affn by Th16;

then len ((f |-- E) | k) = k by A3, FINSEQ_1:59;

then A6: (f |-- E) | k is Element of (TOP-REAL k) by TOPREAL3:46;

assume not x in { v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak ` } ; :: thesis: contradiction

then not (f |-- E) | k in Ak ` ;

then (f |-- E) | k in Ak by A6, XBOOLE_0:def 5;

then f in An by A2;

hence contradiction by A5, XBOOLE_0:def 5; :: thesis: verum

proof

then
An ` = { v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak ` }
by A4;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak ` } or x in An ` )

assume x in { v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak ` } ; :: thesis: x in An `

then consider v being Element of (TOP-REAL n) such that

A7: x = v and

A8: (v |-- E) | k in Ak ` ;

assume not x in An ` ; :: thesis: contradiction

then v in An by A7, XBOOLE_0:def 5;

then ex w being Element of (TOP-REAL n) st

( v = w & (w |-- E) | k in Ak ) by A2;

hence contradiction by A8, XBOOLE_0:def 5; :: thesis: verum

end;assume x in { v where v is Element of (TOP-REAL n) : (v |-- E) | k in Ak ` } ; :: thesis: x in An `

then consider v being Element of (TOP-REAL n) such that

A7: x = v and

A8: (v |-- E) | k in Ak ` ;

assume not x in An ` ; :: thesis: contradiction

then v in An by A7, XBOOLE_0:def 5;

then ex w being Element of (TOP-REAL n) st

( v = w & (w |-- E) | k in Ak ) by A2;

hence contradiction by A8, XBOOLE_0:def 5; :: thesis: verum

then ( Ak ` is open iff An ` is open ) by A1, Th25;

hence ( Ak is closed iff An is closed ) by TOPS_1:3; :: thesis: verum