simplex2.miz



    begin

    reserve M for non empty MetrSpace,

F,G for open Subset-Family of ( TopSpaceMetr M);

    reconsider jj = 1 as positive Real;

    definition

      let M;

      let F be Subset-Family of ( TopSpaceMetr M);

      :: SIMPLEX2:def1

      mode Lebesgue_number of F -> positive Real means

      : Def1: for p be Point of M holds ex A be Subset of ( TopSpaceMetr M) st A in F & ( Ball (p,it )) c= A;

      existence

      proof

        set TM = ( TopSpaceMetr M);

        consider G be Subset-Family of TM such that

         A4: G c= F and

         A5: G is Cover of TM and

         A6: G is finite by A1, A2, A3, COMPTS_1:def 1;

        per cases ;

          suppose

           A7: ( [#] TM) in G;

          take R = jj;

          let x be Point of M;

          take ( [#] TM);

          thus thesis by A4, A7;

        end;

          suppose

           A8: not ( [#] TM) in G;

          set cTM = ( [#] TM);

          set FUNCS = ( Funcs (( [#] TM), REAL ));

          consider g be FinSequence such that

           A9: ( rng g) = G and g is one-to-one by A6, FINSEQ_4: 58;

          defpred P[ Nat, set, set] means for f1,f2 be Function of TM, R^1 st f1 = $2 & f2 = $3 & f1 is continuous holds f2 is continuous & ex A be non empty Subset of TM st (A ` ) = (g . ($1 + 1)) & for x be Point of TM holds (f2 . x) = ( max ((f1 . x),(( dist_min A) . x)));

          ( union G) is non empty by A5, SETFAM_1: 45;

          then

           A10: g is non empty by A9, ZFMISC_1: 2;

          then

           A11: ( len g) >= 1 by NAT_1: 14;

          then

           A12: 1 in ( dom g) by FINSEQ_3: 25;

          then

           A13: (g . 1) in ( rng g) by FUNCT_1:def 3;

          then

          reconsider g1 = (g . 1) as Subset of TM by A9;

          

           A14: ((g1 ` ) ` ) <> ( [#] TM) by A8, A9, A12, FUNCT_1:def 3;

          g1 is open by A2, A4, A9, A13, TOPS_2:def 1;

          then

          reconsider g19 = (g1 ` ) as non empty closed Subset of TM by A14;

          reconsider Dg19 = ( dist_min g19) as Element of FUNCS by FUNCT_2: 8, TOPMETR: 17;

          

           A15: for n be Nat st 1 <= n & n < ( len g) holds for x be Element of FUNCS holds ex y be Element of FUNCS st P[n, x, y]

          proof

            let n be Nat such that 1 <= n and

             A16: n < ( len g);

            let x be Element of FUNCS;

            reconsider fx = x as Function of TM, R^1 by TOPMETR: 17;

            per cases ;

              suppose

               A17: not fx is continuous;

              take y = x;

              thus thesis by A17;

            end;

              suppose

               A18: fx is continuous;

              1 <= (n + 1) & (n + 1) <= ( len g) by A16, NAT_1: 11, NAT_1: 13;

              then

               A19: (n + 1) in ( dom g) by FINSEQ_3: 25;

              then (g . (n + 1)) in G by A9, FUNCT_1:def 3;

              then

              reconsider A = (g . (n + 1)) as Subset of TM;

              ((A ` ) ` ) <> ( [#] TM) by A8, A9, A19, FUNCT_1:def 3;

              then

              reconsider A9 = (A ` ) as non empty Subset of TM;

               R^1 is SubSpace of R^1 by TSEP_1: 2;

              then

              consider h be continuous Function of TM, R^1 such that

               A20: for x be Point of TM holds (h . x) = ( max ((fx . x),(( dist_min A9) . x))) by A18, TOPGEN_5: 50;

              reconsider y = h as Element of FUNCS by FUNCT_2: 8, TOPMETR: 17;

              take y;

              let f1,f2 be Function of TM, R^1 such that

               A21: f1 = x and

               A22: f2 = y and f1 is continuous;

              thus f2 is continuous by A22;

              take A9;

              thus thesis by A20, A21, A22;

            end;

          end;

          consider p be FinSequence of FUNCS such that

           A23: ( len p) = ( len g) and

           A24: (p /. 1) = Dg19 or ( len g) = 0 and

           A25: for n be Nat st 1 <= n & n < ( len g) holds P[n, (p /. n), (p /. (n + 1))] from NAT_2:sch 1( A15);

          

           A26: ( len p) in ( dom p) by A11, A23, FINSEQ_3: 25;

          (p /. ( len p)) is Element of FUNCS;

          then

          reconsider pL = (p /. ( len p)) as Function of TM, R^1 by TOPMETR: 17;

          reconsider rngPL = ( rng pL) as Subset of R^1 by RELAT_1:def 19;

          set cRpL = ( [#] rngPL);

          

           A27: cRpL = ( rng pL) by WEIERSTR:def 1;

          

           A28: ( dom p) = ( dom g) by A23, FINSEQ_3: 29;

          defpred Q[ Nat] means for f be Function of TM, R^1 st $1 in ( dom p) & f = (p /. $1) holds f is continuous & for j be Nat, h be Function of TM, R^1 st j <= $1 & j in ( dom p) & h = (p /. j) holds for x be Point of TM holds (h . x) <= (f . x);

          

           A29: for n be Nat st Q[n] holds Q[(n + 1)]

          proof

            let n be Nat;

            assume

             A30: Q[n];

            let f be Function of TM, R^1 such that

             A31: (n + 1) in ( dom p) and

             A32: f = (p /. (n + 1));

            per cases ;

              suppose

               A33: n = 0 ;

              hence f is continuous by A10, A24, A32;

              let j be Nat, g be Function of TM, R^1 ;

              assume that

               A34: j <= (n + 1) and

               A35: j in ( dom p) and

               A36: g = (p /. j);

              1 <= j by A35, FINSEQ_3: 25;

              hence thesis by A32, A33, A34, A36, XXREAL_0: 1;

            end;

              suppose n > 0 ;

              then

              reconsider n1 = (n - 1) as Element of NAT by NAT_1: 20;

              (p /. n) is Element of FUNCS;

              then

              reconsider pn = (p /. n) as Function of TM, R^1 by TOPMETR: 17;

              (n + 1) <= ( len p) by A31, FINSEQ_3: 25;

              then

               A37: 1 <= (n1 + 1) & n < ( len p) by NAT_1: 11, NAT_1: 13;

              then

               A38: n in ( dom p) by FINSEQ_3: 25;

              then

               A39: pn is continuous by A30;

              hence f is continuous by A23, A25, A32, A37;

              consider A be non empty Subset of TM such that (A ` ) = (g . (n + 1)) and

               A40: for y be Point of TM holds (f . y) = ( max ((pn . y),(( dist_min A) . y))) by A23, A25, A32, A37, A39;

              let j be Nat, h be Function of TM, R^1 such that

               A41: j <= (n + 1) and

               A42: j in ( dom p) and

               A43: h = (p /. j);

              let x be Point of TM;

              

               A44: (f . x) = ( max ((pn . x),(( dist_min A) . x))) by A40;

              per cases by A41, NAT_1: 8;

                suppose

                 A45: j <= n;

                

                 A46: (pn . x) <= (f . x) by A44, XXREAL_0: 25;

                (h . x) <= (pn . x) by A30, A38, A42, A43, A45;

                hence thesis by A46, XXREAL_0: 2;

              end;

                suppose j = (n + 1);

                hence thesis by A32, A43;

              end;

            end;

          end;

          

           A47: Q[ 0 ] by FINSEQ_3: 25;

          

           A48: for n be Nat holds Q[n] from NAT_1:sch 2( A47, A29);

          

           A49: ( dom pL) = cTM by FUNCT_2:def 1;

          then (pL .: cTM) = ( rng pL) by RELAT_1: 113;

          then

           A50: rngPL is compact by A1, A26, A48, WEIERSTR: 9;

          then

           A51: cRpL is compact by WEIERSTR: 13;

          reconsider cRpL as non empty real-bounded Subset of REAL by A50, WEIERSTR: 11, WEIERSTR:def 1;

          set L = ( lower_bound cRpL);

          L in cRpL by A51, RCOMP_1: 14;

          then

          consider x be object such that

           A52: x in ( dom pL) and

           A53: (pL . x) = L by A27, FUNCT_1:def 3;

          ( union G) = ( [#] TM) by A5, SETFAM_1: 45;

          then

          consider Y be set such that

           A54: x in Y and

           A55: Y in ( rng g) by A9, A52, TARSKI:def 4;

          reconsider x as Point of TM by A52;

          consider j be object such that

           A56: j in ( dom g) and

           A57: (g . j) = Y by A55, FUNCT_1:def 3;

          reconsider j as Nat by A56;

          

           A58: j <= ( len g) by A56, FINSEQ_3: 25;

          

           A59: 1 <= j by A56, FINSEQ_3: 25;

          now

            per cases by A59, XXREAL_0: 1;

              suppose

               A60: j = 1;

              then not x in g19 by A54, A57, XBOOLE_0:def 5;

              then (( dist_min g19) . x) <> 0 by HAUSDORF: 9;

              then (( dist_min g19) . x) > 0 by JORDAN1K: 9;

              hence 0 < L by A23, A24, A26, A28, A48, A53, A56, A58, A60;

            end;

              suppose

               A61: j > 1;

              then

              reconsider j1 = (j - 1) as Element of NAT by NAT_1: 20;

              ((p /. j1) is Element of FUNCS) & (p /. j) is Element of FUNCS;

              then

              reconsider pj1 = (p /. j1), pj = (p /. j) as Function of TM, R^1 by TOPMETR: 17;

              (j1 + 1) > 1 by A61;

              then

               A62: 1 <= j1 & j1 < ( len g) by A58, NAT_1: 13;

              then j1 in ( dom p) by A23, FINSEQ_3: 25;

              then

               A63: pj1 is continuous by A48;

               P[j1, pj1, pj] by A25, A28, A48, A56, A62;

              then

              consider A be non empty Subset of TM such that

               A64: (A ` ) = (g . j) and

               A65: for x be Point of TM holds (pj . x) = ( max ((pj1 . x),(( dist_min A) . x))) by A63;

              (A ` ) is open by A2, A4, A9, A55, A57, A64, TOPS_2:def 1;

              then

               A66: A is closed by TOPS_1: 3;

               not x in A by A54, A57, A64, XBOOLE_0:def 5;

              then (( dist_min A) . x) <> 0 by A66, HAUSDORF: 9;

              then

               A67: (( dist_min A) . x) > 0 by JORDAN1K: 9;

              (pj . x) = ( max ((pj1 . x),(( dist_min A) . x))) by A65;

              then (pj . x) > 0 by A67, XXREAL_0: 25;

              hence 0 < L by A23, A26, A28, A48, A53, A56, A58;

            end;

          end;

          then

          reconsider L as positive Real;

          take L;

          let X be Point of M;

          defpred P[ Nat] means $1 in ( dom p) & for f1 be Function of TM, R^1 st (p /. $1) = f1 holds (f1 . X) >= L;

          (pL . X) in cRpL by A27, A49, FUNCT_1:def 3;

          then P[( len p)] by A11, A23, FINSEQ_3: 25, XXREAL_2: 3;

          then

           A68: ex k be Nat st P[k];

          consider k be Nat such that

           A69: P[k] and

           A70: for n be Nat st P[n] holds k <= n from NAT_1:sch 5( A68);

          

           A71: 1 <= k by A69, FINSEQ_3: 25;

          

           A72: k <= ( len p) by A69, FINSEQ_3: 25;

          per cases by A71, XXREAL_0: 1;

            suppose

             A73: k = 1;

            take g1;

            thus g1 in F by A4, A9, A13;

            let y be object such that

             A74: y in ( Ball (X,L));

            reconsider Y = y as Point of M by A74;

            

             A75: ( dist (X,Y)) < L by A74, METRIC_1: 11;

            assume not y in g1;

            then Y in g19 by XBOOLE_0:def 5;

            then

             A76: (( dist_min g19) . X) <= ( dist (X,Y)) by HAUSDORF: 13;

            (( dist_min g19) . X) >= L by A10, A24, A69, A73;

            hence contradiction by A75, A76, XXREAL_0: 2;

          end;

            suppose

             A77: k > 1;

            then

            reconsider k1 = (k - 1) as Element of NAT by NAT_1: 20;

            ((p /. k1) is Element of FUNCS) & (p /. k) is Element of FUNCS;

            then

            reconsider pk1 = (p /. k1), pk = (p /. k) as Function of TM, R^1 by TOPMETR: 17;

            (k1 + 1) > 1 by A77;

            then

             A78: 1 <= k1 & k1 < ( len g) by A23, A72, NAT_1: 13;

            then k1 in ( dom p) by A23, FINSEQ_3: 25;

            then

             A79: pk1 is continuous by A48;

             P[k1, pk1, pk] by A25, A48, A69, A78;

            then

            consider A be non empty Subset of TM such that

             A80: (A ` ) = (g . k) and

             A81: for x be Point of TM holds (pk . x) = ( max ((pk1 . x),(( dist_min A) . x))) by A79;

            take (A ` );

            (A ` ) in G by A9, A28, A69, A80, FUNCT_1:def 3;

            hence (A ` ) in F by A4;

            let y be object such that

             A82: y in ( Ball (X,L));

            reconsider Y = y as Point of M by A82;

            assume not y in (A ` );

            then Y in A by XBOOLE_0:def 5;

            then

             A83: (( dist_min A) . X) <= ( dist (X,Y)) by HAUSDORF: 13;

            ( dist (X,Y)) < L by A82, METRIC_1: 11;

            then

             A84: (( dist_min A) . X) < L by A83, XXREAL_0: 2;

            

             A85: (pk . X) >= L by A69;

            (pk . X) = ( max ((pk1 . X),(( dist_min A) . X))) by A81;

            then P[k1] by A23, A78, A84, A85, FINSEQ_3: 25, XXREAL_0: 16;

            then k1 >= (k1 + 1) by A70;

            hence contradiction by NAT_1: 13;

          end;

        end;

      end;

    end

    reserve L for Lebesgue_number of F;

    theorem :: SIMPLEX2:1

    ( TopSpaceMetr M) is compact & F is Cover of ( TopSpaceMetr M) & F c= G implies L is Lebesgue_number of G

    proof

      assume that

       A1: ( TopSpaceMetr M) is compact and

       A2: F is Cover of ( TopSpaceMetr M) and

       A3: F c= G;

       A4:

      now

        let x be Point of M;

        ex A be Subset of ( TopSpaceMetr M) st A in F & ( Ball (x,L)) c= A by A1, A2, Def1;

        hence ex A be Subset of ( TopSpaceMetr M) st A in G & ( Ball (x,L)) c= A by A3;

      end;

      set TM = ( TopSpaceMetr M);

      ( union F) = ( [#] TM) & ( union F) c= ( union G) by A2, A3, SETFAM_1: 45, ZFMISC_1: 77;

      then G is Cover of TM by SETFAM_1:def 11;

      hence thesis by A1, A4, Def1;

    end;

    theorem :: SIMPLEX2:2

    ( TopSpaceMetr M) is compact & F is Cover of ( TopSpaceMetr M) & F is_finer_than G implies L is Lebesgue_number of G

    proof

      assume that

       A1: ( TopSpaceMetr M) is compact and

       A2: F is Cover of ( TopSpaceMetr M) and

       A3: F is_finer_than G;

      set TM = ( TopSpaceMetr M);

       A4:

      now

        let x be Point of M;

        consider A be Subset of ( TopSpaceMetr M) such that

         A5: A in F and

         A6: ( Ball (x,L)) c= A by A1, A2, Def1;

        consider B be set such that

         A7: B in G and

         A8: A c= B by A3, A5, SETFAM_1:def 2;

        reconsider B as Subset of TM by A7;

        take B;

        thus B in G & ( Ball (x,L)) c= B by A6, A7, A8;

      end;

      ( union F) = ( [#] TM) & ( union F) c= ( union G) by A2, A3, SETFAM_1: 13, SETFAM_1: 45;

      then G is Cover of TM by SETFAM_1:def 11;

      hence thesis by A1, A4, Def1;

    end;

    theorem :: SIMPLEX2:3

    for L1 be positive Real st ( TopSpaceMetr M) is compact & F is Cover of ( TopSpaceMetr M) & L1 <= L holds L1 is Lebesgue_number of F

    proof

      let L9 be positive Real such that

       A1: (( TopSpaceMetr M) is compact) & F is Cover of ( TopSpaceMetr M) and

       A2: L9 <= L;

      now

        let x be Point of M;

        consider A be Subset of ( TopSpaceMetr M) such that

         A3: A in F & ( Ball (x,L)) c= A by A1, Def1;

        take A;

        ( Ball (x,L9)) c= ( Ball (x,L)) by A2, PCOMPS_1: 1;

        hence A in F & ( Ball (x,L9)) c= A by A3;

      end;

      hence thesis by A1, Def1;

    end;

    begin

    reserve n,k for Nat,

r for Real,

X for set,

M for Reflexive non empty MetrStruct,

A for Subset of M,

K for SimplicialComplexStr;

    registration

      let M;

      cluster finite -> bounded for Subset of M;

      coherence

      proof

        let A be Subset of M;

        per cases ;

          suppose A is empty;

          hence thesis;

        end;

          suppose

           A1: A is non empty;

          assume A is finite;

          then

          reconsider a = A as finite non empty Subset of M by A1;

          deffunc D( Point of M, Point of M) = ( dist ($1,$2));

          consider q be object such that

           A2: q in a by XBOOLE_0:def 1;

          set X = { D(x,y) where x be Point of M, y be Point of M : x in a & y in a };

          reconsider q as Point of M by A2;

          

           A3: D(q,q) in X by A2;

           A4:

          now

            let x be object;

            assume x in X;

            then ex y be Point of M, z be Point of M st x = D(y,z) & y in a & z in a;

            hence x is real;

          end;

          

           A5: a is finite;

          X is finite from FRAENKEL:sch 22( A5, A5);

          then

          reconsider X as real-membered non empty finite set by A3, A4, MEMBERED:def 3;

          reconsider sX = ( sup X) as Real;

          reconsider sX1 = (sX + 1) as Real;

          take sX1;

           D(q,q) = 0 & D(q,q) <= sX by A3, METRIC_1: 1, XXREAL_2: 4;

          hence 0 < sX1;

          let x,y be Point of M;

          assume x in A & y in A;

          then D(x,y) in X;

          then D(x,y) <= sX by XXREAL_2: 4;

          hence thesis by XREAL_1: 39;

        end;

      end;

    end

    theorem :: SIMPLEX2:4

    for S be finite non empty Subset of M holds ex p,q be Point of M st p in S & q in S & ( dist (p,q)) = ( diameter S)

    proof

      let S be finite non empty Subset of M;

      set q = the Element of S;

      reconsider q as Point of M;

      deffunc D( Point of M, Point of M) = ( dist ($1,$2));

      set X = { D(x,y) where x be Point of M, y be Point of M : x in S & y in S };

       A1:

      now

        let x be object;

        assume x in X;

        then ex y be Point of M, z be Point of M st x = D(y,z) & y in S & z in S;

        hence x is real;

      end;

      

       A2: D(q,q) in X;

      

       A3: S is finite;

      X is finite from FRAENKEL:sch 22( A3, A3);

      then

      reconsider X as real-membered non empty finite set by A1, A2, MEMBERED:def 3;

      reconsider sX = ( sup X) as Real;

      sX in X by XXREAL_2:def 6;

      then

      consider p,q be Point of M such that

       A4: sX = D(p,q) & p in S & q in S;

      now

        let x,y be Point of M;

        assume x in S & y in S;

        then D(x,y) in X;

        hence D(x,y) <= sX by XXREAL_2: 4;

      end;

      then

       A5: ( diameter S) <= sX by TBSP_1:def 8;

      sX <= ( diameter S) by A4, TBSP_1:def 8;

      hence thesis by A4, A5, XXREAL_0: 1;

    end;

    definition

      let M, K;

      :: SIMPLEX2:def2

      attr K is M bounded means

      : Def2: ex r st for A st A in the topology of K holds A is bounded & ( diameter A) <= r;

    end

    theorem :: SIMPLEX2:5

    

     Th5: for K be non void SimplicialComplexStr st K is M bounded & A is Simplex of K holds A is bounded

    proof

      let K be non void SimplicialComplexStr;

      assume K is M bounded;

      then

       A1: ex r be Real st for A st A in the topology of K holds A is bounded & ( diameter A) <= r;

      assume A is Simplex of K;

      then A in the topology of K by PRE_TOPC:def 2;

      hence thesis by A1;

    end;

    registration

      let M, X;

      cluster M bounded non void for SimplicialComplex of X;

      existence

      proof

        set m = the Element of M;

        take K = ( Complex_of {( {} X)});

        K is M bounded

        proof

          take r = ( diameter ( {} M));

          let A;

          

           A1: the topology of K = ( bool ( {} X)) by SIMPLEX0: 4;

          assume A in the topology of K;

          hence thesis by A1;

        end;

        hence thesis;

      end;

    end

    registration

      let M;

      cluster M bounded non void subset-closed finite-membered for SimplicialComplexStr;

      existence

      proof

        take the M bounded non void SimplicialComplex of the set;

        thus thesis;

      end;

    end

    registration

      let M, X;

      let K be M bounded SimplicialComplexStr of X;

      cluster -> M bounded for SubSimplicialComplex of K;

      coherence

      proof

        let SK be SubSimplicialComplex of K;

        

         A1: the topology of SK c= the topology of K by SIMPLEX0:def 13;

        consider r be Real such that

         A2: for A st A in the topology of K holds A is bounded & ( diameter A) <= r by Def2;

        take r;

        let A;

        assume A in the topology of SK;

        hence thesis by A1, A2;

      end;

    end

    registration

      let M, X;

      let K be M bounded subset-closed SimplicialComplexStr of X;

      let i be dim-like number;

      cluster ( Skeleton_of (K,i)) -> M bounded;

      coherence ;

    end

    theorem :: SIMPLEX2:6

    

     Th6: K is finite-vertices implies K is M bounded

    proof

      set V = ( Vertices K);

      assume K is finite-vertices;

      then V is finite;

      then

      reconsider VM = (V /\ ( [#] M)) as finite Subset of M;

      take ( diameter VM);

      let A;

      assume

       A1: A in the topology of K;

      then

      reconsider S = A as Subset of K;

      S is simplex-like by A1, PRE_TOPC:def 2;

      then A c= V by SIMPLEX0: 17;

      then A c= VM by XBOOLE_1: 19;

      hence thesis by TBSP_1: 24;

    end;

    begin

    definition

      let M;

      let K be SimplicialComplexStr;

      :: SIMPLEX2:def3

      func diameter (M,K) -> Real means

      : Def3: (for A st A in the topology of K holds ( diameter A) <= it ) & for r st (for A 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

      proof

        the topology of K meets ( bool ( [#] M)) implies ex d be Real st (for A st A in the topology of K holds ( diameter A) <= d) & for r be Real st (for A st A in the topology of K holds ( diameter A) <= r) holds r >= d

        proof

          defpred P[ Subset of M] means $1 in the topology of K & $1 is bounded;

          deffunc D( Subset of M) = ( diameter $1);

          set X = { D(S) where S be Subset of M : P[S] };

          now

            let x be object;

            assume x in X;

            then ex S be Subset of M st x = D(S) & P[S];

            hence x is real;

          end;

          then

          reconsider X as real-membered set by MEMBERED:def 3;

          assume the topology of K meets ( bool ( [#] M));

          then

          consider B be object such that

           A2: B in the topology of K and

           A3: B in ( bool ( [#] M)) by XBOOLE_0: 3;

          reconsider B as Subset of M by A3;

          consider rr be Real such that

           A4: for A st A in the topology of K holds A is bounded & D(A) <= rr by A1;

          now

            let x be ExtReal;

            assume x in X;

            then

            consider s be Subset of M such that

             A5: x = D(s) & P[s];

            thus x <= rr by A4, A5;

          end;

          then rr is UpperBound of X by XXREAL_2:def 1;

          then

           A6: X is bounded_above by XXREAL_2:def 10;

          B is bounded by A2, A4;

          then D(B) in X by A2;

          then

          reconsider sX = ( sup X) as Real by A6;

          take sX;

          hereby

            let A;

            assume A in the topology of K;

            then P[A] by A4;

            then D(A) in X;

            hence D(A) <= sX by XXREAL_2: 4;

          end;

          let r be Real such that

           A7: for A st A in the topology of K holds ( diameter A) <= r;

          now

            let x be ExtReal;

            assume x in X;

            then

            consider A such that

             A8: x = D(A) & P[A];

            thus x <= r by A7, A8;

          end;

          then r is UpperBound of X by XXREAL_2:def 1;

          hence thesis by XXREAL_2:def 3;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        now

          let r1,r2 be Real such that

           A9: (for A st A in the topology of K holds ( diameter A) <= r1) & ((for r be Real st (for A st A in the topology of K holds ( diameter A) <= r) holds r >= r1) & for A st A in the topology of K holds ( diameter A) <= r2) & for r be Real st (for A st A in the topology of K holds ( diameter A) <= r) holds r >= r2;

          r1 <= r2 & r2 <= r1 by A9;

          hence r1 = r2 by XXREAL_0: 1;

        end;

        hence thesis;

      end;

      consistency ;

    end

    theorem :: SIMPLEX2:7

    

     Th7: K is M bounded implies 0 <= ( diameter (M,K))

    proof

      assume

       A1: K is M bounded;

      per cases ;

        suppose

         A2: the topology of K meets ( bool ( [#] M));

        then

        consider S be object such that

         A3: S in the topology of K and

         A4: S in ( bool ( [#] M)) by XBOOLE_0: 3;

        reconsider S as Subset of M by A4;

        ex r be Real st for A st A in the topology of K holds A is bounded & ( diameter A) <= r by A1;

        then ( diameter S) >= 0 by A3, TBSP_1: 21;

        hence thesis by A1, A2, A3, Def3;

      end;

        suppose the topology of K misses ( bool ( [#] M));

        hence thesis by A1, Def3;

      end;

    end;

    theorem :: SIMPLEX2:8

    for K be M bounded SimplicialComplexStr of X, KX be SubSimplicialComplex of K holds ( diameter (M,KX)) <= ( diameter (M,K))

    proof

      let K be M bounded SimplicialComplexStr of X, KX be SubSimplicialComplex of K;

      

       A1: the topology of KX c= the topology of K by SIMPLEX0:def 13;

      per cases ;

        suppose

         A2: the topology of KX meets ( bool ( [#] M));

        then the topology of K meets ( bool ( [#] M)) by A1, XBOOLE_1: 63;

        then for A st A in the topology of KX holds ( diameter A) <= ( diameter (M,K)) by A1, Def3;

        hence thesis by A2, Def3;

      end;

        suppose the topology of KX misses ( bool ( [#] M));

        then ( diameter (M,KX)) = 0 by Def3;

        hence thesis by Th7;

      end;

    end;

    theorem :: SIMPLEX2:9

    for K be M bounded subset-closed SimplicialComplexStr of X, i be dim-like number holds ( diameter (M,( Skeleton_of (K,i)))) <= ( diameter (M,K))

    proof

      set r = the Real;

      let K be M bounded subset-closed SimplicialComplexStr of X, i be dim-like number;

      set SK = ( Skeleton_of (K,i));

      

       A1: the topology of SK c= the topology of K by SIMPLEX0:def 13;

      per cases ;

        suppose

         A2: the topology of SK meets ( bool ( [#] M));

        then

         A3: the topology of K meets ( bool ( [#] M)) by A1, XBOOLE_1: 63;

        now

          let A;

          ( 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 SK;

          then

          consider w be 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 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;

        end;

        hence thesis by A2, Def3;

      end;

        suppose the topology of SK misses ( bool ( [#] M));

        then ( diameter (M,SK)) = 0 by Def3;

        hence thesis by Th7;

      end;

    end;

    definition

      let M;

      let K be M bounded non void subset-closed SimplicialComplexStr;

      :: original: diameter

      redefine

      :: SIMPLEX2:def4

      func diameter (M,K) means

      : Def4: (for A st A is Simplex of K holds ( diameter A) <= it ) & for r st (for A st A is Simplex of K holds ( diameter A) <= r) holds r >= it ;

      compatibility

      proof

        let d be Real;

        ( {} 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

          assume

           A2: d = ( diameter (M,K));

          hereby

            let A;

            assume A is Simplex of K;

            then A in the topology of K by PRE_TOPC:def 2;

            hence ( diameter A) <= d by A1, A2, Def3;

          end;

          let r be Real;

          assume

           A3: for A st A is Simplex of K holds ( diameter A) <= r;

          for A st A in the topology of K holds ( diameter A) <= r by A3, PRE_TOPC:def 2;

          hence r >= d by A1, A2, Def3;

        end;

        assume that

         A4: for A st A is Simplex of K holds ( diameter A) <= d and

         A5: for r be Real st (for A st A is Simplex of K holds ( diameter A) <= r) holds r >= d;

        for A st A in the topology of K holds ( diameter A) <= d by A4, PRE_TOPC:def 2;

        then

         A6: ( diameter (M,K)) <= d by A1, Def3;

        now

          let A;

          assume A is Simplex of K;

          then A in the topology of K by PRE_TOPC:def 2;

          hence ( diameter A) <= ( diameter (M,K)) by A1, Def3;

        end;

        then d <= ( diameter (M,K)) by A5;

        hence d = ( diameter (M,K)) by A6, XXREAL_0: 1;

      end;

    end

    theorem :: SIMPLEX2:10

    for S be finite Subset of M holds ( diameter (M,( Complex_of {S}))) = ( diameter S)

    proof

      let S be finite Subset of M;

      set C = ( Complex_of {S});

      reconsider C as M bounded non void SimplicialComplex of M by Th6;

      reconsider s = S as Subset of C;

      

       A1: the topology of C = ( bool S) by SIMPLEX0: 4;

      now

        let W be Subset of M;

        assume W is Simplex of C;

        then W in ( bool S) by A1, PRE_TOPC:def 2;

        hence ( diameter W) <= ( diameter S) by TBSP_1: 24;

      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 thesis by A2, XXREAL_0: 1;

    end;

    definition

      let n;

      let K be SimplicialComplexStr of ( TOP-REAL n);

      :: SIMPLEX2:def5

      attr K is bounded means K is ( Euclid n) bounded;

      :: SIMPLEX2:def6

      func diameter K -> Real equals ( diameter (( Euclid n),K));

      coherence ;

    end

    registration

      let n;

      cluster bounded -> ( Euclid n) bounded for SimplicialComplexStr of ( TOP-REAL n);

      coherence ;

      cluster bounded affinely-independent simplex-join-closed non void finite-degree total for SimplicialComplex of ( TOP-REAL n);

      existence

      proof

        set T = ( TOP-REAL n);

        take C = ( Complex_of {( {} ( TOP-REAL n))});

        C is ( Euclid n) bounded by Th6;

        hence thesis;

      end;

      cluster finite-vertices -> bounded for SimplicialComplexStr of ( TOP-REAL n);

      coherence by Th6;

    end

    

     Lm1: ( [#] ( TOP-REAL n)) = ( [#] ( Euclid n))

    proof

       the TopStruct of ( TOP-REAL n) = ( TopSpaceMetr ( Euclid n)) by EUCLID:def 8;

      hence thesis;

    end;

    begin

    reserve V for RealLinearSpace,

Kv for non void SimplicialComplex of V;

    

     Lm2: for x be set holds {x} is c=-linear

    proof

      let x be set;

      let y,z be set;

      assume that

       A1: y in {x} and

       A2: z in {x};

      y = x by A1, TARSKI:def 1;

      hence thesis by A2, TARSKI:def 1;

    end;

    theorem :: SIMPLEX2:11

    

     Th11: for S be Simplex of ( BCS Kv) holds for F be c=-linear finite finite-membered Subset-Family of V st S = (( center_of_mass V) .: F) holds for a1,a2 be VECTOR of V st a1 in S & a2 in S holds ex b1,b2 be VECTOR of V, r be 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 S be Simplex of ( BCS Kv);

      set cM = ( center_of_mass V);

      let F be c=-linear finite finite-membered Subset-Family of V such that

       A1: S = (cM .: F);

      let a1,a2 be VECTOR of V such that

       A2: a1 in S and

       A3: a2 in S;

      consider A1 be object such that

       A4: A1 in ( dom cM) and

       A5: A1 in F and

       A6: (cM . A1) = a1 by A1, A2, FUNCT_1:def 6;

      consider A2 be object such that

       A7: A2 in ( dom cM) and

       A8: A2 in F and

       A9: (cM . A2) = a2 by A1, A3, FUNCT_1:def 6;

      reconsider A1, A2 as set by TARSKI: 1;

      

       A10: (A1,A2) are_c=-comparable by A5, A8, ORDINAL1:def 8;

      set uF = ( union F);

      set CuF = ( Complex_of {uF});

      

       A11: for a1,a2 be VECTOR of V holds for A1,A2 be set st A1 c= A2 & A1 in ( dom cM) & A1 in F & (cM . A1) = a1 & A1 in ( dom cM) & A2 in F & (cM . A2) = a2 holds ex b1,b2 be VECTOR of V, r be Real st b1 in ( Vertices ( BCS CuF)) & b2 in ( Vertices ( BCS CuF)) & (a1 - a2) = (r * (b1 - b2)) & 0 <= r & r <= ((( card uF) - 1) / ( card uF))

      proof

        let a1,a2 be VECTOR of V;

        

         A12: the topology of CuF = ( bool uF) by SIMPLEX0: 4;

        let A1,A2 be set such that

         A13: A1 c= A2 and

         A14: A1 in ( dom cM) and

         A15: A1 in F and

         A16: (cM . A1) = a1 and A1 in ( dom cM) and

         A17: A2 in F and

         A18: (cM . A2) = a2;

        

         A19: A1 c= uF by A15, ZFMISC_1: 74;

        

         A20: A1 <> {} by A14, ORDERS_1: 1;

        then

         A21: uF is non empty by A19;

        

         A22: A2 c= uF by A17, ZFMISC_1: 74;

        reconsider A1, A2 as non empty finite Subset of V by A13, A15, A17, A20;

        set A21 = (A2 \ A1);

        reconsider AA1 = {A1}, AA2 = {A21} as Subset-Family of CuF;

         {A1} c= ( bool uF) by A19, ZFMISC_1: 31;

        then

         A23: AA1 is c=-linear finite simplex-like by A12, Lm2, SIMPLEX0: 14;

        A21 c= A2 by XBOOLE_1: 36;

        then A21 c= uF by A22;

        then {A21} c= ( bool uF) by ZFMISC_1: 31;

        then

         A24: AA2 is c=-linear finite simplex-like by A12, Lm2, SIMPLEX0: 14;

        

         A25: |.CuF.| c= ( [#] V);

        ( [#] CuF) = ( [#] V);

        then

         A26: ( BCS CuF) = ( subdivision (cM,CuF)) by A25, SIMPLEX1:def 5;

        

         A27: ( [#] ( subdivision (cM,CuF))) = ( [#] CuF) by SIMPLEX0:def 20;

        then

        reconsider aa1 = {a1} as Subset of ( BCS CuF) by A25, SIMPLEX1:def 5;

        

         A28: a1 in aa1 by TARSKI:def 1;

        then

        reconsider d1 = a1 as Element of ( BCS CuF);

        

         A29: ( dom cM) = ( BOOL the carrier of V) by FUNCT_2:def 1;

        (cM .: AA1) = ( Im (cM,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;

        per cases ;

          suppose

           A31: A1 = A2;

          reconsider Z = 0 as Real;

          take b1 = a1, b2 = a1, Z;

          ( card uF) >= 1 by A21, NAT_1: 14;

          then

           A32: (( card uF) - 1) >= (1 - 1) by XREAL_1: 6;

          (a1 - a2) = ( 0. V) by A16, A18, A31, RLVECT_1: 5;

          hence thesis by A30, A32, RLVECT_1: 10, SIMPLEX0:def 4;

        end;

          suppose A1 <> A2;

          then not A2 c= A1 by A13, XBOOLE_0:def 10;

          then

          reconsider A21 as non empty finite Subset of V by XBOOLE_1: 37;

          

           A33: A21 in ( dom cM) by A29, ORDERS_1: 2;

          then (cM . A21) in ( rng cM) by FUNCT_1:def 3;

          then

          reconsider a21 = (cM . A21) as VECTOR of V;

          reconsider aa2 = {a21} as Subset of ( BCS CuF) by A25, A27, SIMPLEX1:def 5;

          

           A34: a21 in aa2 by TARSKI:def 1;

          then

          reconsider d2 = a21 as Element of ( BCS CuF);

          (cM .: AA2) = ( Im (cM,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;

          set r1 = (1 / ( card A1)), r2 = (1 / ( card A2)), r21 = (1 / ( card A21)), r = (( card A21) / ( card A2));

          reconsider r1, r2, r21, r as Real;

          take a1, a21, r;

          

           A36: (r * r21) = ((( card A21) * 1) / (( card A21) * ( card A2))) by XCMPLX_1: 76

          .= r2 by XCMPLX_1: 91;

          consider L1 be 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 be 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 be 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 be Element of V holds ((L1 - L2) . v) = ((r * (L1 - L21)) . v)

          proof

            let v be Element of 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;

            per cases ;

              suppose

               A53: v in A1;

              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 thesis by A13, A41, A46, A49, A51, A52, A53, A54, A55, FUNCT_4: 13;

            end;

              suppose

               A56: v in A2 & not v in A1;

              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 thesis by A36, A58;

            end;

              suppose

               A60: not v in A1 & not v in A2;

              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 thesis by A49, A52, A62, A61, RLVECT_2: 19;

            end;

          end;

          then

           A63: (L1 - L2) = (r * (L1 - L21)) by RLVECT_2:def 9;

          ( card A1) >= 1 & ( card A2) <= ( card uF) by A17, NAT_1: 14, NAT_1: 43, ZFMISC_1: 74;

          then (( card A1) * ( card uF)) >= (1 * ( card A2)) by XREAL_1: 66;

          then ((( card A2) * ( card uF)) - (( card A1) * ( card uF))) <= ((( card uF) * ( card A2)) - ( card A2)) by XREAL_1: 13;

          then

           A64: (( card A21) * ( card uF)) <= ((( card uF) - 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 thesis by A21, A30, A35, A64, SIMPLEX0:def 4, XREAL_1: 102;

        end;

      end;

      per cases by A10, XBOOLE_0:def 9;

        suppose A1 c= A2;

        hence thesis by A4, A5, A6, A8, A9, A11;

      end;

        suppose A2 c= A1;

        then

        consider b1,b2 be VECTOR of V, r be Real such that

         A67: b1 in ( Vertices ( BCS CuF)) & b2 in ( Vertices ( BCS CuF)) and

         A68: (a2 - a1) = (r * (b1 - b2)) and

         A69: 0 <= r & r <= ((( card uF) - 1) / ( card uF)) by A5, A6, A7, A8, A9, A11;

        take b2, b1, r;

        (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 thesis by A67, A69;

      end;

    end;

    theorem :: SIMPLEX2:12

    

     Th12: for A be affinely-independent Subset of ( TOP-REAL n) holds for E be Enumeration of A st (( dom E) \ X) is non empty holds ( conv (E .: X)) = ( meet { ( conv (A \ {(E . k)})) where k be Element of NAT : k in (( dom E) \ X) })

    proof

      let A be affinely-independent Subset of ( TOP-REAL n);

      let E be Enumeration of A such that

       A1: (( dom E) \ X) is non empty;

      set d = ( dom E);

      defpred P[ Nat] means $1 <> 0 implies for X st ( card (( dom E) \ X)) = $1 holds ( conv (A \ (E .: (d \ X)))) = ( meet { ( conv (A \ {(E . k)})) where k be Element of NAT : k in (( dom E) \ X) });

      

       A2: ( rng E) = A by RLAFFIN3:def 1;

      

       A3: for i be Nat st P[i] holds P[(i + 1)]

      proof

        deffunc C( set) = ( conv (A \ {(E . $1)}));

        let i be Nat;

        assume

         A4: P[i];

        set i1 = (i + 1);

        assume i1 <> 0 ;

        let X;

        set U = { C(k) where k be Element of NAT : k in (d \ X) };

        assume

         A5: ( card (d \ X)) = i1;

        then (d \ X) is non empty;

        then

        consider m be object such that

         A6: m in (d \ X) by XBOOLE_0:def 1;

        

         A7: m in d by A6, XBOOLE_0:def 5;

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

        per cases ;

          suppose i = 0 ;

          then

          consider x be object such that

           A9: (d \ X) = {x} by A5, CARD_2: 42;

          

           A10: x = m by A6, A9, TARSKI:def 1;

          

           A11: U c= { C(m)}

          proof

            let u be object;

            assume u in U;

            then ex k be Element of NAT st u = C(k) & k in (d \ X);

            then u = C(m) by A9, A10, TARSKI:def 1;

            hence thesis by TARSKI:def 1;

          end;

           C(m) in U by A6;

          then

           A12: U = { C(m)} by A11, ZFMISC_1: 33;

          (E .: (d \ X)) = {(E . m)} by A6, A8, A9, TARSKI:def 1;

          hence thesis by A12, SETFAM_1: 10;

        end;

          suppose

           A13: i > 0 ;

          set Xm = (X \/ {m});

          set Um = { C(k) where k be Element of NAT : k in (d \ Xm) };

          set t = the Element of (d \ Xm);

          

           A14: (((d \ X) \ {m}) \/ {m}) = (d \ X) by A6, ZFMISC_1: 116;

          

           A15: ((d \ X) \ {m}) = (d \ Xm) by XBOOLE_1: 41;

          

           A16: Um c= U

          proof

            let x be object;

            assume x in Um;

            then

            consider k be Element of NAT such that

             A17: x = C(k) and

             A18: k in (d \ Xm);

            k in (d \ X) by A15, A14, A18, XBOOLE_0:def 3;

            hence thesis by A17;

          end;

          m in {m} by TARSKI:def 1;

          then not m in ((d \ X) \ {m}) by XBOOLE_0:def 5;

          then

           A19: (( card ((d \ X) \ {m})) + 1) = ( card (d \ X)) by A14, CARD_2: 41;

          then (d \ Xm) is non empty by A5, A13, A15;

          then t in (d \ Xm);

          then

           A20: C(t) in Um;

          set c = C(m), CC = {c};

          set CA = ( Complex_of {A});

          

           A21: the topology of CA = ( bool A) by SIMPLEX0: 4;

          

           A22: U c= (Um \/ CC)

          proof

            let x be object;

            assume x in U;

            then

            consider k be Element of NAT such that

             A23: x = C(k) and

             A24: k in (d \ X);

            k in (d \ Xm) or k in {m} by A15, A14, A24, XBOOLE_0:def 3;

            then k in (d \ Xm) or k = m by TARSKI:def 1;

            then x in Um or x in CC by A23, TARSKI:def 1;

            hence thesis by XBOOLE_0:def 3;

          end;

           C(m) in U by A6;

          then CC c= U by ZFMISC_1: 31;

          then

           A25: (Um \/ CC) c= U by A16, XBOOLE_1: 8;

          reconsider A1 = (A \ (E .: (d \ Xm))), A2 = (A \ {(E . m)}) as Subset of CA;

          (A \ {(E . m)}) c= A by XBOOLE_1: 36;

          then

           A26: A2 is simplex-like by A21, PRE_TOPC:def 2;

          (A \ (E .: (d \ Xm))) 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 .: (d \ Xm)) \/ {(E . m)}) = (E .: ((d \ Xm) \/ {m})) by A8, RELAT_1: 120

          .= (E .: (d \ X)) by A14, XBOOLE_1: 41;

          then

           A28: (A1 /\ A2) = (A \ (E .: (d \ X))) by XBOOLE_1: 53;

          ( conv (A \ (E .: (d \ Xm)))) = ( meet Um) by A4, A5, A13, A15, A19;

          

          then ( conv (A \ (E .: (d \ X)))) = (( meet Um) /\ ( meet CC)) by A28, A27, SETFAM_1: 10

          .= ( meet (Um \/ CC)) by A20, SETFAM_1: 9;

          hence thesis by A25, A22, XBOOLE_0:def 10;

        end;

      end;

      

       A29: P[ 0 ];

      for i be Nat holds P[i] from NAT_1:sch 2( A29, A3);

      then

       A30: P[( card (d \ X))];

      (d \ (d \ X)) = (d /\ X) by XBOOLE_1: 48;

      

      then (E .: X) = (E .: (d \ (d \ X))) by RELAT_1: 112

      .= ((E .: d) \ (E .: (d \ X))) by FUNCT_1: 64

      .= (A \ (E .: (d \ X))) by A2, RELAT_1: 113;

      hence thesis by A1, A30;

    end;

    reserve A for Subset of ( TOP-REAL n);

    theorem :: SIMPLEX2:13

    

     Th13: for a be bounded Subset of ( Euclid n) st a = A holds for p be Point of ( Euclid n) st p in ( conv A) holds ( conv A) c= ( cl_Ball (p,( diameter a)))

    proof

      

       A1: the TopStruct of ( TOP-REAL n) = ( TopSpaceMetr ( Euclid n)) by EUCLID:def 8;

      let a be bounded Subset of ( Euclid n) such that

       A2: A = a;

      let x be Point of ( Euclid n) such that

       A3: x in ( conv A);

      

       A4: A c= ( cl_Ball (x,( diameter a)))

      proof

        let p be object;

        assume

         A5: p in A;

        then

        reconsider p as Point of ( Euclid n) by A2;

        reconsider pp = p as Point of ( TOP-REAL n) by A1;

        

         A6: ( cl_Ball (p,( diameter a))) = ( cl_Ball (pp,( diameter a))) by TOPREAL9: 14;

        A c= ( cl_Ball (p,( diameter a)))

        proof

          let y be object;

          assume

           A7: y in A;

          then

          reconsider q = y as Point of ( Euclid n) by A2;

          ( dist (p,q)) <= ( diameter a) by A2, A5, A7, TBSP_1:def 8;

          hence thesis by METRIC_1: 12;

        end;

        then ( conv A) c= ( cl_Ball (pp,( diameter a))) by A6, CONVEX1: 30;

        then ( dist (p,x)) <= ( diameter a) by A3, A6, METRIC_1: 12;

        hence thesis by METRIC_1: 12;

      end;

      reconsider xx = x as Point of ( TOP-REAL n) by A1;

      ( cl_Ball (x,( diameter a))) = ( cl_Ball (xx,( diameter a))) by TOPREAL9: 14;

      hence thesis by A4, CONVEX1: 30;

    end;

    theorem :: SIMPLEX2:14

    

     Th14: A is bounded iff ( conv A) is bounded

    proof

       the TopStruct of ( TOP-REAL n) = ( TopSpaceMetr ( Euclid n)) by EUCLID:def 8;

      then

      reconsider cA = ( conv A), a = A as Subset of ( Euclid n);

      hereby

        assume A is bounded;

        then

        reconsider a as bounded Subset of ( Euclid n) by JORDAN2C: 11;

        set D = ( diameter a);

         A1:

        now

          let x,y be Point of ( Euclid n);

          assume x in cA;

          then

           A2: ( conv A) c= ( cl_Ball (x,D)) by Th13;

          assume y in cA;

          then ( dist (x,y)) <= D by A2, METRIC_1: 12;

          hence ( dist (x,y)) <= (D + 1) by XREAL_1: 39;

        end;

        D >= 0 by TBSP_1: 21;

        then cA is bounded by A1;

        hence ( conv A) is bounded by JORDAN2C: 11;

      end;

      assume ( conv A) is bounded;

      then cA is bounded by JORDAN2C: 11;

      then a is bounded by CONVEX1: 41, TBSP_1: 14;

      hence thesis by JORDAN2C: 11;

    end;

    theorem :: SIMPLEX2:15

    

     Th15: for a,ca be bounded Subset of ( Euclid n) st ca = ( conv A) & a = A holds ( diameter a) = ( diameter ca)

    proof

      let a,ca be bounded Subset of ( Euclid n);

      assume that

       A1: ca = ( conv A) and

       A2: a = A;

      per cases ;

        suppose a is empty;

        hence thesis by A1, A2;

      end;

        suppose

         A3: a is non empty;

        now

          let x,y be Point of ( Euclid n);

          assume x in ca;

          then

           A4: ( conv A) c= ( cl_Ball (x,( diameter a))) by A1, A2, Th13;

          assume y in ca;

          hence ( dist (x,y)) <= ( diameter a) by A1, A4, METRIC_1: 12;

        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 thesis by A5, XXREAL_0: 1;

      end;

    end;

    registration

      let n;

      let K be bounded SimplicialComplexStr of ( TOP-REAL n);

      cluster -> bounded for SubdivisionStr of K;

      coherence

      proof

        let SK be SubdivisionStr of K;

        consider r be Real such that

         A1: for A be Subset of ( Euclid n) st A in the topology of K holds A is bounded & ( diameter A) <= r by Def2;

        take r;

        let A be Subset of ( Euclid n);

        assume

         A2: A in the topology of SK;

        then

        reconsider a = A as Subset of SK;

        a is simplex-like by A2, PRE_TOPC:def 2;

        then

        consider b be 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 Lm1;

        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 thesis by A9, A10, A11, A7, CONVEX1: 41, TBSP_1: 14, XXREAL_0: 2;

      end;

    end

    theorem :: SIMPLEX2:16

    

     Th16: for K be bounded finite-degree non void SimplicialComplex of ( TOP-REAL n) st |.K.| c= ( [#] K) holds ( diameter ( BCS K)) <= ((( degree K) / (( degree K) + 1)) * ( diameter K))

    proof

      set T = ( TOP-REAL n);

      let K be bounded finite-degree non void SimplicialComplex of T;

      set BK = ( BCS K);

      set cM = ( center_of_mass T);

      set dK = ( degree K);

      assume |.K.| c= ( [#] K);

      then

       A1: ( BCS K) = ( subdivision (cM,K)) by SIMPLEX1:def 5;

      for A be Subset of ( Euclid n) st A is Simplex of BK holds ( diameter A) <= ((dK / (dK + 1)) * ( diameter K))

      proof

        let A be Subset of ( Euclid n);

        reconsider ONE = 1 as ExtReal;

        assume

         A2: A is Simplex of BK;

        then

        reconsider a = A as Simplex of BK;

        consider S be c=-linear finite simplex-like Subset-Family of K such that

         A3: A = (cM .: 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 T;

        set Us = ( union s);

        set C = ( Complex_of {Us});

        ( 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 cM) by ORDERS_1: 1;

        then

         A9: ( dom cM) is with_non-empty_elements by SETFAM_1:def 8;

        

         A10: ( [#] T) = ( [#] ( Euclid n)) by Lm1;

        then

        reconsider US = Us as Subset of ( Euclid n);

        

         A11: a in the topology of BK by PRE_TOPC:def 2;

        per cases ;

          suppose K is empty-membered;

          then

           A12: dK = ( - 1) by SIMPLEX0: 22;

          then ( - 1) <= ( degree BK) & ( degree BK) <= ( - 1) by A1, A9, SIMPLEX0: 23, SIMPLEX0: 52;

          then ( degree BK) = ( - 1) by XXREAL_0: 1;

          then BK is empty-membered by SIMPLEX0: 22;

          then the topology of BK is empty-membered;

          then

           A13: a = {} by A11, SETFAM_1:def 10;

          (dK / (dK + 1)) = 0 by A12;

          hence thesis by A13, TBSP_1:def 8;

        end;

          suppose K is non empty-membered;

          then ( degree K) >= ( - 1) & dK <> ( - 1) by SIMPLEX0: 22, SIMPLEX0: 23;

          then dK > ( - 1) by XXREAL_0: 1;

          then

           A14: dK >= (( - 1) + 1) by INT_1: 7;

          then

           A15: ((dK / (dK + 1)) * ( diameter K)) >= 0 by A7;

          per cases ;

            suppose a is empty;

            hence thesis by A15, TBSP_1:def 8;

          end;

            suppose

             A16: a is non empty;

            now

              US is bounded;

              then Us is bounded by JORDAN2C: 11;

              then ( conv Us) is bounded by Th14;

              then

              reconsider cUs = ( conv Us) as bounded Subset of ( Euclid n) by JORDAN2C: 11;

              let x,y be Point of ( Euclid n);

              assume that

               A17: x in A and

               A18: y in A;

              reconsider X = x, Y = y as Element of T by A10;

              

               A19: |.( BCS C).| = |.C.| & |.C.| = ( conv Us) by SIMPLEX1: 8, SIMPLEX1: 10;

              consider p be object such that

               A20: p in ( dom cM) and

               A21: p in s and (cM . p) = x by A3, A17, FUNCT_1:def 6;

              reconsider p as set by TARSKI: 1;

              p c= Us by A21, ZFMISC_1: 74;

              then

               A22: Us <> {} by A8, A20;

              ( card Us) <= (dK + 1) by A6, XXREAL_3:def 2;

              then

               A23: ((dK + 1) " ) <= (( card Us) " ) by A22, XREAL_1: 85;

              

               A24: ( diameter US) <= ( diameter K) by A5, Def4;

              

               A25: ((( card Us) - 1) / ( card Us)) = ((( card Us) / ( card Us)) - (1 / ( card Us)))

              .= (1 - (1 / ( card Us))) by A22, XCMPLX_1: 60;

              

               A26: ( diameter cUs) = ( diameter US) by Th15;

              consider b1,b2 be VECTOR of T, r be Real such that

               A27: b1 in ( Vertices ( BCS C)) and

               A28: b2 in ( Vertices ( BCS C)) and

               A29: (X - Y) = (r * (b1 - b2)) and

               A30: 0 <= r and

               A31: r <= ((( card Us) - 1) / ( card Us)) by A3, A16, A17, A18, Th11;

              reconsider B1 = b1, B2 = b2 as Element of ( BCS C) by A27, A28;

              B1 is vertex-like by A27, SIMPLEX0:def 4;

              then

              consider S1 be Subset of ( BCS C) such that

               A32: S1 is simplex-like and

               A33: B1 in S1;

              

               A34: ( conv ( @ S1)) c= |.( BCS C).| by A32, SIMPLEX1: 5;

              B2 is vertex-like by A28, SIMPLEX0:def 4;

              then

              consider S2 be Subset of ( BCS C) such that

               A35: S2 is simplex-like and

               A36: B2 in S2;

              ( @ 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;

              (dK / (dK + 1)) = (((dK + 1) / (dK + 1)) - (1 / (dK + 1)))

              .= (1 - (1 / (dK + 1))) by A14, XCMPLX_1: 60;

              then ((( card Us) - 1) / ( card Us)) <= (dK / (dK + 1)) by A23, A25, XREAL_1: 10;

              then

               A39: ( dist (bb1,bb2)) >= 0 & r <= (dK / (dK + 1)) by A31, XXREAL_0: 2;

              ( conv ( @ S2)) c= |.( BCS C).| 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

              .= ( |.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)) <= ((dK / (dK + 1)) * ( diameter K)) by A30, A40, A39, XREAL_1: 66;

            end;

            hence thesis by A4, A16, TBSP_1:def 8;

          end;

        end;

      end;

      hence thesis by Def4;

    end;

    theorem :: SIMPLEX2:17

    

     Th17: for K be bounded finite-degree non void SimplicialComplex of ( TOP-REAL n) st |.K.| c= ( [#] K) holds ( diameter ( BCS (k,K))) <= (((( degree K) / (( degree K) + 1)) |^ k) * ( diameter K))

    proof

      let K be bounded finite-degree non void SimplicialComplex of ( TOP-REAL n);

      set dK = ( degree K);

      set ddK = (dK / (dK + 1));

      defpred P[ Nat] means ( diameter ( BCS ($1,K))) <= ((ddK |^ $1) * ( diameter K)) & ( BCS ($1,K)) is finite-degree & ( degree ( BCS ($1,K))) <= dK;

      assume

       A1: |.K.| c= ( [#] K);

      

       A2: for k st P[k] holds P[(k + 1)]

      proof

        let k;

        set T = ( TOP-REAL n);

        set B = ( BCS (k,K));

        set cM = ( center_of_mass T);

        

         A3: ( degree K) >= ( - 1) by SIMPLEX0: 23;

        assume

         A4: P[k];

        then

        reconsider B = ( BCS (k,K)) as bounded finite-degree non void 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 (cM,B)) by A1, SIMPLEX1:def 5;

        

         A10: ( BCS ((k + 1),K)) = ( BCS B) by A1, SIMPLEX1: 20;

        then

         A11: ( diameter ( BCS ((k + 1),K))) <= ((dB / (dB + 1)) * ( diameter B)) by A1, A8, Th16;

         not {} in ( dom cM) by ORDERS_1: 1;

        then ( dom cM) is with_non-empty_elements by SETFAM_1:def 8;

        then

         A12: ( degree ( BCS ((k + 1),K))) <= dB by A9, A10, SIMPLEX0: 52;

        per cases ;

          suppose dB = ( - 1) or dB = 0 ;

          then

           A13: (dB / (dB + 1)) = 0 ;

          per cases ;

            suppose dK = 0 or dK = ( - 1);

            then (dK / (dK + 1)) = 0 ;

            then 0 = ((dK / (dK + 1)) |^ (k + 1)) by NAT_1: 11, NEWTON: 11;

            hence thesis by A1, A4, A9, A11, A12, A13, SIMPLEX1: 20, XXREAL_0: 2;

          end;

            suppose

             A14: dK <> 0 & dK <> ( - 1);

            then dK > ( - 1) by A3, XXREAL_0: 1;

            then dK >= (( - 1) + 1) by INT_1: 7;

            then ddK > 0 by A14, XREAL_1: 139;

            then (ddK |^ (k + 1)) > 0 by NEWTON: 83;

            hence thesis by A1, A4, A6, A9, A11, A12, A13, SIMPLEX1: 20, XXREAL_0: 2;

          end;

        end;

          suppose dB <> ( - 1) & dB <> 0 ;

          then dB > ( - 1) by A5, XXREAL_0: 1;

          then

           A15: dB >= (( - 1) + 1) by INT_1: 7;

          

           A16: (dB / (dB + 1)) = (((dB + 1) / (dB + 1)) - (1 / (dB + 1)))

          .= (1 - (1 / (dB + 1))) by A15, XCMPLX_1: 60;

          

           A17: ddK = (((dK + 1) / (dK + 1)) - (1 / (dK + 1)))

          .= (1 - (1 / (dK + 1))) by A4, A15, XCMPLX_1: 60;

          (dB + 1) <= (dK + 1) by A4, XREAL_1: 6;

          then (1 / (dK + 1)) <= (1 / (dB + 1)) by A15, XREAL_1: 85;

          then (( degree B) / (( degree B) + 1)) <= (dK / (dK + 1)) by A16, A17, XREAL_1: 10;

          then

           A18: ((( degree B) / (( degree B) + 1)) * ( diameter B)) <= ((dK / (dK + 1)) * (((dK / (dK + 1)) |^ k) * ( diameter K))) by A4, A7, A15, XREAL_1: 66;

          ((dK / (dK + 1)) * (((dK / (dK + 1)) |^ k) * ( diameter K))) = (((dK / (dK + 1)) * ((dK / (dK + 1)) |^ k)) * ( diameter K))

          .= (((dK / (dK + 1)) |^ (k + 1)) * ( diameter K)) by NEWTON: 6;

          hence thesis by A1, A4, A9, A11, A12, A18, SIMPLEX1: 20, XXREAL_0: 2;

        end;

      end;

      (ddK |^ 0 qua Nat) = 1 by NEWTON: 4;

      then

       A19: P[ 0 ] by A1, SIMPLEX1: 16;

      for k holds P[k] from NAT_1:sch 2( A19, A2);

      hence thesis;

    end;

    theorem :: SIMPLEX2:18

    

     Th18: for K be bounded finite-degree non void SimplicialComplex of ( TOP-REAL n) st |.K.| c= ( [#] K) holds for r st r > 0 holds ex k st ( diameter ( BCS (k,K))) < r

    proof

      let K be bounded finite-degree non void SimplicialComplex of ( TOP-REAL n) such that

       A1: |.K.| c= ( [#] K);

      set dK = ( degree K);

      let r be Real such that

       A2: r > 0 ;

      set ddK = (dK / (dK + 1));

      per cases ;

        suppose dK = 0 or dK = ( - 1);

        then

         A3: ddK = 0 ;

        ( diameter ( BCS K)) <= (ddK * ( diameter K)) & ( BCS K) = ( BCS (1,K)) by A1, Th16, SIMPLEX1: 17;

        hence thesis by A2, A3;

      end;

        suppose

         A4: ( diameter K) = 0 ;

        K = ( BCS ( 0 ,K)) by A1, SIMPLEX1: 16;

        hence thesis by A2, A4;

      end;

        suppose

         A5: dK <> 0 & dK <> ( - 1) & ( diameter K) <> 0 ;

        dK >= ( - 1) by SIMPLEX0: 23;

        then dK > ( - 1) by A5, XXREAL_0: 1;

        then

         A6: dK >= (( - 1) + 1) by INT_1: 7;

        then

         A7: ddK > 0 by A5, XREAL_1: 139;

        (dK + 1) > dK by XREAL_1: 29;

        then

         A8: ddK < 1 by A6, XREAL_1: 189;

        

         A9: ( diameter K) > 0 by A5, Th7;

        then (r / ( diameter K)) > 0 by A2, XREAL_1: 139;

        then

        consider k be Nat such that

         A10: (ddK to_power k) < (r / ( diameter K)) by A7, A8, TBSP_1: 3;

        

         A11: ((r / ( diameter K)) * ( diameter K)) = r by A5, XCMPLX_1: 87;

        

         A12: ( diameter ( BCS (k,K))) <= ((ddK |^ k) * ( diameter K)) by A1, Th17;

        (ddK to_power k) = (ddK |^ k) by POWER: 41;

        then ((ddK |^ k) * ( diameter K)) < r by A9, A10, A11, XREAL_1: 68;

        then ( diameter ( BCS (k,K))) < r by A12, XXREAL_0: 2;

        hence thesis;

      end;

    end;

    theorem :: SIMPLEX2:19

    

     Th19: for i,j be Element of NAT holds ex f be Function of [:( TOP-REAL i), ( TOP-REAL j):], ( TOP-REAL (i + j)) st f is being_homeomorphism & for fi be Element of ( TOP-REAL i), fj be Element of ( TOP-REAL j) holds (f . (fi,fj)) = (fi ^ fj)

    proof

      let i,j be Element of NAT ;

      set TRi = ( TOP-REAL i), TRj = ( TOP-REAL j), TRij = ( TOP-REAL (i + j));

      set tri = the TopStruct of TRi, trj = the TopStruct of TRj, trij = the TopStruct of TRij;

      

       A1: trj = ( TopSpaceMetr ( Euclid j)) by EUCLID:def 8;

      trij = ( TopSpaceMetr ( Euclid (i + j))) & tri = ( TopSpaceMetr ( Euclid i)) by EUCLID:def 8;

      then

      consider f be Function of [:tri, trj:], trij such that

       A2: f is being_homeomorphism and

       A3: for fi,fj be FinSequence st [fi, fj] in ( dom f) holds (f . (fi,fj)) = (fi ^ fj) by A1, TOPREAL7: 26;

      ( rng f) = ( [#] trij) by A2, TOPS_2: 60;

      then

       A4: ( rng f) = ( [#] TRij);

      

       A5: ( [#] [:TRi, TRj:]) = [:( [#] TRi), ( [#] TRj):] by BORSUK_1:def 2;

      

       A6: [:TRi, TRj:] = ( [:TRi, TRj:] | ( [#] [:TRi, TRj:])) by TSEP_1: 3

      .= [:(TRi | ( [#] TRi)), (TRj | ( [#] TRj)):] by A5, BORSUK_3: 22

      .= [:tri, (TRj | ( [#] TRj)):] by TSEP_1: 93

      .= [:tri, trj:] by TSEP_1: 93;

      then

      reconsider F = f as Function of [:TRi, TRj:], TRij;

       A7:

      now

        let P be Subset of [:TRi, TRj:];

        

        thus (F .: ( Cl P)) = ( Cl (f .: P)) by A2, A6, TOPS_2: 60

        .= ( Cl (F .: P)) by TOPS_3: 80;

      end;

      take F;

      

       A8: F is one-to-one by A2, TOPS_2: 60;

      ( dom F) = ( [#] [:TRi, TRj:]) by A2, A6, TOPS_2: 60;

      hence F is being_homeomorphism by A4, A7, A8, TOPS_2: 60;

      let fi be Element of ( TOP-REAL i), fj be Element of ( TOP-REAL j);

      ( dom F) = [:( [#] TRi), ( [#] TRj):] by A5, FUNCT_2:def 1;

      then [fi, fj] in ( dom F) by ZFMISC_1: 87;

      hence thesis by A3;

    end;

    

     Lm3: for n be Nat holds ( [#] ( TOP-REAL n)) = ( [#] ( TopSpaceMetr ( Euclid n)))

    proof

      let n be Nat;

       the TopStruct of ( TOP-REAL n) = ( TopSpaceMetr ( Euclid n)) by EUCLID:def 8;

      hence thesis;

    end;

    theorem :: SIMPLEX2:20

    

     Th20: for i,j be Element of NAT holds for f be Function of [:( TOP-REAL i), ( TOP-REAL j):], ( TOP-REAL (i + j)) st for fi be Element of ( TOP-REAL i), fj be Element of ( TOP-REAL j) holds (f . (fi,fj)) = (fi ^ fj) holds for r holds for fi be Point of ( Euclid i), fj be Point of ( Euclid j), fij be 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 ;

      let f be Function of [:( TOP-REAL i), ( TOP-REAL j):], ( TOP-REAL (i + j)) such that

       A1: for fi be Element of ( TOP-REAL i), fj be Element of ( TOP-REAL j) holds (f . (fi,fj)) = (fi ^ fj);

      let r be Real, fi be Point of ( Euclid i), fj be Point of ( Euclid j), fij be Point of ( Euclid (i + j)) such that

       A2: fij = (fi ^ fj);

      set Ii = ( Intervals (fi,r)), Ij = ( Intervals (fj,r)), Iij = ( Intervals (fij,r));

      

       A3: ( OpenHypercube (fi,r)) = ( product Ii) by EUCLID_9:def 4;

      

       A4: ( [#] ( TOP-REAL i)) = ( [#] ( TopSpaceMetr ( Euclid i))) by Lm3;

      

       A5: ( [#] ( TOP-REAL j)) = ( [#] ( TopSpaceMetr ( Euclid j))) by Lm3;

      

       A6: ( OpenHypercube (fj,r)) = ( product Ij) by EUCLID_9:def 4;

      

       A7: (Ii ^ Ij) = Iij by A2, RLAFFIN3: 1;

      

       A8: (f .: [:( product Ii), ( product Ij):]) c= ( product Iij)

      proof

        let y be object;

        assume y in (f .: [:( product Ii), ( product Ij):]);

        then

        consider x be object such that x in ( dom f) and

         A9: x in [:( product Ii), ( product Ij):] and

         A10: (f . x) = y by FUNCT_1:def 6;

        consider xi,xj be object such that

         A11: xi in ( product Ii) and

         A12: xj in ( product Ij) and

         A13: x = [xi, xj] by A9, ZFMISC_1:def 2;

        reconsider xi as Element of ( TOP-REAL i) by A3, A4, A11;

        reconsider 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 Iij) by A7, A11, A12, RLAFFIN3: 2;

      end;

      

       A14: ( product Iij) c= (f .: [:( product Ii), ( product Ij):])

      proof

        let y be object;

        assume y in ( product Iij);

        then

        consider p1,p2 be FinSequence such that

         A15: y = (p1 ^ p2) and

         A16: p1 in ( product Ii) & p2 in ( product Ij) by A7, RLAFFIN3: 2;

        

         A17: [p1, p2] in [:( product Ii), ( product Ij):] 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 thesis by A17, A18, FUNCT_1:def 6;

      end;

      ( OpenHypercube (fij,r)) = ( product Iij) by EUCLID_9:def 4;

      hence thesis by A3, A6, A8, A14, XBOOLE_0:def 10;

    end;

    theorem :: SIMPLEX2:21

    

     Th21: A is bounded iff ex p be Point of ( Euclid n), r st A c= ( OpenHypercube (p,r))

    proof

      reconsider B = A as Subset of ( Euclid n) by TOPREAL3: 8;

      thus A is bounded implies ex p be Point of ( Euclid n), r be Real st A c= ( OpenHypercube (p,r))

      proof

        assume A is bounded;

        then

         A1: B is bounded by JORDAN2C: 11;

        per cases ;

          suppose

           A2: A is empty;

          take p = the Point of ( Euclid n), r = the Real;

          thus thesis by A2;

        end;

          suppose A is non empty;

          then

          consider p be object such that

           A3: p in B by XBOOLE_0:def 1;

          reconsider p as Element of ( Euclid n) by A3;

          consider r be Real such that 0 < r and

           A4: for x,y be Point of ( Euclid n) st x in B & y in B holds ( dist (x,y)) <= r by A1;

          take p, r1 = (r + 1);

          

           A5: B c= ( Ball (p,r1))

          proof

            let x be object;

            assume

             A6: x in B;

            then

            reconsider x as Element of ( Euclid n);

            ( dist (p,x)) < r1 by A3, A4, A6, XREAL_1: 39;

            hence thesis by METRIC_1: 11;

          end;

          ( Ball (p,r1)) c= ( OpenHypercube (p,r1)) by EUCLID_9: 22;

          hence A c= ( OpenHypercube (p,r1)) by A5;

        end;

      end;

      given p be Point of ( Euclid n), r be Real such that

       A7: A c= ( OpenHypercube (p,r));

      per cases ;

        suppose n = 0 ;

        then ( OpenHypercube (p,r)) = { {} } by EUCLID_9: 12;

        then B = {} or B = { 0 } by A7, ZFMISC_1: 33;

        hence thesis by JORDAN2C: 11;

      end;

        suppose n <> 0 ;

        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 thesis by JORDAN2C: 11;

      end;

    end;

    

     Lm4: for A be Subset of ( TOP-REAL 1) holds A is closed & A is bounded implies A is compact

    proof

      set TR1 = ( TOP-REAL 1);

      let A be Subset of TR1 such that

       A1: A is closed and

       A2: A is bounded;

      consider r be Real such that

       A3: for q be Point of TR1 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 be Function of TR1, R^1 such that

       A4: for p be Element of TR1 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) = ( [#] TR1) by A5, TOPS_2:def 5;

      

       A8: A c= (F " L)

      proof

        let x be object;

        assume

         A9: x in A;

        then

        reconsider v = x as Element of TR1;

        set v1 = (v . 1);

        

         A10: ( len v) = 1 by CARD_1:def 7;

        then v = <*v1*> by FINSEQ_1: 40;

        then

         A11: |.v.| = |.v1.| by TOPREALC: 18;

         |.v.| < r by A3, A9;

        then v1 <= r & ( - r) <= v1 by A11, ABSVALUE: 5;

        then

         A12: v1 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) = v1 by PARTFUN1:def 6;

        (f . v) = (v /. 1) by A4;

        hence thesis by A7, A12, A13, FUNCT_1:def 7;

      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 thesis by A1, A6, A8, COMPTS_1: 9;

    end;

    

     Lm5: for A be Subset of ( TOP-REAL n) holds A is closed & A is bounded implies A is compact

    proof

      defpred P[ Nat] means for A be Subset of ( TOP-REAL $1) holds A is closed & A is bounded implies A is compact;

      

       A1: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat such that

         A2: P[n];

        per cases ;

          suppose n = 0 ;

          hence thesis by Lm4;

        end;

          suppose

           A3: n <> 0 ;

          set n1 = (n + 1);

          set TR1 = ( TOP-REAL 1);

          set TRn = ( TOP-REAL n);

          set TRn1 = ( TOP-REAL n1);

          let A be Subset of TRn1;

          assume that

           A4: A is closed and

           A5: A is bounded;

          consider p be Point of ( Euclid n1), r be Real such that

           A6: A c= ( OpenHypercube (p,r)) by A5, Th21;

          n in NAT by ORDINAL1:def 12;

          then

          consider f be Function of [:TRn, TR1:], TRn1 such that

           A7: f is being_homeomorphism and

           A8: for fi be Element of TRn, fj be Element of TR1 holds (f . (fi,fj)) = (fi ^ fj) by Th19;

          

           A9: f is one-to-one & ( dom f) = ( [#] [:TRn, TR1:]) by A7, TOPGRP_1: 24;

          ( len p) = n1 by CARD_1:def 7;

          then

          consider q1,q2 be FinSequence such that

           A10: ( len q1) = n and

           A11: ( len q2) = 1 and

           A12: p = (q1 ^ q2) by FINSEQ_2: 22;

          ( rng p) c= REAL ;

          then

           A13: p is FinSequence of REAL by FINSEQ_1:def 4;

          then

           A14: q1 is FinSequence of REAL by A12, FINSEQ_1: 36;

          

           A15: q2 is FinSequence of REAL by A12, A13, FINSEQ_1: 36;

          reconsider q1 as Element of ( Euclid n) by A10, A14, TOPREAL3: 45;

          reconsider q2 as Element of ( Euclid 1) by A11, A15, TOPREAL3: 45;

          

           A16: f is continuous by A7, TOPS_2:def 5;

          reconsider Bn = ( cl_Ball (q1,(r * ( sqrt n)))) as Subset of TRn by TOPREAL3: 8;

          reconsider B1 = ( cl_Ball (q2,(r * ( sqrt 1)))) as Subset of TR1 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

           A17: ( OpenHypercube (q2,r)) c= B1;

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

          then

           A18: [:( OpenHypercube (q1,r)), ( OpenHypercube (q2,r)):] c= [:Bn, B1:] by A17, ZFMISC_1: 96;

          ( cl_Ball (q2,(r * ( sqrt 1)))) is bounded by TOPREAL6: 59;

          then B1 is bounded by JORDAN2C: 11;

          then

           A19: B1 is compact by Lm4, 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, TOPREAL6: 58;

          then

           A20: [:Bn, B1:] is compact Subset of [:TRn, TR1:] by A19, BORSUK_3: 23;

          ( rng f) = ( [#] TRn1) by A7, TOPGRP_1: 24;

          then

           A21: (f .: (f " A)) = A by FUNCT_1: 77;

          (f .: [:( OpenHypercube (q1,r)), ( OpenHypercube (q2,r)):]) = ( OpenHypercube (p,r)) by A8, A10, A12, Th20;

          then

           A22: (f " A) c= [:( OpenHypercube (q1,r)), ( OpenHypercube (q2,r)):] by A6, A9, A21, FUNCT_1: 87;

          (f " A) is closed by A4, A7, TOPGRP_1: 24;

          then (f " A) is compact by A18, A20, A22, COMPTS_1: 9, XBOOLE_1: 1;

          hence thesis by A16, A21, WEIERSTR: 8;

        end;

      end;

      

       A23: P[ 0 ];

      for n holds P[n] from NAT_1:sch 2( A23, A1);

      hence thesis;

    end;

    registration

      let n;

      cluster closed bounded -> compact for Subset of ( TOP-REAL n);

      coherence by Lm5;

    end

    registration

      let n;

      let A be affinely-independent Subset of ( TOP-REAL n);

      cluster ( conv A) -> compact;

      coherence

      proof

        n in NAT by ORDINAL1:def 12;

        then ( conv A) is bounded by Th14;

        hence thesis;

      end;

    end

    begin

    theorem :: SIMPLEX2:22

    

     Th22: for A be non empty affinely-independent Subset of ( TOP-REAL n) holds for E be Enumeration of A holds for F be FinSequence of ( bool the carrier of (( TOP-REAL n) | ( conv A))) st ( len F) = ( card A) & ( rng F) is closed & for S be Subset of ( dom F) holds ( conv (E .: S)) c= ( union (F .: S)) holds ( meet ( rng F)) is non empty

    proof

      set TRn = ( TOP-REAL n);

      let A be non empty affinely-independent Subset of TRn;

      set cA = ( conv A);

      let E be Enumeration of A;

      let F be FinSequence of ( bool the carrier of (TRn | cA)) such that

       A1: ( len F) = ( card A) and

       A2: ( rng F) is closed and

       A3: for S be Subset of ( dom F) holds ( conv (E .: S)) c= ( union (F .: S));

      

       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 P[ object, object] means $1 in (F . ((E " ) . $2)) & for B be Subset of TRn st B c= A & $1 in ( conv B) holds $2 in B;

      

       A7: ( TopSpaceMetr En) = the TopStruct of TRn by EUCLID:def 8;

      then

      reconsider CA = cA as non empty Subset of ( TopSpaceMetr En);

      reconsider ca = cA as non empty Subset of En by A7;

      

       A8: (( TopSpaceMetr En) | CA) = ( TopSpaceMetr (En | ca)) by HAUSDORF: 16;

      then

      reconsider CrF = ( COMPLEMENT ( rng F)) as Subset-Family of ( TopSpaceMetr (En | ca)) by A7, PRE_TOPC: 36;

      CA is compact by A7, COMPTS_1: 23;

      then

       A9: ( TopSpaceMetr (En | ca)) is compact by A8, COMPTS_1: 3;

      

       A10: (( TopSpaceMetr En) | CA) = (TRn | cA) by A7, PRE_TOPC: 36;

      assume ( meet ( rng F)) is empty;

      

      then ( [#] (TRn | cA)) = (( meet ( rng F)) ` )

      .= ( union CrF) by A4, TOPS_2: 7;

      then

       A11: CrF is Cover of ( TopSpaceMetr (En | ca)) by A8, A10, SETFAM_1: 45;

      set L = the Lebesgue_number of CrF;

      

       A12: |.Comp.| c= ( [#] Comp);

      then

      consider k be Nat such that

       A13: ( diameter ( BCS (k,Comp))) < L by Th18;

      set Bcs = ( BCS (k,Comp));

      

       A14: |.Bcs.| = |.Comp.| by A12, SIMPLEX1: 19;

      

       A15: the topology of Comp = ( bool A) by SIMPLEX0: 4;

      

       A16: for x be object st x in ( Vertices Bcs) holds ex y be object st y in A & P[x, y]

      proof

        let x be object;

        assume

         A17: x in ( Vertices Bcs);

        then

        reconsider v = x as Element of Bcs;

        v is vertex-like by A17, SIMPLEX0:def 4;

        then

        consider S be Subset of Bcs such that

         A18: S is simplex-like and

         A19: v in S;

        ( @ S) c= ( conv ( @ S)) by RLAFFIN1: 2;

        then

         A20: v in ( conv ( @ S)) by A19;

        ( conv ( @ S)) c= |.Comp.| by A14, A18, SIMPLEX1: 5;

        then

        consider W be Subset of Comp 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 Comp 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 be set such that

         A25: v in Y and

         A26: Y in (F .: (E " W)) by A23, TARSKI:def 4;

        consider i be object 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);

        

         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;

        let B be Subset of TRn;

        assume that

         A30: B c= A and

         A31: x in ( conv B);

        reconsider b = B as Simplex of Comp 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 thesis by A29;

      end;

      consider G be Function of ( Vertices Bcs), A such that

       A32: for x be object st x in ( Vertices Bcs) holds P[x, (G . x)] from FUNCT_2:sch 1( A16);

      

       A33: |.Comp.| = ( conv A) by SIMPLEX1: 8;

      then Bcs is with_non-empty_element by A14, SIMPLEX1: 7;

      then for v be Vertex of Bcs, B be Subset of TRn st B c= A & v in ( conv B) holds (G . v) in B by A32;

      then

      consider S be Simplex of (( card A) - 1), Bcs such that

       A34: (G .: S) = A by SIMPLEX1: 47;

      

       A35: ( [#] Bcs) = ( [#] Comp) by A12, SIMPLEX1: 18;

      then

      reconsider SS = S as Subset of En by A7;

      S is non empty by A34;

      then

      consider s be object such that

       A36: s in S by XBOOLE_0:def 1;

      

       A37: ( conv ( @ S)) c= cA by A14, A33, SIMPLEX1: 5;

      reconsider s as Point of En 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 (En | ca) by A37, TOPMETR:def 2;

      

       A39: SS is bounded;

      CrF is open by A2, A8, A10, TOPS_2: 9;

      then

      consider CRF be Subset of ( TopSpaceMetr (En | ca)) such that

       A40: CRF in CrF and

       A41: ( Ball (ss,L)) c= CRF by A9, A11, Def1;

      (CRF ` ) in ( rng F) by A8, A10, A40, SETFAM_1:def 7;

      then

      consider i be object 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 be object 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= cA by A14, A33, SIMPLEX1: 5;

      then

       A49: ( [#] (En | ca)) = ca & w in cA by A47, TOPMETR:def 2;

      reconsider SS = S as bounded Subset of En by A39;

      ( diameter SS) <= ( diameter ( BCS (k,Comp))) by Def4;

      then

       A50: ( diameter SS) < L 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 as Point of En by A49;

      reconsider ww = w as Point of (En | 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)) < L by A50, XXREAL_0: 2;

      then ww in ( Ball (ss,L)) by METRIC_1: 11;

      hence contradiction by A41, A43, A51, XBOOLE_0:def 5;

    end;

    reserve A for affinely-independent Subset of ( TOP-REAL n);

    theorem :: SIMPLEX2:23

    

     Th23: for A st ( card A) = (n + 1) holds for f be continuous Function of (( TOP-REAL n) | ( conv A)), (( TOP-REAL n) | ( conv A)) holds ex p be Point of ( TOP-REAL n) st p in ( dom f) & (f . p) = p

    proof

      set TRn = ( TOP-REAL n);

      let A be affinely-independent Subset of TRn such that

       A1: ( card A) = (n + 1);

      

       A2: A is non empty by A1;

      set cA = ( conv A);

      let f be continuous Function of (TRn | cA), (TRn | cA);

      reconsider cA as non empty Subset of TRn by A2;

      set T = (TRn | cA);

      reconsider ff = f as continuous Function of T, T;

      set E = the Enumeration of A;

      deffunc P( object) = { v where v be Element of T : (( |-- (A,(E . $1))) . (f . v)) <= (( |-- (A,(E . $1))) . v) };

      consider F be FinSequence such that

       A3: ( len F) = ( card A) & for k st k in ( dom F) holds (F . k) = P(k) from FINSEQ_1:sch 2;

      ( rng F) c= ( bool the carrier of T)

      proof

        let y be object;

        assume y in ( rng F);

        then

        consider x be object such that

         A4: x in ( dom F) and

         A5: (F . x) = y by FUNCT_1:def 3;

        

         A6: P(x) c= the carrier of T

        proof

          let z be object;

          assume z in P(x);

          then ex v be Element of T st z = v & (( |-- (A,(E . x))) . (f . v)) <= (( |-- (A,(E . x))) . v);

          hence thesis;

        end;

        (F . x) = P(x) by A3, A4;

        hence thesis by A5, A6;

      end;

      then

      reconsider F as FinSequence of ( bool the carrier of T) by FINSEQ_1:def 4;

      

       A7: ( [#] T) = cA by PRE_TOPC:def 5;

      

       A8: ( dom f) = the carrier of T by FUNCT_2:def 1;

      now

        let W be Subset of T;

        reconsider Z = 0 as Real;

        reconsider L = ]. -infty , Z.] as Subset of R^1 by TOPMETR: 17;

        assume W in ( rng F);

        then

        consider i be object such that

         A9: i in ( dom F) and

         A10: (F . i) = W by FUNCT_1:def 3;

        reconsider AEi = ( |-- (A,(E . i))) as continuous Function of TRn, R^1 by A1, RLAFFIN3: 32;

        set AT = (AEi | T);

        set Af = (AT * ff);

        set AfT = (Af - AT);

        

         A11: ( dom AfT) = the carrier of T by FUNCT_2:def 1;

        reconsider AfT as Function of T, R^1 by TOPMETR: 17;

        

         A12: ( dom AT) = the carrier of T by FUNCT_2:def 1;

        

         A13: AT = (AEi | the carrier of T) by A7, TMAP_1:def 3;

        

         A14: ( dom Af) = the carrier of T by FUNCT_2:def 1;

        

         A15: (AfT " L) c= P(i)

        proof

          let x be object;

          reconsider xx = x as set by TARSKI: 1;

          assume

           A16: x in (AfT " L);

          then

          reconsider v = x as Point of T;

          x in ( dom AfT) by A16, FUNCT_1:def 7;

          then

           A17: (AfT . x) = ((Af . xx) - (AT . xx)) by VALUED_1: 13;

          (AfT . x) in L & (Af . x) = (AT . (f . x)) by A14, A16, FUNCT_1: 12, FUNCT_1:def 7;

          then ((AT . (f . xx)) - (AT . xx)) <= 0 by A17, XXREAL_1: 2;

          then

           A18: (AT . (f . x)) <= (AT . xx) by XREAL_1: 50;

          (f . x) in ( dom AT) by A14, A16, FUNCT_1: 11;

          then

           A19: (AT . (f . x)) = (AEi . (f . v)) by A13, FUNCT_1: 47;

          (AT . x) = (AEi . v) by A12, A13, FUNCT_1: 47;

          hence thesis by A18, A19;

        end;

        

         A20: P(i) c= (AfT " L)

        proof

          let x be object;

          assume x in P(i);

          then

          consider v be Element of T 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)) = (AT . (f . v)) by A12, A13, FUNCT_1: 47;

          (AEi . v) = (AT . v) by A12, A13, FUNCT_1: 47;

          then (Af . v) <= (AT . v) by A14, A22, A23, FUNCT_1: 12;

          then ((Af . v) - (AT . 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 thesis by A11, A21, FUNCT_1:def 7;

        end;

        L is closed by BORSUK_5: 41;

        then

         A24: (AfT " L) is closed by PRE_TOPC:def 6;

        (F . i) = P(i) by A3, A9;

        hence W is closed by A10, A15, A20, A24, XBOOLE_0:def 10;

      end;

      then

       A25: ( rng F) is closed by TOPS_2:def 2;

      

       A26: ( dom E) = ( Seg ( len E)) by FINSEQ_1:def 3;

      

       A27: ( conv A) c= ( Affin A) by RLAFFIN1: 65;

      

       A28: ( rng E) = A by RLAFFIN3:def 1;

      then ( len E) = ( card A) by FINSEQ_4: 62;

      then

       A29: ( dom F) = ( dom E) by A3, FINSEQ_3: 29;

      for S be Subset of ( dom F) holds ( conv (E .: S)) c= ( union (F .: S))

      proof

        let S be Subset of ( dom F);

        set ES = (E .: S);

        per cases ;

          suppose S is empty;

          then ( conv ES) is empty;

          hence thesis;

        end;

          suppose

           A30: S is non empty;

          let x be object;

          set fx = (f . x), xES = (x |-- ES), fxA = (fx |-- A), xA = (x |-- A);

          assume

           A31: x in ( conv ES);

          

           A32: ( conv ES) c= ( conv A) by A28, RELAT_1: 111, RLAFFIN1: 3;

          then

          reconsider v = x as Point of T by A7, A31;

          

           A33: ( len (fxA * E)) = ( len E) by FINSEQ_2: 33;

          

           A34: ( len E) = ( len (xES * E)) by FINSEQ_2: 33;

          then

          reconsider fxAE = (fxA * E), xESE = (xES * E) as Element of (( len E) -tuples_on REAL ) by A33, FINSEQ_2: 92;

          

           A35: ( dom fxAE) = ( Seg ( len E)) by A33, FINSEQ_1:def 3;

          

           A36: ( conv ES) c= ( Affin ES) by RLAFFIN1: 65;

          then

           A37: xA = xES by A28, A31, RELAT_1: 111, RLAFFIN1: 77;

          

           A38: ES c= A by A28, RELAT_1: 111;

          

           A39: ( Carrier xES) c= ES by RLVECT_2:def 6;

          ES is affinely-independent by A28, RELAT_1: 111, RLAFFIN1: 43;

          then ( sum xES) = 1 & ( Carrier xES) c= A by A31, A36, A38, A39, RLAFFIN1:def 7;

          then

           A40: ( Carrier fxA) c= A & 1 = ( Sum (xES * E)) by A28, RLAFFIN1: 30, RLVECT_2:def 6;

          

           A41: fx in ( rng f) by A7, A8, A31, A32, FUNCT_1:def 3;

          then

           A42: fx in ( conv A) by A7;

          then ( sum fxA) = 1 by A27, RLAFFIN1:def 7;

          then

           A43: ( Sum fxAE) = ( Sum xESE) by A28, A40, RLAFFIN1: 30;

          

           A44: ( dom xESE) = ( Seg ( len E)) by A34, FINSEQ_1:def 3;

          per cases by A43, RVSUM_1: 83;

            suppose ex j be Nat st j in ( Seg ( len E)) & (fxAE . j) < (xESE . j);

            then

            consider j be Nat such that

             A45: j in ( Seg ( len E)) and

             A46: (fxAE . j) < (xESE . j);

            

             A47: (fxAE . j) = (fxA . (E . j)) by A35, A45, FUNCT_1: 12;

            

             A48: (xESE . j) = (xES . (E . j)) by A44, A45, FUNCT_1: 12;

            then (xESE . j) = (( |-- (A,(E . j))) . x) by A31, A37, RLAFFIN3:def 3;

            then

             A49: (( |-- (A,(E . j))) . (f . v)) <= (( |-- (A,(E . j))) . v) by A42, A46, A47, RLAFFIN3:def 3;

            

             A50: (E . j) in ( dom fxA) by A35, A45, FUNCT_1: 11;

            then 0 < (xES . (E . j)) by A7, A41, A46, A47, A48, RLAFFIN1: 71;

            then (E . j) in ( Carrier xES) by A50, RLVECT_2: 19;

            then

            consider i be object such that

             A51: i in ( dom E) and

             A52: i in S and

             A53: (E . i) = (E . 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;

             P(j) = (F . j) by A3, A26, A29, A45;

            then x in (F . j) by A49;

            hence thesis by A54, TARSKI:def 4;

          end;

            suppose

             A55: for j be Nat st j in ( Seg ( len E)) holds (fxAE . j) <= (xESE . j);

            consider j be object such that

             A56: j in S by A30, XBOOLE_0:def 1;

            reconsider j as Nat by A56;

            

             A57: (fxAE . j) <= (xESE . j) by A26, A29, A55, A56;

            

             A58: P(j) = (F . j) by A3, A56;

            (xESE . j) = (xES . (E . j)) by A26, A29, A44, A56, FUNCT_1: 12;

            then

             A59: (xESE . j) = (( |-- (A,(E . j))) . x) by A31, A37, RLAFFIN3:def 3;

            (fxAE . j) = (fxA . (E . j)) by A26, A29, A35, A56, FUNCT_1: 12;

            then (( |-- (A,(E . j))) . (f . v)) <= (( |-- (A,(E . 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 thesis by A60, TARSKI:def 4;

          end;

        end;

      end;

      then ( meet ( rng F)) is non empty by A2, A3, A25, Th22;

      then

      consider v be object such that

       A61: v in ( meet ( rng F)) by XBOOLE_0:def 1;

      

       A62: v in cA by A7, A61;

      then

      reconsider v as Element of TRn;

      set fv = (f . v), vA = (v |-- A), fvA = (fv |-- A);

      

       A63: ( len (fvA * E)) = ( len E) by FINSEQ_2: 33;

      fv in ( rng f) by A8, A61, FUNCT_1:def 3;

      then

       A64: fv in cA by A7;

      then ( Carrier fvA) c= A & ( sum fvA) = 1 by A27, RLAFFIN1:def 7, RLVECT_2:def 6;

      then

       A65: ( Carrier vA) c= A & 1 = ( Sum (fvA * E)) by A28, RLAFFIN1: 30, RLVECT_2:def 6;

      

       A66: ( len E) = ( len (vA * E)) by FINSEQ_2: 33;

      then

      reconsider fvAE = (fvA * E), vAE = (vA * E) as Element of (( len E) -tuples_on REAL ) by A63, FINSEQ_2: 92;

      

       A67: ( dom fvAE) = ( Seg ( len E)) by A63, FINSEQ_1:def 3;

      

       A68: ( dom vAE) = ( Seg ( len E)) by A66, FINSEQ_1:def 3;

      

       A69: for j be Nat st j in ( Seg ( len E)) holds (fvAE . j) <= (vAE . j)

      proof

        let j be Nat;

        assume

         A70: j in ( Seg ( len E));

        then (F . j) = P(j) & (F . j) in ( rng F) by A3, A26, A29, FUNCT_1:def 3;

        then v in P(j) by A61, SETFAM_1:def 1;

        then

         A71: ex w be Element of T st w = v & (( |-- (A,(E . j))) . (f . w)) <= (( |-- (A,(E . j))) . w);

        

         A72: (( |-- (A,(E . j))) . v) = (vA . (E . j)) by RLAFFIN3:def 3

        .= (vAE . j) by A68, A70, FUNCT_1: 12;

        (( |-- (A,(E . j))) . fv) = (fvA . (E . j)) by A64, RLAFFIN3:def 3

        .= (fvAE . j) by A67, A70, FUNCT_1: 12;

        hence thesis by A71, A72;

      end;

      

       A73: ( Carrier vA) c= A by RLVECT_2:def 6;

      ( sum vA) = 1 by A27, A62, RLAFFIN1:def 7;

      then

       A74: ( Sum fvAE) = ( Sum vAE) by A28, A65, RLAFFIN1: 30;

      

       A75: ( Carrier fvA) c= A by RLVECT_2:def 6;

       A76:

      now

        let w be Element of TRn;

        per cases ;

          suppose w in A;

          then

          consider j be object such that

           A77: j in ( dom E) and

           A78: (E . j) = w by A28, FUNCT_1:def 3;

          

           A79: (fvAE . j) = (fvA . w) & (vAE . j) = (vA . w) by A77, A78, FUNCT_1: 13;

          (fvAE . j) <= (vAE . j) & (fvAE . j) >= (vAE . j) by A26, A74, A69, A77, RVSUM_1: 83;

          hence (vA . w) = (fvA . w) by A79, XXREAL_0: 1;

        end;

          suppose

           A80: not w in A;

          then not w in ( Carrier vA) by A73;

          then

           A81: (vA . w) = 0 by RLVECT_2: 19;

           not w in ( Carrier fvA) by A75, A80;

          hence (vA . w) = (fvA . w) by A81, RLVECT_2: 19;

        end;

      end;

      

       A82: ( Sum vA) = v by A27, A62, RLAFFIN1:def 7;

      ( Sum fvA) = fv by A27, A64, RLAFFIN1:def 7;

      then v = fv by A76, A82, RLVECT_2:def 9;

      hence thesis by A8, A61;

    end;

    theorem :: SIMPLEX2:24

    for A st ( card A) = (n + 1) holds for f be continuous Function of (( TOP-REAL n) | ( conv A)), (( TOP-REAL n) | ( conv A)) holds f is with_fixpoint

    proof

      let A be affinely-independent Subset of ( TOP-REAL n) such that

       A1: ( card A) = (n + 1);

      let f be continuous Function of (( TOP-REAL n) | ( conv A)), (( TOP-REAL n) | ( conv A));

      consider x be 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 thesis by ABIAN:def 5;

    end;

    theorem :: SIMPLEX2:25

    

     Th25: ( card A) = (n + 1) implies ( ind ( conv A)) = n

    proof

      set TR = ( TOP-REAL n);

      assume

       A1: ( card A) = (n + 1);

      set C = ( conv A);

      

       A2: ( ind C) >= n

      proof

        set E = the Enumeration of A;

        assume

         A3: ( ind C) < n;

        A is non empty by A1;

        then

        reconsider C as non empty Subset of TR;

        ( ind C) is natural;

        then

        reconsider n1 = (n - 1) as Nat by A3;

        deffunc F( object) = (C \ ( conv (A \ {(E . $1)})));

        reconsider c = C as Subset of the TopStruct of TR;

        set TRC = (TR | C);

        set carr = the carrier of TRC;

        

         A4: the TopStruct of TR = ( TopSpaceMetr ( Euclid n)) & the TopStruct of TRC = ( the TopStruct of TR | c) by EUCLID:def 8, PRE_TOPC: 36;

        consider f be FinSequence such that

         A5: ( len f) = ( len E) & for k st k in ( dom f) holds (f . k) = F(k) from FINSEQ_1:sch 2;

        

         A6: ( [#] TRC) = C by PRE_TOPC:def 5;

        ( rng f) c= ( bool carr)

        proof

          let y be object;

          assume y in ( rng f);

          then

          consider x be object such that

           A7: x in ( dom f) and

           A8: (f . x) = y by FUNCT_1:def 3;

          (f . x) = F(x) by A5, A7;

          then (f . x) c= C by XBOOLE_1: 36;

          hence thesis by A6, A8;

        end;

        then

        reconsider R = ( rng f) as finite Subset-Family of TRC;

        

         A9: ( rng E) = A by RLAFFIN3:def 1;

        then

         A10: ( len E) = ( card A) by FINSEQ_4: 62;

        

         A11: ( dom f) = ( dom E) by A5, FINSEQ_3: 29;

        the carrier of TRC c= ( union R)

        proof

          let x be object;

          assume

           A12: x in the carrier of TRC;

          assume

           A13: not x in ( union R);

          now

            let y be set;

            assume

             A14: y in A;

            then

            consider n be object such that

             A15: n in ( dom E) and

             A16: (E . n) = y by A9, FUNCT_1:def 3;

            reconsider n as Nat by A15;

            (f . n) = F(n) by A5, A11, A15;

            then F(n) in R by A11, A15, FUNCT_1:def 3;

            then not x in F(n) by A13, TARSKI:def 4;

            then ( conv (A \ {(E . n)})) c= ( Affin (A \ {(E . n)})) & x in ( conv (A \ {(E . n)})) by A6, A12, RLAFFIN1: 65, XBOOLE_0:def 5;

            then

             A17: (x |-- A) = (x |-- (A \ {(E . n)})) by RLAFFIN1: 77, XBOOLE_1: 36;

            ( Carrier (x |-- (A \ {(E . n)}))) c= (A \ {(E . n)}) & (E . n) in {(E . n)} by RLVECT_2:def 6, TARSKI:def 1;

            then not (E . n) in ( Carrier (x |-- (A \ {(E . n)}))) by XBOOLE_0:def 5;

            hence ((x |-- A) . y) = 0 by A14, A16, A17, RLVECT_2: 19;

          end;

          then

           A18: x in ( conv (A \ A)) by A6, A12, RLAFFIN1: 76;

          (A \ A) = {} by XBOOLE_1: 37;

          hence contradiction by A18;

        end;

        then

         A19: R is Cover of TRC by SETFAM_1:def 11;

        now

          let U be Subset of TRC;

          assume U in R;

          then

          consider x be object such that

           A20: x in ( dom f) & (f . x) = U by FUNCT_1:def 3;

          reconsider cAE = ( conv (A \ {(E . x)})) as Subset of TRC by A6, RLAFFIN1: 3, XBOOLE_1: 36;

          (A \ {(E . 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;

        end;

        then

         A22: ( ind TRC) = ( 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 be finite Subset-Family of TRC such that

         A23: G is open and

         A24: G is Cover of TRC 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 P[ Nat, set, set] means $3 = { g where g be Subset of TRC : g in G & (g c= (f . ($1 + 1)) or g in $2) };

        defpred P[ set] means $1 in G & $1 c= (f . 1);

        consider G0 be Subset-Family of TRC such that

         A27: for x be set holds x in G0 iff x in ( bool carr) & P[x] from SUBSET_1:sch 1;

        

         A28: for k be Nat st 1 <= k & k < ( len E) holds for x be Element of ( bool ( bool carr)) holds ex y be Element of ( bool ( bool carr)) st P[k, x, y]

        proof

          let k be Nat such that 1 <= k and k < ( len E);

          let x be Element of ( bool ( bool carr));

          set y = { g where g be Subset of TRC : g in G & (g c= (f . (k + 1)) or g in x) };

          y c= ( bool carr)

          proof

            let z be object;

            assume z in y;

            then ex g be Subset of TRC st g = z & g in G & (g c= (f . (k + 1)) or g in x);

            hence thesis;

          end;

          hence thesis;

        end;

        consider p be FinSequence of ( bool ( bool carr)) such that

         A29: ( len p) = ( len E) and

         A30: (p /. 1) = G0 or ( len E) = 0 and

         A31: for k be Nat st 1 <= k & k < ( len E) holds P[k, (p /. k), (p /. (k + 1))] from NAT_2:sch 1( A28);

        defpred H[ Nat, object] means ($1 = 1 implies $2 = ( union G0)) & ($1 <> 1 implies $2 = ( union ((p . $1) \ (p . ($1 - 1)))));

        

         A32: for k be Nat st k in ( Seg ( len E)) holds ex x be object st H[k, x]

        proof

          let k be Nat;

          k = 1 or k <> 1;

          hence thesis;

        end;

        consider h be FinSequence such that

         A33: ( dom h) = ( Seg ( len E)) and

         A34: for k be Nat st k in ( Seg ( len E)) holds H[k, (h . k)] from FINSEQ_1:sch 1( A32);

        

         A35: ( dom p) = ( Seg ( len E)) by A29, FINSEQ_1:def 3;

        ( rng h) c= ( bool carr)

        proof

          let y be object;

          assume y in ( rng h);

          then

          consider x be object such that

           A36: x in ( dom h) and

           A37: (h . x) = y by FUNCT_1:def 3;

          reconsider 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 TRC;

          y = ( union G0) or y = ( union (px \ (p . (x - 1)))) by A33, A34, A36, A37;

          hence thesis;

        end;

        then

        reconsider h as FinSequence of ( bool carr) 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 TRC c= ( union ( rng h))

        proof

          let x be object;

          assume x in the carrier of TRC;

          then x in ( union G) by A24, SETFAM_1: 45;

          then

          consider y be set such that

           A40: x in y and

           A41: y in G by TARSKI:def 4;

          consider z be set such that

           A42: z in R and

           A43: y c= z by A25, A41, SETFAM_1:def 2;

          consider k be object such that

           A44: k in ( dom f) and

           A45: (f . k) = z by A42, FUNCT_1:def 3;

          reconsider k as Nat by A44;

          

           A46: k >= 1 by A44, FINSEQ_3: 25;

          

           A47: ( len E) >= k by A5, A44, FINSEQ_3: 25;

          per cases by A46, XXREAL_0: 1;

            suppose

             A48: k = 1 or y in G0;

            

             A49: 1 in ( Seg ( len E)) 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 thesis by A51, TARSKI:def 4;

          end;

            suppose

             A52: k > 1 & not y in G0;

            defpred Q[ Nat] means $1 > 1 & $1 <= ( len E) & y c= (f . $1);

            

             A53: ex k be Nat st Q[k] by A43, A45, A47, A52;

            consider m be Nat such that

             A54: Q[m] & for n be Nat st Q[n] holds m <= n from NAT_1:sch 5( A53);

            reconsider m1 = (m - 1) as Element of NAT by A54, NAT_1: 20;

            defpred R[ Nat] means 1 <= $1 & $1 <= m1 implies not y in (p /. $1);

            (m1 + 1) <= ( len E) by A54;

            then

             A55: m1 < ( len E) by NAT_1: 13;

            

             A56: for n be Nat st R[n] holds R[(n + 1)]

            proof

              let n be Nat such that

               A57: R[n];

              set n1 = (n + 1);

              assume that 1 <= n1 and

               A58: n1 <= m1;

              n < m1 by A58, NAT_1: 13;

              then

               A59: n < ( len E) by A55, XXREAL_0: 2;

              per cases by NAT_1: 14;

                suppose n = 0 ;

                hence thesis by A1, A9, A30, A52, FINSEQ_4: 62;

              end;

                suppose

                 A60: n >= 1;

                assume

                 A61: y in (p /. n1);

                (p /. n1) = { g where g be Subset of TRC : g in G & (g c= (f . n1) or g in (p /. n)) } by A31, A59, A60;

                then ex g be Subset of TRC st y = g & g in G & (g c= (f . n1) or g in (p /. n)) by A61;

                then Q[n1] by A55, A57, A58, A60, NAT_1: 13, XXREAL_0: 2;

                then m <= n1 by A54;

                then (m1 + 1) <= m1 by A58, XXREAL_0: 2;

                hence contradiction by NAT_1: 13;

              end;

            end;

            

             A62: R[ 0 ];

            

             A63: for n holds R[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 be Subset of TRC : 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 thesis by A69, A65, TARSKI:def 4;

          end;

        end;

        then

         A70: ( rng h) is Cover of TRC by SETFAM_1:def 11;

        now

          let A be Subset of TRC;

          assume A in ( rng h);

          then

          consider k be object such that

           A71: k in ( dom h) and

           A72: (h . k) = A by FUNCT_1:def 3;

          reconsider k as Nat by A71;

          

           A73: k >= 1 by A33, A71, FINSEQ_1: 1;

          per cases by A73, XXREAL_0: 1;

            suppose

             A74: k = 1;

            

             A75: G0 c= G by A27;

            (h . k) = ( union G0) by A33, A34, A71, A74;

            hence A is open by A23, A72, A75, TOPS_2: 11, TOPS_2: 19;

          end;

            suppose

             A76: k > 1;

            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 E) by A33, A71, FINSEQ_1: 1;

            then

             A78: k1 < ( len E) 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: P[k1, (p /. k1), (p /. (k1 + 1))] by A31, A77, A78;

            (p /. k) c= G

            proof

              let x be object;

              assume x in (p /. k);

              then ex g be Subset of TRC st x = g & g in G & (g c= (f . k) or g in (p /. k1)) by A80;

              hence thesis;

            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;

          end;

        end;

        then

         A83: ( rng h) is open by TOPS_2:def 1;

        TRC is compact by COMPTS_1: 3;

        then

        consider gx be Subset-Family of TRC such that gx is open and

         A84: gx is Cover of TRC 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 G[ object, object] means $2 = ( union { u where u be Subset of TRC : u in cgx & u c= (h . $1) });

        

         A87: for k be Nat st k in ( Seg ( len E)) holds ex x be Element of ( bool carr) st G[k, x]

        proof

          let k be Nat;

          set U = { u where u be Subset of TRC : u in cgx & u c= (h . k) };

          U c= ( bool carr)

          proof

            let x be object;

            assume x in U;

            then ex u be Subset of TRC st u = x & u in cgx & u c= (h . k);

            hence thesis;

          end;

          then

          reconsider U as Subset-Family of TRC;

          ( union U) is Subset of TRC;

          hence thesis;

        end;

        consider GX be FinSequence of ( bool carr) such that

         A88: ( dom GX) = ( Seg ( len E)) & for k be Nat st k in ( Seg ( len E)) holds G[k, (GX . k)] from FINSEQ_1:sch 5( A87);

        

         A89: for i be Nat st i in ( dom GX) holds (GX . i) c= (h . i)

        proof

          let i be Nat;

          set U = { u where u be Subset of TRC : u in cgx & u c= (h . i) };

          now

            let x be set;

            assume x in U;

            then ex u be Subset of TRC st x = u & u in cgx & u c= (h . i);

            hence x c= (h . i);

          end;

          then

           A90: ( union U) c= (h . i) by ZFMISC_1: 76;

          assume i in ( dom GX);

          hence thesis by A88, A90;

        end;

        

         A91: ( dom E) = ( Seg ( len E)) by FINSEQ_1:def 3;

        

         A92: for k be Nat st k in ( Seg ( len E)) holds (h . k) misses ( conv (A \ {(E . k)}))

        proof

          let k be Nat;

          assume

           A93: k in ( Seg ( len E));

          then

           A94: k >= 1 by FINSEQ_1: 1;

          

           A95: H[k, (h . k)] by A34, A93;

          assume (h . k) meets ( conv (A \ {(E . k)}));

          then

          consider x be object such that

           A96: x in (h . k) and

           A97: x in ( conv (A \ {(E . k)})) by XBOOLE_0: 3;

          per cases by A94, XXREAL_0: 1;

            suppose

             A98: k = 1;

            then

            consider y be set such that

             A99: x in y and

             A100: y in G0 by A95, A96, TARSKI:def 4;

             P[y] by A27, A100;

            then y c= F(k) by A5, A11, A91, A93, A98;

            hence contradiction by A97, A99, XBOOLE_0:def 5;

          end;

            suppose

             A101: k > 1;

            then

            reconsider k1 = (k - 1) as Element of NAT by NAT_1: 20;

            ( len E) >= (k1 + 1) by A93, FINSEQ_1: 1;

            then

             A102: ( len E) > k1 by NAT_1: 13;

            (k1 + 1) > 1 by A101;

            then

             A103: k1 >= 1 by NAT_1: 13;

            then

             A104: P[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 be 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 be Subset of TRC 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) = F(k) by A5, A11, A91, A93;

            hence contradiction by A97, A107, A108, A109, A110, XBOOLE_0:def 5;

          end;

        end;

        carr c= ( union ( rng GX))

        proof

          let x be object;

          assume

           A111: x in carr;

          ( union gx) = carr & ( union gx) c= ( union cgx) by A84, PCOMPS_1: 19, SETFAM_1: 45;

          then

          consider y be set such that

           A112: x in y and

           A113: y in cgx by A111, TARSKI:def 4;

          consider r be set such that

           A114: r in ( rng h) and

           A115: y c= r by A85, A113, SETFAM_1:def 2;

          consider k be object such that

           A116: k in ( dom h) and

           A117: (h . k) = r by A114, FUNCT_1:def 3;

          

           A118: G[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 be Subset of TRC : u in cgx & u c= (h . k) } by A113, A115, A117;

          then x in (GX . k) by A112, A118, TARSKI:def 4;

          hence thesis by A119, TARSKI:def 4;

        end;

        then

         A120: ( rng GX) is Cover of TRC by SETFAM_1:def 11;

        

         A121: for S be Subset of ( dom GX) holds ( conv (E .: S)) c= ( union (GX .: S))

        proof

          let S be Subset of ( dom GX);

          

           A122: ( rng GX) = (GX .: ( dom GX)) by RELAT_1: 113;

          

           A123: ( union ( rng GX)) = carr by A120, SETFAM_1: 45;

          per cases by XBOOLE_0:def 10;

            suppose S = ( dom GX);

            hence thesis by A6, A9, A91, A88, A122, A123, RELAT_1: 113;

          end;

            suppose

             A124: not ( dom GX) c= S;

            set U = { ( conv (A \ {(E . i)})) where i be Element of NAT : i in (( dom E) \ S) };

            (( dom GX) \ S) is non empty by A124, XBOOLE_1: 37;

            then

             A125: ( conv (E .: S)) = ( meet U) by A91, A88, Th12;

            

             A126: ( meet U) misses ( union (GX .: (( dom E) \ S)))

            proof

              assume ( meet U) meets ( union (GX .: (( dom E) \ S)));

              then

              consider x be object such that

               A127: x in ( meet U) and

               A128: x in ( union (GX .: (( dom E) \ S))) by XBOOLE_0: 3;

              consider y be set such that

               A129: x in y and

               A130: y in (GX .: (( dom E) \ S)) by A128, TARSKI:def 4;

              consider i be object such that

               A131: i in ( dom GX) and

               A132: i in (( dom E) \ S) and

               A133: (GX . i) = y by A130, FUNCT_1:def 6;

              reconsider i as Element of NAT by A131;

              ( conv (A \ {(E . i)})) in U by A132;

              then

               A134: ( meet U) c= ( conv (A \ {(E . i)})) by SETFAM_1: 7;

              y c= (h . i) by A89, A131, A133;

              then (h . i) meets ( conv (A \ {(E . i)})) by A127, A129, A134, XBOOLE_0: 3;

              hence contradiction by A92, A88, A131;

            end;

            ( dom GX) = ( dom E) by A88, FINSEQ_1:def 3;

            

            then ( rng GX) = (GX .: (S \/ (( dom E) \ S))) by A122, XBOOLE_1: 45

            .= ((GX .: S) \/ (GX .: (( dom E) \ S))) by RELAT_1: 120;

            then

             A135: (( union (GX .: S)) \/ ( union (GX .: (( dom E) \ S)))) = C by A6, A123, ZFMISC_1: 78;

            ( conv (E .: S)) c= C by A9, RELAT_1: 111, RLAFFIN1: 3;

            hence thesis by A125, A135, A126, XBOOLE_1: 73;

          end;

        end;

        

         A136: cgx is locally_finite by A86, PCOMPS_1: 18;

        now

          let A be Subset of TRC;

          assume A in ( rng GX);

          then

          consider k be object such that

           A137: k in ( dom GX) & (GX . k) = A by FUNCT_1:def 3;

          set U = { u where u be Subset of TRC : u in cgx & u c= (h . k) };

          

           A138: U c= cgx

          proof

            let x be object;

            assume x in U;

            then ex u be Subset of TRC st x = u & u in cgx & u c= (h . k);

            hence thesis;

          end;

          then

          reconsider U as Subset-Family of TRC 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;

        end;

        then

         A139: ( rng GX) is closed by TOPS_2:def 2;

        ( len GX) = ( card A) by A10, A88, FINSEQ_1:def 3;

        then ( meet ( rng GX)) is non empty by A139, A38, A121, Th22;

        then

        consider I be object such that

         A140: I in ( meet ( rng GX)) by XBOOLE_0:def 1;

        defpred T[ 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 be Nat st k in ( Seg ( len E)) holds ex x be Element of ( bool carr) st T[k, x]

        proof

          let k be Nat;

          assume

           A142: k in ( Seg ( len E));

          then

           A143: k >= 1 by FINSEQ_1: 1;

          

           A144: k <= ( len E) by A142, FINSEQ_1: 1;

          

           A145: (GX . k) c= (h . k) & H[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;

          per cases by A143, XXREAL_0: 1;

            suppose

             A147: k = 1;

            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 be 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 thesis by A147, A149, A150, A148;

          end;

            suppose

             A151: k > 1;

            then

            reconsider k1 = (k - 1) as Nat;

            

             A152: (k1 + 1) = k;

            then

             A153: k1 < ( len E) by A144, NAT_1: 13;

            k1 >= 1 by A151, A152, NAT_1: 13;

            then

             A154: P[k1, (p /. k1), (p /. k)] by A31, A153;

            

             A155: (p . k) = (p /. k) by A35, A142, PARTFUN1:def 6;

            consider g be 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 be Subset of TRC st g = gg & gg in G & (gg c= (f . (k1 + 1)) or gg in (p /. k1)) by A154, A155;

            hence thesis by A156, A157, A158;

          end;

        end;

        consider t be FinSequence of ( bool carr) such that

         A159: ( dom t) = ( Seg ( len E)) & for k be Nat st k in ( Seg ( len E)) holds T[k, (t . k)] from FINSEQ_1:sch 5( A141);

         A160:

        now

          let i,j be Nat;

          assume that

           A161: i in ( dom t) and

           A162: j in ( dom t) and

           A163: i < j;

          

           A164: j <= ( len E) by A159, A162, FINSEQ_1: 1;

          defpred P[ Nat] means i <= $1 & $1 < j implies (t . i) in (p . $1);

          

           A165: T[i, (t . i)] by A159, A161;

          

           A166: 1 <= i by A159, A161, FINSEQ_1: 1;

          

           A167: for k st P[k] holds P[(k + 1)]

          proof

            let k;

            assume

             A168: P[k];

            set k1 = (k + 1);

            assume that

             A169: i <= k1 and

             A170: k1 < j;

            

             A171: k < j by A170, NAT_1: 13;

            per cases by A169, NAT_1: 8;

              suppose i = k1;

              hence thesis by A159, A161;

            end;

              suppose

               A172: i <= k;

              1 <= k1 & k1 <= ( len E) by A166, A164, A169, A170, XXREAL_0: 2;

              then

               A173: k1 in ( dom p) by A35, FINSEQ_1: 1;

              

               A174: k < ( len E) 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;

               P[k, (p /. k), (p /. k1)] by A31, A175, A174;

              then (p . k1) = { g where g be Subset of TRC : g in G & (g c= (f . k1) or g in (p . k)) } by A173, A176, PARTFUN1:def 6;

              hence thesis by A165, A168, A170, A172, NAT_1: 13;

            end;

          end;

          

           A177: P[ 0 ] by A165;

          

           A178: for k holds P[k] from NAT_1:sch 2( A177, A167);

          reconsider j1 = (j - 1) as Nat by A163;

          assume

           A179: (t . i) = (t . j);

          

           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;

        end;

        now

          let x1,x2 be object;

          assume

           A183: x1 in ( dom t) & x2 in ( dom t);

          then

          reconsider i1 = x1, i2 = x2 as Nat;

          assume

           A184: (t . x1) = (t . x2);

          assume x1 <> x2;

          then i1 > i2 or i1 < i2 by XXREAL_0: 1;

          hence contradiction by A160, A183, A184;

        end;

        then t is one-to-one by FUNCT_1:def 4;

        

        then

         A185: ( card ( rng t)) = ( len t) by FINSEQ_4: 62

        .= ( len E) by A159, FINSEQ_1:def 3

        .= (n + 1) by A1, A9, FINSEQ_4: 62;

        then

         A186: ( rng t) is non empty;

         A187:

        now

          let x be set;

          assume x in ( rng t);

          then

          consider i be object such that

           A188: i in ( dom t) & (t . i) = x by FUNCT_1:def 3;

          thus I in x by A159, A188;

        end;

        

         A189: ( rng t) c= G

        proof

          let y be object;

          assume y in ( rng t);

          then

          consider x be object such that

           A190: x in ( dom t) & (t . x) = y by FUNCT_1:def 3;

          thus thesis by A159, A190;

        end;

        n < ( card ( rng t)) by A185, NAT_1: 13;

        then ( card ( Segm n)) in ( card ( Segm ( card ( rng t)))) by NAT_1: 41;

        then (n1 + 1) in ( card ( rng t));

        then ( meet ( rng t)) is empty by A26, A189, TOPDIM_2: 2;

        hence contradiction by A186, A187, SETFAM_1:def 1;

      end;

      ( ind C) <= ( ind TR) & ( ind TR) <= n by TOPDIM_1: 20, TOPDIM_2: 21;

      then ( ind C) <= n by XXREAL_0: 2;

      hence thesis by A2, XXREAL_0: 1;

    end;

    theorem :: SIMPLEX2:26

    ( ind ( TOP-REAL n)) = n

    proof

      set T = ( TOP-REAL n);

      consider I be affinely-independent Subset of T such that

       A1: ( {} T) c= I & I c= ( [#] T) & ( Affin I) = ( Affin ( [#] T)) by RLAFFIN1: 60;

      ( [#] T) is Affine by RUSUB_4: 22;

      then ( dim T) = n & ( Affin ( [#] T)) = ( [#] T) by RLAFFIN1: 50, RLAFFIN3: 4;

      then ( card I) = (n + 1) by A1, RLAFFIN3: 6;

      then ( ind ( conv I)) = n by Th25;

      then ( ind T) >= n & ( ind T) <= n by TOPDIM_1: 20, TOPDIM_2: 21;

      hence thesis by XXREAL_0: 1;

    end;