let n, k be Nat; :: thesis: for K being non void finite-degree bounded SimplicialComplex of (TOP-REAL n) st |.K.| c= [#] K holds
diameter (BCS (k,K)) <= (((degree K) / ((degree K) + 1)) |^ k) * (diameter K)
let K be non void finite-degree bounded SimplicialComplex of (TOP-REAL n); :: thesis: ( |.K.| c= [#] K implies diameter (BCS (k,K)) <= (((degree K) / ((degree K) + 1)) |^ k) * (diameter K) )
set dK = degree K;
set ddK = (degree K) / ((degree K) + 1);
defpred S₁[ Nat] means ( diameter (BCS ($1,K)) <= (((degree K) / ((degree K) + 1)) |^ $1) * (diameter K) & BCS ($1,K) is finite-degree & degree (BCS ($1,K)) <= degree K );
assume A1: |.K.| c= [#] K ; :: thesis: diameter (BCS (k,K)) <= (((degree K) / ((degree K) + 1)) |^ k) * (diameter K)
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
set T = TOP-REAL n;
set B = BCS (k,K);
set cM = center_of_mass (TOP-REAL n);
A3: degree K >= - 1 by SIMPLEX0:23;
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
then reconsider B = BCS (k,K) as non void finite-degree bounded SimplicialComplex of (TOP-REAL n) ;
set dB = degree B;
A5: degree B >= - 1 by SIMPLEX0:23;
A6: 0 <= diameter K by Th7;
A7: 0 <= diameter B by Th7;
A8: ( |.B.| = |.K.| & [#] B = [#] K ) by A1, SIMPLEX1:18, SIMPLEX1:19;
then A9: BCS B = subdivision ((center_of_mass (TOP-REAL n)),B) by A1, SIMPLEX1:def 5;
A10: BCS ((k + 1),K) = BCS B by A1, SIMPLEX1:20;
then A11: diameter (BCS ((k + 1),K)) <= ((degree B) / ((degree B) + 1)) * (diameter B) by A1, A8, Th16;
not {} in dom (center_of_mass (TOP-REAL n)) by ORDERS_1:1;
then dom (center_of_mass (TOP-REAL n)) is with_non-empty_elements by SETFAM_1:def 8;
then A12: degree (BCS ((k + 1),K)) <= degree B by A9, A10, SIMPLEX0:52;

per cases ( degree B = - 1 or degree B = 0 or ( degree B <> - 1 & degree B <> 0 ) ) ;

suppose ( degree B = - 1 or degree B = 0 ) ; :: thesis: S₁[k + 1]

then A13: (degree B) / ((degree B) + 1) = 0 ;

per cases ( degree K = 0 or degree K = - 1 or ( degree K <> 0 & degree K <> - 1 ) ) ;

suppose ( degree K = 0 or degree K = - 1 ) ; :: thesis: S₁[k + 1]

then (degree K) / ((degree K) + 1) = 0 ;
then 0 = ((degree K) / ((degree K) + 1)) |^ (k + 1) by NAT_1:11, NEWTON:11;
hence S₁[k + 1] by A1, A4, A9, A11, A12, A13, SIMPLEX1:20, XXREAL_0:2; :: thesis: verum

end;

suppose A14: ( degree K <> 0 & degree K <> - 1 ) ; :: thesis: S₁[k + 1]

then degree K > - 1 by A3, XXREAL_0:1;
then degree K >= (- 1) + 1 by INT_1:7;
then (degree K) / ((degree K) + 1) > 0 by A14, XREAL_1:139;
then ((degree K) / ((degree K) + 1)) |^ (k + 1) > 0 by NEWTON:83;
hence S₁[k + 1] by A1, A4, A6, A9, A11, A12, A13, SIMPLEX1:20, XXREAL_0:2; :: thesis: verum

end;

end;

end;

suppose ( degree B <> - 1 & degree B <> 0 ) ; :: thesis: S₁[k + 1]

then degree B > - 1 by A5, XXREAL_0:1;
then A15: degree B >= (- 1) + 1 by INT_1:7;
A16: (degree B) / ((degree B) + 1) = (((degree B) + 1) / ((degree B) + 1)) - (1 / ((degree B) + 1))
.= 1 - (1 / ((degree B) + 1)) by A15, XCMPLX_1:60 ;
A17: (degree K) / ((degree K) + 1) = (((degree K) + 1) / ((degree K) + 1)) - (1 / ((degree K) + 1))
.= 1 - (1 / ((degree K) + 1)) by A4, A15, XCMPLX_1:60 ;
(degree B) + 1 <= (degree K) + 1 by A4, XREAL_1:6;
then 1 / ((degree K) + 1) <= 1 / ((degree B) + 1) by A15, XREAL_1:85;
then (degree B) / ((degree B) + 1) <= (degree K) / ((degree K) + 1) by A16, A17, XREAL_1:10;
then A18: ((degree B) / ((degree B) + 1)) * (diameter B) <= ((degree K) / ((degree K) + 1)) * ((((degree K) / ((degree K) + 1)) |^ k) * (diameter K)) by A4, A7, A15, XREAL_1:66;
((degree K) / ((degree K) + 1)) * ((((degree K) / ((degree K) + 1)) |^ k) * (diameter K)) = (((degree K) / ((degree K) + 1)) * (((degree K) / ((degree K) + 1)) |^ k)) * (diameter K)
.= (((degree K) / ((degree K) + 1)) |^ (k + 1)) * (diameter K) by NEWTON:6 ;
hence S₁[k + 1] by A1, A4, A9, A11, A12, A18, SIMPLEX1:20, XXREAL_0:2; :: thesis: verum

end;

end;

end;

((degree K) / ((degree K) + 1)) |^ 0 = 1 by NEWTON:4;
then A19: S₁[ 0 ] by A1, SIMPLEX1:16;
for k being Nat holds S₁[k] from NAT_1:sch 2(A19, A2);
hence diameter (BCS (k,K)) <= (((degree K) / ((degree K) + 1)) |^ k) * (diameter K) ; :: thesis: verum