let T be non empty Reflexive symmetric triangle MetrStruct ; for P, Q being Subset of T st P is bounded & Q is bounded & P meets Q holds
diameter (P \/ Q) <= (diameter P) + (diameter Q)
let P, Q be Subset of T; ( P is bounded & Q is bounded & P meets Q implies diameter (P \/ Q) <= (diameter P) + (diameter Q) )
assume that
A1:
P is bounded
and
A2:
Q is bounded
and
A3:
P /\ Q <> {}
; XBOOLE_0:def 7 diameter (P \/ Q) <= (diameter P) + (diameter Q)
set g = the Element of P /\ Q;
A4:
the Element of P /\ Q in Q
by A3, XBOOLE_0:def 4;
set s = (diameter P) + (diameter Q);
set b = diameter Q;
A5:
diameter Q <= (diameter P) + (diameter Q)
by A1, Th21, XREAL_1:31;
set a = diameter P;
A6:
the Element of P /\ Q in P
by A3, XBOOLE_0:def 4;
reconsider g = the Element of P /\ Q as Element of T by A3, TARSKI:def 3;
A7:
diameter P <= (diameter P) + (diameter Q)
by A2, Th21, XREAL_1:31;
A8:
for x, y being Point of T st x in P \/ Q & y in P \/ Q holds
dist (x,y) <= (diameter P) + (diameter Q)
proof
let x,
y be
Point of
T;
( x in P \/ Q & y in P \/ Q implies dist (x,y) <= (diameter P) + (diameter Q) )
assume that A9:
x in P \/ Q
and A10:
y in P \/ Q
;
dist (x,y) <= (diameter P) + (diameter Q)
A11:
dist (
x,
y)
<= (dist (x,g)) + (dist (g,y))
by METRIC_1:4;
now dist (x,y) <= (diameter P) + (diameter Q)per cases
( x in P or x in Q )
by A9, XBOOLE_0:def 3;
suppose A12:
x in P
;
dist (x,y) <= (diameter P) + (diameter Q)now dist (x,y) <= (diameter P) + (diameter Q)per cases
( y in P or y in Q )
by A10, XBOOLE_0:def 3;
suppose A13:
y in Q
;
dist (x,y) <= (diameter P) + (diameter Q)A14:
dist (
x,
g)
<= diameter P
by A1, A6, A12, Def8;
dist (
g,
y)
<= diameter Q
by A2, A4, A13, Def8;
then
(dist (x,g)) + (dist (g,y)) <= (diameter P) + (diameter Q)
by A14, XREAL_1:7;
hence
dist (
x,
y)
<= (diameter P) + (diameter Q)
by A11, XXREAL_0:2;
verum end; end; end; hence
dist (
x,
y)
<= (diameter P) + (diameter Q)
;
verum end; suppose A15:
x in Q
;
dist (x,y) <= (diameter P) + (diameter Q)now dist (x,y) <= (diameter P) + (diameter Q)per cases
( y in P or y in Q )
by A10, XBOOLE_0:def 3;
suppose A16:
y in P
;
dist (x,y) <= (diameter P) + (diameter Q)A17:
dist (
x,
g)
<= diameter Q
by A2, A4, A15, Def8;
dist (
g,
y)
<= diameter P
by A1, A6, A16, Def8;
then
(dist (x,g)) + (dist (g,y)) <= (diameter Q) + (diameter P)
by A17, XREAL_1:7;
hence
dist (
x,
y)
<= (diameter P) + (diameter Q)
by A11, XXREAL_0:2;
verum end; end; end; hence
dist (
x,
y)
<= (diameter P) + (diameter Q)
;
verum end; end; end;
hence
dist (
x,
y)
<= (diameter P) + (diameter Q)
;
verum
end;
( P <> {} & P \/ Q is bounded )
by A1, A2, A3, Th13;
hence
diameter (P \/ Q) <= (diameter P) + (diameter Q)
by A8, Def8; verum