let n be Nat; :: thesis: for A being Subset of (TOP-REAL n)
for a, ca being bounded Subset of (Euclid n) st ca = conv A & a = A holds
diameter a = diameter ca
let A be Subset of (TOP-REAL n); :: thesis: for a, ca being bounded Subset of (Euclid n) st ca = conv A & a = A holds
diameter a = diameter ca
let a, ca be bounded Subset of (Euclid n); :: thesis: ( ca = conv A & a = A implies diameter a = diameter ca )
assume that
A1: ca = conv A and
A2: a = A ; :: thesis: diameter a = diameter ca
per cases ( a is empty or not a is empty ) ;
suppose a is empty ; :: thesis: diameter a = diameter ca
hence diameter a = diameter ca by A1, A2; :: thesis: verum
end;
suppose A3: not a is empty ; :: thesis: diameter a = diameter ca
now :: thesis: for x, y being Point of (Euclid n) st x in ca & y in ca holds
dist (x,y) <= diameter a
let x, y be Point of (Euclid n); :: thesis: ( x in ca & y in ca implies dist (x,y) <= diameter a )
assume x in ca ; :: thesis: ( y in ca implies dist (x,y) <= diameter a )
then A4: conv A c= cl_Ball (x,(diameter a)) by A1, A2, Th13;
assume y in ca ; :: thesis: dist (x,y) <= diameter a
hence dist (x,y) <= diameter a by A1, A4, METRIC_1:12; :: thesis: verum
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 diameter a = diameter ca by A5, XXREAL_0:1; :: thesis: verum
end;
end;