let x be set ; for n being Nat
for Affn being affinely-independent Subset of (TOP-REAL n) st card Affn = n + 1 holds
|-- (Affn,x) is continuous
let n be Nat; for Affn being affinely-independent Subset of (TOP-REAL n) st card Affn = n + 1 holds
|-- (Affn,x) is continuous
let Affn be affinely-independent Subset of (TOP-REAL n); ( card Affn = n + 1 implies |-- (Affn,x) is continuous )
set TRn = TOP-REAL n;
set AA = Affin Affn;
set Ax = |-- (Affn,x);
reconsider AxA = (|-- (Affn,x)) | (Affin Affn) as continuous Function of ((TOP-REAL n) | (Affin Affn)),R^1 by Th31;
assume A1:
card Affn = n + 1
; |-- (Affn,x) is continuous
dim (TOP-REAL n) = n
by Th4;
then A2:
Affin Affn = [#] (TOP-REAL n)
by A1, Th6;
then A3:
(TOP-REAL n) | (Affin Affn) = TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #)
by TSEP_1:93;
A4:
dom (|-- (Affn,x)) = Affin Affn
by A2, FUNCT_2:def 1;
now for P being Subset of R^1 st P is closed holds
(|-- (Affn,x)) " P is closed let P be
Subset of
R^1;
( P is closed implies (|-- (Affn,x)) " P is closed )assume
P is
closed
;
(|-- (Affn,x)) " P is closed then
AxA " P is
closed
by PRE_TOPC:def 6;
then A5:
(AxA " P) ` in the
topology of
TopStruct(# the
carrier of
(TOP-REAL n), the
topology of
(TOP-REAL n) #)
by A3, PRE_TOPC:def 2;
(AxA " P) ` = ((|-- (Affn,x)) " P) `
by A4, A3, RELAT_1:69;
then
((|-- (Affn,x)) " P) ` is
open
by A5, PRE_TOPC:def 2;
hence
(|-- (Affn,x)) " P is
closed
by TOPS_1:3;
verum end;
hence
|-- (Affn,x) is continuous
by PRE_TOPC:def 6; verum