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