:: SIMPLEX2 semantic presentation
begin
definition
let M be non empty MetrSpace;
assume B1: TopSpaceMetr M is compact ;
let F be Subset-Family of (TopSpaceMetr M);
assume that
B2: F is open and
B3: F is Cover of (TopSpaceMetr M) ;
mode Lebesgue_number of F -> positive Real means :Def1: :: SIMPLEX2:def 1
for p being Point of M ex A being Subset of (TopSpaceMetr M) st
( A in F & Ball (p,it) c= A );
existence
ex b1 being positive Real st
for p being Point of M ex A being Subset of (TopSpaceMetr M) st
( A in F & Ball (p,b1) c= A )
proof
set TM = TopSpaceMetr M;
consider G being Subset-Family of (TopSpaceMetr M) such that
A1: G c= F and
A2: G is Cover of (TopSpaceMetr M) and
A3: G is finite by B1, B2, B3, COMPTS_1:def_1;
percases ( [#] (TopSpaceMetr M) in G or not [#] (TopSpaceMetr M) in G ) ;
supposeA4: [#] (TopSpaceMetr M) in G ; ::_thesis: ex b1 being positive Real st
for p being Point of M ex A being Subset of (TopSpaceMetr M) st
( A in F & Ball (p,b1) c= A )
take R = 1; ::_thesis: for p being Point of M ex A being Subset of (TopSpaceMetr M) st
( A in F & Ball (p,R) c= A )
let x be Point of M; ::_thesis: ex A being Subset of (TopSpaceMetr M) st
( A in F & Ball (x,R) c= A )
take [#] (TopSpaceMetr M) ; ::_thesis: ( [#] (TopSpaceMetr M) in F & Ball (x,R) c= [#] (TopSpaceMetr M) )
thus ( [#] (TopSpaceMetr M) in F & Ball (x,R) c= [#] (TopSpaceMetr M) ) by A1, A4; ::_thesis: verum
end;
supposeA5: not [#] (TopSpaceMetr M) in G ; ::_thesis: ex b1 being positive Real st
for p being Point of M ex A being Subset of (TopSpaceMetr M) st
( A in F & Ball (p,b1) c= A )
set cTM = [#] (TopSpaceMetr M);
set FUNCS = Funcs (([#] (TopSpaceMetr M)),REAL);
consider g being FinSequence such that
A6: rng g = G and
g is one-to-one by A3, FINSEQ_4:58;
defpred S1[ Nat, set , set ] means for f1, f2 being Function of (TopSpaceMetr M),R^1 st f1 = $2 & f2 = $3 & f1 is continuous holds
( f2 is continuous & ex A being non empty Subset of (TopSpaceMetr M) st
( A ` = g . ($1 + 1) & ( for x being Point of (TopSpaceMetr M) holds f2 . x = max ((f1 . x),((dist_min A) . x)) ) ) );
not union G is empty by A2, SETFAM_1:45;
then A7: not g is empty by A6, ZFMISC_1:2;
then A8: len g >= 1 by NAT_1:14;
then A9: 1 in dom g by FINSEQ_3:25;
then A10: g . 1 in rng g by FUNCT_1:def_3;
then reconsider g1 = g . 1 as Subset of (TopSpaceMetr M) by A6;
A11: (g1 `) ` <> [#] (TopSpaceMetr M) by A5, A6, A9, FUNCT_1:def_3;
g1 is open by B2, A1, A6, A10, TOPS_2:def_1;
then reconsider g19 = g1 ` as non empty closed Subset of (TopSpaceMetr M) by A11;
reconsider Dg19 = dist_min g19 as Element of Funcs (([#] (TopSpaceMetr M)),REAL) by FUNCT_2:8, TOPMETR:17;
A12: for n being Nat st 1 <= n & n < len g holds
for x being Element of Funcs (([#] (TopSpaceMetr M)),REAL) ex y being Element of Funcs (([#] (TopSpaceMetr M)),REAL) st S1[n,x,y]
proof
let n be Nat; ::_thesis: ( 1 <= n & n < len g implies for x being Element of Funcs (([#] (TopSpaceMetr M)),REAL) ex y being Element of Funcs (([#] (TopSpaceMetr M)),REAL) st S1[n,x,y] )
assume that
1 <= n and
A13: n < len g ; ::_thesis: for x being Element of Funcs (([#] (TopSpaceMetr M)),REAL) ex y being Element of Funcs (([#] (TopSpaceMetr M)),REAL) st S1[n,x,y]
let x be Element of Funcs (([#] (TopSpaceMetr M)),REAL); ::_thesis: ex y being Element of Funcs (([#] (TopSpaceMetr M)),REAL) st S1[n,x,y]
reconsider fx = x as Function of (TopSpaceMetr M),R^1 by TOPMETR:17;
percases ( not fx is continuous or fx is continuous ) ;
supposeA14: not fx is continuous ; ::_thesis: ex y being Element of Funcs (([#] (TopSpaceMetr M)),REAL) st S1[n,x,y]
take y = x; ::_thesis: S1[n,x,y]
thus S1[n,x,y] by A14; ::_thesis: verum
end;
supposeA15: fx is continuous ; ::_thesis: ex y being Element of Funcs (([#] (TopSpaceMetr M)),REAL) st S1[n,x,y]
( 1 <= n + 1 & n + 1 <= len g ) by A13, NAT_1:11, NAT_1:13;
then A16: n + 1 in dom g by FINSEQ_3:25;
then g . (n + 1) in G by A6, FUNCT_1:def_3;
then reconsider A = g . (n + 1) as Subset of (TopSpaceMetr M) ;
(A `) ` <> [#] (TopSpaceMetr M) by A5, A6, A16, FUNCT_1:def_3;
then reconsider A9 = A ` as non empty Subset of (TopSpaceMetr M) ;
R^1 is SubSpace of R^1 by TSEP_1:2;
then consider h being continuous Function of (TopSpaceMetr M),R^1 such that
A17: for x being Point of (TopSpaceMetr M) holds h . x = max ((fx . x),((dist_min A9) . x)) by A15, TOPGEN_5:50;
reconsider y = h as Element of Funcs (([#] (TopSpaceMetr M)),REAL) by FUNCT_2:8, TOPMETR:17;
take y ; ::_thesis: S1[n,x,y]
let f1, f2 be Function of (TopSpaceMetr M),R^1; ::_thesis: ( f1 = x & f2 = y & f1 is continuous implies ( f2 is continuous & ex A being non empty Subset of (TopSpaceMetr M) st
( A ` = g . (n + 1) & ( for x being Point of (TopSpaceMetr M) holds f2 . x = max ((f1 . x),((dist_min A) . x)) ) ) ) )
assume that
A18: f1 = x and
A19: f2 = y and
f1 is continuous ; ::_thesis: ( f2 is continuous & ex A being non empty Subset of (TopSpaceMetr M) st
( A ` = g . (n + 1) & ( for x being Point of (TopSpaceMetr M) holds f2 . x = max ((f1 . x),((dist_min A) . x)) ) ) )
thus f2 is continuous by A19; ::_thesis: ex A being non empty Subset of (TopSpaceMetr M) st
( A ` = g . (n + 1) & ( for x being Point of (TopSpaceMetr M) holds f2 . x = max ((f1 . x),((dist_min A) . x)) ) )
take A9 ; ::_thesis: ( A9 ` = g . (n + 1) & ( for x being Point of (TopSpaceMetr M) holds f2 . x = max ((f1 . x),((dist_min A9) . x)) ) )
thus ( A9 ` = g . (n + 1) & ( for x being Point of (TopSpaceMetr M) holds f2 . x = max ((f1 . x),((dist_min A9) . x)) ) ) by A17, A18, A19; ::_thesis: verum
end;
end;
end;
consider p being FinSequence of Funcs (([#] (TopSpaceMetr M)),REAL) such that
A20: len p = len g and
A21: ( p /. 1 = Dg19 or len g = 0 ) and
A22: for n being Nat st 1 <= n & n < len g holds
S1[n,p /. n,p /. (n + 1)] from NAT_2:sch_1(A12);
A23: len p in dom p by A8, A20, FINSEQ_3:25;
p /. (len p) is Element of Funcs (([#] (TopSpaceMetr M)),REAL) ;
then reconsider pL = p /. (len p) as Function of (TopSpaceMetr M),R^1 by TOPMETR:17;
reconsider rngPL = rng pL as Subset of R^1 by RELAT_1:def_19;
set cRpL = [#] rngPL;
A24: [#] rngPL = rng pL by WEIERSTR:def_1;
A25: dom p = dom g by A20, FINSEQ_3:29;
defpred S2[ Nat] means for f being Function of (TopSpaceMetr M),R^1 st $1 in dom p & f = p /. $1 holds
( f is continuous & ( for j being Nat
for h being Function of (TopSpaceMetr M),R^1 st j <= $1 & j in dom p & h = p /. j holds
for x being Point of (TopSpaceMetr M) holds h . x <= f . x ) );
A26: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; ::_thesis: ( S2[n] implies S2[n + 1] )
assume A27: S2[n] ; ::_thesis: S2[n + 1]
let f be Function of (TopSpaceMetr M),R^1; ::_thesis: ( n + 1 in dom p & f = p /. (n + 1) implies ( f is continuous & ( for j being Nat
for h being Function of (TopSpaceMetr M),R^1 st j <= n + 1 & j in dom p & h = p /. j holds
for x being Point of (TopSpaceMetr M) holds h . x <= f . x ) ) )
assume that
A28: n + 1 in dom p and
A29: f = p /. (n + 1) ; ::_thesis: ( f is continuous & ( for j being Nat
for h being Function of (TopSpaceMetr M),R^1 st j <= n + 1 & j in dom p & h = p /. j holds
for x being Point of (TopSpaceMetr M) holds h . x <= f . x ) )
percases ( n = 0 or n > 0 ) ;
supposeA30: n = 0 ; ::_thesis: ( f is continuous & ( for j being Nat
for h being Function of (TopSpaceMetr M),R^1 st j <= n + 1 & j in dom p & h = p /. j holds
for x being Point of (TopSpaceMetr M) holds h . x <= f . x ) )
hence f is continuous by A7, A21, A29; ::_thesis: for j being Nat
for h being Function of (TopSpaceMetr M),R^1 st j <= n + 1 & j in dom p & h = p /. j holds
for x being Point of (TopSpaceMetr M) holds h . x <= f . x
let j be Nat; ::_thesis: for h being Function of (TopSpaceMetr M),R^1 st j <= n + 1 & j in dom p & h = p /. j holds
for x being Point of (TopSpaceMetr M) holds h . x <= f . x
let g be Function of (TopSpaceMetr M),R^1; ::_thesis: ( j <= n + 1 & j in dom p & g = p /. j implies for x being Point of (TopSpaceMetr M) holds g . x <= f . x )
assume that
A31: j <= n + 1 and
A32: j in dom p and
A33: g = p /. j ; ::_thesis: for x being Point of (TopSpaceMetr M) holds g . x <= f . x
1 <= j by A32, FINSEQ_3:25;
hence for x being Point of (TopSpaceMetr M) holds g . x <= f . x by A29, A30, A31, A33, XXREAL_0:1; ::_thesis: verum
end;
suppose n > 0 ; ::_thesis: ( f is continuous & ( for j being Nat
for h being Function of (TopSpaceMetr M),R^1 st j <= n + 1 & j in dom p & h = p /. j holds
for x being Point of (TopSpaceMetr M) holds h . x <= f . x ) )
then reconsider n1 = n - 1 as Element of NAT by NAT_1:20;
p /. n is Element of Funcs (([#] (TopSpaceMetr M)),REAL) ;
then reconsider pn = p /. n as Function of (TopSpaceMetr M),R^1 by TOPMETR:17;
n + 1 <= len p by A28, FINSEQ_3:25;
then A34: ( 1 <= n1 + 1 & n < len p ) by NAT_1:11, NAT_1:13;
then A35: n in dom p by FINSEQ_3:25;
then A36: pn is continuous by A27;
hence f is continuous by A20, A22, A29, A34; ::_thesis: for j being Nat
for h being Function of (TopSpaceMetr M),R^1 st j <= n + 1 & j in dom p & h = p /. j holds
for x being Point of (TopSpaceMetr M) holds h . x <= f . x
consider A being non empty Subset of (TopSpaceMetr M) such that
A ` = g . (n + 1) and
A37: for y being Point of (TopSpaceMetr M) holds f . y = max ((pn . y),((dist_min A) . y)) by A20, A22, A29, A34, A36;
let j be Nat; ::_thesis: for h being Function of (TopSpaceMetr M),R^1 st j <= n + 1 & j in dom p & h = p /. j holds
for x being Point of (TopSpaceMetr M) holds h . x <= f . x
let h be Function of (TopSpaceMetr M),R^1; ::_thesis: ( j <= n + 1 & j in dom p & h = p /. j implies for x being Point of (TopSpaceMetr M) holds h . x <= f . x )
assume that
A38: j <= n + 1 and
A39: j in dom p and
A40: h = p /. j ; ::_thesis: for x being Point of (TopSpaceMetr M) holds h . x <= f . x
let x be Point of (TopSpaceMetr M); ::_thesis: h . x <= f . x
A41: f . x = max ((pn . x),((dist_min A) . x)) by A37;
percases ( j <= n or j = n + 1 ) by A38, NAT_1:8;
supposeA42: j <= n ; ::_thesis: h . x <= f . x
A43: pn . x <= f . x by A41, XXREAL_0:25;
h . x <= pn . x by A27, A35, A39, A40, A42;
hence h . x <= f . x by A43, XXREAL_0:2; ::_thesis: verum
end;
suppose j = n + 1 ; ::_thesis: h . x <= f . x
hence h . x <= f . x by A29, A40; ::_thesis: verum
end;
end;
end;
end;
end;
A44: S2[ 0 ] by FINSEQ_3:25;
A45: for n being Nat holds S2[n] from NAT_1:sch_2(A44, A26);
A46: dom pL = [#] (TopSpaceMetr M) by FUNCT_2:def_1;
then pL .: ([#] (TopSpaceMetr M)) = rng pL by RELAT_1:113;
then A47: rngPL is compact by B1, A23, A45, WEIERSTR:9;
then A48: [#] rngPL is compact by WEIERSTR:13;
reconsider cRpL = [#] rngPL as non empty real-bounded Subset of REAL by A47, WEIERSTR:11, WEIERSTR:def_1;
set L = lower_bound cRpL;
lower_bound cRpL in cRpL by A48, RCOMP_1:14;
then consider x being set such that
A49: x in dom pL and
A50: pL . x = lower_bound cRpL by A24, FUNCT_1:def_3;
union G = [#] (TopSpaceMetr M) by A2, SETFAM_1:45;
then consider Y being set such that
A51: x in Y and
A52: Y in rng g by A6, A49, TARSKI:def_4;
reconsider x = x as Point of (TopSpaceMetr M) by A49;
consider j being set such that
A53: j in dom g and
A54: g . j = Y by A52, FUNCT_1:def_3;
reconsider j = j as Nat by A53;
A55: j <= len g by A53, FINSEQ_3:25;
A56: 1 <= j by A53, FINSEQ_3:25;
now__::_thesis:_0_<_lower_bound_cRpL
percases ( j = 1 or j > 1 ) by A56, XXREAL_0:1;
supposeA57: j = 1 ; ::_thesis: 0 < lower_bound cRpL
then not x in g19 by A51, A54, XBOOLE_0:def_5;
then (dist_min g19) . x <> 0 by HAUSDORF:9;
then (dist_min g19) . x > 0 by JORDAN1K:9;
hence 0 < lower_bound cRpL by A20, A21, A23, A25, A45, A50, A53, A55, A57; ::_thesis: verum
end;
supposeA58: j > 1 ; ::_thesis: 0 < lower_bound cRpL
then reconsider j1 = j - 1 as Element of NAT by NAT_1:20;
( p /. j1 is Element of Funcs (([#] (TopSpaceMetr M)),REAL) & p /. j is Element of Funcs (([#] (TopSpaceMetr M)),REAL) ) ;
then reconsider pj1 = p /. j1, pj = p /. j as Function of (TopSpaceMetr M),R^1 by TOPMETR:17;
j1 + 1 > 1 by A58;
then A59: ( 1 <= j1 & j1 < len g ) by A55, NAT_1:13;
then j1 in dom p by A20, FINSEQ_3:25;
then A60: pj1 is continuous by A45;
S1[j1,pj1,pj] by A22, A25, A45, A53, A59;
then consider A being non empty Subset of (TopSpaceMetr M) such that
A61: A ` = g . j and
A62: for x being Point of (TopSpaceMetr M) holds pj . x = max ((pj1 . x),((dist_min A) . x)) by A60;
A ` is open by B2, A1, A6, A52, A54, A61, TOPS_2:def_1;
then A63: A is closed by TOPS_1:3;
not x in A by A51, A54, A61, XBOOLE_0:def_5;
then (dist_min A) . x <> 0 by A63, HAUSDORF:9;
then A64: (dist_min A) . x > 0 by JORDAN1K:9;
pj . x = max ((pj1 . x),((dist_min A) . x)) by A62;
then pj . x > 0 by A64, XXREAL_0:25;
hence 0 < lower_bound cRpL by A20, A23, A25, A45, A50, A53, A55; ::_thesis: verum
end;
end;
end;
then reconsider L = lower_bound cRpL as positive Real ;
take L ; ::_thesis: for p being Point of M ex A being Subset of (TopSpaceMetr M) st
( A in F & Ball (p,L) c= A )
let X be Point of M; ::_thesis: ex A being Subset of (TopSpaceMetr M) st
( A in F & Ball (X,L) c= A )
defpred S3[ Nat] means ( $1 in dom p & ( for f1 being Function of (TopSpaceMetr M),R^1 st p /. $1 = f1 holds
f1 . X >= L ) );
pL . X in cRpL by A24, A46, FUNCT_1:def_3;
then S3[ len p] by A8, A20, FINSEQ_3:25, XXREAL_2:3;
then A65: ex k being Nat st S3[k] ;
consider k being Nat such that
A66: S3[k] and
A67: for n being Nat st S3[n] holds
k <= n from NAT_1:sch_5(A65);
A68: 1 <= k by A66, FINSEQ_3:25;
A69: k <= len p by A66, FINSEQ_3:25;
percases ( k = 1 or k > 1 ) by A68, XXREAL_0:1;
supposeA70: k = 1 ; ::_thesis: ex A being Subset of (TopSpaceMetr M) st
( A in F & Ball (X,L) c= A )
take g1 ; ::_thesis: ( g1 in F & Ball (X,L) c= g1 )
thus g1 in F by A1, A6, A10; ::_thesis: Ball (X,L) c= g1
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Ball (X,L) or y in g1 )
assume A71: y in Ball (X,L) ; ::_thesis: y in g1
reconsider Y = y as Point of M by A71;
A72: dist (X,Y) < L by A71, METRIC_1:11;
assume not y in g1 ; ::_thesis: contradiction
then Y in g19 by XBOOLE_0:def_5;
then A73: (dist_min g19) . X <= dist (X,Y) by HAUSDORF:13;
(dist_min g19) . X >= L by A7, A21, A66, A70;
hence contradiction by A72, A73, XXREAL_0:2; ::_thesis: verum
end;
supposeA74: k > 1 ; ::_thesis: ex A being Subset of (TopSpaceMetr M) st
( A in F & Ball (X,L) c= A )
then reconsider k1 = k - 1 as Element of NAT by NAT_1:20;
( p /. k1 is Element of Funcs (([#] (TopSpaceMetr M)),REAL) & p /. k is Element of Funcs (([#] (TopSpaceMetr M)),REAL) ) ;
then reconsider pk1 = p /. k1, pk = p /. k as Function of (TopSpaceMetr M),R^1 by TOPMETR:17;
k1 + 1 > 1 by A74;
then A75: ( 1 <= k1 & k1 < len g ) by A20, A69, NAT_1:13;
then k1 in dom p by A20, FINSEQ_3:25;
then A76: pk1 is continuous by A45;
S1[k1,pk1,pk] by A22, A45, A66, A75;
then consider A being non empty Subset of (TopSpaceMetr M) such that
A77: A ` = g . k and
A78: for x being Point of (TopSpaceMetr M) holds pk . x = max ((pk1 . x),((dist_min A) . x)) by A76;
take A ` ; ::_thesis: ( A ` in F & Ball (X,L) c= A ` )
A ` in G by A6, A25, A66, A77, FUNCT_1:def_3;
hence A ` in F by A1; ::_thesis: Ball (X,L) c= A `
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Ball (X,L) or y in A ` )
assume A79: y in Ball (X,L) ; ::_thesis: y in A `
reconsider Y = y as Point of M by A79;
assume not y in A ` ; ::_thesis: contradiction
then Y in A by XBOOLE_0:def_5;
then A80: (dist_min A) . X <= dist (X,Y) by HAUSDORF:13;
dist (X,Y) < L by A79, METRIC_1:11;
then A81: (dist_min A) . X < L by A80, XXREAL_0:2;
A82: pk . X >= L by A66;
pk . X = max ((pk1 . X),((dist_min A) . X)) by A78;
then S3[k1] by A20, A75, A81, A82, FINSEQ_3:25, XXREAL_0:16;
then k1 >= k1 + 1 by A67;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
end;
end;
end;
end;
end;
:: deftheorem Def1 defines Lebesgue_number SIMPLEX2:def_1_:_
for M being non empty MetrSpace st TopSpaceMetr M is compact holds
for F being Subset-Family of (TopSpaceMetr M) st F is open & F is Cover of (TopSpaceMetr M) holds
for b3 being positive Real holds
( b3 is Lebesgue_number of F iff for p being Point of M ex A being Subset of (TopSpaceMetr M) st
( A in F & Ball (p,b3) c= A ) );
theorem :: SIMPLEX2:1
for M being non empty MetrSpace
for F, G being open Subset-Family of (TopSpaceMetr M)
for L being Lebesgue_number of F st TopSpaceMetr M is compact & F is Cover of (TopSpaceMetr M) & F c= G holds
L is Lebesgue_number of G
proof
let M be non empty MetrSpace; ::_thesis: for F, G being open Subset-Family of (TopSpaceMetr M)
for L being Lebesgue_number of F st TopSpaceMetr M is compact & F is Cover of (TopSpaceMetr M) & F c= G holds
L is Lebesgue_number of G
let F, G be open Subset-Family of (TopSpaceMetr M); ::_thesis: for L being Lebesgue_number of F st TopSpaceMetr M is compact & F is Cover of (TopSpaceMetr M) & F c= G holds
L is Lebesgue_number of G
let L be Lebesgue_number of F; ::_thesis: ( TopSpaceMetr M is compact & F is Cover of (TopSpaceMetr M) & F c= G implies L is Lebesgue_number of G )
assume that
A1: TopSpaceMetr M is compact and
A2: F is Cover of (TopSpaceMetr M) and
A3: F c= G ; ::_thesis: L is Lebesgue_number of G
A4: now__::_thesis:_for_x_being_Point_of_M_ex_A_being_Subset_of_(TopSpaceMetr_M)_st_
(_A_in_G_&_Ball_(x,L)_c=_A_)
let x be Point of M; ::_thesis: ex A being Subset of (TopSpaceMetr M) st
( A in G & Ball (x,L) c= A )
ex A being Subset of (TopSpaceMetr M) st
( A in F & Ball (x,L) c= A ) by A1, A2, Def1;
hence ex A being Subset of (TopSpaceMetr M) st
( A in G & Ball (x,L) c= A ) by A3; ::_thesis: verum
end;
set TM = TopSpaceMetr M;
( union F = [#] (TopSpaceMetr M) & union F c= union G ) by A2, A3, SETFAM_1:45, ZFMISC_1:77;
then G is Cover of (TopSpaceMetr M) by SETFAM_1:def_11;
hence L is Lebesgue_number of G by A1, A4, Def1; ::_thesis: verum
end;
theorem :: SIMPLEX2:2
for M being non empty MetrSpace
for F, G being open Subset-Family of (TopSpaceMetr M)
for L being Lebesgue_number of F st TopSpaceMetr M is compact & F is Cover of (TopSpaceMetr M) & F is_finer_than G holds
L is Lebesgue_number of G
proof
let M be non empty MetrSpace; ::_thesis: for F, G being open Subset-Family of (TopSpaceMetr M)
for L being Lebesgue_number of F st TopSpaceMetr M is compact & F is Cover of (TopSpaceMetr M) & F is_finer_than G holds
L is Lebesgue_number of G
let F, G be open Subset-Family of (TopSpaceMetr M); ::_thesis: for L being Lebesgue_number of F st TopSpaceMetr M is compact & F is Cover of (TopSpaceMetr M) & F is_finer_than G holds
L is Lebesgue_number of G
let L be Lebesgue_number of F; ::_thesis: ( TopSpaceMetr M is compact & F is Cover of (TopSpaceMetr M) & F is_finer_than G implies L is Lebesgue_number of G )
assume that
A1: TopSpaceMetr M is compact and
A2: F is Cover of (TopSpaceMetr M) and
A3: F is_finer_than G ; ::_thesis: L is Lebesgue_number of G
set TM = TopSpaceMetr M;
A4: now__::_thesis:_for_x_being_Point_of_M_ex_B_being_Subset_of_(TopSpaceMetr_M)_st_
(_B_in_G_&_Ball_(x,L)_c=_B_)
let x be Point of M; ::_thesis: ex B being Subset of (TopSpaceMetr M) st
( B in G & Ball (x,L) c= B )
consider A being Subset of (TopSpaceMetr M) such that
A5: A in F and
A6: Ball (x,L) c= A by A1, A2, Def1;
consider B being set such that
A7: B in G and
A8: A c= B by A3, A5, SETFAM_1:def_2;
reconsider B = B as Subset of (TopSpaceMetr M) by A7;
take B = B; ::_thesis: ( B in G & Ball (x,L) c= B )
thus ( B in G & Ball (x,L) c= B ) by A6, A7, A8, XBOOLE_1:1; ::_thesis: verum
end;
( union F = [#] (TopSpaceMetr M) & union F c= union G ) by A2, A3, SETFAM_1:13, SETFAM_1:45;
then G is Cover of (TopSpaceMetr M) by SETFAM_1:def_11;
hence L is Lebesgue_number of G by A1, A4, Def1; ::_thesis: verum
end;
theorem :: SIMPLEX2:3
for M being non empty MetrSpace
for F being open Subset-Family of (TopSpaceMetr M)
for L being Lebesgue_number of F
for L1 being positive Real st TopSpaceMetr M is compact & F is Cover of (TopSpaceMetr M) & L1 <= L holds
L1 is Lebesgue_number of F
proof
let M be non empty MetrSpace; ::_thesis: for F being open Subset-Family of (TopSpaceMetr M)
for L being Lebesgue_number of F
for L1 being positive Real st TopSpaceMetr M is compact & F is Cover of (TopSpaceMetr M) & L1 <= L holds
L1 is Lebesgue_number of F
let F be open Subset-Family of (TopSpaceMetr M); ::_thesis: for L being Lebesgue_number of F
for L1 being positive Real st TopSpaceMetr M is compact & F is Cover of (TopSpaceMetr M) & L1 <= L holds
L1 is Lebesgue_number of F
let L be Lebesgue_number of F; ::_thesis: for L1 being positive Real st TopSpaceMetr M is compact & F is Cover of (TopSpaceMetr M) & L1 <= L holds
L1 is Lebesgue_number of F
let L9 be positive Real; ::_thesis: ( TopSpaceMetr M is compact & F is Cover of (TopSpaceMetr M) & L9 <= L implies L9 is Lebesgue_number of F )
assume that
A1: ( TopSpaceMetr M is compact & F is Cover of (TopSpaceMetr M) ) and
A2: L9 <= L ; ::_thesis: L9 is Lebesgue_number of F
now__::_thesis:_for_x_being_Point_of_M_ex_A_being_Subset_of_(TopSpaceMetr_M)_st_
(_A_in_F_&_Ball_(x,L9)_c=_A_)
let x be Point of M; ::_thesis: ex A being Subset of (TopSpaceMetr M) st
( A in F & Ball (x,L9) c= A )
consider A being Subset of (TopSpaceMetr M) such that
A3: ( A in F & Ball (x,L) c= A ) by A1, Def1;
take A = A; ::_thesis: ( A in F & Ball (x,L9) c= A )
Ball (x,L9) c= Ball (x,L) by A2, PCOMPS_1:1;
hence ( A in F & Ball (x,L9) c= A ) by A3, XBOOLE_1:1; ::_thesis: verum
end;
hence L9 is Lebesgue_number of F by A1, Def1; ::_thesis: verum
end;
begin
registration
let M be non empty Reflexive MetrStruct ;
cluster finite -> bounded for Element of bool the carrier of M;
coherence
for b1 being Subset of M st b1 is finite holds
b1 is bounded
proof
let A be Subset of M; ::_thesis: ( A is finite implies A is bounded )
percases ( A is empty or not A is empty ) ;
suppose A is empty ; ::_thesis: ( A is finite implies A is bounded )
hence ( A is finite implies A is bounded ) ; ::_thesis: verum
end;
supposeA1: not A is empty ; ::_thesis: ( A is finite implies A is bounded )
assume A is finite ; ::_thesis: A is bounded
then reconsider a = A as non empty finite Subset of M by A1;
deffunc H1( Point of M, Point of M) -> Element of REAL = dist (M,c2);
consider q being set such that
A2: q in a by XBOOLE_0:def_1;
set X = { H1(x,y) where x, y is Point of M : ( x in a & y in a ) } ;
reconsider q = q as Point of M by A2;
A3: H1(q,q) in { H1(x,y) where x, y is Point of M : ( x in a & y in a ) } by A2;
A4: now__::_thesis:_for_x_being_set_st_x_in__{__H1(x,y)_where_x,_y_is_Point_of_M_:_(_x_in_a_&_y_in_a_)__}__holds_
x_is_real
let x be set ; ::_thesis: ( x in { H1(x,y) where x, y is Point of M : ( x in a & y in a ) } implies x is real )
assume x in { H1(x,y) where x, y is Point of M : ( x in a & y in a ) } ; ::_thesis: x is real
then ex y, z being Point of M st
( x = H1(y,z) & y in a & z in a ) ;
hence x is real ; ::_thesis: verum
end;
A5: a is finite ;
{ H1(x,y) where x, y is Point of M : ( x in a & y in a ) } is finite from FRAENKEL:sch_22(A5, A5);
then reconsider X = { H1(x,y) where x, y is Point of M : ( x in a & y in a ) } as non empty finite real-membered set by A3, A4, MEMBERED:def_3;
reconsider sX = sup X as Real by XREAL_0:def_1;
reconsider sX1 = sX + 1 as Real ;
take sX1 ; :: according to TBSP_1:def_7 ::_thesis: ( not sX1 <= 0 & ( for b1, b2 being Element of the carrier of M holds
( not b1 in A or not b2 in A or dist (b1,b2) <= sX1 ) ) )
( H1(q,q) = 0 & H1(q,q) <= sX ) by A3, METRIC_1:1, XXREAL_2:4;
hence 0 < sX1 ; ::_thesis: for b1, b2 being Element of the carrier of M holds
( not b1 in A or not b2 in A or dist (b1,b2) <= sX1 )
let x, y be Point of M; ::_thesis: ( not x in A or not y in A or dist (x,y) <= sX1 )
assume ( x in A & y in A ) ; ::_thesis: dist (x,y) <= sX1
then H1(x,y) in X ;
then H1(x,y) <= sX by XXREAL_2:4;
hence dist (x,y) <= sX1 by XREAL_1:39; ::_thesis: verum
end;
end;
end;
end;
theorem :: SIMPLEX2:4
for M being non empty Reflexive MetrStruct
for S being non empty finite Subset of M ex p, q being Point of M st
( p in S & q in S & dist (p,q) = diameter S )
proof
let M be non empty Reflexive MetrStruct ; ::_thesis: for S being non empty finite Subset of M ex p, q being Point of M st
( p in S & q in S & dist (p,q) = diameter S )
let S be non empty finite Subset of M; ::_thesis: ex p, q being Point of M st
( p in S & q in S & dist (p,q) = diameter S )
set q = the Element of S;
reconsider q = the Element of S as Point of M ;
deffunc H1( Point of M, Point of M) -> Element of REAL = dist ($1,$2);
set X = { H1(x,y) where x, y is Point of M : ( x in S & y in S ) } ;
A1: now__::_thesis:_for_x_being_set_st_x_in__{__H1(x,y)_where_x,_y_is_Point_of_M_:_(_x_in_S_&_y_in_S_)__}__holds_
x_is_real
let x be set ; ::_thesis: ( x in { H1(x,y) where x, y is Point of M : ( x in S & y in S ) } implies x is real )
assume x in { H1(x,y) where x, y is Point of M : ( x in S & y in S ) } ; ::_thesis: x is real
then ex y, z being Point of M st
( x = H1(y,z) & y in S & z in S ) ;
hence x is real ; ::_thesis: verum
end;
A2: H1(q,q) in { H1(x,y) where x, y is Point of M : ( x in S & y in S ) } ;
A3: S is finite ;
{ H1(x,y) where x, y is Point of M : ( x in S & y in S ) } is finite from FRAENKEL:sch_22(A3, A3);
then reconsider X = { H1(x,y) where x, y is Point of M : ( x in S & y in S ) } as non empty finite real-membered set by A1, A2, MEMBERED:def_3;
reconsider sX = sup X as Real by XREAL_0:def_1;
sX in X by XXREAL_2:def_6;
then consider p, q being Point of M such that
A4: ( sX = H1(p,q) & p in S & q in S ) ;
now__::_thesis:_for_x,_y_being_Point_of_M_st_x_in_S_&_y_in_S_holds_
H1(x,y)_<=_sX
let x, y be Point of M; ::_thesis: ( x in S & y in S implies H1(x,y) <= sX )
assume ( x in S & y in S ) ; ::_thesis: H1(x,y) <= sX
then H1(x,y) in X ;
hence H1(x,y) <= sX by XXREAL_2:4; ::_thesis: verum
end;
then A5: diameter S <= sX by TBSP_1:def_8;
sX <= diameter S by A4, TBSP_1:def_8;
hence ex p, q being Point of M st
( p in S & q in S & dist (p,q) = diameter S ) by A4, A5, XXREAL_0:1; ::_thesis: verum
end;
definition
let M be non empty Reflexive MetrStruct ;
let K be SimplicialComplexStr;
attrK is M bounded means :Def2: :: SIMPLEX2:def 2
ex r being real number st
for A being Subset of M st A in the topology of K holds
( A is bounded & diameter A <= r );
end;
:: deftheorem Def2 defines bounded SIMPLEX2:def_2_:_
for M being non empty Reflexive MetrStruct
for K being SimplicialComplexStr holds
( K is M bounded iff ex r being real number st
for A being Subset of M st A in the topology of K holds
( A is bounded & diameter A <= r ) );
theorem Th5: :: SIMPLEX2:5
for M being non empty Reflexive MetrStruct
for A being Subset of M
for K being non void SimplicialComplexStr st K is M bounded & A is Simplex of K holds
A is bounded
proof
let M be non empty Reflexive MetrStruct ; ::_thesis: for A being Subset of M
for K being non void SimplicialComplexStr st K is M bounded & A is Simplex of K holds
A is bounded
let A be Subset of M; ::_thesis: for K being non void SimplicialComplexStr st K is M bounded & A is Simplex of K holds
A is bounded
let K be non void SimplicialComplexStr; ::_thesis: ( K is M bounded & A is Simplex of K implies A is bounded )
assume K is M bounded ; ::_thesis: ( not A is Simplex of K or A is bounded )
then A1: ex r being real number st
for A being Subset of M st A in the topology of K holds
( A is bounded & diameter A <= r ) by Def2;
assume A is Simplex of K ; ::_thesis: A is bounded
then A in the topology of K by PRE_TOPC:def_2;
hence A is bounded by A1; ::_thesis: verum
end;
registration
let M be non empty Reflexive MetrStruct ;
let X be set ;
cluster non void subset-closed finite-membered M bounded for SimplicialComplexStr of X;
existence
ex b1 being SimplicialComplex of X st
( b1 is M bounded & not b1 is void )
proof
set m = the Element of M;
take K = Complex_of {({} X)}; ::_thesis: ( K is M bounded & not K is void )
K is M bounded
proof
take r = diameter ({} M); :: according to SIMPLEX2:def_2 ::_thesis: for A being Subset of M st A in the topology of K holds
( A is bounded & diameter A <= r )
let A be Subset of M; ::_thesis: ( A in the topology of K implies ( A is bounded & diameter A <= r ) )
A1: the topology of K = bool ({} X) by SIMPLEX0:4;
assume A in the topology of K ; ::_thesis: ( A is bounded & diameter A <= r )
hence ( A is bounded & diameter A <= r ) by A1; ::_thesis: verum
end;
hence ( K is M bounded & not K is void ) ; ::_thesis: verum
end;
end;
registration
let M be non empty Reflexive MetrStruct ;
cluster non void subset-closed finite-membered M bounded for TopStruct ;
existence
ex b1 being SimplicialComplexStr st
( b1 is M bounded & not b1 is void & b1 is subset-closed & b1 is finite-membered )
proof
take the non void M bounded SimplicialComplex of the set ; ::_thesis: ( the non void M bounded SimplicialComplex of the set is M bounded & not the non void M bounded SimplicialComplex of the set is void & the non void M bounded SimplicialComplex of the set is subset-closed & the non void M bounded SimplicialComplex of the set is finite-membered )
thus ( the non void M bounded SimplicialComplex of the set is M bounded & not the non void M bounded SimplicialComplex of the set is void & the non void M bounded SimplicialComplex of the set is subset-closed & the non void M bounded SimplicialComplex of the set is finite-membered ) ; ::_thesis: verum
end;
end;
registration
let M be non empty Reflexive MetrStruct ;
let X be set ;
let K be M bounded SimplicialComplexStr of X;
cluster -> M bounded for SubSimplicialComplex of K;
coherence
for b1 being SubSimplicialComplex of K holds b1 is M bounded
proof
let SK be SubSimplicialComplex of K; ::_thesis: SK is M bounded
A1: the topology of SK c= the topology of K by SIMPLEX0:def_13;
consider r being real number such that
A2: for A being Subset of M st A in the topology of K holds
( A is bounded & diameter A <= r ) by Def2;
take r ; :: according to SIMPLEX2:def_2 ::_thesis: for A being Subset of M st A in the topology of SK holds
( A is bounded & diameter A <= r )
let A be Subset of M; ::_thesis: ( A in the topology of SK implies ( A is bounded & diameter A <= r ) )
assume A in the topology of SK ; ::_thesis: ( A is bounded & diameter A <= r )
hence ( A is bounded & diameter A <= r ) by A1, A2; ::_thesis: verum
end;
end;
registration
let M be non empty Reflexive MetrStruct ;
let X be set ;
let K be subset-closed M bounded SimplicialComplexStr of X;
let i be Integer;
cluster Skeleton_of (K,i) -> M bounded ;
coherence
Skeleton_of (K,i) is M bounded ;
end;
theorem Th6: :: SIMPLEX2:6
for M being non empty Reflexive MetrStruct
for K being SimplicialComplexStr st K is finite-vertices holds
K is M bounded
proof
let M be non empty Reflexive MetrStruct ; ::_thesis: for K being SimplicialComplexStr st K is finite-vertices holds
K is M bounded
let K be SimplicialComplexStr; ::_thesis: ( K is finite-vertices implies K is M bounded )
set V = Vertices K;
assume K is finite-vertices ; ::_thesis: K is M bounded
then Vertices K is finite by SIMPLEX0:def_5;
then reconsider VM = (Vertices K) /\ ([#] M) as finite Subset of M ;
take diameter VM ; :: according to SIMPLEX2:def_2 ::_thesis: for A being Subset of M st A in the topology of K holds
( A is bounded & diameter A <= diameter VM )
let A be Subset of M; ::_thesis: ( A in the topology of K implies ( A is bounded & diameter A <= diameter VM ) )
assume A1: A in the topology of K ; ::_thesis: ( A is bounded & diameter A <= diameter VM )
then reconsider S = A as Subset of K ;
S is simplex-like by A1, PRE_TOPC:def_2;
then A c= Vertices K by SIMPLEX0:17;
then A c= VM by XBOOLE_1:19;
hence ( A is bounded & diameter A <= diameter VM ) by TBSP_1:24; ::_thesis: verum
end;
begin
Lm1: 0 in REAL
by XREAL_0:def_1;
definition
let M be non empty Reflexive MetrStruct ;
let K be SimplicialComplexStr;
assume B1: K is M bounded ;
func diameter (M,K) -> Real means :Def3: :: SIMPLEX2:def 3
( ( for A being Subset of M st A in the topology of K holds
diameter A <= it ) & ( for r being real number st ( for A being Subset of M st A in the topology of K holds
diameter A <= r ) holds
r >= it ) ) if the topology of K meets bool ([#] M)
otherwise it = 0 ;
existence
( ( the topology of K meets bool ([#] M) implies ex b1 being Real st
( ( for A being Subset of M st A in the topology of K holds
diameter A <= b1 ) & ( for r being real number st ( for A being Subset of M st A in the topology of K holds
diameter A <= r ) holds
r >= b1 ) ) ) & ( not the topology of K meets bool ([#] M) implies ex b1 being Real st b1 = 0 ) )
proof
( the topology of K meets bool ([#] M) implies ex d being Real st
( ( for A being Subset of M st A in the topology of K holds
diameter A <= d ) & ( for r being real number st ( for A being Subset of M st A in the topology of K holds
diameter A <= r ) holds
r >= d ) ) )
proof
defpred S1[ Subset of M] means ( $1 in the topology of K & $1 is bounded );
deffunc H1( Subset of M) -> Element of REAL = diameter $1;
set X = { H1(S) where S is Subset of M : S1[S] } ;
now__::_thesis:_for_x_being_set_st_x_in__{__H1(S)_where_S_is_Subset_of_M_:_S1[S]__}__holds_
x_is_real
let x be set ; ::_thesis: ( x in { H1(S) where S is Subset of M : S1[S] } implies x is real )
assume x in { H1(S) where S is Subset of M : S1[S] } ; ::_thesis: x is real
then ex S being Subset of M st
( x = H1(S) & S1[S] ) ;
hence x is real ; ::_thesis: verum
end;
then reconsider X = { H1(S) where S is Subset of M : S1[S] } as real-membered set by MEMBERED:def_3;
assume the topology of K meets bool ([#] M) ; ::_thesis: ex d being Real st
( ( for A being Subset of M st A in the topology of K holds
diameter A <= d ) & ( for r being real number st ( for A being Subset of M st A in the topology of K holds
diameter A <= r ) holds
r >= d ) )
then consider B being set such that
A1: B in the topology of K and
A2: B in bool ([#] M) by XBOOLE_0:3;
reconsider B = B as Subset of M by A2;
consider rr being real number such that
A3: for A being Subset of M st A in the topology of K holds
( A is bounded & H1(A) <= rr ) by B1, Def2;
now__::_thesis:_for_x_being_ext-real_number_st_x_in_X_holds_
x_<=_rr
let x be ext-real number ; ::_thesis: ( x in X implies x <= rr )
assume x in X ; ::_thesis: x <= rr
then consider s being Subset of M such that
A4: ( x = H1(s) & S1[s] ) ;
thus x <= rr by A3, A4; ::_thesis: verum
end;
then rr is UpperBound of X by XXREAL_2:def_1;
then A5: X is bounded_above by XXREAL_2:def_10;
B is bounded by A1, A3;
then H1(B) in X by A1;
then reconsider sX = sup X as Real by A5, XXREAL_2:16;
take sX ; ::_thesis: ( ( for A being Subset of M st A in the topology of K holds
diameter A <= sX ) & ( for r being real number st ( for A being Subset of M st A in the topology of K holds
diameter A <= r ) holds
r >= sX ) )
hereby ::_thesis: for r being real number st ( for A being Subset of M st A in the topology of K holds
diameter A <= r ) holds
r >= sX
let A be Subset of M; ::_thesis: ( A in the topology of K implies H1(A) <= sX )
assume A in the topology of K ; ::_thesis: H1(A) <= sX
then S1[A] by A3;
then H1(A) in X ;
hence H1(A) <= sX by XXREAL_2:4; ::_thesis: verum
end;
let r be real number ; ::_thesis: ( ( for A being Subset of M st A in the topology of K holds
diameter A <= r ) implies r >= sX )
assume A6: for A being Subset of M st A in the topology of K holds
diameter A <= r ; ::_thesis: r >= sX
now__::_thesis:_for_x_being_ext-real_number_st_x_in_X_holds_
x_<=_r
let x be ext-real number ; ::_thesis: ( x in X implies x <= r )
assume x in X ; ::_thesis: x <= r
then consider A being Subset of M such that
A7: ( x = H1(A) & S1[A] ) ;
thus x <= r by A6, A7; ::_thesis: verum
end;
then r is UpperBound of X by XXREAL_2:def_1;
hence r >= sX by XXREAL_2:def_3; ::_thesis: verum
end;
hence ( ( the topology of K meets bool ([#] M) implies ex b1 being Real st
( ( for A being Subset of M st A in the topology of K holds
diameter A <= b1 ) & ( for r being real number st ( for A being Subset of M st A in the topology of K holds
diameter A <= r ) holds
r >= b1 ) ) ) & ( not the topology of K meets bool ([#] M) implies ex b1 being Real st b1 = 0 ) ) by Lm1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Real holds
( ( the topology of K meets bool ([#] M) & ( for A being Subset of M st A in the topology of K holds
diameter A <= b1 ) & ( for r being real number st ( for A being Subset of M st A in the topology of K holds
diameter A <= r ) holds
r >= b1 ) & ( for A being Subset of M st A in the topology of K holds
diameter A <= b2 ) & ( for r being real number st ( for A being Subset of M st A in the topology of K holds
diameter A <= r ) holds
r >= b2 ) implies b1 = b2 ) & ( not the topology of K meets bool ([#] M) & b1 = 0 & b2 = 0 implies b1 = b2 ) )
proof
now__::_thesis:_for_r1,_r2_being_Real_st_(_for_A_being_Subset_of_M_st_A_in_the_topology_of_K_holds_
diameter_A_<=_r1_)_&_(_for_r_being_real_number_st_(_for_A_being_Subset_of_M_st_A_in_the_topology_of_K_holds_
diameter_A_<=_r_)_holds_
r_>=_r1_)_&_(_for_A_being_Subset_of_M_st_A_in_the_topology_of_K_holds_
diameter_A_<=_r2_)_&_(_for_r_being_real_number_st_(_for_A_being_Subset_of_M_st_A_in_the_topology_of_K_holds_
diameter_A_<=_r_)_holds_
r_>=_r2_)_holds_
r1_=_r2
let r1, r2 be Real; ::_thesis: ( ( for A being Subset of M st A in the topology of K holds
diameter A <= r1 ) & ( for r being real number st ( for A being Subset of M st A in the topology of K holds
diameter A <= r ) holds
r >= r1 ) & ( for A being Subset of M st A in the topology of K holds
diameter A <= r2 ) & ( for r being real number st ( for A being Subset of M st A in the topology of K holds
diameter A <= r ) holds
r >= r2 ) implies r1 = r2 )
assume A8: ( ( for A being Subset of M st A in the topology of K holds
diameter A <= r1 ) & ( for r being real number st ( for A being Subset of M st A in the topology of K holds
diameter A <= r ) holds
r >= r1 ) & ( for A being Subset of M st A in the topology of K holds
diameter A <= r2 ) & ( for r being real number st ( for A being Subset of M st A in the topology of K holds
diameter A <= r ) holds
r >= r2 ) ) ; ::_thesis: r1 = r2
( r1 <= r2 & r2 <= r1 ) by A8;
hence r1 = r2 by XXREAL_0:1; ::_thesis: verum
end;
hence for b1, b2 being Real holds
( ( the topology of K meets bool ([#] M) & ( for A being Subset of M st A in the topology of K holds
diameter A <= b1 ) & ( for r being real number st ( for A being Subset of M st A in the topology of K holds
diameter A <= r ) holds
r >= b1 ) & ( for A being Subset of M st A in the topology of K holds
diameter A <= b2 ) & ( for r being real number st ( for A being Subset of M st A in the topology of K holds
diameter A <= r ) holds
r >= b2 ) implies b1 = b2 ) & ( not the topology of K meets bool ([#] M) & b1 = 0 & b2 = 0 implies b1 = b2 ) ) ; ::_thesis: verum
end;
consistency
for b1 being Real holds verum ;
end;
:: deftheorem Def3 defines diameter SIMPLEX2:def_3_:_
for M being non empty Reflexive MetrStruct
for K being SimplicialComplexStr st K is M bounded holds
for b3 being Real holds
( ( the topology of K meets bool ([#] M) implies ( b3 = diameter (M,K) iff ( ( for A being Subset of M st A in the topology of K holds
diameter A <= b3 ) & ( for r being real number st ( for A being Subset of M st A in the topology of K holds
diameter A <= r ) holds
r >= b3 ) ) ) ) & ( not the topology of K meets bool ([#] M) implies ( b3 = diameter (M,K) iff b3 = 0 ) ) );
theorem Th7: :: SIMPLEX2:7
for M being non empty Reflexive MetrStruct
for K being SimplicialComplexStr st K is M bounded holds
0 <= diameter (M,K)
proof
let M be non empty Reflexive MetrStruct ; ::_thesis: for K being SimplicialComplexStr st K is M bounded holds
0 <= diameter (M,K)
let K be SimplicialComplexStr; ::_thesis: ( K is M bounded implies 0 <= diameter (M,K) )
assume A1: K is M bounded ; ::_thesis: 0 <= diameter (M,K)
percases ( the topology of K meets bool ([#] M) or the topology of K misses bool ([#] M) ) ;
supposeA2: the topology of K meets bool ([#] M) ; ::_thesis: 0 <= diameter (M,K)
then consider S being set such that
A3: S in the topology of K and
A4: S in bool ([#] M) by XBOOLE_0:3;
reconsider S = S as Subset of M by A4;
ex r being real number st
for A being Subset of M st A in the topology of K holds
( A is bounded & diameter A <= r ) by A1, Def2;
then diameter S >= 0 by A3, TBSP_1:21;
hence 0 <= diameter (M,K) by A1, A2, A3, Def3; ::_thesis: verum
end;
suppose the topology of K misses bool ([#] M) ; ::_thesis: 0 <= diameter (M,K)
hence 0 <= diameter (M,K) by A1, Def3; ::_thesis: verum
end;
end;
end;
theorem :: SIMPLEX2:8
for X being set
for M being non empty Reflexive MetrStruct
for K being b2 bounded SimplicialComplexStr of X
for KX being SubSimplicialComplex of K holds diameter (M,KX) <= diameter (M,K)
proof
let X be set ; ::_thesis: for M being non empty Reflexive MetrStruct
for K being b1 bounded SimplicialComplexStr of X
for KX being SubSimplicialComplex of K holds diameter (M,KX) <= diameter (M,K)
let M be non empty Reflexive MetrStruct ; ::_thesis: for K being M bounded SimplicialComplexStr of X
for KX being SubSimplicialComplex of K holds diameter (M,KX) <= diameter (M,K)
let K be M bounded SimplicialComplexStr of X; ::_thesis: for KX being SubSimplicialComplex of K holds diameter (M,KX) <= diameter (M,K)
let KX be SubSimplicialComplex of K; ::_thesis: diameter (M,KX) <= diameter (M,K)
A1: the topology of KX c= the topology of K by SIMPLEX0:def_13;
percases ( the topology of KX meets bool ([#] M) or the topology of KX misses bool ([#] M) ) ;
supposeA2: the topology of KX meets bool ([#] M) ; ::_thesis: diameter (M,KX) <= diameter (M,K)
then the topology of K meets bool ([#] M) by A1, XBOOLE_1:63;
then for A being Subset of M st A in the topology of KX holds
diameter A <= diameter (M,K) by A1, Def3;
hence diameter (M,KX) <= diameter (M,K) by A2, Def3; ::_thesis: verum
end;
suppose the topology of KX misses bool ([#] M) ; ::_thesis: diameter (M,KX) <= diameter (M,K)
then diameter (M,KX) = 0 by Def3;
hence diameter (M,KX) <= diameter (M,K) by Th7; ::_thesis: verum
end;
end;
end;
theorem :: SIMPLEX2:9
for X being set
for M being non empty Reflexive MetrStruct
for K being subset-closed b2 bounded SimplicialComplexStr of X
for i being Integer holds diameter (M,(Skeleton_of (K,i))) <= diameter (M,K)
proof
let X be set ; ::_thesis: for M being non empty Reflexive MetrStruct
for K being subset-closed b1 bounded SimplicialComplexStr of X
for i being Integer holds diameter (M,(Skeleton_of (K,i))) <= diameter (M,K)
let M be non empty Reflexive MetrStruct ; ::_thesis: for K being subset-closed M bounded SimplicialComplexStr of X
for i being Integer holds diameter (M,(Skeleton_of (K,i))) <= diameter (M,K)
set r = the Real;
let K be subset-closed M bounded SimplicialComplexStr of X; ::_thesis: for i being Integer holds diameter (M,(Skeleton_of (K,i))) <= diameter (M,K)
let i be Integer; ::_thesis: diameter (M,(Skeleton_of (K,i))) <= diameter (M,K)
set SK = Skeleton_of (K,i);
A1: the topology of (Skeleton_of (K,i)) c= the topology of K by SIMPLEX0:def_13;
percases ( the topology of (Skeleton_of (K,i)) meets bool ([#] M) or the topology of (Skeleton_of (K,i)) misses bool ([#] M) ) ;
supposeA2: the topology of (Skeleton_of (K,i)) meets bool ([#] M) ; ::_thesis: diameter (M,(Skeleton_of (K,i))) <= diameter (M,K)
then A3: the topology of K meets bool ([#] M) by A1, XBOOLE_1:63;
now__::_thesis:_for_A_being_Subset_of_M_st_A_in_the_topology_of_(Skeleton_of_(K,i))_holds_
diameter_A_<=_diameter_(M,K)
let A be Subset of M; ::_thesis: ( A in the topology of (Skeleton_of (K,i)) implies diameter A <= diameter (M,K) )
the_family_of K is subset-closed by MATROID0:def_3;
then A4: the topology of K is subset-closed by MATROID0:def_1;
assume A in the topology of (Skeleton_of (K,i)) ; ::_thesis: diameter A <= diameter (M,K)
then consider w being set such that
A5: A c= w and
A6: w in the_subsets_with_limited_card ((i + 1), the topology of K) by SIMPLEX0:2;
reconsider w = w as Subset of K by A6;
w in the topology of K by A6, SIMPLEX0:def_2;
then A in the topology of K by A4, A5, CLASSES1:def_1;
hence diameter A <= diameter (M,K) by A3, Def3; ::_thesis: verum
end;
hence diameter (M,(Skeleton_of (K,i))) <= diameter (M,K) by A2, Def3; ::_thesis: verum
end;
suppose the topology of (Skeleton_of (K,i)) misses bool ([#] M) ; ::_thesis: diameter (M,(Skeleton_of (K,i))) <= diameter (M,K)
then diameter (M,(Skeleton_of (K,i))) = 0 by Def3;
hence diameter (M,(Skeleton_of (K,i))) <= diameter (M,K) by Th7; ::_thesis: verum
end;
end;
end;
definition
let M be non empty Reflexive MetrStruct ;
let K be non void subset-closed M bounded SimplicialComplexStr;
:: original: diameter
redefine func diameter (M,K) -> Real means :Def4: :: SIMPLEX2:def 4
( ( for A being Subset of M st A is Simplex of K holds
diameter A <= it ) & ( for r being real number st ( for A being Subset of M st A is Simplex of K holds
diameter A <= r ) holds
r >= it ) );
coherence
diameter (M,K) is Real ;
compatibility
for b1 being Real holds
( b1 = diameter (M,K) iff ( ( for A being Subset of M st A is Simplex of K holds
diameter A <= b1 ) & ( for r being real number st ( for A being Subset of M st A is Simplex of K holds
diameter A <= r ) holds
r >= b1 ) ) )
proof
let d be Real; ::_thesis: ( d = diameter (M,K) iff ( ( for A being Subset of M st A is Simplex of K holds
diameter A <= d ) & ( for r being real number st ( for A being Subset of M st A is Simplex of K holds
diameter A <= r ) holds
r >= d ) ) )
{} K is simplex-like ;
then {} M in the topology of K by PRE_TOPC:def_2;
then A1: the topology of K meets bool ([#] M) by XBOOLE_0:3;
hereby ::_thesis: ( ( for A being Subset of M st A is Simplex of K holds
diameter A <= d ) & ( for r being real number st ( for A being Subset of M st A is Simplex of K holds
diameter A <= r ) holds
r >= d ) implies d = diameter (M,K) )
assume A2: d = diameter (M,K) ; ::_thesis: ( ( for A being Subset of M st A is Simplex of K holds
diameter A <= d ) & ( for r being real number st ( for A being Subset of M st A is Simplex of K holds
diameter A <= r ) holds
r >= d ) )
hereby ::_thesis: for r being real number st ( for A being Subset of M st A is Simplex of K holds
diameter A <= r ) holds
r >= d
let A be Subset of M; ::_thesis: ( A is Simplex of K implies diameter A <= d )
assume A is Simplex of K ; ::_thesis: diameter A <= d
then A in the topology of K by PRE_TOPC:def_2;
hence diameter A <= d by A1, A2, Def3; ::_thesis: verum
end;
let r be real number ; ::_thesis: ( ( for A being Subset of M st A is Simplex of K holds
diameter A <= r ) implies r >= d )
assume A3: for A being Subset of M st A is Simplex of K holds
diameter A <= r ; ::_thesis: r >= d
now__::_thesis:_for_A_being_Subset_of_M_st_A_in_the_topology_of_K_holds_
diameter_A_<=_r
let A be Subset of M; ::_thesis: ( A in the topology of K implies diameter A <= r )
assume A in the topology of K ; ::_thesis: diameter A <= r
then A is Simplex of K by PRE_TOPC:def_2;
hence diameter A <= r by A3; ::_thesis: verum
end;
hence r >= d by A1, A2, Def3; ::_thesis: verum
end;
assume that
A4: for A being Subset of M st A is Simplex of K holds
diameter A <= d and
A5: for r being real number st ( for A being Subset of M st A is Simplex of K holds
diameter A <= r ) holds
r >= d ; ::_thesis: d = diameter (M,K)
now__::_thesis:_for_A_being_Subset_of_M_st_A_in_the_topology_of_K_holds_
diameter_A_<=_d
let A be Subset of M; ::_thesis: ( A in the topology of K implies diameter A <= d )
assume A in the topology of K ; ::_thesis: diameter A <= d
then A is Simplex of K by PRE_TOPC:def_2;
hence diameter A <= d by A4; ::_thesis: verum
end;
then A6: diameter (M,K) <= d by A1, Def3;
now__::_thesis:_for_A_being_Subset_of_M_st_A_is_Simplex_of_K_holds_
diameter_A_<=_diameter_(M,K)
let A be Subset of M; ::_thesis: ( A is Simplex of K implies diameter A <= diameter (M,K) )
assume A is Simplex of K ; ::_thesis: diameter A <= diameter (M,K)
then A in the topology of K by PRE_TOPC:def_2;
hence diameter A <= diameter (M,K) by A1, Def3; ::_thesis: verum
end;
then d <= diameter (M,K) by A5;
hence d = diameter (M,K) by A6, XXREAL_0:1; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines diameter SIMPLEX2:def_4_:_
for M being non empty Reflexive MetrStruct
for K being non void subset-closed b1 bounded SimplicialComplexStr
for b3 being Real holds
( b3 = diameter (M,K) iff ( ( for A being Subset of M st A is Simplex of K holds
diameter A <= b3 ) & ( for r being real number st ( for A being Subset of M st A is Simplex of K holds
diameter A <= r ) holds
r >= b3 ) ) );
theorem :: SIMPLEX2:10
for M being non empty Reflexive MetrStruct
for S being finite Subset of M holds diameter (M,(Complex_of {S})) = diameter S
proof
let M be non empty Reflexive MetrStruct ; ::_thesis: for S being finite Subset of M holds diameter (M,(Complex_of {S})) = diameter S
let S be finite Subset of M; ::_thesis: diameter (M,(Complex_of {S})) = diameter S
set C = Complex_of {S};
reconsider C = Complex_of {S} as non void M bounded SimplicialComplex of M by Th6;
reconsider s = S as Subset of C ;
A1: the topology of C = bool S by SIMPLEX0:4;
now__::_thesis:_for_W_being_Subset_of_M_st_W_is_Simplex_of_C_holds_
diameter_W_<=_diameter_S
let W be Subset of M; ::_thesis: ( W is Simplex of C implies diameter W <= diameter S )
assume W is Simplex of C ; ::_thesis: diameter W <= diameter S
then W in bool S by A1, PRE_TOPC:def_2;
hence diameter W <= diameter S by TBSP_1:24; ::_thesis: verum
end;
then A2: diameter (M,C) <= diameter S by Def4;
S c= S ;
then s is simplex-like by A1, PRE_TOPC:def_2;
then diameter S <= diameter (M,C) by Def4;
hence diameter (M,(Complex_of {S})) = diameter S by A2, XXREAL_0:1; ::_thesis: verum
end;
definition
let n be Nat;
let K be SimplicialComplexStr of (TOP-REAL n);
attrK is bounded means :Def5: :: SIMPLEX2:def 5
K is Euclid n bounded ;
func diameter K -> Real equals :: SIMPLEX2:def 6
diameter ((Euclid n),K);
coherence
diameter ((Euclid n),K) is Real ;
end;
:: deftheorem Def5 defines bounded SIMPLEX2:def_5_:_
for n being Nat
for K being SimplicialComplexStr of (TOP-REAL n) holds
( K is bounded iff K is Euclid n bounded );
:: deftheorem defines diameter SIMPLEX2:def_6_:_
for n being Nat
for K being SimplicialComplexStr of (TOP-REAL n) holds diameter K = diameter ((Euclid n),K);
registration
let n be Nat;
cluster bounded -> Euclid n bounded for SimplicialComplexStr of the carrier of (TOP-REAL n);
coherence
for b1 being SimplicialComplexStr of (TOP-REAL n) st b1 is bounded holds
b1 is Euclid n bounded by Def5;
cluster non void subset-closed finite-membered finite-degree total affinely-independent simplex-join-closed bounded for SimplicialComplexStr of the carrier of (TOP-REAL n);
existence
ex b1 being SimplicialComplex of (TOP-REAL n) st
( b1 is bounded & b1 is affinely-independent & b1 is simplex-join-closed & not b1 is void & b1 is finite-degree & b1 is total )
proof
set T = TOP-REAL n;
take C = Complex_of {({} (TOP-REAL n))}; ::_thesis: ( C is bounded & C is affinely-independent & C is simplex-join-closed & not C is void & C is finite-degree & C is total )
C is Euclid n bounded by Th6;
hence ( C is bounded & C is affinely-independent & C is simplex-join-closed & not C is void & C is finite-degree & C is total ) by Def5; ::_thesis: verum
end;
cluster finite-vertices -> bounded for SimplicialComplexStr of the carrier of (TOP-REAL n);
coherence
for b1 being SimplicialComplexStr of (TOP-REAL n) st b1 is finite-vertices holds
b1 is bounded
proof
let K be SimplicialComplexStr of (TOP-REAL n); ::_thesis: ( K is finite-vertices implies K is bounded )
assume K is finite-vertices ; ::_thesis: K is bounded
then K is Euclid n bounded by Th6;
hence K is bounded by Def5; ::_thesis: verum
end;
end;
Lm2: for n being Nat holds [#] (TOP-REAL n) = [#] (Euclid n)
proof
let n be Nat; ::_thesis: [#] (TOP-REAL n) = [#] (Euclid n)
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
hence [#] (TOP-REAL n) = [#] (Euclid n) ; ::_thesis: verum
end;
begin
Lm3: for x being set holds {x} is c=-linear
proof
let x be set ; ::_thesis: {x} is c=-linear
let y, z be set ; :: according to ORDINAL1:def_8 ::_thesis: ( not y in {x} or not z in {x} or y,z are_c=-comparable )
assume that
A1: y in {x} and
A2: z in {x} ; ::_thesis: y,z are_c=-comparable
y = x by A1, TARSKI:def_1;
hence y,z are_c=-comparable by A2, TARSKI:def_1; ::_thesis: verum
end;
theorem Th11: :: SIMPLEX2:11
for V being RealLinearSpace
for Kv being non void SimplicialComplex of V
for S being Simplex of (BCS Kv)
for F being c=-linear finite finite-membered Subset-Family of V st S = (center_of_mass V) .: F holds
for a1, a2 being VECTOR of V st a1 in S & a2 in S holds
ex b1, b2 being VECTOR of V ex r being Real st
( b1 in Vertices (BCS (Complex_of {(union F)})) & b2 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = r * (b1 - b2) & 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) )
proof
let V be RealLinearSpace; ::_thesis: for Kv being non void SimplicialComplex of V
for S being Simplex of (BCS Kv)
for F being c=-linear finite finite-membered Subset-Family of V st S = (center_of_mass V) .: F holds
for a1, a2 being VECTOR of V st a1 in S & a2 in S holds
ex b1, b2 being VECTOR of V ex r being Real st
( b1 in Vertices (BCS (Complex_of {(union F)})) & b2 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = r * (b1 - b2) & 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) )
let Kv be non void SimplicialComplex of V; ::_thesis: for S being Simplex of (BCS Kv)
for F being c=-linear finite finite-membered Subset-Family of V st S = (center_of_mass V) .: F holds
for a1, a2 being VECTOR of V st a1 in S & a2 in S holds
ex b1, b2 being VECTOR of V ex r being Real st
( b1 in Vertices (BCS (Complex_of {(union F)})) & b2 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = r * (b1 - b2) & 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) )
let S be Simplex of (BCS Kv); ::_thesis: for F being c=-linear finite finite-membered Subset-Family of V st S = (center_of_mass V) .: F holds
for a1, a2 being VECTOR of V st a1 in S & a2 in S holds
ex b1, b2 being VECTOR of V ex r being Real st
( b1 in Vertices (BCS (Complex_of {(union F)})) & b2 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = r * (b1 - b2) & 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) )
set cM = center_of_mass V;
let F be c=-linear finite finite-membered Subset-Family of V; ::_thesis: ( S = (center_of_mass V) .: F implies for a1, a2 being VECTOR of V st a1 in S & a2 in S holds
ex b1, b2 being VECTOR of V ex r being Real st
( b1 in Vertices (BCS (Complex_of {(union F)})) & b2 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = r * (b1 - b2) & 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) ) )
assume A1: S = (center_of_mass V) .: F ; ::_thesis: for a1, a2 being VECTOR of V st a1 in S & a2 in S holds
ex b1, b2 being VECTOR of V ex r being Real st
( b1 in Vertices (BCS (Complex_of {(union F)})) & b2 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = r * (b1 - b2) & 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) )
let a1, a2 be VECTOR of V; ::_thesis: ( a1 in S & a2 in S implies ex b1, b2 being VECTOR of V ex r being Real st
( b1 in Vertices (BCS (Complex_of {(union F)})) & b2 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = r * (b1 - b2) & 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) ) )
assume that
A2: a1 in S and
A3: a2 in S ; ::_thesis: ex b1, b2 being VECTOR of V ex r being Real st
( b1 in Vertices (BCS (Complex_of {(union F)})) & b2 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = r * (b1 - b2) & 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) )
consider A1 being set such that
A4: A1 in dom (center_of_mass V) and
A5: A1 in F and
A6: (center_of_mass V) . A1 = a1 by A1, A2, FUNCT_1:def_6;
consider A2 being set such that
A7: A2 in dom (center_of_mass V) and
A8: A2 in F and
A9: (center_of_mass V) . A2 = a2 by A1, A3, FUNCT_1:def_6;
A10: A1,A2 are_c=-comparable by A5, A8, ORDINAL1:def_8;
set uF = union F;
set CuF = Complex_of {(union F)};
A11: for a1, a2 being VECTOR of V
for A1, A2 being set st A1 c= A2 & A1 in dom (center_of_mass V) & A1 in F & (center_of_mass V) . A1 = a1 & A1 in dom (center_of_mass V) & A2 in F & (center_of_mass V) . A2 = a2 holds
ex b1, b2 being VECTOR of V ex r being Real st
( b1 in Vertices (BCS (Complex_of {(union F)})) & b2 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = r * (b1 - b2) & 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) )
proof
let a1, a2 be VECTOR of V; ::_thesis: for A1, A2 being set st A1 c= A2 & A1 in dom (center_of_mass V) & A1 in F & (center_of_mass V) . A1 = a1 & A1 in dom (center_of_mass V) & A2 in F & (center_of_mass V) . A2 = a2 holds
ex b1, b2 being VECTOR of V ex r being Real st
( b1 in Vertices (BCS (Complex_of {(union F)})) & b2 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = r * (b1 - b2) & 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) )
A12: the topology of (Complex_of {(union F)}) = bool (union F) by SIMPLEX0:4;
let A1, A2 be set ; ::_thesis: ( A1 c= A2 & A1 in dom (center_of_mass V) & A1 in F & (center_of_mass V) . A1 = a1 & A1 in dom (center_of_mass V) & A2 in F & (center_of_mass V) . A2 = a2 implies ex b1, b2 being VECTOR of V ex r being Real st
( b1 in Vertices (BCS (Complex_of {(union F)})) & b2 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = r * (b1 - b2) & 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) ) )
assume that
A13: A1 c= A2 and
A14: A1 in dom (center_of_mass V) and
A15: A1 in F and
A16: (center_of_mass V) . A1 = a1 and
A1 in dom (center_of_mass V) and
A17: A2 in F and
A18: (center_of_mass V) . A2 = a2 ; ::_thesis: ex b1, b2 being VECTOR of V ex r being Real st
( b1 in Vertices (BCS (Complex_of {(union F)})) & b2 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = r * (b1 - b2) & 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) )
A19: A1 c= union F by A15, ZFMISC_1:74;
A20: A1 <> {} by A14, ORDERS_1:1;
then A21: not union F is empty by A19;
A22: A2 c= union F by A17, ZFMISC_1:74;
reconsider A1 = A1, A2 = A2 as non empty finite Subset of V by A13, A15, A17, A20;
set A21 = A2 \ A1;
reconsider AA1 = {A1}, AA2 = {(A2 \ A1)} as Subset-Family of (Complex_of {(union F)}) ;
{A1} c= bool (union F) by A19, ZFMISC_1:31;
then A23: ( AA1 is c=-linear & AA1 is finite & AA1 is simplex-like ) by A12, Lm3, SIMPLEX0:14;
A2 \ A1 c= A2 by XBOOLE_1:36;
then A2 \ A1 c= union F by A22, XBOOLE_1:1;
then {(A2 \ A1)} c= bool (union F) by ZFMISC_1:31;
then A24: ( AA2 is c=-linear & AA2 is finite & AA2 is simplex-like ) by A12, Lm3, SIMPLEX0:14;
A25: |.(Complex_of {(union F)}).| c= [#] V ;
[#] (Complex_of {(union F)}) = [#] V ;
then A26: BCS (Complex_of {(union F)}) = subdivision ((center_of_mass V),(Complex_of {(union F)})) by A25, SIMPLEX1:def_5;
A27: [#] (subdivision ((center_of_mass V),(Complex_of {(union F)}))) = [#] (Complex_of {(union F)}) by SIMPLEX0:def_20;
then reconsider aa1 = {a1} as Subset of (BCS (Complex_of {(union F)})) by A25, SIMPLEX1:def_5;
A28: a1 in aa1 by TARSKI:def_1;
then reconsider d1 = a1 as Element of (BCS (Complex_of {(union F)})) ;
A29: dom (center_of_mass V) = BOOL the carrier of V by FUNCT_2:def_1;
(center_of_mass V) .: AA1 = Im ((center_of_mass V),A1) by RELAT_1:def_16
.= {a1} by A14, A16, FUNCT_1:59 ;
then aa1 is simplex-like by A23, A26, SIMPLEX0:def_20;
then A30: d1 is vertex-like by A28, SIMPLEX0:def_3;
percases ( A1 = A2 or A1 <> A2 ) ;
supposeA31: A1 = A2 ; ::_thesis: ex b1, b2 being VECTOR of V ex r being Real st
( b1 in Vertices (BCS (Complex_of {(union F)})) & b2 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = r * (b1 - b2) & 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) )
reconsider Z = 0 as Real by XREAL_0:def_1;
take b1 = a1; ::_thesis: ex b2 being VECTOR of V ex r being Real st
( b1 in Vertices (BCS (Complex_of {(union F)})) & b2 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = r * (b1 - b2) & 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) )
take b2 = a1; ::_thesis: ex r being Real st
( b1 in Vertices (BCS (Complex_of {(union F)})) & b2 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = r * (b1 - b2) & 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) )
take Z ; ::_thesis: ( b1 in Vertices (BCS (Complex_of {(union F)})) & b2 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = Z * (b1 - b2) & 0 <= Z & Z <= ((card (union F)) - 1) / (card (union F)) )
card (union F) >= 1 by A21, NAT_1:14;
then A32: (card (union F)) - 1 >= 1 - 1 by XREAL_1:6;
a1 - a2 = 0. V by A16, A18, A31, RLVECT_1:5;
hence ( b1 in Vertices (BCS (Complex_of {(union F)})) & b2 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = Z * (b1 - b2) & 0 <= Z & Z <= ((card (union F)) - 1) / (card (union F)) ) by A30, A32, RLVECT_1:10, SIMPLEX0:def_4; ::_thesis: verum
end;
suppose A1 <> A2 ; ::_thesis: ex b1, b2 being VECTOR of V ex r being Real st
( b1 in Vertices (BCS (Complex_of {(union F)})) & b2 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = r * (b1 - b2) & 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) )
then not A2 c= A1 by A13, XBOOLE_0:def_10;
then reconsider A21 = A2 \ A1 as non empty finite Subset of V by XBOOLE_1:37;
A33: A21 in dom (center_of_mass V) by A29, ORDERS_1:2;
then (center_of_mass V) . A21 in rng (center_of_mass V) by FUNCT_1:def_3;
then reconsider a21 = (center_of_mass V) . A21 as VECTOR of V ;
reconsider aa2 = {a21} as Subset of (BCS (Complex_of {(union F)})) by A25, A27, SIMPLEX1:def_5;
A34: a21 in aa2 by TARSKI:def_1;
then reconsider d2 = a21 as Element of (BCS (Complex_of {(union F)})) ;
(center_of_mass V) .: AA2 = Im ((center_of_mass V),A21) by RELAT_1:def_16
.= {a21} by A33, FUNCT_1:59 ;
then aa2 is simplex-like by A24, A26, SIMPLEX0:def_20;
then A35: d2 is vertex-like by A34, SIMPLEX0:def_3;
set r1 = 1 / (card A1);
set r2 = 1 / (card A2);
set r21 = 1 / (card A21);
set r = (card A21) / (card A2);
reconsider r1 = 1 / (card A1), r2 = 1 / (card A2), r21 = 1 / (card A21), r = (card A21) / (card A2) as Real by XREAL_0:def_1;
take a1 ; ::_thesis: ex b2 being VECTOR of V ex r being Real st
( a1 in Vertices (BCS (Complex_of {(union F)})) & b2 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = r * (a1 - b2) & 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) )
take a21 ; ::_thesis: ex r being Real st
( a1 in Vertices (BCS (Complex_of {(union F)})) & a21 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = r * (a1 - a21) & 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) )
take r ; ::_thesis: ( a1 in Vertices (BCS (Complex_of {(union F)})) & a21 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = r * (a1 - a21) & 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) )
A36: r * r21 = ((card A21) * 1) / ((card A21) * (card A2)) by XCMPLX_1:76
.= r2 by XCMPLX_1:91 ;
consider L1 being Linear_Combination of A1 such that
A37: Sum L1 = r1 * (Sum A1) and
sum L1 = r1 * (card A1) and
A38: L1 = (ZeroLC V) +* (A1 --> r1) by RLAFFIN2:15;
A39: Carrier L1 c= A1 by RLVECT_2:def_6;
A40: card A21 = (1 * (card A2)) - (1 * (card A1)) by A13, CARD_2:44;
then A41: r1 - r2 = ((card A21) * 1) / ((card A2) * (card A1)) by XCMPLX_1:130
.= r * r1 by XCMPLX_1:76 ;
consider L21 being Linear_Combination of A21 such that
A42: Sum L21 = r21 * (Sum A21) and
sum L21 = r21 * (card A21) and
A43: L21 = (ZeroLC V) +* (A21 --> r21) by RLAFFIN2:15;
A44: Carrier L21 c= A21 by RLVECT_2:def_6;
consider L2 being Linear_Combination of A2 such that
A45: Sum L2 = r2 * (Sum A2) and
sum L2 = r2 * (card A2) and
A46: L2 = (ZeroLC V) +* (A2 --> r2) by RLAFFIN2:15;
A47: Carrier L2 c= A2 by RLVECT_2:def_6;
for v being Element of V holds (L1 - L2) . v = (r * (L1 - L21)) . v
proof
let v be Element of V; ::_thesis: (L1 - L2) . v = (r * (L1 - L21)) . v
A48: dom (A21 --> r21) = A21 by FUNCOP_1:13;
A49: (L1 - L2) . v = (L1 . v) - (L2 . v) by RLVECT_2:54;
A50: dom (A1 --> r1) = A1 by FUNCOP_1:13;
A51: dom (A2 --> r2) = A2 by FUNCOP_1:13;
(r * (L1 - L21)) . v = r * ((L1 - L21) . v) by RLVECT_2:def_11;
then A52: (r * (L1 - L21)) . v = r * ((L1 . v) - (L21 . v)) by RLVECT_2:54;
percases ( v in A1 or ( v in A2 & not v in A1 ) or ( not v in A1 & not v in A2 ) ) ;
supposeA53: v in A1 ; ::_thesis: (L1 - L2) . v = (r * (L1 - L21)) . v
then not v in Carrier L21 by A44, XBOOLE_0:def_5;
then A54: L21 . v = 0 by RLVECT_2:19;
A55: ( (A2 --> r2) . v = r2 & (A1 --> r1) . v = r1 ) by A13, A53, FUNCOP_1:7;
L1 . v = (A1 --> r1) . v by A38, A50, A53, FUNCT_4:13;
hence (L1 - L2) . v = (r * (L1 - L21)) . v by A13, A41, A46, A49, A51, A52, A53, A54, A55, FUNCT_4:13; ::_thesis: verum
end;
supposeA56: ( v in A2 & not v in A1 ) ; ::_thesis: (L1 - L2) . v = (r * (L1 - L21)) . v
then not v in Carrier L1 by A39;
then A57: L1 . v = 0 by RLVECT_2:19;
(A2 --> r2) . v = r2 by A56, FUNCOP_1:7;
then A58: (L1 - L2) . v = - r2 by A46, A49, A51, A56, A57, FUNCT_4:13;
A59: v in A21 by A56, XBOOLE_0:def_5;
then (A21 --> r21) . v = r21 by FUNCOP_1:7;
then (r * (L1 - L21)) . v = r * (- r21) by A43, A48, A52, A57, A59, FUNCT_4:13;
hence (L1 - L2) . v = (r * (L1 - L21)) . v by A36, A58; ::_thesis: verum
end;
supposeA60: ( not v in A1 & not v in A2 ) ; ::_thesis: (L1 - L2) . v = (r * (L1 - L21)) . v
then not v in Carrier L1 by A39;
then A61: L1 . v = 0 by RLVECT_2:19;
not v in Carrier L21 by A44, A60, XBOOLE_0:def_5;
then A62: L21 . v = 0 by RLVECT_2:19;
not v in Carrier L2 by A47, A60;
hence (L1 - L2) . v = (r * (L1 - L21)) . v by A49, A52, A62, A61, RLVECT_2:19; ::_thesis: verum
end;
end;
end;
then A63: L1 - L2 = r * (L1 - L21) by RLVECT_2:def_9;
( card A1 >= 1 & card A2 <= card (union F) ) by A17, NAT_1:14, NAT_1:43, ZFMISC_1:74;
then (card A1) * (card (union F)) >= 1 * (card A2) by XREAL_1:66;
then ((card A2) * (card (union F))) - ((card A1) * (card (union F))) <= ((card (union F)) * (card A2)) - (card A2) by XREAL_1:13;
then A64: (card A21) * (card (union F)) <= ((card (union F)) - 1) * (card A2) by A40;
A65: Sum L21 = a21 by A42, RLAFFIN2:def_2;
A66: Sum L1 = a1 by A16, A37, RLAFFIN2:def_2;
Sum L2 = a2 by A18, A45, RLAFFIN2:def_2;
then a1 - a2 = Sum (r * (L1 - L21)) by A63, A66, RLVECT_3:4
.= r * (Sum (L1 - L21)) by RLVECT_3:2
.= r * (a1 - a21) by A65, A66, RLVECT_3:4 ;
hence ( a1 in Vertices (BCS (Complex_of {(union F)})) & a21 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = r * (a1 - a21) & 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) ) by A21, A30, A35, A64, SIMPLEX0:def_4, XREAL_1:102; ::_thesis: verum
end;
end;
end;
percases ( A1 c= A2 or A2 c= A1 ) by A10, XBOOLE_0:def_9;
suppose A1 c= A2 ; ::_thesis: ex b1, b2 being VECTOR of V ex r being Real st
( b1 in Vertices (BCS (Complex_of {(union F)})) & b2 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = r * (b1 - b2) & 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) )
hence ex b1, b2 being VECTOR of V ex r being Real st
( b1 in Vertices (BCS (Complex_of {(union F)})) & b2 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = r * (b1 - b2) & 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) ) by A4, A5, A6, A8, A9, A11; ::_thesis: verum
end;
suppose A2 c= A1 ; ::_thesis: ex b1, b2 being VECTOR of V ex r being Real st
( b1 in Vertices (BCS (Complex_of {(union F)})) & b2 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = r * (b1 - b2) & 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) )
then consider b1, b2 being VECTOR of V, r being Real such that
A67: ( b1 in Vertices (BCS (Complex_of {(union F)})) & b2 in Vertices (BCS (Complex_of {(union F)})) ) and
A68: a2 - a1 = r * (b1 - b2) and
A69: ( 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) ) by A5, A6, A7, A8, A9, A11;
take b2 ; ::_thesis: ex b2 being VECTOR of V ex r being Real st
( b2 in Vertices (BCS (Complex_of {(union F)})) & b2 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = r * (b2 - b2) & 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) )
take b1 ; ::_thesis: ex r being Real st
( b2 in Vertices (BCS (Complex_of {(union F)})) & b1 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = r * (b2 - b1) & 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) )
take r ; ::_thesis: ( b2 in Vertices (BCS (Complex_of {(union F)})) & b1 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = r * (b2 - b1) & 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) )
a1 - a2 = - (r * (b1 - b2)) by A68, RLVECT_1:33
.= r * (- (b1 - b2)) by RLVECT_1:25
.= r * (b2 - b1) by RLVECT_1:33 ;
hence ( b2 in Vertices (BCS (Complex_of {(union F)})) & b1 in Vertices (BCS (Complex_of {(union F)})) & a1 - a2 = r * (b2 - b1) & 0 <= r & r <= ((card (union F)) - 1) / (card (union F)) ) by A67, A69; ::_thesis: verum
end;
end;
end;
theorem Th12: :: SIMPLEX2:12
for n being Nat
for X being set
for A being affinely-independent Subset of (TOP-REAL n)
for E being Enumeration of A st not (dom E) \ X is empty holds
conv (E .: X) = meet { (conv (A \ {(E . k)})) where k is Element of NAT : k in (dom E) \ X }
proof
let n be Nat; ::_thesis: for X being set
for A being affinely-independent Subset of (TOP-REAL n)
for E being Enumeration of A st not (dom E) \ X is empty holds
conv (E .: X) = meet { (conv (A \ {(E . k)})) where k is Element of NAT : k in (dom E) \ X }
let X be set ; ::_thesis: for A being affinely-independent Subset of (TOP-REAL n)
for E being Enumeration of A st not (dom E) \ X is empty holds
conv (E .: X) = meet { (conv (A \ {(E . k)})) where k is Element of NAT : k in (dom E) \ X }
let A be affinely-independent Subset of (TOP-REAL n); ::_thesis: for E being Enumeration of A st not (dom E) \ X is empty holds
conv (E .: X) = meet { (conv (A \ {(E . k)})) where k is Element of NAT : k in (dom E) \ X }
let E be Enumeration of A; ::_thesis: ( not (dom E) \ X is empty implies conv (E .: X) = meet { (conv (A \ {(E . k)})) where k is Element of NAT : k in (dom E) \ X } )
assume A1: not (dom E) \ X is empty ; ::_thesis: conv (E .: X) = meet { (conv (A \ {(E . k)})) where k is Element of NAT : k in (dom E) \ X }
set d = dom E;
defpred S1[ Nat] means ( $1 <> 0 implies for X being set st card ((dom E) \ X) = $1 holds
conv (A \ (E .: ((dom E) \ X))) = meet { (conv (A \ {(E . k)})) where k is Element of NAT : k in (dom E) \ X } );
A2: rng E = A by RLAFFIN3:def_1;
A3: for i being Nat st S1[i] holds
S1[i + 1]
proof
deffunc H1( set ) -> Element of bool the carrier of (TOP-REAL n) = conv (A \ {(E . $1)});
let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A4: S1[i] ; ::_thesis: S1[i + 1]
set i1 = i + 1;
assume i + 1 <> 0 ; ::_thesis: for X being set st card ((dom E) \ X) = i + 1 holds
conv (A \ (E .: ((dom E) \ X))) = meet { (conv (A \ {(E . k)})) where k is Element of NAT : k in (dom E) \ X }
let X be set ; ::_thesis: ( card ((dom E) \ X) = i + 1 implies conv (A \ (E .: ((dom E) \ X))) = meet { (conv (A \ {(E . k)})) where k is Element of NAT : k in (dom E) \ X } )
set U = { H1(k) where k is Element of NAT : k in (dom E) \ X } ;
assume A5: card ((dom E) \ X) = i + 1 ; ::_thesis: conv (A \ (E .: ((dom E) \ X))) = meet { (conv (A \ {(E . k)})) where k is Element of NAT : k in (dom E) \ X }
then not (dom E) \ X is empty ;
then consider m being set such that
A6: m in (dom E) \ X by XBOOLE_0:def_1;
A7: m in dom E by A6, XBOOLE_0:def_5;
reconsider m = m as Element of NAT by A6;
A8: E .: {m} = Im (E,m) by RELAT_1:def_16
.= {(E . m)} by A7, FUNCT_1:59 ;
percases ( i = 0 or i > 0 ) ;
suppose i = 0 ; ::_thesis: conv (A \ (E .: ((dom E) \ X))) = meet { (conv (A \ {(E . k)})) where k is Element of NAT : k in (dom E) \ X }
then consider x being set such that
A9: (dom E) \ X = {x} by A5, CARD_2:42;
A10: x = m by A6, A9, TARSKI:def_1;
A11: { H1(k) where k is Element of NAT : k in (dom E) \ X } c= {H1(m)}
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { H1(k) where k is Element of NAT : k in (dom E) \ X } or u in {H1(m)} )
assume u in { H1(k) where k is Element of NAT : k in (dom E) \ X } ; ::_thesis: u in {H1(m)}
then ex k being Element of NAT st
( u = H1(k) & k in (dom E) \ X ) ;
then u = H1(m) by A9, A10, TARSKI:def_1;
hence u in {H1(m)} by TARSKI:def_1; ::_thesis: verum
end;
H1(m) in { H1(k) where k is Element of NAT : k in (dom E) \ X } by A6;
then A12: { H1(k) where k is Element of NAT : k in (dom E) \ X } = {H1(m)} by A11, ZFMISC_1:33;
E .: ((dom E) \ X) = {(E . m)} by A6, A8, A9, TARSKI:def_1;
hence conv (A \ (E .: ((dom E) \ X))) = meet { (conv (A \ {(E . k)})) where k is Element of NAT : k in (dom E) \ X } by A12, SETFAM_1:10; ::_thesis: verum
end;
supposeA13: i > 0 ; ::_thesis: conv (A \ (E .: ((dom E) \ X))) = meet { (conv (A \ {(E . k)})) where k is Element of NAT : k in (dom E) \ X }
set Xm = X \/ {m};
set Um = { H1(k) where k is Element of NAT : k in (dom E) \ (X \/ {m}) } ;
set t = the Element of (dom E) \ (X \/ {m});
A14: (((dom E) \ X) \ {m}) \/ {m} = (dom E) \ X by A6, ZFMISC_1:116;
A15: ((dom E) \ X) \ {m} = (dom E) \ (X \/ {m}) by XBOOLE_1:41;
A16: { H1(k) where k is Element of NAT : k in (dom E) \ (X \/ {m}) } c= { H1(k) where k is Element of NAT : k in (dom E) \ X }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { H1(k) where k is Element of NAT : k in (dom E) \ (X \/ {m}) } or x in { H1(k) where k is Element of NAT : k in (dom E) \ X } )
assume x in { H1(k) where k is Element of NAT : k in (dom E) \ (X \/ {m}) } ; ::_thesis: x in { H1(k) where k is Element of NAT : k in (dom E) \ X }
then consider k being Element of NAT such that
A17: x = H1(k) and
A18: k in (dom E) \ (X \/ {m}) ;
k in (dom E) \ X by A15, A14, A18, XBOOLE_0:def_3;
hence x in { H1(k) where k is Element of NAT : k in (dom E) \ X } by A17; ::_thesis: verum
end;
m in {m} by TARSKI:def_1;
then not m in ((dom E) \ X) \ {m} by XBOOLE_0:def_5;
then A19: (card (((dom E) \ X) \ {m})) + 1 = card ((dom E) \ X) by A14, CARD_2:41;
then not (dom E) \ (X \/ {m}) is empty by A5, A13, A15;
then the Element of (dom E) \ (X \/ {m}) in (dom E) \ (X \/ {m}) ;
then A20: H1( the Element of (dom E) \ (X \/ {m})) in { H1(k) where k is Element of NAT : k in (dom E) \ (X \/ {m}) } ;
set c = H1(m);
set CC = {H1(m)};
set CA = Complex_of {A};
A21: the topology of (Complex_of {A}) = bool A by SIMPLEX0:4;
A22: { H1(k) where k is Element of NAT : k in (dom E) \ X } c= { H1(k) where k is Element of NAT : k in (dom E) \ (X \/ {m}) } \/ {H1(m)}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { H1(k) where k is Element of NAT : k in (dom E) \ X } or x in { H1(k) where k is Element of NAT : k in (dom E) \ (X \/ {m}) } \/ {H1(m)} )
assume x in { H1(k) where k is Element of NAT : k in (dom E) \ X } ; ::_thesis: x in { H1(k) where k is Element of NAT : k in (dom E) \ (X \/ {m}) } \/ {H1(m)}
then consider k being Element of NAT such that
A23: x = H1(k) and
A24: k in (dom E) \ X ;
( k in (dom E) \ (X \/ {m}) or k in {m} ) by A15, A14, A24, XBOOLE_0:def_3;
then ( k in (dom E) \ (X \/ {m}) or k = m ) by TARSKI:def_1;
then ( x in { H1(k) where k is Element of NAT : k in (dom E) \ (X \/ {m}) } or x in {H1(m)} ) by A23, TARSKI:def_1;
hence x in { H1(k) where k is Element of NAT : k in (dom E) \ (X \/ {m}) } \/ {H1(m)} by XBOOLE_0:def_3; ::_thesis: verum
end;
H1(m) in { H1(k) where k is Element of NAT : k in (dom E) \ X } by A6;
then {H1(m)} c= { H1(k) where k is Element of NAT : k in (dom E) \ X } by ZFMISC_1:31;
then A25: { H1(k) where k is Element of NAT : k in (dom E) \ (X \/ {m}) } \/ {H1(m)} c= { H1(k) where k is Element of NAT : k in (dom E) \ X } by A16, XBOOLE_1:8;
reconsider A1 = A \ (E .: ((dom E) \ (X \/ {m}))), A2 = A \ {(E . m)} as Subset of (Complex_of {A}) ;
A \ {(E . m)} c= A by XBOOLE_1:36;
then A26: A2 is simplex-like by A21, PRE_TOPC:def_2;
A \ (E .: ((dom E) \ (X \/ {m}))) c= A by XBOOLE_1:36;
then A1 is simplex-like by A21, PRE_TOPC:def_2;
then A27: (conv (@ A1)) /\ (conv (@ A2)) = conv (@ (A1 /\ A2)) by A26, SIMPLEX1:def_8;
(E .: ((dom E) \ (X \/ {m}))) \/ {(E . m)} = E .: (((dom E) \ (X \/ {m})) \/ {m}) by A8, RELAT_1:120
.= E .: ((dom E) \ X) by A14, XBOOLE_1:41 ;
then A28: A1 /\ A2 = A \ (E .: ((dom E) \ X)) by XBOOLE_1:53;
conv (A \ (E .: ((dom E) \ (X \/ {m})))) = meet { H1(k) where k is Element of NAT : k in (dom E) \ (X \/ {m}) } by A4, A5, A13, A15, A19;
then conv (A \ (E .: ((dom E) \ X))) = (meet { H1(k) where k is Element of NAT : k in (dom E) \ (X \/ {m}) } ) /\ (meet {H1(m)}) by A28, A27, SETFAM_1:10
.= meet ( { H1(k) where k is Element of NAT : k in (dom E) \ (X \/ {m}) } \/ {H1(m)}) by A20, SETFAM_1:9 ;
hence conv (A \ (E .: ((dom E) \ X))) = meet { (conv (A \ {(E . k)})) where k is Element of NAT : k in (dom E) \ X } by A25, A22, XBOOLE_0:def_10; ::_thesis: verum
end;
end;
end;
A29: S1[ 0 ] ;
for i being Nat holds S1[i] from NAT_1:sch_2(A29, A3);
then A30: S1[ card ((dom E) \ X)] ;
(dom E) \ ((dom E) \ X) = (dom E) /\ X by XBOOLE_1:48;
then E .: X = E .: ((dom E) \ ((dom E) \ X)) by RELAT_1:112
.= (E .: (dom E)) \ (E .: ((dom E) \ X)) by FUNCT_1:64
.= A \ (E .: ((dom E) \ X)) by A2, RELAT_1:113 ;
hence conv (E .: X) = meet { (conv (A \ {(E . k)})) where k is Element of NAT : k in (dom E) \ X } by A1, A30; ::_thesis: verum
end;
theorem Th13: :: SIMPLEX2:13
for n being Nat
for A being Subset of (TOP-REAL n)
for a being bounded Subset of (Euclid n) st a = A holds
for p being Point of (Euclid n) st p in conv A holds
conv A c= cl_Ball (p,(diameter a))
proof
let n be Nat; ::_thesis: for A being Subset of (TOP-REAL n)
for a being bounded Subset of (Euclid n) st a = A holds
for p being Point of (Euclid n) st p in conv A holds
conv A c= cl_Ball (p,(diameter a))
let A be Subset of (TOP-REAL n); ::_thesis: for a being bounded Subset of (Euclid n) st a = A holds
for p being Point of (Euclid n) st p in conv A holds
conv A c= cl_Ball (p,(diameter a))
A1: n in NAT by ORDINAL1:def_12;
A2: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
let a be bounded Subset of (Euclid n); ::_thesis: ( a = A implies for p being Point of (Euclid n) st p in conv A holds
conv A c= cl_Ball (p,(diameter a)) )
assume A3: A = a ; ::_thesis: for p being Point of (Euclid n) st p in conv A holds
conv A c= cl_Ball (p,(diameter a))
let x be Point of (Euclid n); ::_thesis: ( x in conv A implies conv A c= cl_Ball (x,(diameter a)) )
assume A4: x in conv A ; ::_thesis: conv A c= cl_Ball (x,(diameter a))
A5: A c= cl_Ball (x,(diameter a))
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in A or p in cl_Ball (x,(diameter a)) )
assume A6: p in A ; ::_thesis: p in cl_Ball (x,(diameter a))
then reconsider p = p as Point of (Euclid n) by A3;
reconsider pp = p as Point of (TOP-REAL n) by A2;
A7: cl_Ball (p,(diameter a)) = cl_Ball (pp,(diameter a)) by A1, TOPREAL9:14;
A c= cl_Ball (p,(diameter a))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in A or y in cl_Ball (p,(diameter a)) )
assume A8: y in A ; ::_thesis: y in cl_Ball (p,(diameter a))
then reconsider q = y as Point of (Euclid n) by A3;
dist (p,q) <= diameter a by A3, A6, A8, TBSP_1:def_8;
hence y in cl_Ball (p,(diameter a)) by METRIC_1:12; ::_thesis: verum
end;
then conv A c= cl_Ball (pp,(diameter a)) by A7, CONVEX1:30;
then dist (p,x) <= diameter a by A4, A7, METRIC_1:12;
hence p in cl_Ball (x,(diameter a)) by METRIC_1:12; ::_thesis: verum
end;
reconsider xx = x as Point of (TOP-REAL n) by A2;
cl_Ball (x,(diameter a)) = cl_Ball (xx,(diameter a)) by A1, TOPREAL9:14;
hence conv A c= cl_Ball (x,(diameter a)) by A5, CONVEX1:30; ::_thesis: verum
end;
theorem Th14: :: SIMPLEX2:14
for n being Nat
for A being Subset of (TOP-REAL n) holds
( A is bounded iff conv A is bounded )
proof
let n be Nat; ::_thesis: for A being Subset of (TOP-REAL n) holds
( A is bounded iff conv A is bounded )
let A be Subset of (TOP-REAL n); ::_thesis: ( A is bounded iff conv A is bounded )
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
then reconsider cA = conv A, a = A as Subset of (Euclid n) ;
hereby ::_thesis: ( conv A is bounded implies A is bounded )
assume A is bounded ; ::_thesis: conv A is bounded
then reconsider a = a as bounded Subset of (Euclid n) by JORDAN2C:11;
set D = diameter a;
A1: now__::_thesis:_for_x,_y_being_Point_of_(Euclid_n)_st_x_in_cA_&_y_in_cA_holds_
dist_(x,y)_<=_(diameter_a)_+_1
let x, y be Point of (Euclid n); ::_thesis: ( x in cA & y in cA implies dist (x,y) <= (diameter a) + 1 )
assume x in cA ; ::_thesis: ( y in cA implies dist (x,y) <= (diameter a) + 1 )
then A2: conv A c= cl_Ball (x,(diameter a)) by Th13;
assume y in cA ; ::_thesis: dist (x,y) <= (diameter a) + 1
then dist (x,y) <= diameter a by A2, METRIC_1:12;
hence dist (x,y) <= (diameter a) + 1 by XREAL_1:39; ::_thesis: verum
end;
diameter a >= 0 by TBSP_1:21;
then cA is bounded by A1, TBSP_1:def_7;
hence conv A is bounded by JORDAN2C:11; ::_thesis: verum
end;
assume conv A is bounded ; ::_thesis: A is bounded
then cA is bounded by JORDAN2C:11;
then a is bounded by CONVEX1:41, TBSP_1:14;
hence A is bounded by JORDAN2C:11; ::_thesis: verum
end;
theorem Th15: :: SIMPLEX2:15
for n being Nat
for A being Subset of (TOP-REAL n)
for a, ca being bounded Subset of (Euclid n) st ca = conv A & a = A holds
diameter a = diameter ca
proof
let n be Nat; ::_thesis: for A being Subset of (TOP-REAL n)
for a, ca being bounded Subset of (Euclid n) st ca = conv A & a = A holds
diameter a = diameter ca
let A be Subset of (TOP-REAL n); ::_thesis: for a, ca being bounded Subset of (Euclid n) st ca = conv A & a = A holds
diameter a = diameter ca
let a, ca be bounded Subset of (Euclid n); ::_thesis: ( ca = conv A & a = A implies diameter a = diameter ca )
assume that
A1: ca = conv A and
A2: a = A ; ::_thesis: diameter a = diameter ca
percases ( a is empty or not a is empty ) ;
suppose a is empty ; ::_thesis: diameter a = diameter ca
hence diameter a = diameter ca by A1, A2; ::_thesis: verum
end;
supposeA3: not a is empty ; ::_thesis: diameter a = diameter ca
now__::_thesis:_for_x,_y_being_Point_of_(Euclid_n)_st_x_in_ca_&_y_in_ca_holds_
dist_(x,y)_<=_diameter_a
let x, y be Point of (Euclid n); ::_thesis: ( x in ca & y in ca implies dist (x,y) <= diameter a )
assume x in ca ; ::_thesis: ( y in ca implies dist (x,y) <= diameter a )
then A4: conv A c= cl_Ball (x,(diameter a)) by A1, A2, Th13;
assume y in ca ; ::_thesis: dist (x,y) <= diameter a
hence dist (x,y) <= diameter a by A1, A4, METRIC_1:12; ::_thesis: verum
end;
then A5: diameter ca <= diameter a by A1, A2, A3, TBSP_1:def_8;
diameter a <= diameter ca by A1, A2, CONVEX1:41, TBSP_1:24;
hence diameter a = diameter ca by A5, XXREAL_0:1; ::_thesis: verum
end;
end;
end;
registration
let n be Nat;
let K be bounded SimplicialComplexStr of (TOP-REAL n);
cluster -> bounded for SubdivisionStr of K;
coherence
for b1 being SubdivisionStr of K holds b1 is bounded
proof
let SK be SubdivisionStr of K; ::_thesis: SK is bounded
consider r being real number such that
A1: for A being Subset of (Euclid n) st A in the topology of K holds
( A is bounded & diameter A <= r ) by Def2;
take r ; :: according to SIMPLEX2:def_2,SIMPLEX2:def_5 ::_thesis: for A being Subset of (Euclid n) st A in the topology of SK holds
( A is bounded & diameter A <= r )
let A be Subset of (Euclid n); ::_thesis: ( A in the topology of SK implies ( A is bounded & diameter A <= r ) )
assume A2: A in the topology of SK ; ::_thesis: ( A is bounded & diameter A <= r )
then reconsider a = A as Subset of SK ;
a is simplex-like by A2, PRE_TOPC:def_2;
then consider b being Subset of K such that
A3: b is simplex-like and
A4: conv (@ a) c= conv (@ b) by SIMPLEX1:def_4;
A5: [#] (TOP-REAL n) = [#] (Euclid n) by Lm2;
then reconsider cA = conv (@ a) as Subset of (Euclid n) ;
[#] K c= [#] (TOP-REAL n) by SIMPLEX0:def_9;
then reconsider B = b as Subset of (Euclid n) by A5, XBOOLE_1:1;
A6: B in the topology of K by A3, PRE_TOPC:def_2;
then A7: diameter B <= r by A1;
A8: B is bounded by A1, A6;
then @ b is bounded by JORDAN2C:11;
then conv (@ b) is bounded by Th14;
then reconsider cB = conv (@ b) as bounded Subset of (Euclid n) by JORDAN2C:11;
A9: diameter cA <= diameter cB by A4, TBSP_1:24;
cA c= cB by A4;
then A10: cA is bounded by TBSP_1:14;
then A is bounded by CONVEX1:41, TBSP_1:14;
then A11: diameter cA = diameter A by A10, Th15;
diameter cB = diameter B by A8, Th15;
hence ( A is bounded & diameter A <= r ) by A9, A10, A11, A7, CONVEX1:41, TBSP_1:14, XXREAL_0:2; ::_thesis: verum
end;
end;
theorem Th16: :: SIMPLEX2:16
for n being Nat
for K being non void finite-degree bounded SimplicialComplex of (TOP-REAL n) st |.K.| c= [#] K holds
diameter (BCS K) <= ((degree K) / ((degree K) + 1)) * (diameter K)
proof
let n be Nat; ::_thesis: for K being non void finite-degree bounded SimplicialComplex of (TOP-REAL n) st |.K.| c= [#] K holds
diameter (BCS K) <= ((degree K) / ((degree K) + 1)) * (diameter K)
set T = TOP-REAL n;
let K be non void finite-degree bounded SimplicialComplex of (TOP-REAL n); ::_thesis: ( |.K.| c= [#] K implies diameter (BCS K) <= ((degree K) / ((degree K) + 1)) * (diameter K) )
set BK = BCS K;
set cM = center_of_mass (TOP-REAL n);
set dK = degree K;
assume |.K.| c= [#] K ; ::_thesis: diameter (BCS K) <= ((degree K) / ((degree K) + 1)) * (diameter K)
then A1: BCS K = subdivision ((center_of_mass (TOP-REAL n)),K) by SIMPLEX1:def_5;
for A being Subset of (Euclid n) st A is Simplex of (BCS K) holds
diameter A <= ((degree K) / ((degree K) + 1)) * (diameter K)
proof
let A be Subset of (Euclid n); ::_thesis: ( A is Simplex of (BCS K) implies diameter A <= ((degree K) / ((degree K) + 1)) * (diameter K) )
reconsider ONE = 1 as ext-real number ;
assume A2: A is Simplex of (BCS K) ; ::_thesis: diameter A <= ((degree K) / ((degree K) + 1)) * (diameter K)
then reconsider a = A as Simplex of (BCS K) ;
consider S being c=-linear finite simplex-like Subset-Family of K such that
A3: A = (center_of_mass (TOP-REAL n)) .: S by A1, A2, SIMPLEX0:def_20;
A4: A is bounded by A2, Th5;
reconsider s = @ S as c=-linear finite finite-membered Subset-Family of (TOP-REAL n) ;
set Us = union s;
set C = Complex_of {(union s)};
( union S is empty or union S in S ) by SIMPLEX0:9, ZFMISC_1:2;
then A5: union S is simplex-like by TOPS_2:def_1;
then A6: card (union S) <= (degree K) + ONE by SIMPLEX0:24;
A7: diameter K >= 0 by Th7;
A8: not {} in dom (center_of_mass (TOP-REAL n)) by ORDERS_1:1;
then A9: dom (center_of_mass (TOP-REAL n)) is with_non-empty_elements by SETFAM_1:def_8;
A10: [#] (TOP-REAL n) = [#] (Euclid n) by Lm2;
then reconsider US = union s as Subset of (Euclid n) ;
A11: a in the topology of (BCS K) by PRE_TOPC:def_2;
percases ( K is empty-membered or not K is empty-membered ) ;
suppose K is empty-membered ; ::_thesis: diameter A <= ((degree K) / ((degree K) + 1)) * (diameter K)
then A12: degree K = - 1 by SIMPLEX0:22;
then ( - 1 <= degree (BCS K) & degree (BCS K) <= - 1 ) by A1, A9, SIMPLEX0:23, SIMPLEX0:52;
then degree (BCS K) = - 1 by XXREAL_0:1;
then BCS K is empty-membered by SIMPLEX0:22;
then the topology of (BCS K) is empty-membered by SIMPLEX0:def_7;
then A13: a = {} by A11, SETFAM_1:def_10;
(degree K) / ((degree K) + 1) = 0 by A12;
hence diameter A <= ((degree K) / ((degree K) + 1)) * (diameter K) by A13, TBSP_1:def_8; ::_thesis: verum
end;
suppose not K is empty-membered ; ::_thesis: diameter A <= ((degree K) / ((degree K) + 1)) * (diameter K)
then ( degree K >= - 1 & degree K <> - 1 ) by SIMPLEX0:22, SIMPLEX0:23;
then degree K > - 1 by XXREAL_0:1;
then A14: degree K >= (- 1) + 1 by INT_1:7;
then A15: ((degree K) / ((degree K) + 1)) * (diameter K) >= 0 by A7;
percases ( a is empty or not a is empty ) ;
suppose a is empty ; ::_thesis: diameter A <= ((degree K) / ((degree K) + 1)) * (diameter K)
hence diameter A <= ((degree K) / ((degree K) + 1)) * (diameter K) by A15, TBSP_1:def_8; ::_thesis: verum
end;
supposeA16: not a is empty ; ::_thesis: diameter A <= ((degree K) / ((degree K) + 1)) * (diameter K)
now__::_thesis:_for_x,_y_being_Point_of_(Euclid_n)_st_x_in_A_&_y_in_A_holds_
dist_(x,y)_<=_((degree_K)_/_((degree_K)_+_1))_*_(diameter_K)
US is bounded ;
then union s is bounded by JORDAN2C:11;
then conv (union s) is bounded by Th14;
then reconsider cUs = conv (union s) as bounded Subset of (Euclid n) by JORDAN2C:11;
let x, y be Point of (Euclid n); ::_thesis: ( x in A & y in A implies dist (x,y) <= ((degree K) / ((degree K) + 1)) * (diameter K) )
assume that
A17: x in A and
A18: y in A ; ::_thesis: dist (x,y) <= ((degree K) / ((degree K) + 1)) * (diameter K)
reconsider X = x, Y = y as Element of (TOP-REAL n) by A10;
A19: ( |.(BCS (Complex_of {(union s)})).| = |.(Complex_of {(union s)}).| & |.(Complex_of {(union s)}).| = conv (union s) ) by SIMPLEX1:8, SIMPLEX1:10;
consider p being set such that
A20: p in dom (center_of_mass (TOP-REAL n)) and
A21: p in s and
(center_of_mass (TOP-REAL n)) . p = x by A3, A17, FUNCT_1:def_6;
p c= union s by A21, ZFMISC_1:74;
then A22: union s <> {} by A8, A20;
card (union s) <= (degree K) + 1 by A6, XXREAL_3:def_2;
then A23: ((degree K) + 1) " <= (card (union s)) " by A22, XREAL_1:85;
A24: diameter US <= diameter K by A5, Def4;
A25: ((card (union s)) - 1) / (card (union s)) = ((card (union s)) / (card (union s))) - (1 / (card (union s)))
.= 1 - (1 / (card (union s))) by A22, XCMPLX_1:60 ;
A26: diameter cUs = diameter US by Th15;
consider b1, b2 being VECTOR of (TOP-REAL n), r being Real such that
A27: b1 in Vertices (BCS (Complex_of {(union s)})) and
A28: b2 in Vertices (BCS (Complex_of {(union s)})) and
A29: X - Y = r * (b1 - b2) and
A30: 0 <= r and
A31: r <= ((card (union s)) - 1) / (card (union s)) by A3, A16, A17, A18, Th11;
reconsider B1 = b1, B2 = b2 as Element of (BCS (Complex_of {(union s)})) by A27, A28;
B1 is vertex-like by A27, SIMPLEX0:def_4;
then consider S1 being Subset of (BCS (Complex_of {(union s)})) such that
A32: S1 is simplex-like and
A33: B1 in S1 by SIMPLEX0:def_3;
A34: conv (@ S1) c= |.(BCS (Complex_of {(union s)})).| by A32, SIMPLEX1:5;
B2 is vertex-like by A28, SIMPLEX0:def_4;
then consider S2 being Subset of (BCS (Complex_of {(union s)})) such that
A35: S2 is simplex-like and
A36: B2 in S2 by SIMPLEX0:def_3;
@ S2 c= conv (@ S2) by CONVEX1:41;
then A37: B2 in conv (@ S2) by A36;
@ S1 c= conv (@ S1) by CONVEX1:41;
then A38: B1 in conv (@ S1) by A33;
reconsider bb1 = b1, bb2 = b2 as Point of (Euclid n) by A10;
(degree K) / ((degree K) + 1) = (((degree K) + 1) / ((degree K) + 1)) - (1 / ((degree K) + 1))
.= 1 - (1 / ((degree K) + 1)) by A14, XCMPLX_1:60 ;
then ((card (union s)) - 1) / (card (union s)) <= (degree K) / ((degree K) + 1) by A23, A25, XREAL_1:10;
then A39: ( dist (bb1,bb2) >= 0 & r <= (degree K) / ((degree K) + 1) ) by A31, XXREAL_0:2;
conv (@ S2) c= |.(BCS (Complex_of {(union s)})).| by A35, SIMPLEX1:5;
then dist (bb1,bb2) <= diameter US by A19, A26, A38, A37, A34, TBSP_1:def_8;
then A40: dist (bb1,bb2) <= diameter K by A24, XXREAL_0:2;
dist (x,y) = |.(x - y).| by EUCLID:def_6
.= |.(X - Y).|
.= |.(r * (bb1 - bb2)).| by A29
.= (abs r) * |.(bb1 - bb2).| by EUCLID:11
.= r * |.(bb1 - bb2).| by A30, ABSVALUE:def_1
.= r * (dist (bb1,bb2)) by EUCLID:def_6 ;
hence dist (x,y) <= ((degree K) / ((degree K) + 1)) * (diameter K) by A30, A40, A39, XREAL_1:66; ::_thesis: verum
end;
hence diameter A <= ((degree K) / ((degree K) + 1)) * (diameter K) by A4, A16, TBSP_1:def_8; ::_thesis: verum
end;
end;
end;
end;
end;
hence diameter (BCS K) <= ((degree K) / ((degree K) + 1)) * (diameter K) by Def4; ::_thesis: verum
end;
theorem Th17: :: SIMPLEX2:17
for n, k being Nat
for K being non void finite-degree bounded SimplicialComplex of (TOP-REAL n) st |.K.| c= [#] K holds
diameter (BCS (k,K)) <= (((degree K) / ((degree K) + 1)) |^ k) * (diameter K)
proof
let n, k be Nat; ::_thesis: for K being non void finite-degree bounded SimplicialComplex of (TOP-REAL n) st |.K.| c= [#] K holds
diameter (BCS (k,K)) <= (((degree K) / ((degree K) + 1)) |^ k) * (diameter K)
let K be non void finite-degree bounded SimplicialComplex of (TOP-REAL n); ::_thesis: ( |.K.| c= [#] K implies diameter (BCS (k,K)) <= (((degree K) / ((degree K) + 1)) |^ k) * (diameter K) )
set dK = degree K;
set ddK = (degree K) / ((degree K) + 1);
defpred S1[ Nat] means ( diameter (BCS ($1,K)) <= (((degree K) / ((degree K) + 1)) |^ $1) * (diameter K) & BCS ($1,K) is finite-degree & degree (BCS ($1,K)) <= degree K );
assume A1: |.K.| c= [#] K ; ::_thesis: diameter (BCS (k,K)) <= (((degree K) / ((degree K) + 1)) |^ k) * (diameter K)
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
set T = TOP-REAL n;
set B = BCS (k,K);
set cM = center_of_mass (TOP-REAL n);
A3: degree K >= - 1 by SIMPLEX0:23;
assume A4: S1[k] ; ::_thesis: S1[k + 1]
then reconsider B = BCS (k,K) as non void finite-degree bounded SimplicialComplex of (TOP-REAL n) ;
set dB = degree B;
A5: degree B >= - 1 by SIMPLEX0:23;
A6: 0 <= diameter K by Th7;
A7: 0 <= diameter B by Th7;
A8: ( |.B.| = |.K.| & [#] B = [#] K ) by A1, SIMPLEX1:18, SIMPLEX1:19;
then A9: BCS B = subdivision ((center_of_mass (TOP-REAL n)),B) by A1, SIMPLEX1:def_5;
A10: BCS ((k + 1),K) = BCS B by A1, SIMPLEX1:20;
then A11: diameter (BCS ((k + 1),K)) <= ((degree B) / ((degree B) + 1)) * (diameter B) by A1, A8, Th16;
not {} in dom (center_of_mass (TOP-REAL n)) by ORDERS_1:1;
then dom (center_of_mass (TOP-REAL n)) is with_non-empty_elements by SETFAM_1:def_8;
then A12: degree (BCS ((k + 1),K)) <= degree B by A9, A10, SIMPLEX0:52;
percases ( degree B = - 1 or degree B = 0 or ( degree B <> - 1 & degree B <> 0 ) ) ;
suppose ( degree B = - 1 or degree B = 0 ) ; ::_thesis: S1[k + 1]
then A13: (degree B) / ((degree B) + 1) = 0 ;
percases ( degree K = 0 or degree K = - 1 or ( degree K <> 0 & degree K <> - 1 ) ) ;
suppose ( degree K = 0 or degree K = - 1 ) ; ::_thesis: S1[k + 1]
then (degree K) / ((degree K) + 1) = 0 ;
then 0 = ((degree K) / ((degree K) + 1)) |^ (k + 1) by NAT_1:11, NEWTON:11;
hence S1[k + 1] by A1, A4, A9, A11, A12, A13, SIMPLEX1:20, XXREAL_0:2; ::_thesis: verum
end;
supposeA14: ( degree K <> 0 & degree K <> - 1 ) ; ::_thesis: S1[k + 1]
then degree K > - 1 by A3, XXREAL_0:1;
then degree K >= (- 1) + 1 by INT_1:7;
then (degree K) / ((degree K) + 1) > 0 by A14, XREAL_1:139;
then ((degree K) / ((degree K) + 1)) |^ (k + 1) > 0 by NEWTON:83;
hence S1[k + 1] by A1, A4, A6, A9, A11, A12, A13, SIMPLEX1:20, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
suppose ( degree B <> - 1 & degree B <> 0 ) ; ::_thesis: S1[k + 1]
then degree B > - 1 by A5, XXREAL_0:1;
then A15: degree B >= (- 1) + 1 by INT_1:7;
A16: (degree B) / ((degree B) + 1) = (((degree B) + 1) / ((degree B) + 1)) - (1 / ((degree B) + 1))
.= 1 - (1 / ((degree B) + 1)) by A15, XCMPLX_1:60 ;
A17: (degree K) / ((degree K) + 1) = (((degree K) + 1) / ((degree K) + 1)) - (1 / ((degree K) + 1))
.= 1 - (1 / ((degree K) + 1)) by A4, A15, XCMPLX_1:60 ;
(degree B) + 1 <= (degree K) + 1 by A4, XREAL_1:6;
then 1 / ((degree K) + 1) <= 1 / ((degree B) + 1) by A15, XREAL_1:85;
then (degree B) / ((degree B) + 1) <= (degree K) / ((degree K) + 1) by A16, A17, XREAL_1:10;
then A18: ((degree B) / ((degree B) + 1)) * (diameter B) <= ((degree K) / ((degree K) + 1)) * ((((degree K) / ((degree K) + 1)) |^ k) * (diameter K)) by A4, A7, A15, XREAL_1:66;
((degree K) / ((degree K) + 1)) * ((((degree K) / ((degree K) + 1)) |^ k) * (diameter K)) = (((degree K) / ((degree K) + 1)) * (((degree K) / ((degree K) + 1)) |^ k)) * (diameter K)
.= (((degree K) / ((degree K) + 1)) |^ (k + 1)) * (diameter K) by NEWTON:6 ;
hence S1[k + 1] by A1, A4, A9, A11, A12, A18, SIMPLEX1:20, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
((degree K) / ((degree K) + 1)) |^ 0 = 1 by NEWTON:4;
then A19: S1[ 0 ] by A1, SIMPLEX1:16;
for k being Nat holds S1[k] from NAT_1:sch_2(A19, A2);
hence diameter (BCS (k,K)) <= (((degree K) / ((degree K) + 1)) |^ k) * (diameter K) ; ::_thesis: verum
end;
theorem Th18: :: SIMPLEX2:18
for n being Nat
for K being non void finite-degree bounded SimplicialComplex of (TOP-REAL n) st |.K.| c= [#] K holds
for r being real number st r > 0 holds
ex k being Nat st diameter (BCS (k,K)) < r
proof
let n be Nat; ::_thesis: for K being non void finite-degree bounded SimplicialComplex of (TOP-REAL n) st |.K.| c= [#] K holds
for r being real number st r > 0 holds
ex k being Nat st diameter (BCS (k,K)) < r
let K be non void finite-degree bounded SimplicialComplex of (TOP-REAL n); ::_thesis: ( |.K.| c= [#] K implies for r being real number st r > 0 holds
ex k being Nat st diameter (BCS (k,K)) < r )
assume A1: |.K.| c= [#] K ; ::_thesis: for r being real number st r > 0 holds
ex k being Nat st diameter (BCS (k,K)) < r
set dK = degree K;
let r be real number ; ::_thesis: ( r > 0 implies ex k being Nat st diameter (BCS (k,K)) < r )
assume A2: r > 0 ; ::_thesis: ex k being Nat st diameter (BCS (k,K)) < r
set ddK = (degree K) / ((degree K) + 1);
percases ( degree K = 0 or degree K = - 1 or diameter K = 0 or ( degree K <> 0 & degree K <> - 1 & diameter K <> 0 ) ) ;
suppose ( degree K = 0 or degree K = - 1 ) ; ::_thesis: ex k being Nat st diameter (BCS (k,K)) < r
then A3: (degree K) / ((degree K) + 1) = 0 ;
( diameter (BCS K) <= ((degree K) / ((degree K) + 1)) * (diameter K) & BCS K = BCS (1,K) ) by A1, Th16, SIMPLEX1:17;
hence ex k being Nat st diameter (BCS (k,K)) < r by A2, A3; ::_thesis: verum
end;
supposeA4: diameter K = 0 ; ::_thesis: ex k being Nat st diameter (BCS (k,K)) < r
K = BCS (0,K) by A1, SIMPLEX1:16;
hence ex k being Nat st diameter (BCS (k,K)) < r by A2, A4; ::_thesis: verum
end;
supposeA5: ( degree K <> 0 & degree K <> - 1 & diameter K <> 0 ) ; ::_thesis: ex k being Nat st diameter (BCS (k,K)) < r
degree K >= - 1 by SIMPLEX0:23;
then degree K > - 1 by A5, XXREAL_0:1;
then A6: degree K >= (- 1) + 1 by INT_1:7;
then A7: (degree K) / ((degree K) + 1) > 0 by A5, XREAL_1:139;
(degree K) + 1 > degree K by XREAL_1:29;
then A8: (degree K) / ((degree K) + 1) < 1 by A6, XREAL_1:189;
A9: ( (degree K) / ((degree K) + 1) in REAL & r / (diameter K) in REAL ) by XREAL_0:def_1;
A10: diameter K > 0 by A5, Th7;
then r / (diameter K) > 0 by A2, XREAL_1:139;
then consider k being Element of NAT such that
A11: ((degree K) / ((degree K) + 1)) to_power k < r / (diameter K) by A7, A8, A9, TBSP_1:3;
A12: (r / (diameter K)) * (diameter K) = r by A5, XCMPLX_1:87;
A13: diameter (BCS (k,K)) <= (((degree K) / ((degree K) + 1)) |^ k) * (diameter K) by A1, Th17;
((degree K) / ((degree K) + 1)) to_power k = ((degree K) / ((degree K) + 1)) |^ k by POWER:41;
then (((degree K) / ((degree K) + 1)) |^ k) * (diameter K) < r by A10, A11, A12, XREAL_1:68;
then diameter (BCS (k,K)) < r by A13, XXREAL_0:2;
hence ex k being Nat st diameter (BCS (k,K)) < r ; ::_thesis: verum
end;
end;
end;
theorem Th19: :: SIMPLEX2:19
for i, j being Element of NAT ex f being Function of [:(TOP-REAL i),(TOP-REAL j):],(TOP-REAL (i + j)) st
( f is being_homeomorphism & ( for fi being Element of (TOP-REAL i)
for fj being Element of (TOP-REAL j) holds f . (fi,fj) = fi ^ fj ) )
proof
let i, j be Element of NAT ; ::_thesis: ex f being Function of [:(TOP-REAL i),(TOP-REAL j):],(TOP-REAL (i + j)) st
( f is being_homeomorphism & ( for fi being Element of (TOP-REAL i)
for fj being Element of (TOP-REAL j) holds f . (fi,fj) = fi ^ fj ) )
set TRi = TOP-REAL i;
set TRj = TOP-REAL j;
set TRij = TOP-REAL (i + j);
set tri = TopStruct(# the carrier of (TOP-REAL i), the topology of (TOP-REAL i) #);
set trj = TopStruct(# the carrier of (TOP-REAL j), the topology of (TOP-REAL j) #);
set trij = TopStruct(# the carrier of (TOP-REAL (i + j)), the topology of (TOP-REAL (i + j)) #);
A1: TopStruct(# the carrier of (TOP-REAL j), the topology of (TOP-REAL j) #) = TopSpaceMetr (Euclid j) by EUCLID:def_8;
( TopStruct(# the carrier of (TOP-REAL (i + j)), the topology of (TOP-REAL (i + j)) #) = TopSpaceMetr (Euclid (i + j)) & TopStruct(# the carrier of (TOP-REAL i), the topology of (TOP-REAL i) #) = TopSpaceMetr (Euclid i) ) by EUCLID:def_8;
then consider f being Function of [:TopStruct(# the carrier of (TOP-REAL i), the topology of (TOP-REAL i) #),TopStruct(# the carrier of (TOP-REAL j), the topology of (TOP-REAL j) #):],TopStruct(# the carrier of (TOP-REAL (i + j)), the topology of (TOP-REAL (i + j)) #) such that
A2: f is being_homeomorphism and
A3: for fi, fj being FinSequence st [fi,fj] in dom f holds
f . (fi,fj) = fi ^ fj by A1, TOPREAL7:26;
rng f = [#] TopStruct(# the carrier of (TOP-REAL (i + j)), the topology of (TOP-REAL (i + j)) #) by A2, TOPS_2:60;
then A4: rng f = [#] (TOP-REAL (i + j)) ;
A5: [#] [:(TOP-REAL i),(TOP-REAL j):] = [:([#] (TOP-REAL i)),([#] (TOP-REAL j)):] by BORSUK_1:def_2;
A6: [:(TOP-REAL i),(TOP-REAL j):] = [:(TOP-REAL i),(TOP-REAL j):] | ([#] [:(TOP-REAL i),(TOP-REAL j):]) by TSEP_1:3
.= [:((TOP-REAL i) | ([#] (TOP-REAL i))),((TOP-REAL j) | ([#] (TOP-REAL j))):] by A5, BORSUK_3:22
.= [:TopStruct(# the carrier of (TOP-REAL i), the topology of (TOP-REAL i) #),((TOP-REAL j) | ([#] (TOP-REAL j))):] by TSEP_1:93
.= [:TopStruct(# the carrier of (TOP-REAL i), the topology of (TOP-REAL i) #),TopStruct(# the carrier of (TOP-REAL j), the topology of (TOP-REAL j) #):] by TSEP_1:93 ;
then reconsider F = f as Function of [:(TOP-REAL i),(TOP-REAL j):],(TOP-REAL (i + j)) ;
A7: now__::_thesis:_for_P_being_Subset_of_[:(TOP-REAL_i),(TOP-REAL_j):]_holds_F_.:_(Cl_P)_=_Cl_(F_.:_P)
let P be Subset of [:(TOP-REAL i),(TOP-REAL j):]; ::_thesis: F .: (Cl P) = Cl (F .: P)
thus F .: (Cl P) = Cl (f .: P) by A2, A6, TOPS_2:60
.= Cl (F .: P) by TOPS_3:80 ; ::_thesis: verum
end;
take F ; ::_thesis: ( F is being_homeomorphism & ( for fi being Element of (TOP-REAL i)
for fj being Element of (TOP-REAL j) holds F . (fi,fj) = fi ^ fj ) )
A8: F is one-to-one by A2, TOPS_2:60;
dom F = [#] [:(TOP-REAL i),(TOP-REAL j):] by A2, A6, TOPS_2:60;
hence F is being_homeomorphism by A4, A7, A8, TOPS_2:60; ::_thesis: for fi being Element of (TOP-REAL i)
for fj being Element of (TOP-REAL j) holds F . (fi,fj) = fi ^ fj
let fi be Element of (TOP-REAL i); ::_thesis: for fj being Element of (TOP-REAL j) holds F . (fi,fj) = fi ^ fj
let fj be Element of (TOP-REAL j); ::_thesis: F . (fi,fj) = fi ^ fj
dom F = [:([#] (TOP-REAL i)),([#] (TOP-REAL j)):] by A5, FUNCT_2:def_1;
then [fi,fj] in dom F by ZFMISC_1:87;
hence F . (fi,fj) = fi ^ fj by A3; ::_thesis: verum
end;
Lm4: for n being Nat holds [#] (TOP-REAL n) = [#] (TopSpaceMetr (Euclid n))
proof
let n be Nat; ::_thesis: [#] (TOP-REAL n) = [#] (TopSpaceMetr (Euclid n))
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
hence [#] (TOP-REAL n) = [#] (TopSpaceMetr (Euclid n)) ; ::_thesis: verum
end;
theorem Th20: :: SIMPLEX2:20
for i, j being Element of NAT
for f being Function of [:(TOP-REAL i),(TOP-REAL j):],(TOP-REAL (i + j)) st ( for fi being Element of (TOP-REAL i)
for fj being Element of (TOP-REAL j) holds f . (fi,fj) = fi ^ fj ) holds
for r being real number
for fi being Point of (Euclid i)
for fj being Point of (Euclid j)
for fij being Point of (Euclid (i + j)) st fij = fi ^ fj holds
f .: [:(OpenHypercube (fi,r)),(OpenHypercube (fj,r)):] = OpenHypercube (fij,r)
proof
let i, j be Element of NAT ; ::_thesis: for f being Function of [:(TOP-REAL i),(TOP-REAL j):],(TOP-REAL (i + j)) st ( for fi being Element of (TOP-REAL i)
for fj being Element of (TOP-REAL j) holds f . (fi,fj) = fi ^ fj ) holds
for r being real number
for fi being Point of (Euclid i)
for fj being Point of (Euclid j)
for fij being Point of (Euclid (i + j)) st fij = fi ^ fj holds
f .: [:(OpenHypercube (fi,r)),(OpenHypercube (fj,r)):] = OpenHypercube (fij,r)
let f be Function of [:(TOP-REAL i),(TOP-REAL j):],(TOP-REAL (i + j)); ::_thesis: ( ( for fi being Element of (TOP-REAL i)
for fj being Element of (TOP-REAL j) holds f . (fi,fj) = fi ^ fj ) implies for r being real number
for fi being Point of (Euclid i)
for fj being Point of (Euclid j)
for fij being Point of (Euclid (i + j)) st fij = fi ^ fj holds
f .: [:(OpenHypercube (fi,r)),(OpenHypercube (fj,r)):] = OpenHypercube (fij,r) )
assume A1: for fi being Element of (TOP-REAL i)
for fj being Element of (TOP-REAL j) holds f . (fi,fj) = fi ^ fj ; ::_thesis: for r being real number
for fi being Point of (Euclid i)
for fj being Point of (Euclid j)
for fij being Point of (Euclid (i + j)) st fij = fi ^ fj holds
f .: [:(OpenHypercube (fi,r)),(OpenHypercube (fj,r)):] = OpenHypercube (fij,r)
let r be real number ; ::_thesis: for fi being Point of (Euclid i)
for fj being Point of (Euclid j)
for fij being Point of (Euclid (i + j)) st fij = fi ^ fj holds
f .: [:(OpenHypercube (fi,r)),(OpenHypercube (fj,r)):] = OpenHypercube (fij,r)
let fi be Point of (Euclid i); ::_thesis: for fj being Point of (Euclid j)
for fij being Point of (Euclid (i + j)) st fij = fi ^ fj holds
f .: [:(OpenHypercube (fi,r)),(OpenHypercube (fj,r)):] = OpenHypercube (fij,r)
let fj be Point of (Euclid j); ::_thesis: for fij being Point of (Euclid (i + j)) st fij = fi ^ fj holds
f .: [:(OpenHypercube (fi,r)),(OpenHypercube (fj,r)):] = OpenHypercube (fij,r)
let fij be Point of (Euclid (i + j)); ::_thesis: ( fij = fi ^ fj implies f .: [:(OpenHypercube (fi,r)),(OpenHypercube (fj,r)):] = OpenHypercube (fij,r) )
assume A2: fij = fi ^ fj ; ::_thesis: f .: [:(OpenHypercube (fi,r)),(OpenHypercube (fj,r)):] = OpenHypercube (fij,r)
set Ii = Intervals (fi,r);
set Ij = Intervals (fj,r);
set Iij = Intervals (fij,r);
A3: OpenHypercube (fi,r) = product (Intervals (fi,r)) by EUCLID_9:def_4;
A4: [#] (TOP-REAL i) = [#] (TopSpaceMetr (Euclid i)) by Lm4;
A5: [#] (TOP-REAL j) = [#] (TopSpaceMetr (Euclid j)) by Lm4;
A6: OpenHypercube (fj,r) = product (Intervals (fj,r)) by EUCLID_9:def_4;
A7: (Intervals (fi,r)) ^ (Intervals (fj,r)) = Intervals (fij,r) by A2, RLAFFIN3:1;
A8: f .: [:(product (Intervals (fi,r))),(product (Intervals (fj,r))):] c= product (Intervals (fij,r))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: [:(product (Intervals (fi,r))),(product (Intervals (fj,r))):] or y in product (Intervals (fij,r)) )
assume y in f .: [:(product (Intervals (fi,r))),(product (Intervals (fj,r))):] ; ::_thesis: y in product (Intervals (fij,r))
then consider x being set such that
x in dom f and
A9: x in [:(product (Intervals (fi,r))),(product (Intervals (fj,r))):] and
A10: f . x = y by FUNCT_1:def_6;
consider xi, xj being set such that
A11: xi in product (Intervals (fi,r)) and
A12: xj in product (Intervals (fj,r)) and
A13: x = [xi,xj] by A9, ZFMISC_1:def_2;
reconsider xi = xi as Element of (TOP-REAL i) by A3, A4, A11;
reconsider xj = xj as Element of (TOP-REAL j) by A5, A6, A12;
y = f . (xi,xj) by A10, A13, BINOP_1:def_1
.= xi ^ xj by A1 ;
hence y in product (Intervals (fij,r)) by A7, A11, A12, RLAFFIN3:2; ::_thesis: verum
end;
A14: product (Intervals (fij,r)) c= f .: [:(product (Intervals (fi,r))),(product (Intervals (fj,r))):]
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in product (Intervals (fij,r)) or y in f .: [:(product (Intervals (fi,r))),(product (Intervals (fj,r))):] )
assume y in product (Intervals (fij,r)) ; ::_thesis: y in f .: [:(product (Intervals (fi,r))),(product (Intervals (fj,r))):]
then consider p1, p2 being FinSequence such that
A15: y = p1 ^ p2 and
A16: ( p1 in product (Intervals (fi,r)) & p2 in product (Intervals (fj,r)) ) by A7, RLAFFIN3:2;
A17: [p1,p2] in [:(product (Intervals (fi,r))),(product (Intervals (fj,r))):] by A16, ZFMISC_1:87;
[p1,p2] in [:([#] (TOP-REAL i)),([#] (TOP-REAL j)):] by A3, A5, A4, A6, A16, ZFMISC_1:87;
then [p1,p2] in [#] [:(TOP-REAL i),(TOP-REAL j):] ;
then A18: [p1,p2] in dom f by FUNCT_2:def_1;
y = f . (p1,p2) by A1, A3, A5, A4, A6, A15, A16
.= f . [p1,p2] by BINOP_1:def_1 ;
hence y in f .: [:(product (Intervals (fi,r))),(product (Intervals (fj,r))):] by A17, A18, FUNCT_1:def_6; ::_thesis: verum
end;
OpenHypercube (fij,r) = product (Intervals (fij,r)) by EUCLID_9:def_4;
hence f .: [:(OpenHypercube (fi,r)),(OpenHypercube (fj,r)):] = OpenHypercube (fij,r) by A3, A6, A8, A14, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th21: :: SIMPLEX2:21
for n being Nat
for A being Subset of (TOP-REAL n) holds
( A is bounded iff ex p being Point of (Euclid n) ex r being real number st A c= OpenHypercube (p,r) )
proof
let n be Nat; ::_thesis: for A being Subset of (TOP-REAL n) holds
( A is bounded iff ex p being Point of (Euclid n) ex r being real number st A c= OpenHypercube (p,r) )
let A be Subset of (TOP-REAL n); ::_thesis: ( A is bounded iff ex p being Point of (Euclid n) ex r being real number st A c= OpenHypercube (p,r) )
reconsider B = A as Subset of (Euclid n) by TOPREAL3:8;
thus ( A is bounded implies ex p being Point of (Euclid n) ex r being real number st A c= OpenHypercube (p,r) ) ::_thesis: ( ex p being Point of (Euclid n) ex r being real number st A c= OpenHypercube (p,r) implies A is bounded )
proof
assume A is bounded ; ::_thesis: ex p being Point of (Euclid n) ex r being real number st A c= OpenHypercube (p,r)
then A1: B is bounded by JORDAN2C:11;
percases ( A is empty or not A is empty ) ;
supposeA2: A is empty ; ::_thesis: ex p being Point of (Euclid n) ex r being real number st A c= OpenHypercube (p,r)
take p = the Point of (Euclid n); ::_thesis: ex r being real number st A c= OpenHypercube (p,r)
take r = the real number ; ::_thesis: A c= OpenHypercube (p,r)
thus A c= OpenHypercube (p,r) by A2, XBOOLE_1:2; ::_thesis: verum
end;
suppose not A is empty ; ::_thesis: ex p being Point of (Euclid n) ex r being real number st A c= OpenHypercube (p,r)
then consider p being set such that
A3: p in B by XBOOLE_0:def_1;
reconsider p = p as Element of (Euclid n) by A3;
consider r being Real such that
0 < r and
A4: for x, y being Point of (Euclid n) st x in B & y in B holds
dist (x,y) <= r by A1, TBSP_1:def_7;
take p ; ::_thesis: ex r being real number st A c= OpenHypercube (p,r)
take r1 = r + 1; ::_thesis: A c= OpenHypercube (p,r1)
A5: B c= Ball (p,r1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in Ball (p,r1) )
assume A6: x in B ; ::_thesis: x in Ball (p,r1)
then reconsider x = x as Element of (Euclid n) ;
dist (p,x) < r1 by A3, A4, A6, XREAL_1:39;
hence x in Ball (p,r1) by METRIC_1:11; ::_thesis: verum
end;
Ball (p,r1) c= OpenHypercube (p,r1) by EUCLID_9:22;
hence A c= OpenHypercube (p,r1) by A5, XBOOLE_1:1; ::_thesis: verum
end;
end;
end;
given p being Point of (Euclid n), r being real number such that A7: A c= OpenHypercube (p,r) ; ::_thesis: A is bounded
percases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; ::_thesis: A is bounded
then OpenHypercube (p,r) = {{}} by EUCLID_9:12;
then ( B = {} or B = {0} ) by A7, ZFMISC_1:33;
hence A is bounded by JORDAN2C:11; ::_thesis: verum
end;
suppose n <> 0 ; ::_thesis: A is bounded
then OpenHypercube (p,r) c= Ball (p,(r * (sqrt n))) by EUCLID_9:18;
then B is bounded by A7, TBSP_1:14, XBOOLE_1:1;
hence A is bounded by JORDAN2C:11; ::_thesis: verum
end;
end;
end;
Lm5: for A being Subset of (TOP-REAL 1) st A is closed & A is bounded holds
A is compact
proof
set TR1 = TOP-REAL 1;
let A be Subset of (TOP-REAL 1); ::_thesis: ( A is closed & A is bounded implies A is compact )
assume that
A1: A is closed and
A2: A is bounded ; ::_thesis: A is compact
consider r being Real such that
A3: for q being Point of (TOP-REAL 1) st q in A holds
|.q.| < r by A2, JORDAN2C:34;
reconsider L = [.(- r),r.] as Subset of R^1 by TOPMETR:17;
consider f being Function of (TOP-REAL 1),R^1 such that
A4: for p being Element of (TOP-REAL 1) holds f . p = p /. 1 by JORDAN2B:1;
A5: f is being_homeomorphism by A4, JORDAN2B:28;
then reconsider F = f as one-to-one Function by TOPS_2:def_5;
rng f = [#] R^1 by A5, TOPS_2:def_5;
then f is onto by FUNCT_2:def_3;
then f /" = F " by TOPS_2:def_4;
then A6: (f /") .: L = F " L by FUNCT_1:85;
A7: dom f = [#] (TOP-REAL 1) by A5, TOPS_2:def_5;
A8: A c= F " L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in F " L )
assume A9: x in A ; ::_thesis: x in F " L
then reconsider v = x as Element of (TOP-REAL 1) ;
set v1 = v . 1;
A10: len v = 1 by CARD_1:def_7;
then v = <*(v . 1)*> by FINSEQ_1:40;
then A11: |.v.| = abs (v . 1) by TOPREALC:18;
|.v.| < r by A3, A9;
then ( v . 1 <= r & - r <= v . 1 ) by A11, ABSVALUE:5;
then A12: v . 1 in L by XXREAL_1:1;
( 1 in Seg 1 & dom v = Seg 1 ) by A10, FINSEQ_1:1, FINSEQ_1:def_3;
then A13: v /. 1 = v . 1 by PARTFUN1:def_6;
f . v = v /. 1 by A4;
hence x in F " L by A7, A12, A13, FUNCT_1:def_7; ::_thesis: verum
end;
[.(- r),r.] is compact by RCOMP_1:6;
then A14: L is compact by JORDAN5A:25;
f " is continuous by A5, TOPS_2:def_5;
then (f /") .: L is compact by A14, WEIERSTR:8;
hence A is compact by A1, A6, A8, COMPTS_1:9; ::_thesis: verum
end;
Lm6: for n being Nat
for A being Subset of (TOP-REAL n) st A is closed & A is bounded holds
A is compact
proof
let n be Nat; ::_thesis: for A being Subset of (TOP-REAL n) st A is closed & A is bounded holds
A is compact
defpred S1[ Nat] means for A being Subset of (TOP-REAL $1) st A is closed & A is bounded holds
A is compact ;
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
percases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; ::_thesis: S1[n + 1]
hence S1[n + 1] by Lm5; ::_thesis: verum
end;
supposeA3: n <> 0 ; ::_thesis: S1[n + 1]
set n1 = n + 1;
set TR1 = TOP-REAL 1;
set TRn = TOP-REAL n;
set TRn1 = TOP-REAL (n + 1);
let A be Subset of (TOP-REAL (n + 1)); ::_thesis: ( A is closed & A is bounded implies A is compact )
assume that
A4: A is closed and
A5: A is bounded ; ::_thesis: A is compact
consider p being Point of (Euclid (n + 1)), r being real number such that
A6: A c= OpenHypercube (p,r) by A5, Th21;
A7: n in NAT by ORDINAL1:def_12;
then consider f being Function of [:(TOP-REAL n),(TOP-REAL 1):],(TOP-REAL (n + 1)) such that
A8: f is being_homeomorphism and
A9: for fi being Element of (TOP-REAL n)
for fj being Element of (TOP-REAL 1) holds f . (fi,fj) = fi ^ fj by Th19;
A10: ( f is one-to-one & dom f = [#] [:(TOP-REAL n),(TOP-REAL 1):] ) by A8, TOPGRP_1:24;
len p = n + 1 by CARD_1:def_7;
then consider q1, q2 being FinSequence such that
A11: len q1 = n and
A12: len q2 = 1 and
A13: p = q1 ^ q2 by FINSEQ_2:22;
rng p c= REAL ;
then A14: p is FinSequence of REAL by FINSEQ_1:def_4;
then A15: q1 is FinSequence of REAL by A13, FINSEQ_1:36;
A16: q2 is FinSequence of REAL by A13, A14, FINSEQ_1:36;
reconsider q1 = q1 as Element of (Euclid n) by A11, A15, TOPREAL3:45;
reconsider q2 = q2 as Element of (Euclid 1) by A12, A16, TOPREAL3:45;
A17: f is continuous by A8, TOPS_2:def_5;
reconsider Bn = cl_Ball (q1,(r * (sqrt n))) as Subset of (TOP-REAL n) by TOPREAL3:8;
reconsider B1 = cl_Ball (q2,(r * (sqrt 1))) as Subset of (TOP-REAL 1) by TOPREAL3:8;
( Ball (q2,(r * (sqrt 1))) c= B1 & OpenHypercube (q2,r) c= Ball (q2,(r * (sqrt 1))) ) by EUCLID_9:18, METRIC_1:14;
then A18: OpenHypercube (q2,r) c= B1 by XBOOLE_1:1;
( Ball (q1,(r * (sqrt n))) c= Bn & OpenHypercube (q1,r) c= Ball (q1,(r * (sqrt n))) ) by A3, EUCLID_9:18, METRIC_1:14;
then OpenHypercube (q1,r) c= Bn by XBOOLE_1:1;
then A19: [:(OpenHypercube (q1,r)),(OpenHypercube (q2,r)):] c= [:Bn,B1:] by A18, ZFMISC_1:96;
cl_Ball (q2,(r * (sqrt 1))) is bounded by TOPREAL6:59;
then B1 is bounded by JORDAN2C:11;
then A20: B1 is compact by Lm5, TOPREAL6:58;
cl_Ball (q1,(r * (sqrt n))) is bounded by TOPREAL6:59;
then Bn is bounded by JORDAN2C:11;
then Bn is compact by A2, A7, TOPREAL6:58;
then A21: [:Bn,B1:] is compact Subset of [:(TOP-REAL n),(TOP-REAL 1):] by A20, BORSUK_3:23;
rng f = [#] (TOP-REAL (n + 1)) by A8, TOPGRP_1:24;
then A22: f .: (f " A) = A by FUNCT_1:77;
f .: [:(OpenHypercube (q1,r)),(OpenHypercube (q2,r)):] = OpenHypercube (p,r) by A9, A11, A13, Th20;
then A23: f " A c= [:(OpenHypercube (q1,r)),(OpenHypercube (q2,r)):] by A6, A10, A22, FUNCT_1:87;
f " A is closed by A4, A8, TOPGRP_1:24;
then f " A is compact by A19, A21, A23, COMPTS_1:9, XBOOLE_1:1;
hence A is compact by A17, A22, WEIERSTR:8; ::_thesis: verum
end;
end;
end;
A24: S1[ 0 ] ;
for n being Nat holds S1[n] from NAT_1:sch_2(A24, A1);
hence for A being Subset of (TOP-REAL n) st A is closed & A is bounded holds
A is compact ; ::_thesis: verum
end;
registration
let n be Nat;
cluster closed bounded -> compact for Element of bool the carrier of (TOP-REAL n);
coherence
for b1 being Subset of (TOP-REAL n) st b1 is closed & b1 is bounded holds
b1 is compact by Lm6;
end;
registration
let n be Nat;
let A be affinely-independent Subset of (TOP-REAL n);
cluster conv A -> compact ;
coherence
conv A is compact
proof
n in NAT by ORDINAL1:def_12;
then conv A is bounded by Th14;
hence conv A is compact ; ::_thesis: verum
end;
end;
begin
theorem Th22: :: SIMPLEX2:22
for n being Nat
for A being non empty affinely-independent Subset of (TOP-REAL n)
for E being Enumeration of A
for F being FinSequence of bool the carrier of ((TOP-REAL n) | (conv A)) st len F = card A & rng F is closed & ( for S being Subset of (dom F) holds conv (E .: S) c= union (F .: S) ) holds
not meet (rng F) is empty
proof
let n be Nat; ::_thesis: for A being non empty affinely-independent Subset of (TOP-REAL n)
for E being Enumeration of A
for F being FinSequence of bool the carrier of ((TOP-REAL n) | (conv A)) st len F = card A & rng F is closed & ( for S being Subset of (dom F) holds conv (E .: S) c= union (F .: S) ) holds
not meet (rng F) is empty
set TRn = TOP-REAL n;
let A be non empty affinely-independent Subset of (TOP-REAL n); ::_thesis: for E being Enumeration of A
for F being FinSequence of bool the carrier of ((TOP-REAL n) | (conv A)) st len F = card A & rng F is closed & ( for S being Subset of (dom F) holds conv (E .: S) c= union (F .: S) ) holds
not meet (rng F) is empty
set cA = conv A;
let E be Enumeration of A; ::_thesis: for F being FinSequence of bool the carrier of ((TOP-REAL n) | (conv A)) st len F = card A & rng F is closed & ( for S being Subset of (dom F) holds conv (E .: S) c= union (F .: S) ) holds
not meet (rng F) is empty
let F be FinSequence of bool the carrier of ((TOP-REAL n) | (conv A)); ::_thesis: ( len F = card A & rng F is closed & ( for S being Subset of (dom F) holds conv (E .: S) c= union (F .: S) ) implies not meet (rng F) is empty )
assume that
A1: len F = card A and
A2: rng F is closed and
A3: for S being Subset of (dom F) holds conv (E .: S) c= union (F .: S) ; ::_thesis: not meet (rng F) is empty
A4: F <> {} by A1;
A5: rng E = A by RLAFFIN3:def_1;
then len E = card A by FINSEQ_4:62;
then A6: dom E = dom F by A1, FINSEQ_3:29;
set En = Euclid n;
set Comp = Complex_of {A};
defpred S1[ set , set ] means ( $1 in F . ((E ") . $2) & ( for B being Subset of (TOP-REAL n) st B c= A & $1 in conv B holds
$2 in B ) );
A7: TopSpaceMetr (Euclid n) = TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by EUCLID:def_8;
then reconsider CA = conv A as non empty Subset of (TopSpaceMetr (Euclid n)) ;
reconsider ca = conv A as non empty Subset of (Euclid n) by A7;
A8: (TopSpaceMetr (Euclid n)) | CA = TopSpaceMetr ((Euclid n) | ca) by HAUSDORF:16;
then reconsider CrF = COMPLEMENT (rng F) as Subset-Family of (TopSpaceMetr ((Euclid n) | ca)) by A7, PRE_TOPC:36;
CA is compact by A7, COMPTS_1:23;
then A9: TopSpaceMetr ((Euclid n) | ca) is compact by A8, COMPTS_1:3;
A10: (TopSpaceMetr (Euclid n)) | CA = (TOP-REAL n) | (conv A) by A7, PRE_TOPC:36;
assume meet (rng F) is empty ; ::_thesis: contradiction
then [#] ((TOP-REAL n) | (conv A)) = (meet (rng F)) `
.= union CrF by A4, TOPS_2:7 ;
then A11: CrF is Cover of (TopSpaceMetr ((Euclid n) | ca)) by A8, A10, SETFAM_1:45;
set L = the Lebesgue_number of CrF;
A12: |.(Complex_of {A}).| c= [#] (Complex_of {A}) ;
then consider k being Nat such that
A13: diameter (BCS (k,(Complex_of {A}))) < the Lebesgue_number of CrF by Th18;
set Bcs = BCS (k,(Complex_of {A}));
A14: |.(BCS (k,(Complex_of {A}))).| = |.(Complex_of {A}).| by A12, SIMPLEX1:19;
A15: the topology of (Complex_of {A}) = bool A by SIMPLEX0:4;
A16: for x being set st x in Vertices (BCS (k,(Complex_of {A}))) holds
ex y being set st
( y in A & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in Vertices (BCS (k,(Complex_of {A}))) implies ex y being set st
( y in A & S1[x,y] ) )
assume A17: x in Vertices (BCS (k,(Complex_of {A}))) ; ::_thesis: ex y being set st
( y in A & S1[x,y] )
then reconsider v = x as Element of (BCS (k,(Complex_of {A}))) ;
v is vertex-like by A17, SIMPLEX0:def_4;
then consider S being Subset of (BCS (k,(Complex_of {A}))) such that
A18: S is simplex-like and
A19: v in S by SIMPLEX0:def_3;
@ S c= conv (@ S) by RLAFFIN1:2;
then A20: v in conv (@ S) by A19;
conv (@ S) c= |.(Complex_of {A}).| by A14, A18, SIMPLEX1:5;
then consider W being Subset of (Complex_of {A}) such that
A21: W is simplex-like and
A22: v in Int (@ W) by A20, SIMPLEX1:6;
A23: v in conv (@ W) by A22, RLAFFIN2:def_1;
A24: W in the topology of (Complex_of {A}) by A21, PRE_TOPC:def_2;
then ( E " W c= dom E & E .: (E " W) = W ) by A5, A15, FUNCT_1:77, RELAT_1:132;
then conv (@ W) c= union (F .: (E " W)) by A3, A6;
then consider Y being set such that
A25: v in Y and
A26: Y in F .: (E " W) by A23, TARSKI:def_4;
consider i being set such that
i in dom F and
A27: i in E " W and
A28: F . i = Y by A26, FUNCT_1:def_6;
take y = E . i; ::_thesis: ( y in A & S1[x,y] )
A29: y in W by A27, FUNCT_1:def_7;
i in dom E by A27, FUNCT_1:def_7;
hence ( y in A & x in F . ((E ") . y) ) by A15, A24, A25, A28, A29, FUNCT_1:34; ::_thesis: for B being Subset of (TOP-REAL n) st B c= A & x in conv B holds
y in B
let B be Subset of (TOP-REAL n); ::_thesis: ( B c= A & x in conv B implies y in B )
assume that
A30: B c= A and
A31: x in conv B ; ::_thesis: y in B
reconsider b = B as Simplex of (Complex_of {A}) by A15, A30, PRE_TOPC:def_2;
conv (@ b) meets Int (@ W) by A22, A31, XBOOLE_0:3;
then W c= b by A21, SIMPLEX1:26;
hence y in B by A29; ::_thesis: verum
end;
consider G being Function of (Vertices (BCS (k,(Complex_of {A})))),A such that
A32: for x being set st x in Vertices (BCS (k,(Complex_of {A}))) holds
S1[x,G . x] from FUNCT_2:sch_1(A16);
A33: |.(Complex_of {A}).| = conv A by SIMPLEX1:8;
then BCS (k,(Complex_of {A})) is with_non-empty_element by A14, SIMPLEX1:7;
then for v being Vertex of (BCS (k,(Complex_of {A})))
for B being Subset of (TOP-REAL n) st B c= A & v in conv B holds
G . v in B by A32;
then consider S being Simplex of (card A) - 1, BCS (k,(Complex_of {A})) such that
A34: G .: S = A by SIMPLEX1:47;
A35: [#] (BCS (k,(Complex_of {A}))) = [#] (Complex_of {A}) by A12, SIMPLEX1:18;
then reconsider SS = S as Subset of (Euclid n) by A7;
not S is empty by A34;
then consider s being set such that
A36: s in S by XBOOLE_0:def_1;
A37: conv (@ S) c= conv A by A14, A33, SIMPLEX1:5;
reconsider s = s as Point of (Euclid n) by A7, A35, A36;
A38: S c= conv (@ S) by RLAFFIN1:2;
then s in conv (@ S) by A36;
then reconsider ss = s as Point of ((Euclid n) | ca) by A37, TOPMETR:def_2;
A39: SS is bounded ;
CrF is open by A2, A8, A10, TOPS_2:9;
then consider CRF being Subset of (TopSpaceMetr ((Euclid n) | ca)) such that
A40: CRF in CrF and
A41: Ball (ss, the Lebesgue_number of CrF) c= CRF by A9, A11, Def1;
CRF ` in rng F by A8, A10, A40, SETFAM_1:def_7;
then consider i being set such that
A42: i in dom F and
A43: F . i = CRF ` by FUNCT_1:def_3;
E . i in A by A5, A6, A42, FUNCT_1:def_3;
then consider w being set such that
A44: w in dom G and
A45: w in S and
A46: G . w = E . i by A34, FUNCT_1:def_6;
A47: w in conv (@ S) by A38, A45;
A48: conv (@ S) c= conv A by A14, A33, SIMPLEX1:5;
then A49: ( [#] ((Euclid n) | ca) = ca & w in conv A ) by A47, TOPMETR:def_2;
reconsider SS = S as bounded Subset of (Euclid n) by A39;
diameter SS <= diameter (BCS (k,(Complex_of {A}))) by Def4;
then A50: diameter SS < the Lebesgue_number of CrF by A13, XXREAL_0:2;
w in F . ((E ") . (G . w)) by A32, A44;
then A51: w in F . i by A6, A42, A46, FUNCT_1:34;
reconsider w = w as Point of (Euclid n) by A49;
reconsider ww = w as Point of ((Euclid n) | ca) by A47, A48, TOPMETR:def_2;
conv (@ S) c= cl_Ball (s,(diameter SS)) by A36, A38, Th13;
then ( dist (s,w) = dist (ss,ww) & dist (s,w) <= diameter SS ) by A47, METRIC_1:12, TOPMETR:def_1;
then dist (ss,ww) < the Lebesgue_number of CrF by A50, XXREAL_0:2;
then ww in Ball (ss, the Lebesgue_number of CrF) by METRIC_1:11;
hence contradiction by A41, A43, A51, XBOOLE_0:def_5; ::_thesis: verum
end;
theorem Th23: :: SIMPLEX2:23
for n being Nat
for A being affinely-independent Subset of (TOP-REAL n) st card A = n + 1 holds
for f being continuous Function of ((TOP-REAL n) | (conv A)),((TOP-REAL n) | (conv A)) ex p being Point of (TOP-REAL n) st
( p in dom f & f . p = p )
proof
let n be Nat; ::_thesis: for A being affinely-independent Subset of (TOP-REAL n) st card A = n + 1 holds
for f being continuous Function of ((TOP-REAL n) | (conv A)),((TOP-REAL n) | (conv A)) ex p being Point of (TOP-REAL n) st
( p in dom f & f . p = p )
set TRn = TOP-REAL n;
let A be affinely-independent Subset of (TOP-REAL n); ::_thesis: ( card A = n + 1 implies for f being continuous Function of ((TOP-REAL n) | (conv A)),((TOP-REAL n) | (conv A)) ex p being Point of (TOP-REAL n) st
( p in dom f & f . p = p ) )
assume A1: card A = n + 1 ; ::_thesis: for f being continuous Function of ((TOP-REAL n) | (conv A)),((TOP-REAL n) | (conv A)) ex p being Point of (TOP-REAL n) st
( p in dom f & f . p = p )
A2: not A is empty by A1;
set cA = conv A;
let f be continuous Function of ((TOP-REAL n) | (conv A)),((TOP-REAL n) | (conv A)); ::_thesis: ex p being Point of (TOP-REAL n) st
( p in dom f & f . p = p )
reconsider cA = conv A as non empty Subset of (TOP-REAL n) by A2;
set T = (TOP-REAL n) | cA;
reconsider ff = f as continuous Function of ((TOP-REAL n) | cA),((TOP-REAL n) | cA) ;
set E = the Enumeration of A;
deffunc H1( set ) -> set = { v where v is Element of ((TOP-REAL n) | cA) : (|-- (A,( the Enumeration of A . $1))) . (f . v) <= (|-- (A,( the Enumeration of A . $1))) . v } ;
consider F being FinSequence such that
A3: ( len F = card A & ( for k being Nat st k in dom F holds
F . k = H1(k) ) ) from FINSEQ_1:sch_2();
rng F c= bool the carrier of ((TOP-REAL n) | cA)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng F or y in bool the carrier of ((TOP-REAL n) | cA) )
assume y in rng F ; ::_thesis: y in bool the carrier of ((TOP-REAL n) | cA)
then consider x being set such that
A4: x in dom F and
A5: F . x = y by FUNCT_1:def_3;
A6: H1(x) c= the carrier of ((TOP-REAL n) | cA)
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in H1(x) or z in the carrier of ((TOP-REAL n) | cA) )
assume z in H1(x) ; ::_thesis: z in the carrier of ((TOP-REAL n) | cA)
then ex v being Element of ((TOP-REAL n) | cA) st
( z = v & (|-- (A,( the Enumeration of A . x))) . (f . v) <= (|-- (A,( the Enumeration of A . x))) . v ) ;
hence z in the carrier of ((TOP-REAL n) | cA) ; ::_thesis: verum
end;
F . x = H1(x) by A3, A4;
hence y in bool the carrier of ((TOP-REAL n) | cA) by A5, A6; ::_thesis: verum
end;
then reconsider F = F as FinSequence of bool the carrier of ((TOP-REAL n) | cA) by FINSEQ_1:def_4;
A7: [#] ((TOP-REAL n) | cA) = cA by PRE_TOPC:def_5;
A8: dom f = the carrier of ((TOP-REAL n) | cA) by FUNCT_2:def_1;
now__::_thesis:_for_W_being_Subset_of_((TOP-REAL_n)_|_cA)_st_W_in_rng_F_holds_
W_is_closed
let W be Subset of ((TOP-REAL n) | cA); ::_thesis: ( W in rng F implies W is closed )
reconsider Z = 0 as real number ;
reconsider L = ].-infty,Z.] as Subset of R^1 by TOPMETR:17;
assume W in rng F ; ::_thesis: W is closed
then consider i being set such that
A9: i in dom F and
A10: F . i = W by FUNCT_1:def_3;
reconsider AEi = |-- (A,( the Enumeration of A . i)) as continuous Function of (TOP-REAL n),R^1 by A1, RLAFFIN3:32;
set AT = AEi | ((TOP-REAL n) | cA);
set Af = (AEi | ((TOP-REAL n) | cA)) * ff;
set AfT = ((AEi | ((TOP-REAL n) | cA)) * ff) - (AEi | ((TOP-REAL n) | cA));
A11: dom (((AEi | ((TOP-REAL n) | cA)) * ff) - (AEi | ((TOP-REAL n) | cA))) = the carrier of ((TOP-REAL n) | cA) by FUNCT_2:def_1;
reconsider AfT = ((AEi | ((TOP-REAL n) | cA)) * ff) - (AEi | ((TOP-REAL n) | cA)) as Function of ((TOP-REAL n) | cA),R^1 by TOPMETR:17;
A12: dom (AEi | ((TOP-REAL n) | cA)) = the carrier of ((TOP-REAL n) | cA) by FUNCT_2:def_1;
A13: AEi | ((TOP-REAL n) | cA) = AEi | the carrier of ((TOP-REAL n) | cA) by A7, TMAP_1:def_3;
A14: dom ((AEi | ((TOP-REAL n) | cA)) * ff) = the carrier of ((TOP-REAL n) | cA) by FUNCT_2:def_1;
A15: AfT " L c= H1(i)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in AfT " L or x in H1(i) )
assume A16: x in AfT " L ; ::_thesis: x in H1(i)
then reconsider v = x as Point of ((TOP-REAL n) | cA) ;
x in dom AfT by A16, FUNCT_1:def_7;
then A17: AfT . x = (((AEi | ((TOP-REAL n) | cA)) * ff) . x) - ((AEi | ((TOP-REAL n) | cA)) . x) by VALUED_1:13;
( AfT . x in L & ((AEi | ((TOP-REAL n) | cA)) * ff) . x = (AEi | ((TOP-REAL n) | cA)) . (f . x) ) by A14, A16, FUNCT_1:12, FUNCT_1:def_7;
then ((AEi | ((TOP-REAL n) | cA)) . (f . x)) - ((AEi | ((TOP-REAL n) | cA)) . x) <= 0 by A17, XXREAL_1:2;
then A18: (AEi | ((TOP-REAL n) | cA)) . (f . x) <= (AEi | ((TOP-REAL n) | cA)) . x by XREAL_1:50;
f . x in dom (AEi | ((TOP-REAL n) | cA)) by A14, A16, FUNCT_1:11;
then A19: (AEi | ((TOP-REAL n) | cA)) . (f . x) = AEi . (f . v) by A13, FUNCT_1:47;
(AEi | ((TOP-REAL n) | cA)) . x = AEi . v by A12, A13, FUNCT_1:47;
hence x in H1(i) by A18, A19; ::_thesis: verum
end;
A20: H1(i) c= AfT " L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in H1(i) or x in AfT " L )
assume x in H1(i) ; ::_thesis: x in AfT " L
then consider v being Element of ((TOP-REAL n) | cA) such that
A21: x = v and
A22: AEi . (f . v) <= AEi . v ;
f . v in rng f by A8, FUNCT_1:def_3;
then A23: AEi . (f . v) = (AEi | ((TOP-REAL n) | cA)) . (f . v) by A12, A13, FUNCT_1:47;
AEi . v = (AEi | ((TOP-REAL n) | cA)) . v by A12, A13, FUNCT_1:47;
then ((AEi | ((TOP-REAL n) | cA)) * ff) . v <= (AEi | ((TOP-REAL n) | cA)) . v by A14, A22, A23, FUNCT_1:12;
then (((AEi | ((TOP-REAL n) | cA)) * ff) . v) - ((AEi | ((TOP-REAL n) | cA)) . v) <= 0 by XREAL_1:47;
then AfT . v <= 0 by A11, VALUED_1:13;
then AfT . v in L by XXREAL_1:234;
hence x in AfT " L by A11, A21, FUNCT_1:def_7; ::_thesis: verum
end;
L is closed by BORSUK_5:41;
then A24: AfT " L is closed by PRE_TOPC:def_6;
F . i = H1(i) by A3, A9;
hence W is closed by A10, A15, A20, A24, XBOOLE_0:def_10; ::_thesis: verum
end;
then A25: rng F is closed by TOPS_2:def_2;
A26: dom the Enumeration of A = Seg (len the Enumeration of A) by FINSEQ_1:def_3;
A27: conv A c= Affin A by RLAFFIN1:65;
A28: rng the Enumeration of A = A by RLAFFIN3:def_1;
then len the Enumeration of A = card A by FINSEQ_4:62;
then A29: dom F = dom the Enumeration of A by A3, FINSEQ_3:29;
for S being Subset of (dom F) holds conv ( the Enumeration of A .: S) c= union (F .: S)
proof
let S be Subset of (dom F); ::_thesis: conv ( the Enumeration of A .: S) c= union (F .: S)
set ES = the Enumeration of A .: S;
percases ( S is empty or not S is empty ) ;
suppose S is empty ; ::_thesis: conv ( the Enumeration of A .: S) c= union (F .: S)
then conv ( the Enumeration of A .: S) is empty ;
hence conv ( the Enumeration of A .: S) c= union (F .: S) by XBOOLE_1:2; ::_thesis: verum
end;
supposeA30: not S is empty ; ::_thesis: conv ( the Enumeration of A .: S) c= union (F .: S)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in conv ( the Enumeration of A .: S) or x in union (F .: S) )
set fx = f . x;
set xES = x |-- ( the Enumeration of A .: S);
set fxA = (f . x) |-- A;
set xA = x |-- A;
assume A31: x in conv ( the Enumeration of A .: S) ; ::_thesis: x in union (F .: S)
A32: conv ( the Enumeration of A .: S) c= conv A by A28, RELAT_1:111, RLAFFIN1:3;
then reconsider v = x as Point of ((TOP-REAL n) | cA) by A7, A31;
A33: len (((f . x) |-- A) * the Enumeration of A) = len the Enumeration of A by FINSEQ_2:33;
A34: len the Enumeration of A = len ((x |-- ( the Enumeration of A .: S)) * the Enumeration of A) by FINSEQ_2:33;
then reconsider fxAE = ((f . x) |-- A) * the Enumeration of A, xESE = (x |-- ( the Enumeration of A .: S)) * the Enumeration of A as Element of (len the Enumeration of A) -tuples_on REAL by A33, FINSEQ_2:92;
A35: dom fxAE = Seg (len the Enumeration of A) by A33, FINSEQ_1:def_3;
A36: conv ( the Enumeration of A .: S) c= Affin ( the Enumeration of A .: S) by RLAFFIN1:65;
then A37: x |-- A = x |-- ( the Enumeration of A .: S) by A28, A31, RELAT_1:111, RLAFFIN1:77;
A38: the Enumeration of A .: S c= A by A28, RELAT_1:111;
A39: Carrier (x |-- ( the Enumeration of A .: S)) c= the Enumeration of A .: S by RLVECT_2:def_6;
the Enumeration of A .: S is affinely-independent by A28, RELAT_1:111, RLAFFIN1:43;
then ( sum (x |-- ( the Enumeration of A .: S)) = 1 & Carrier (x |-- ( the Enumeration of A .: S)) c= A ) by A31, A36, A38, A39, RLAFFIN1:def_7, XBOOLE_1:1;
then A40: ( Carrier ((f . x) |-- A) c= A & 1 = Sum ((x |-- ( the Enumeration of A .: S)) * the Enumeration of A) ) by A28, RLAFFIN1:30, RLVECT_2:def_6;
A41: f . x in rng f by A7, A8, A31, A32, FUNCT_1:def_3;
then A42: f . x in conv A by A7;
then sum ((f . x) |-- A) = 1 by A27, RLAFFIN1:def_7;
then A43: Sum fxAE = Sum xESE by A28, A40, RLAFFIN1:30;
A44: dom xESE = Seg (len the Enumeration of A) by A34, FINSEQ_1:def_3;
percases ( ex j being Nat st
( j in Seg (len the Enumeration of A) & fxAE . j < xESE . j ) or for j being Nat st j in Seg (len the Enumeration of A) holds
fxAE . j <= xESE . j ) by A43, RVSUM_1:83;
suppose ex j being Nat st
( j in Seg (len the Enumeration of A) & fxAE . j < xESE . j ) ; ::_thesis: x in union (F .: S)
then consider j being Nat such that
A45: j in Seg (len the Enumeration of A) and
A46: fxAE . j < xESE . j ;
A47: fxAE . j = ((f . x) |-- A) . ( the Enumeration of A . j) by A35, A45, FUNCT_1:12;
A48: xESE . j = (x |-- ( the Enumeration of A .: S)) . ( the Enumeration of A . j) by A44, A45, FUNCT_1:12;
then xESE . j = (|-- (A,( the Enumeration of A . j))) . x by A31, A37, RLAFFIN3:def_3;
then A49: (|-- (A,( the Enumeration of A . j))) . (f . v) <= (|-- (A,( the Enumeration of A . j))) . v by A42, A46, A47, RLAFFIN3:def_3;
A50: the Enumeration of A . j in dom ((f . x) |-- A) by A35, A45, FUNCT_1:11;
then 0 < (x |-- ( the Enumeration of A .: S)) . ( the Enumeration of A . j) by A7, A41, A46, A47, A48, RLAFFIN1:71;
then the Enumeration of A . j in Carrier (x |-- ( the Enumeration of A .: S)) by A50, RLVECT_2:19;
then consider i being set such that
A51: i in dom the Enumeration of A and
A52: i in S and
A53: the Enumeration of A . i = the Enumeration of A . j by A39, FUNCT_1:def_6;
i = j by A26, A45, A51, A53, FUNCT_1:def_4;
then A54: F . j in F .: S by A52, FUNCT_1:def_6;
H1(j) = F . j by A3, A26, A29, A45;
then x in F . j by A49;
hence x in union (F .: S) by A54, TARSKI:def_4; ::_thesis: verum
end;
supposeA55: for j being Nat st j in Seg (len the Enumeration of A) holds
fxAE . j <= xESE . j ; ::_thesis: x in union (F .: S)
consider j being set such that
A56: j in S by A30, XBOOLE_0:def_1;
reconsider j = j as Nat by A56;
A57: fxAE . j <= xESE . j by A26, A29, A55, A56;
A58: H1(j) = F . j by A3, A56;
xESE . j = (x |-- ( the Enumeration of A .: S)) . ( the Enumeration of A . j) by A26, A29, A44, A56, FUNCT_1:12;
then A59: xESE . j = (|-- (A,( the Enumeration of A . j))) . x by A31, A37, RLAFFIN3:def_3;
fxAE . j = ((f . x) |-- A) . ( the Enumeration of A . j) by A26, A29, A35, A56, FUNCT_1:12;
then (|-- (A,( the Enumeration of A . j))) . (f . v) <= (|-- (A,( the Enumeration of A . j))) . v by A42, A59, A57, RLAFFIN3:def_3;
then A60: x in F . j by A58;
F . j in F .: S by A56, FUNCT_1:def_6;
hence x in union (F .: S) by A60, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
end;
end;
then not meet (rng F) is empty by A2, A3, A25, Th22;
then consider v being set such that
A61: v in meet (rng F) by XBOOLE_0:def_1;
A62: v in cA by A7, A61;
then reconsider v = v as Element of (TOP-REAL n) ;
set fv = f . v;
set vA = v |-- A;
set fvA = (f . v) |-- A;
A63: len (((f . v) |-- A) * the Enumeration of A) = len the Enumeration of A by FINSEQ_2:33;
f . v in rng f by A8, A61, FUNCT_1:def_3;
then A64: f . v in cA by A7;
then ( Carrier ((f . v) |-- A) c= A & sum ((f . v) |-- A) = 1 ) by A27, RLAFFIN1:def_7, RLVECT_2:def_6;
then A65: ( Carrier (v |-- A) c= A & 1 = Sum (((f . v) |-- A) * the Enumeration of A) ) by A28, RLAFFIN1:30, RLVECT_2:def_6;
A66: len the Enumeration of A = len ((v |-- A) * the Enumeration of A) by FINSEQ_2:33;
then reconsider fvAE = ((f . v) |-- A) * the Enumeration of A, vAE = (v |-- A) * the Enumeration of A as Element of (len the Enumeration of A) -tuples_on REAL by A63, FINSEQ_2:92;
A67: dom fvAE = Seg (len the Enumeration of A) by A63, FINSEQ_1:def_3;
A68: dom vAE = Seg (len the Enumeration of A) by A66, FINSEQ_1:def_3;
A69: for j being Nat st j in Seg (len the Enumeration of A) holds
fvAE . j <= vAE . j
proof
let j be Nat; ::_thesis: ( j in Seg (len the Enumeration of A) implies fvAE . j <= vAE . j )
assume A70: j in Seg (len the Enumeration of A) ; ::_thesis: fvAE . j <= vAE . j
then ( F . j = H1(j) & F . j in rng F ) by A3, A26, A29, FUNCT_1:def_3;
then v in H1(j) by A61, SETFAM_1:def_1;
then A71: ex w being Element of ((TOP-REAL n) | cA) st
( w = v & (|-- (A,( the Enumeration of A . j))) . (f . w) <= (|-- (A,( the Enumeration of A . j))) . w ) ;
A72: (|-- (A,( the Enumeration of A . j))) . v = (v |-- A) . ( the Enumeration of A . j) by RLAFFIN3:def_3
.= vAE . j by A68, A70, FUNCT_1:12 ;
(|-- (A,( the Enumeration of A . j))) . (f . v) = ((f . v) |-- A) . ( the Enumeration of A . j) by A64, RLAFFIN3:def_3
.= fvAE . j by A67, A70, FUNCT_1:12 ;
hence fvAE . j <= vAE . j by A71, A72; ::_thesis: verum
end;
A73: Carrier (v |-- A) c= A by RLVECT_2:def_6;
sum (v |-- A) = 1 by A27, A62, RLAFFIN1:def_7;
then A74: Sum fvAE = Sum vAE by A28, A65, RLAFFIN1:30;
A75: Carrier ((f . v) |-- A) c= A by RLVECT_2:def_6;
A76: now__::_thesis:_for_w_being_Element_of_(TOP-REAL_n)_holds_(v_|--_A)_._w_=_((f_._v)_|--_A)_._w
let w be Element of (TOP-REAL n); ::_thesis: (v |-- A) . b1 = ((f . v) |-- A) . b1
percases ( w in A or not w in A ) ;
suppose w in A ; ::_thesis: (v |-- A) . b1 = ((f . v) |-- A) . b1
then consider j being set such that
A77: j in dom the Enumeration of A and
A78: the Enumeration of A . j = w by A28, FUNCT_1:def_3;
A79: ( fvAE . j = ((f . v) |-- A) . w & vAE . j = (v |-- A) . w ) by A77, A78, FUNCT_1:13;
( fvAE . j <= vAE . j & fvAE . j >= vAE . j ) by A26, A74, A69, A77, RVSUM_1:83;
hence (v |-- A) . w = ((f . v) |-- A) . w by A79, XXREAL_0:1; ::_thesis: verum
end;
supposeA80: not w in A ; ::_thesis: (v |-- A) . b1 = ((f . v) |-- A) . b1
then not w in Carrier (v |-- A) by A73;
then A81: (v |-- A) . w = 0 by RLVECT_2:19;
not w in Carrier ((f . v) |-- A) by A75, A80;
hence (v |-- A) . w = ((f . v) |-- A) . w by A81, RLVECT_2:19; ::_thesis: verum
end;
end;
end;
A82: Sum (v |-- A) = v by A27, A62, RLAFFIN1:def_7;
Sum ((f . v) |-- A) = f . v by A27, A64, RLAFFIN1:def_7;
then v = f . v by A76, A82, RLVECT_2:def_9;
hence ex p being Point of (TOP-REAL n) st
( p in dom f & f . p = p ) by A8, A61; ::_thesis: verum
end;
theorem :: SIMPLEX2:24
for n being Nat
for A being affinely-independent Subset of (TOP-REAL n) st card A = n + 1 holds
for f being continuous Function of ((TOP-REAL n) | (conv A)),((TOP-REAL n) | (conv A)) holds f is with_fixpoint
proof
let n be Nat; ::_thesis: for A being affinely-independent Subset of (TOP-REAL n) st card A = n + 1 holds
for f being continuous Function of ((TOP-REAL n) | (conv A)),((TOP-REAL n) | (conv A)) holds f is with_fixpoint
let A be affinely-independent Subset of (TOP-REAL n); ::_thesis: ( card A = n + 1 implies for f being continuous Function of ((TOP-REAL n) | (conv A)),((TOP-REAL n) | (conv A)) holds f is with_fixpoint )
assume A1: card A = n + 1 ; ::_thesis: for f being continuous Function of ((TOP-REAL n) | (conv A)),((TOP-REAL n) | (conv A)) holds f is with_fixpoint
let f be continuous Function of ((TOP-REAL n) | (conv A)),((TOP-REAL n) | (conv A)); ::_thesis: f is with_fixpoint
consider x being Point of (TOP-REAL n) such that
A2: ( x in dom f & f . x = x ) by A1, Th23;
x is_a_fixpoint_of f by A2, ABIAN:def_3;
hence f is with_fixpoint by ABIAN:def_5; ::_thesis: verum
end;
theorem Th25: :: SIMPLEX2:25
for n being Nat
for A being affinely-independent Subset of (TOP-REAL n) st card A = n + 1 holds
ind (conv A) = n
proof
let n be Nat; ::_thesis: for A being affinely-independent Subset of (TOP-REAL n) st card A = n + 1 holds
ind (conv A) = n
let A be affinely-independent Subset of (TOP-REAL n); ::_thesis: ( card A = n + 1 implies ind (conv A) = n )
set TR = TOP-REAL n;
assume A1: card A = n + 1 ; ::_thesis: ind (conv A) = n
set C = conv A;
A2: ind (conv A) >= n
proof
set E = the Enumeration of A;
assume A3: ind (conv A) < n ; ::_thesis: contradiction
not A is empty by A1;
then reconsider C = conv A as non empty Subset of (TOP-REAL n) ;
ind C is natural ;
then reconsider n1 = n - 1 as Nat by A3, NAT_1:20;
deffunc H1( set ) -> Element of bool the carrier of (TOP-REAL n) = C \ (conv (A \ {( the Enumeration of A . $1)}));
reconsider c = C as Subset of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) ;
set TRC = (TOP-REAL n) | C;
set carr = the carrier of ((TOP-REAL n) | C);
A4: ( TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) & TopStruct(# the carrier of ((TOP-REAL n) | C), the topology of ((TOP-REAL n) | C) #) = TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) | c ) by EUCLID:def_8, PRE_TOPC:36;
consider f being FinSequence such that
A5: ( len f = len the Enumeration of A & ( for k being Nat st k in dom f holds
f . k = H1(k) ) ) from FINSEQ_1:sch_2();
A6: [#] ((TOP-REAL n) | C) = C by PRE_TOPC:def_5;
rng f c= bool the carrier of ((TOP-REAL n) | C)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in bool the carrier of ((TOP-REAL n) | C) )
assume y in rng f ; ::_thesis: y in bool the carrier of ((TOP-REAL n) | C)
then consider x being set such that
A7: x in dom f and
A8: f . x = y by FUNCT_1:def_3;
f . x = H1(x) by A5, A7;
then f . x c= C by XBOOLE_1:36;
hence y in bool the carrier of ((TOP-REAL n) | C) by A6, A8; ::_thesis: verum
end;
then reconsider R = rng f as finite Subset-Family of ((TOP-REAL n) | C) ;
A9: rng the Enumeration of A = A by RLAFFIN3:def_1;
then A10: len the Enumeration of A = card A by FINSEQ_4:62;
A11: dom f = dom the Enumeration of A by A5, FINSEQ_3:29;
the carrier of ((TOP-REAL n) | C) c= union R
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of ((TOP-REAL n) | C) or x in union R )
assume A12: x in the carrier of ((TOP-REAL n) | C) ; ::_thesis: x in union R
assume A13: not x in union R ; ::_thesis: contradiction
now__::_thesis:_for_y_being_set_st_y_in_A_holds_
(x_|--_A)_._y_=_0
let y be set ; ::_thesis: ( y in A implies (x |-- A) . y = 0 )
assume A14: y in A ; ::_thesis: (x |-- A) . y = 0
then consider n being set such that
A15: n in dom the Enumeration of A and
A16: the Enumeration of A . n = y by A9, FUNCT_1:def_3;
reconsider n = n as Nat by A15;
f . n = H1(n) by A5, A11, A15;
then H1(n) in R by A11, A15, FUNCT_1:def_3;
then not x in H1(n) by A13, TARSKI:def_4;
then ( conv (A \ {( the Enumeration of A . n)}) c= Affin (A \ {( the Enumeration of A . n)}) & x in conv (A \ {( the Enumeration of A . n)}) ) by A6, A12, RLAFFIN1:65, XBOOLE_0:def_5;
then A17: x |-- A = x |-- (A \ {( the Enumeration of A . n)}) by RLAFFIN1:77, XBOOLE_1:36;
( Carrier (x |-- (A \ {( the Enumeration of A . n)})) c= A \ {( the Enumeration of A . n)} & the Enumeration of A . n in {( the Enumeration of A . n)} ) by RLVECT_2:def_6, TARSKI:def_1;
then not the Enumeration of A . n in Carrier (x |-- (A \ {( the Enumeration of A . n)})) by XBOOLE_0:def_5;
hence (x |-- A) . y = 0 by A14, A16, A17, RLVECT_2:19; ::_thesis: verum
end;
then A18: x in conv (A \ A) by A6, A12, RLAFFIN1:76;
A \ A = {} by XBOOLE_1:37;
hence contradiction by A18; ::_thesis: verum
end;
then A19: R is Cover of ((TOP-REAL n) | C) by SETFAM_1:def_11;
now__::_thesis:_for_U_being_Subset_of_((TOP-REAL_n)_|_C)_st_U_in_R_holds_
U_is_open
let U be Subset of ((TOP-REAL n) | C); ::_thesis: ( U in R implies U is open )
assume U in R ; ::_thesis: U is open
then consider x being set such that
A20: ( x in dom f & f . x = U ) by FUNCT_1:def_3;
reconsider cAE = conv (A \ {( the Enumeration of A . x)}) as Subset of ((TOP-REAL n) | C) by A6, RLAFFIN1:3, XBOOLE_1:36;
A \ {( the Enumeration of A . x)} is affinely-independent by RLAFFIN1:43, XBOOLE_1:36;
then A21: cAE is closed by TSEP_1:8;
U = cAE ` by A6, A5, A20;
hence U is open by A21; ::_thesis: verum
end;
then A22: ( ind ((TOP-REAL n) | C) = ind C & R is open ) by TOPDIM_1:17, TOPS_2:def_1;
ind C < n1 + 1 by A3;
then ind C <= n1 by NAT_1:13;
then consider G being finite Subset-Family of ((TOP-REAL n) | C) such that
A23: G is open and
A24: G is Cover of ((TOP-REAL n) | C) and
A25: G is_finer_than R and
card G <= (card R) * (n1 + 1) and
A26: order G <= n1 by A4, A22, A19, TOPDIM_2:23;
defpred S1[ Nat, set , set ] means $3 = { g where g is Subset of ((TOP-REAL n) | C) : ( g in G & ( g c= f . ($1 + 1) or g in $2 ) ) } ;
defpred S2[ set ] means ( $1 in G & $1 c= f . 1 );
consider G0 being Subset-Family of ((TOP-REAL n) | C) such that
A27: for x being set holds
( x in G0 iff ( x in bool the carrier of ((TOP-REAL n) | C) & S2[x] ) ) from SUBSET_1:sch_1();
A28: for k being Nat st 1 <= k & k < len the Enumeration of A holds
for x being Element of bool (bool the carrier of ((TOP-REAL n) | C)) ex y being Element of bool (bool the carrier of ((TOP-REAL n) | C)) st S1[k,x,y]
proof
let k be Nat; ::_thesis: ( 1 <= k & k < len the Enumeration of A implies for x being Element of bool (bool the carrier of ((TOP-REAL n) | C)) ex y being Element of bool (bool the carrier of ((TOP-REAL n) | C)) st S1[k,x,y] )
assume that
1 <= k and
k < len the Enumeration of A ; ::_thesis: for x being Element of bool (bool the carrier of ((TOP-REAL n) | C)) ex y being Element of bool (bool the carrier of ((TOP-REAL n) | C)) st S1[k,x,y]
let x be Element of bool (bool the carrier of ((TOP-REAL n) | C)); ::_thesis: ex y being Element of bool (bool the carrier of ((TOP-REAL n) | C)) st S1[k,x,y]
set y = { g where g is Subset of ((TOP-REAL n) | C) : ( g in G & ( g c= f . (k + 1) or g in x ) ) } ;
{ g where g is Subset of ((TOP-REAL n) | C) : ( g in G & ( g c= f . (k + 1) or g in x ) ) } c= bool the carrier of ((TOP-REAL n) | C)
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { g where g is Subset of ((TOP-REAL n) | C) : ( g in G & ( g c= f . (k + 1) or g in x ) ) } or z in bool the carrier of ((TOP-REAL n) | C) )
assume z in { g where g is Subset of ((TOP-REAL n) | C) : ( g in G & ( g c= f . (k + 1) or g in x ) ) } ; ::_thesis: z in bool the carrier of ((TOP-REAL n) | C)
then ex g being Subset of ((TOP-REAL n) | C) st
( g = z & g in G & ( g c= f . (k + 1) or g in x ) ) ;
hence z in bool the carrier of ((TOP-REAL n) | C) ; ::_thesis: verum
end;
hence ex y being Element of bool (bool the carrier of ((TOP-REAL n) | C)) st S1[k,x,y] ; ::_thesis: verum
end;
consider p being FinSequence of bool (bool the carrier of ((TOP-REAL n) | C)) such that
A29: len p = len the Enumeration of A and
A30: ( p /. 1 = G0 or len the Enumeration of A = 0 ) and
A31: for k being Nat st 1 <= k & k < len the Enumeration of A holds
S1[k,p /. k,p /. (k + 1)] from NAT_2:sch_1(A28);
defpred S3[ Nat, set ] means ( ( $1 = 1 implies $2 = union G0 ) & ( $1 <> 1 implies $2 = union ((p . $1) \ (p . ($1 - 1))) ) );
A32: for k being Nat st k in Seg (len the Enumeration of A) holds
ex x being set st S3[k,x]
proof
let k be Nat; ::_thesis: ( k in Seg (len the Enumeration of A) implies ex x being set st S3[k,x] )
( k = 1 or k <> 1 ) ;
hence ( k in Seg (len the Enumeration of A) implies ex x being set st S3[k,x] ) ; ::_thesis: verum
end;
consider h being FinSequence such that
A33: dom h = Seg (len the Enumeration of A) and
A34: for k being Nat st k in Seg (len the Enumeration of A) holds
S3[k,h . k] from FINSEQ_1:sch_1(A32);
A35: dom p = Seg (len the Enumeration of A) by A29, FINSEQ_1:def_3;
rng h c= bool the carrier of ((TOP-REAL n) | C)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng h or y in bool the carrier of ((TOP-REAL n) | C) )
assume y in rng h ; ::_thesis: y in bool the carrier of ((TOP-REAL n) | C)
then consider x being set such that
A36: x in dom h and
A37: h . x = y by FUNCT_1:def_3;
reconsider x = x as Nat by A36;
p . x in rng p by A35, A33, A36, FUNCT_1:def_3;
then reconsider px = p . x as Subset-Family of ((TOP-REAL n) | C) ;
( y = union G0 or y = union (px \ (p . (x - 1))) ) by A33, A34, A36, A37;
hence y in bool the carrier of ((TOP-REAL n) | C) ; ::_thesis: verum
end;
then reconsider h = h as FinSequence of bool the carrier of ((TOP-REAL n) | C) by FINSEQ_1:def_4;
A38: A is non empty affinely-independent Subset of (TOP-REAL n) by A1;
A39: 1 <= n + 1 by NAT_1:11;
the carrier of ((TOP-REAL n) | C) c= union (rng h)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of ((TOP-REAL n) | C) or x in union (rng h) )
assume x in the carrier of ((TOP-REAL n) | C) ; ::_thesis: x in union (rng h)
then x in union G by A24, SETFAM_1:45;
then consider y being set such that
A40: x in y and
A41: y in G by TARSKI:def_4;
consider z being set such that
A42: z in R and
A43: y c= z by A25, A41, SETFAM_1:def_2;
consider k being set such that
A44: k in dom f and
A45: f . k = z by A42, FUNCT_1:def_3;
reconsider k = k as Nat by A44;
A46: k >= 1 by A44, FINSEQ_3:25;
A47: len the Enumeration of A >= k by A5, A44, FINSEQ_3:25;
percases ( k = 1 or y in G0 or ( k > 1 & not y in G0 ) ) by A46, XXREAL_0:1;
supposeA48: ( k = 1 or y in G0 ) ; ::_thesis: x in union (rng h)
A49: 1 in Seg (len the Enumeration of A) by A1, A10, A39, FINSEQ_1:1;
then A50: h . 1 = union G0 by A34;
y in G0 by A27, A41, A43, A45, A48;
then A51: x in h . 1 by A40, A50, TARSKI:def_4;
h . 1 in rng h by A33, A49, FUNCT_1:def_3;
hence x in union (rng h) by A51, TARSKI:def_4; ::_thesis: verum
end;
supposeA52: ( k > 1 & not y in G0 ) ; ::_thesis: x in union (rng h)
defpred S4[ Nat] means ( $1 > 1 & $1 <= len the Enumeration of A & y c= f . $1 );
A53: ex k being Nat st S4[k] by A43, A45, A47, A52;
consider m being Nat such that
A54: ( S4[m] & ( for n being Nat st S4[n] holds
m <= n ) ) from NAT_1:sch_5(A53);
reconsider m1 = m - 1 as Element of NAT by A54, NAT_1:20;
defpred S5[ Nat] means ( 1 <= $1 & $1 <= m1 implies not y in p /. $1 );
m1 + 1 <= len the Enumeration of A by A54;
then A55: m1 < len the Enumeration of A by NAT_1:13;
A56: for n being Nat st S5[n] holds
S5[n + 1]
proof
let n be Nat; ::_thesis: ( S5[n] implies S5[n + 1] )
assume A57: S5[n] ; ::_thesis: S5[n + 1]
set n1 = n + 1;
assume that
1 <= n + 1 and
A58: n + 1 <= m1 ; ::_thesis: not y in p /. (n + 1)
n < m1 by A58, NAT_1:13;
then A59: n < len the Enumeration of A by A55, XXREAL_0:2;
percases ( n = 0 or n >= 1 ) by NAT_1:14;
suppose n = 0 ; ::_thesis: not y in p /. (n + 1)
hence not y in p /. (n + 1) by A1, A9, A30, A52, FINSEQ_4:62; ::_thesis: verum
end;
supposeA60: n >= 1 ; ::_thesis: not y in p /. (n + 1)
assume A61: y in p /. (n + 1) ; ::_thesis: contradiction
p /. (n + 1) = { g where g is Subset of ((TOP-REAL n) | C) : ( g in G & ( g c= f . (n + 1) or g in p /. n ) ) } by A31, A59, A60;
then ex g being Subset of ((TOP-REAL n) | C) st
( y = g & g in G & ( g c= f . (n + 1) or g in p /. n ) ) by A61;
then S4[n + 1] by A55, A57, A58, A60, NAT_1:13, XXREAL_0:2;
then m <= n + 1 by A54;
then m1 + 1 <= m1 by A58, XXREAL_0:2;
hence contradiction by NAT_1:13; ::_thesis: verum
end;
end;
end;
A62: S5[ 0 ] ;
A63: for n being Nat holds S5[n] from NAT_1:sch_2(A62, A56);
A64: m in dom p by A29, A54, FINSEQ_3:25;
then A65: h . m in rng h by A35, A33, FUNCT_1:def_3;
m1 + 1 > 1 by A54;
then A66: m1 >= 1 by NAT_1:13;
then A67: p /. m = { g where g is Subset of ((TOP-REAL n) | C) : ( g in G & ( g c= f . (m1 + 1) or g in p /. m1 ) ) } by A31, A55;
m1 in dom p by A29, A66, A55, FINSEQ_3:25;
then p . m1 = p /. m1 by PARTFUN1:def_6;
then A68: not y in p . m1 by A66, A63;
p . m = p /. m by A64, PARTFUN1:def_6;
then y in p . m by A41, A54, A67;
then y in (p . m) \ (p . m1) by A68, XBOOLE_0:def_5;
then A69: x in union ((p . m) \ (p . m1)) by A40, TARSKI:def_4;
h . m = union ((p . m) \ (p . m1)) by A35, A34, A54, A64;
hence x in union (rng h) by A69, A65, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
then A70: rng h is Cover of ((TOP-REAL n) | C) by SETFAM_1:def_11;
now__::_thesis:_for_A_being_Subset_of_((TOP-REAL_n)_|_C)_st_A_in_rng_h_holds_
A_is_open
let A be Subset of ((TOP-REAL n) | C); ::_thesis: ( A in rng h implies b1 is open )
assume A in rng h ; ::_thesis: b1 is open
then consider k being set such that
A71: k in dom h and
A72: h . k = A by FUNCT_1:def_3;
reconsider k = k as Nat by A71;
A73: k >= 1 by A33, A71, FINSEQ_1:1;
percases ( k = 1 or k > 1 ) by A73, XXREAL_0:1;
supposeA74: k = 1 ; ::_thesis: b1 is open
A75: G0 c= G
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in G0 or x in G )
assume x in G0 ; ::_thesis: x in G
hence x in G by A27; ::_thesis: verum
end;
h . k = union G0 by A33, A34, A71, A74;
hence A is open by A23, A72, A75, TOPS_2:11, TOPS_2:19; ::_thesis: verum
end;
supposeA76: k > 1 ; ::_thesis: b1 is open
then reconsider k1 = k - 1 as Element of NAT by NAT_1:20;
k1 + 1 > 1 by A76;
then A77: k1 >= 1 by NAT_1:13;
k1 + 1 <= len the Enumeration of A by A33, A71, FINSEQ_1:1;
then A78: k1 < len the Enumeration of A by NAT_1:13;
then k1 in dom p by A29, A77, FINSEQ_3:25;
then A79: p . k1 = p /. k1 by PARTFUN1:def_6;
A80: S1[k1,p /. k1,p /. (k1 + 1)] by A31, A77, A78;
p /. k c= G
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in p /. k or x in G )
assume x in p /. k ; ::_thesis: x in G
then ex g being Subset of ((TOP-REAL n) | C) st
( x = g & g in G & ( g c= f . k or g in p /. k1 ) ) by A80;
hence x in G ; ::_thesis: verum
end;
then p /. k is open by A23, TOPS_2:11;
then A81: (p /. k) \ (p /. (k - 1)) is open by TOPS_2:15;
A82: p . k = p /. k by A35, A33, A71, PARTFUN1:def_6;
A = union ((p . k) \ (p . (k - 1))) by A33, A34, A71, A72, A76;
hence A is open by A82, A81, A79, TOPS_2:19; ::_thesis: verum
end;
end;
end;
then A83: rng h is open by TOPS_2:def_1;
(TOP-REAL n) | C is compact by COMPTS_1:3;
then consider gx being Subset-Family of ((TOP-REAL n) | C) such that
gx is open and
A84: gx is Cover of ((TOP-REAL n) | C) and
A85: clf gx is_finer_than rng h and
A86: gx is locally_finite by A4, A70, A83, PCOMPS_1:22, PCOMPS_2:3;
set cgx = clf gx;
defpred S4[ set , set ] means $2 = union { u where u is Subset of ((TOP-REAL n) | C) : ( u in clf gx & u c= h . $1 ) } ;
A87: for k being Nat st k in Seg (len the Enumeration of A) holds
ex x being Element of bool the carrier of ((TOP-REAL n) | C) st S4[k,x]
proof
let k be Nat; ::_thesis: ( k in Seg (len the Enumeration of A) implies ex x being Element of bool the carrier of ((TOP-REAL n) | C) st S4[k,x] )
set U = { u where u is Subset of ((TOP-REAL n) | C) : ( u in clf gx & u c= h . k ) } ;
{ u where u is Subset of ((TOP-REAL n) | C) : ( u in clf gx & u c= h . k ) } c= bool the carrier of ((TOP-REAL n) | C)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { u where u is Subset of ((TOP-REAL n) | C) : ( u in clf gx & u c= h . k ) } or x in bool the carrier of ((TOP-REAL n) | C) )
assume x in { u where u is Subset of ((TOP-REAL n) | C) : ( u in clf gx & u c= h . k ) } ; ::_thesis: x in bool the carrier of ((TOP-REAL n) | C)
then ex u being Subset of ((TOP-REAL n) | C) st
( u = x & u in clf gx & u c= h . k ) ;
hence x in bool the carrier of ((TOP-REAL n) | C) ; ::_thesis: verum
end;
then reconsider U = { u where u is Subset of ((TOP-REAL n) | C) : ( u in clf gx & u c= h . k ) } as Subset-Family of ((TOP-REAL n) | C) ;
union U is Subset of ((TOP-REAL n) | C) ;
hence ( k in Seg (len the Enumeration of A) implies ex x being Element of bool the carrier of ((TOP-REAL n) | C) st S4[k,x] ) ; ::_thesis: verum
end;
consider GX being FinSequence of bool the carrier of ((TOP-REAL n) | C) such that
A88: ( dom GX = Seg (len the Enumeration of A) & ( for k being Nat st k in Seg (len the Enumeration of A) holds
S4[k,GX . k] ) ) from FINSEQ_1:sch_5(A87);
A89: for i being Nat st i in dom GX holds
GX . i c= h . i
proof
let i be Nat; ::_thesis: ( i in dom GX implies GX . i c= h . i )
set U = { u where u is Subset of ((TOP-REAL n) | C) : ( u in clf gx & u c= h . i ) } ;
now__::_thesis:_for_x_being_set_st_x_in__{__u_where_u_is_Subset_of_((TOP-REAL_n)_|_C)_:_(_u_in_clf_gx_&_u_c=_h_._i_)__}__holds_
x_c=_h_._i
let x be set ; ::_thesis: ( x in { u where u is Subset of ((TOP-REAL n) | C) : ( u in clf gx & u c= h . i ) } implies x c= h . i )
assume x in { u where u is Subset of ((TOP-REAL n) | C) : ( u in clf gx & u c= h . i ) } ; ::_thesis: x c= h . i
then ex u being Subset of ((TOP-REAL n) | C) st
( x = u & u in clf gx & u c= h . i ) ;
hence x c= h . i ; ::_thesis: verum
end;
then A90: union { u where u is Subset of ((TOP-REAL n) | C) : ( u in clf gx & u c= h . i ) } c= h . i by ZFMISC_1:76;
assume i in dom GX ; ::_thesis: GX . i c= h . i
hence GX . i c= h . i by A88, A90; ::_thesis: verum
end;
A91: dom the Enumeration of A = Seg (len the Enumeration of A) by FINSEQ_1:def_3;
A92: for k being Nat st k in Seg (len the Enumeration of A) holds
h . k misses conv (A \ {( the Enumeration of A . k)})
proof
let k be Nat; ::_thesis: ( k in Seg (len the Enumeration of A) implies h . k misses conv (A \ {( the Enumeration of A . k)}) )
assume A93: k in Seg (len the Enumeration of A) ; ::_thesis: h . k misses conv (A \ {( the Enumeration of A . k)})
then A94: k >= 1 by FINSEQ_1:1;
A95: S3[k,h . k] by A34, A93;
assume h . k meets conv (A \ {( the Enumeration of A . k)}) ; ::_thesis: contradiction
then consider x being set such that
A96: x in h . k and
A97: x in conv (A \ {( the Enumeration of A . k)}) by XBOOLE_0:3;
percases ( k = 1 or k > 1 ) by A94, XXREAL_0:1;
supposeA98: k = 1 ; ::_thesis: contradiction
then consider y being set such that
A99: x in y and
A100: y in G0 by A95, A96, TARSKI:def_4;
S2[y] by A27, A100;
then y c= H1(k) by A5, A11, A91, A93, A98;
hence contradiction by A97, A99, XBOOLE_0:def_5; ::_thesis: verum
end;
supposeA101: k > 1 ; ::_thesis: contradiction
then reconsider k1 = k - 1 as Element of NAT by NAT_1:20;
len the Enumeration of A >= k1 + 1 by A93, FINSEQ_1:1;
then A102: len the Enumeration of A > k1 by NAT_1:13;
k1 + 1 > 1 by A101;
then A103: k1 >= 1 by NAT_1:13;
then A104: S1[k1,p /. k1,p /. (k1 + 1)] by A31, A102;
k1 in dom p by A29, A103, A102, FINSEQ_3:25;
then A105: p /. k1 = p . k1 by PARTFUN1:def_6;
A106: p /. k = p . k by A35, A93, PARTFUN1:def_6;
consider y being set such that
A107: x in y and
A108: y in (p . k) \ (p . (k - 1)) by A95, A96, A101, TARSKI:def_4;
y in p . k by A108;
then consider g being Subset of ((TOP-REAL n) | C) such that
A109: y = g and
g in G and
A110: ( g c= f . k or g in p . k1 ) by A104, A106, A105;
f . k = H1(k) by A5, A11, A91, A93;
hence contradiction by A97, A107, A108, A109, A110, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
end;
the carrier of ((TOP-REAL n) | C) c= union (rng GX)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of ((TOP-REAL n) | C) or x in union (rng GX) )
assume A111: x in the carrier of ((TOP-REAL n) | C) ; ::_thesis: x in union (rng GX)
( union gx = the carrier of ((TOP-REAL n) | C) & union gx c= union (clf gx) ) by A84, PCOMPS_1:19, SETFAM_1:45;
then consider y being set such that
A112: x in y and
A113: y in clf gx by A111, TARSKI:def_4;
consider r being set such that
A114: r in rng h and
A115: y c= r by A85, A113, SETFAM_1:def_2;
consider k being set such that
A116: k in dom h and
A117: h . k = r by A114, FUNCT_1:def_3;
A118: S4[k,GX . k] by A33, A88, A116;
A119: GX . k in rng GX by A33, A88, A116, FUNCT_1:def_3;
y in { u where u is Subset of ((TOP-REAL n) | C) : ( u in clf gx & u c= h . k ) } by A113, A115, A117;
then x in GX . k by A112, A118, TARSKI:def_4;
hence x in union (rng GX) by A119, TARSKI:def_4; ::_thesis: verum
end;
then A120: rng GX is Cover of ((TOP-REAL n) | C) by SETFAM_1:def_11;
A121: for S being Subset of (dom GX) holds conv ( the Enumeration of A .: S) c= union (GX .: S)
proof
let S be Subset of (dom GX); ::_thesis: conv ( the Enumeration of A .: S) c= union (GX .: S)
A122: rng GX = GX .: (dom GX) by RELAT_1:113;
A123: union (rng GX) = the carrier of ((TOP-REAL n) | C) by A120, SETFAM_1:45;
percases ( S = dom GX or not dom GX c= S ) by XBOOLE_0:def_10;
suppose S = dom GX ; ::_thesis: conv ( the Enumeration of A .: S) c= union (GX .: S)
hence conv ( the Enumeration of A .: S) c= union (GX .: S) by A6, A9, A91, A88, A122, A123, RELAT_1:113; ::_thesis: verum
end;
supposeA124: not dom GX c= S ; ::_thesis: conv ( the Enumeration of A .: S) c= union (GX .: S)
set U = { (conv (A \ {( the Enumeration of A . i)})) where i is Element of NAT : i in (dom the Enumeration of A) \ S } ;
not (dom GX) \ S is empty by A124, XBOOLE_1:37;
then A125: conv ( the Enumeration of A .: S) = meet { (conv (A \ {( the Enumeration of A . i)})) where i is Element of NAT : i in (dom the Enumeration of A) \ S } by A91, A88, Th12;
A126: meet { (conv (A \ {( the Enumeration of A . i)})) where i is Element of NAT : i in (dom the Enumeration of A) \ S } misses union (GX .: ((dom the Enumeration of A) \ S))
proof
assume meet { (conv (A \ {( the Enumeration of A . i)})) where i is Element of NAT : i in (dom the Enumeration of A) \ S } meets union (GX .: ((dom the Enumeration of A) \ S)) ; ::_thesis: contradiction
then consider x being set such that
A127: x in meet { (conv (A \ {( the Enumeration of A . i)})) where i is Element of NAT : i in (dom the Enumeration of A) \ S } and
A128: x in union (GX .: ((dom the Enumeration of A) \ S)) by XBOOLE_0:3;
consider y being set such that
A129: x in y and
A130: y in GX .: ((dom the Enumeration of A) \ S) by A128, TARSKI:def_4;
consider i being set such that
A131: i in dom GX and
A132: i in (dom the Enumeration of A) \ S and
A133: GX . i = y by A130, FUNCT_1:def_6;
reconsider i = i as Element of NAT by A131;
conv (A \ {( the Enumeration of A . i)}) in { (conv (A \ {( the Enumeration of A . i)})) where i is Element of NAT : i in (dom the Enumeration of A) \ S } by A132;
then A134: meet { (conv (A \ {( the Enumeration of A . i)})) where i is Element of NAT : i in (dom the Enumeration of A) \ S } c= conv (A \ {( the Enumeration of A . i)}) by SETFAM_1:7;
y c= h . i by A89, A131, A133;
then h . i meets conv (A \ {( the Enumeration of A . i)}) by A127, A129, A134, XBOOLE_0:3;
hence contradiction by A92, A88, A131; ::_thesis: verum
end;
dom GX = dom the Enumeration of A by A88, FINSEQ_1:def_3;
then rng GX = GX .: (S \/ ((dom the Enumeration of A) \ S)) by A122, XBOOLE_1:45
.= (GX .: S) \/ (GX .: ((dom the Enumeration of A) \ S)) by RELAT_1:120 ;
then A135: (union (GX .: S)) \/ (union (GX .: ((dom the Enumeration of A) \ S))) = C by A6, A123, ZFMISC_1:78;
conv ( the Enumeration of A .: S) c= C by A9, RELAT_1:111, RLAFFIN1:3;
hence conv ( the Enumeration of A .: S) c= union (GX .: S) by A125, A135, A126, XBOOLE_1:73; ::_thesis: verum
end;
end;
end;
A136: clf gx is locally_finite by A86, PCOMPS_1:18;
now__::_thesis:_for_A_being_Subset_of_((TOP-REAL_n)_|_C)_st_A_in_rng_GX_holds_
A_is_closed
let A be Subset of ((TOP-REAL n) | C); ::_thesis: ( A in rng GX implies A is closed )
assume A in rng GX ; ::_thesis: A is closed
then consider k being set such that
A137: ( k in dom GX & GX . k = A ) by FUNCT_1:def_3;
set U = { u where u is Subset of ((TOP-REAL n) | C) : ( u in clf gx & u c= h . k ) } ;
A138: { u where u is Subset of ((TOP-REAL n) | C) : ( u in clf gx & u c= h . k ) } c= clf gx
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { u where u is Subset of ((TOP-REAL n) | C) : ( u in clf gx & u c= h . k ) } or x in clf gx )
assume x in { u where u is Subset of ((TOP-REAL n) | C) : ( u in clf gx & u c= h . k ) } ; ::_thesis: x in clf gx
then ex u being Subset of ((TOP-REAL n) | C) st
( x = u & u in clf gx & u c= h . k ) ;
hence x in clf gx ; ::_thesis: verum
end;
then reconsider U = { u where u is Subset of ((TOP-REAL n) | C) : ( u in clf gx & u c= h . k ) } as Subset-Family of ((TOP-REAL n) | C) by XBOOLE_1:1;
U is closed by A138, PCOMPS_1:11, TOPS_2:12;
then union U is closed by A136, A138, PCOMPS_1:9, PCOMPS_1:21;
hence A is closed by A88, A137; ::_thesis: verum
end;
then A139: rng GX is closed by TOPS_2:def_2;
len GX = card A by A10, A88, FINSEQ_1:def_3;
then not meet (rng GX) is empty by A139, A38, A121, Th22;
then consider I being set such that
A140: I in meet (rng GX) by XBOOLE_0:def_1;
defpred S5[ Nat, set ] means ( $2 in G & I in $2 & $2 in p . $1 & ( $1 <> 1 implies not $2 in p . ($1 - 1) ) );
A141: for k being Nat st k in Seg (len the Enumeration of A) holds
ex x being Element of bool the carrier of ((TOP-REAL n) | C) st S5[k,x]
proof
let k be Nat; ::_thesis: ( k in Seg (len the Enumeration of A) implies ex x being Element of bool the carrier of ((TOP-REAL n) | C) st S5[k,x] )
assume A142: k in Seg (len the Enumeration of A) ; ::_thesis: ex x being Element of bool the carrier of ((TOP-REAL n) | C) st S5[k,x]
then A143: k >= 1 by FINSEQ_1:1;
A144: k <= len the Enumeration of A by A142, FINSEQ_1:1;
A145: ( GX . k c= h . k & S3[k,h . k] ) by A34, A88, A89, A142;
GX . k in rng GX by A88, A142, FUNCT_1:def_3;
then meet (rng GX) c= GX . k by SETFAM_1:7;
then A146: I in GX . k by A140;
percases ( k = 1 or k > 1 ) by A143, XXREAL_0:1;
supposeA147: k = 1 ; ::_thesis: ex x being Element of bool the carrier of ((TOP-REAL n) | C) st S5[k,x]
1 in dom p by A1, A10, A35, A39, FINSEQ_1:1;
then A148: p . 1 = G0 by A1, A9, A30, FINSEQ_4:62, PARTFUN1:def_6;
consider g being set such that
A149: I in g and
A150: g in G0 by A146, A145, A147, TARSKI:def_4;
g in G by A27, A150;
hence ex x being Element of bool the carrier of ((TOP-REAL n) | C) st S5[k,x] by A147, A149, A150, A148; ::_thesis: verum
end;
supposeA151: k > 1 ; ::_thesis: ex x being Element of bool the carrier of ((TOP-REAL n) | C) st S5[k,x]
then reconsider k1 = k - 1 as Nat by NAT_1:20;
A152: k1 + 1 = k ;
then A153: k1 < len the Enumeration of A by A144, NAT_1:13;
k1 >= 1 by A151, A152, NAT_1:13;
then A154: S1[k1,p /. k1,p /. k] by A31, A153;
A155: p . k = p /. k by A35, A142, PARTFUN1:def_6;
consider g being set such that
A156: I in g and
A157: g in (p . k) \ (p . (k - 1)) by A146, A145, A151, TARSKI:def_4;
A158: not g in p . (k - 1) by A157, XBOOLE_0:def_5;
g in p . k by A157;
then ex gg being Subset of ((TOP-REAL n) | C) st
( g = gg & gg in G & ( gg c= f . (k1 + 1) or gg in p /. k1 ) ) by A154, A155;
hence ex x being Element of bool the carrier of ((TOP-REAL n) | C) st S5[k,x] by A156, A157, A158; ::_thesis: verum
end;
end;
end;
consider t being FinSequence of bool the carrier of ((TOP-REAL n) | C) such that
A159: ( dom t = Seg (len the Enumeration of A) & ( for k being Nat st k in Seg (len the Enumeration of A) holds
S5[k,t . k] ) ) from FINSEQ_1:sch_5(A141);
A160: now__::_thesis:_for_i,_j_being_Nat_st_i_in_dom_t_&_j_in_dom_t_&_i_<_j_holds_
not_t_._i_=_t_._j
let i, j be Nat; ::_thesis: ( i in dom t & j in dom t & i < j implies not t . i = t . j )
assume that
A161: i in dom t and
A162: j in dom t and
A163: i < j ; ::_thesis: not t . i = t . j
A164: j <= len the Enumeration of A by A159, A162, FINSEQ_1:1;
defpred S6[ Nat] means ( i <= $1 & $1 < j implies t . i in p . $1 );
A165: S5[i,t . i] by A159, A161;
A166: 1 <= i by A159, A161, FINSEQ_1:1;
A167: for k being Nat st S6[k] holds
S6[k + 1]
proof
let k be Nat; ::_thesis: ( S6[k] implies S6[k + 1] )
assume A168: S6[k] ; ::_thesis: S6[k + 1]
set k1 = k + 1;
assume that
A169: i <= k + 1 and
A170: k + 1 < j ; ::_thesis: t . i in p . (k + 1)
A171: k < j by A170, NAT_1:13;
percases ( i = k + 1 or i <= k ) by A169, NAT_1:8;
suppose i = k + 1 ; ::_thesis: t . i in p . (k + 1)
hence t . i in p . (k + 1) by A159, A161; ::_thesis: verum
end;
supposeA172: i <= k ; ::_thesis: t . i in p . (k + 1)
( 1 <= k + 1 & k + 1 <= len the Enumeration of A ) by A166, A164, A169, A170, XXREAL_0:2;
then A173: k + 1 in dom p by A35, FINSEQ_1:1;
A174: k < len the Enumeration of A by A164, A171, XXREAL_0:2;
A175: 1 <= k by A166, A172, XXREAL_0:2;
then k in dom p by A35, A174, FINSEQ_1:1;
then A176: p . k = p /. k by PARTFUN1:def_6;
S1[k,p /. k,p /. (k + 1)] by A31, A175, A174;
then p . (k + 1) = { g where g is Subset of ((TOP-REAL n) | C) : ( g in G & ( g c= f . (k + 1) or g in p . k ) ) } by A173, A176, PARTFUN1:def_6;
hence t . i in p . (k + 1) by A165, A168, A170, A172, NAT_1:13; ::_thesis: verum
end;
end;
end;
A177: S6[ 0 ] by A165;
A178: for k being Nat holds S6[k] from NAT_1:sch_2(A177, A167);
reconsider j1 = j - 1 as Nat by A163, NAT_1:20;
assume A179: t . i = t . j ; ::_thesis: contradiction
A180: j1 + 1 = j ;
then A181: j1 < j by NAT_1:13;
A182: j <> 1 by A159, A161, A163, FINSEQ_1:1;
i <= j1 by A163, A180, NAT_1:13;
then t . i in p . j1 by A181, A178;
hence contradiction by A159, A162, A179, A182; ::_thesis: verum
end;
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_t_&_x2_in_dom_t_&_t_._x1_=_t_._x2_holds_
not_x1_<>_x2
let x1, x2 be set ; ::_thesis: ( x1 in dom t & x2 in dom t & t . x1 = t . x2 implies not x1 <> x2 )
assume A183: ( x1 in dom t & x2 in dom t ) ; ::_thesis: ( t . x1 = t . x2 implies not x1 <> x2 )
then reconsider i1 = x1, i2 = x2 as Nat ;
assume A184: t . x1 = t . x2 ; ::_thesis: not x1 <> x2
assume x1 <> x2 ; ::_thesis: contradiction
then ( i1 > i2 or i1 < i2 ) by XXREAL_0:1;
hence contradiction by A160, A183, A184; ::_thesis: verum
end;
then t is one-to-one by FUNCT_1:def_4;
then A185: card (rng t) = len t by FINSEQ_4:62
.= len the Enumeration of A by A159, FINSEQ_1:def_3
.= n + 1 by A1, A9, FINSEQ_4:62 ;
then A186: not rng t is empty ;
A187: now__::_thesis:_for_x_being_set_st_x_in_rng_t_holds_
I_in_x
let x be set ; ::_thesis: ( x in rng t implies I in x )
assume x in rng t ; ::_thesis: I in x
then consider i being set such that
A188: ( i in dom t & t . i = x ) by FUNCT_1:def_3;
thus I in x by A159, A188; ::_thesis: verum
end;
A189: rng t c= G
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng t or y in G )
assume y in rng t ; ::_thesis: y in G
then consider x being set such that
A190: ( x in dom t & t . x = y ) by FUNCT_1:def_3;
thus y in G by A159, A190; ::_thesis: verum
end;
n < card (rng t) by A185, NAT_1:13;
then card n in card (card (rng t)) by NAT_1:41;
then n1 + 1 in card (rng t) by CARD_1:42;
then meet (rng t) is empty by A26, A189, TOPDIM_2:2;
hence contradiction by A186, A187, SETFAM_1:def_1; ::_thesis: verum
end;
( ind (conv A) <= ind (TOP-REAL n) & ind (TOP-REAL n) <= n ) by TOPDIM_1:20, TOPDIM_2:21;
then ind (conv A) <= n by XXREAL_0:2;
hence ind (conv A) = n by A2, XXREAL_0:1; ::_thesis: verum
end;
theorem :: SIMPLEX2:26
for n being Nat holds ind (TOP-REAL n) = n
proof
let n be Nat; ::_thesis: ind (TOP-REAL n) = n
set T = TOP-REAL n;
consider I being affinely-independent Subset of (TOP-REAL n) such that
A1: ( {} (TOP-REAL n) c= I & I c= [#] (TOP-REAL n) & Affin I = Affin ([#] (TOP-REAL n)) ) by RLAFFIN1:60;
[#] (TOP-REAL n) is Affine by RUSUB_4:22;
then ( dim (TOP-REAL n) = n & Affin ([#] (TOP-REAL n)) = [#] (TOP-REAL n) ) by RLAFFIN1:50, RLAFFIN3:4;
then card I = n + 1 by A1, RLAFFIN3:6;
then ind (conv I) = n by Th25;
then ( ind (TOP-REAL n) >= n & ind (TOP-REAL n) <= n ) by TOPDIM_1:20, TOPDIM_2:21;
hence ind (TOP-REAL n) = n by XXREAL_0:1; ::_thesis: verum
end;