reconsider ZS = {0} as non empty set ;
deffunc H1( Element of ZS, Element of ZS) -> Element of REAL = In (0,REAL);
consider F being Function of [:ZS,ZS:],REAL such that
A1:
for x, y being Element of ZS holds F . (x,y) = H1(x,y)
from BINOP_1:sch 4();
reconsider V = MetrStruct(# ZS,F #) as non empty MetrStruct ;
A4:
now for a, b, c being Element of V holds dist (a,c) <= (dist (a,b)) + (dist (b,c))let a,
b,
c be
Element of
V;
dist (a,c) <= (dist (a,b)) + (dist (b,c))A5:
c = 0
by TARSKI:def 1;
a = 0
by TARSKI:def 1;
then
(
b = 0 &
dist (
a,
c)
= 0 )
by A3, A5, TARSKI:def 1;
hence
dist (
a,
c)
<= (dist (a,b)) + (dist (b,c))
by A3, A5;
verum end;
then reconsider V = V as non empty Reflexive discerning symmetric triangle MetrStruct by A3, A2, A4, METRIC_1:1, METRIC_1:2, METRIC_1:3, METRIC_1:4;
take
V
; V is convex
let x, y be Element of V; VECTMETR:def 1 for r being Real st 0 <= r & r <= 1 holds
ex z being Element of V st
( dist (x,z) = r * (dist (x,y)) & dist (z,y) = (1 - r) * (dist (x,y)) )
let r be Real; ( 0 <= r & r <= 1 implies ex z being Element of V st
( dist (x,z) = r * (dist (x,y)) & dist (z,y) = (1 - r) * (dist (x,y)) ) )
assume that
0 <= r
and
r <= 1
; ex z being Element of V st
( dist (x,z) = r * (dist (x,y)) & dist (z,y) = (1 - r) * (dist (x,y)) )
take z = x; ( dist (x,z) = r * (dist (x,y)) & dist (z,y) = (1 - r) * (dist (x,y)) )
A6: dist (z,y) =
F . (z,y)
by METRIC_1:def 1
.=
0
by A1
;
dist (x,z) =
F . (x,z)
by METRIC_1:def 1
.=
0
by A1
;
hence
( dist (x,z) = r * (dist (x,y)) & dist (z,y) = (1 - r) * (dist (x,y)) )
by A6; verum