let n be Nat; for K being non void finite-degree bounded SimplicialComplex of (TOP-REAL n) st |.K.| c= [#] K holds
diameter (BCS K) <= ((degree K) / ((degree K) + 1)) * (diameter K)
set T = TOP-REAL n;
let K be non void finite-degree bounded SimplicialComplex of (TOP-REAL n); ( |.K.| c= [#] K implies diameter (BCS K) <= ((degree K) / ((degree K) + 1)) * (diameter K) )
set BK = BCS K;
set cM = center_of_mass (TOP-REAL n);
set dK = degree K;
assume
|.K.| c= [#] K
; diameter (BCS K) <= ((degree K) / ((degree K) + 1)) * (diameter K)
then A2:
BCS K = subdivision ((center_of_mass (TOP-REAL n)),K)
by SIMPLEX1:def 5;
for A being Subset of (Euclid n) st A is Simplex of (BCS K) holds
diameter A <= ((degree K) / ((degree K) + 1)) * (diameter K)
proof
let A be
Subset of
(Euclid n);
( A is Simplex of (BCS K) implies diameter A <= ((degree K) / ((degree K) + 1)) * (diameter K) )
reconsider ONE = 1 as
ext-real number ;
assume A3:
A is
Simplex of
(BCS K)
;
diameter A <= ((degree K) / ((degree K) + 1)) * (diameter K)
then reconsider a =
A as
Simplex of
(BCS K) ;
consider S being
c=-linear finite simplex-like Subset-Family of
K such that A4:
A = (center_of_mass (TOP-REAL n)) .: S
by A2, A3, SIMPLEX0:def 20;
A5:
A is
bounded
by A3, Th5;
reconsider s =
@ S as
c=-linear finite finite-membered Subset-Family of
(TOP-REAL n) ;
set Us =
union s;
set C =
Complex_of {(union s)};
(
union S is
empty or
union S in S )
by SIMPLEX0:9, ZFMISC_1:2;
then A6:
union S is
open
by TOPS_2:def 1;
then A7:
card (union S) <= (degree K) + ONE
by SIMPLEX0:24;
A8:
diameter K >= 0
by Th7;
A9:
not
{} in dom (center_of_mass (TOP-REAL n))
by ORDERS_1:1;
then A10:
dom (center_of_mass (TOP-REAL n)) is
with_non-empty_elements
by SETFAM_1:def 8;
A11:
[#] (TOP-REAL n) = [#] (Euclid n)
by Lm1;
then reconsider US =
union s as
Subset of
(Euclid n) ;
A12:
a in the
topology of
(BCS K)
by PRE_TOPC:def 2;
per cases
( K is empty-membered or not K is empty-membered )
;
suppose
not
K is
empty-membered
;
diameter A <= ((degree K) / ((degree K) + 1)) * (diameter K)then
(
degree K >= - 1 &
degree K <> - 1 )
by SIMPLEX0:22, SIMPLEX0:23;
then
degree K > - 1
by XXREAL_0:1;
then A15:
degree K >= (- 1) + 1
by INT_1:7;
then A16:
((degree K) / ((degree K) + 1)) * (diameter K) >= 0
by A8;
per cases
( a is empty or not a is empty )
;
suppose A17:
not
a is
empty
;
diameter A <= ((degree K) / ((degree K) + 1)) * (diameter K)now
US is
bounded
;
then
union s is
Bounded
by JORDAN2C:def 1;
then
conv (union s) is
Bounded
by Th14;
then reconsider cUs =
conv (union s) as
bounded Subset of
(Euclid n) by JORDAN2C:def 1;
let x,
y be
Point of
(Euclid n);
( x in A & y in A implies dist (x,y) <= ((degree K) / ((degree K) + 1)) * (diameter K) )assume that A18:
x in A
and A19:
y in A
;
dist (x,y) <= ((degree K) / ((degree K) + 1)) * (diameter K)reconsider X =
x,
Y =
y as
Element of
(TOP-REAL n) by A11;
A20:
(
|.(BCS (Complex_of {(union s)})).| = |.(Complex_of {(union s)}).| &
|.(Complex_of {(union s)}).| = conv (union s) )
by SIMPLEX1:8, SIMPLEX1:10;
consider p being
set such that A21:
p in dom (center_of_mass (TOP-REAL n))
and A22:
p in s
and
(center_of_mass (TOP-REAL n)) . p = x
by A4, A18, FUNCT_1:def 6;
p c= union s
by A22, ZFMISC_1:74;
then A23:
union s <> {}
by A9, A21;
card (union s) <= (degree K) + 1
by A7, XXREAL_3:def 2;
then A24:
((degree K) + 1) " <= (card (union s)) "
by A23, XREAL_1:85;
A25:
diameter US <= diameter K
by A6, Def4;
A26:
((card (union s)) - 1) / (card (union s)) =
((card (union s)) / (card (union s))) - (1 / (card (union s)))
.=
1
- (1 / (card (union s)))
by A23, XCMPLX_1:60
;
A27:
diameter cUs = diameter US
by Th15;
consider b1,
b2 being
VECTOR of
(TOP-REAL n),
r being
Real such that A28:
b1 in Vertices (BCS (Complex_of {(union s)}))
and A29:
b2 in Vertices (BCS (Complex_of {(union s)}))
and A30:
X - Y = r * (b1 - b2)
and A31:
0 <= r
and A32:
r <= ((card (union s)) - 1) / (card (union s))
by A4, A17, A18, A19, Th11;
reconsider B1 =
b1,
B2 =
b2 as
Element of
(BCS (Complex_of {(union s)})) by A28, A29;
B1 is
vertex-like
by A28, SIMPLEX0:def 4;
then consider S1 being
Subset of
(BCS (Complex_of {(union s)})) such that A33:
S1 is
open
and A34:
B1 in S1
by SIMPLEX0:def 3;
A35:
conv (@ S1) c= |.(BCS (Complex_of {(union s)})).|
by A33, SIMPLEX1:5;
B2 is
vertex-like
by A29, SIMPLEX0:def 4;
then consider S2 being
Subset of
(BCS (Complex_of {(union s)})) such that A36:
S2 is
open
and A37:
B2 in S2
by SIMPLEX0:def 3;
@ S2 c= conv (@ S2)
by CONVEX1:41;
then A38:
B2 in conv (@ S2)
by A37;
@ S1 c= conv (@ S1)
by CONVEX1:41;
then A39:
B1 in conv (@ S1)
by A34;
reconsider bb1 =
b1,
bb2 =
b2 as
Point of
(Euclid n) by A11;
(degree K) / ((degree K) + 1) =
(((degree K) + 1) / ((degree K) + 1)) - (1 / ((degree K) + 1))
.=
1
- (1 / ((degree K) + 1))
by A15, XCMPLX_1:60
;
then
((card (union s)) - 1) / (card (union s)) <= (degree K) / ((degree K) + 1)
by A24, A26, XREAL_1:10;
then A41:
(
dist (
bb1,
bb2)
>= 0 &
r <= (degree K) / ((degree K) + 1) )
by A32, XXREAL_0:2;
conv (@ S2) c= |.(BCS (Complex_of {(union s)})).|
by A36, SIMPLEX1:5;
then
dist (
bb1,
bb2)
<= diameter US
by A20, A27, A39, A38, A35, TBSP_1:def 8;
then A42:
dist (
bb1,
bb2)
<= diameter K
by A25, XXREAL_0:2;
dist (
x,
y) =
|.(x - y).|
by EUCLID:def 6
.=
|.(X - Y).|
.=
|.(r * (bb1 - bb2)).|
by A30
.=
(abs r) * |.(bb1 - bb2).|
by EUCLID:11
.=
r * |.(bb1 - bb2).|
by A31, ABSVALUE:def 1
.=
r * (dist (bb1,bb2))
by EUCLID:def 6
;
hence
dist (
x,
y)
<= ((degree K) / ((degree K) + 1)) * (diameter K)
by A31, A42, A41, XREAL_1:66;
verum end; hence
diameter A <= ((degree K) / ((degree K) + 1)) * (diameter K)
by A5, A17, TBSP_1:def 8;
verum end;
end;
hence
diameter (BCS K) <= ((degree K) / ((degree K) + 1)) * (diameter K)
by Def4; verum