:: 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;