let n be Nat; for K being non void finite-degree bounded SimplicialComplex of (TOP-REAL n) st |.K.| c= [#] K holds
for r being Real st r > 0 holds
ex k being Nat st diameter (BCS (k,K)) < r
let K be non void finite-degree bounded SimplicialComplex of (TOP-REAL n); ( |.K.| c= [#] K implies for r being Real st r > 0 holds
ex k being Nat st diameter (BCS (k,K)) < r )
assume A1:
|.K.| c= [#] K
; for r being Real st r > 0 holds
ex k being Nat st diameter (BCS (k,K)) < r
set dK = degree K;
let r be Real; ( r > 0 implies ex k being Nat st diameter (BCS (k,K)) < r )
assume A2:
r > 0
; ex k being Nat st diameter (BCS (k,K)) < r
set ddK = (degree K) / ((degree K) + 1);
per cases
( degree K = 0 or degree K = - 1 or diameter K = 0 or ( degree K <> 0 & degree K <> - 1 & diameter K <> 0 ) )
;
suppose A5:
(
degree K <> 0 &
degree K <> - 1 &
diameter K <> 0 )
;
ex k being Nat st diameter (BCS (k,K)) < r
degree K >= - 1
by SIMPLEX0:23;
then
degree K > - 1
by A5, XXREAL_0:1;
then A6:
degree K >= (- 1) + 1
by INT_1:7;
then A7:
(degree K) / ((degree K) + 1) > 0
by A5, XREAL_1:139;
(degree K) + 1
> degree K
by XREAL_1:29;
then A8:
(degree K) / ((degree K) + 1) < 1
by A6, XREAL_1:189;
A9:
diameter K > 0
by A5, Th7;
then
r / (diameter K) > 0
by A2, XREAL_1:139;
then consider k being
Nat such that A10:
((degree K) / ((degree K) + 1)) 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)) <= (((degree K) / ((degree K) + 1)) |^ k) * (diameter K)
by A1, Th17;
((degree K) / ((degree K) + 1)) to_power k = ((degree K) / ((degree K) + 1)) |^ k
by POWER:41;
then
(((degree K) / ((degree K) + 1)) |^ k) * (diameter K) < r
by A9, A10, A11, XREAL_1:68;
then
diameter (BCS (k,K)) < r
by A12, XXREAL_0:2;
hence
ex
k being
Nat st
diameter (BCS (k,K)) < r
;
verum end;