set M = MetrStruct(# A,(discrete_dist A) #);
A1:
the distance of MetrStruct(# A,(discrete_dist A) #) is discerning
by Def10;
A2:
the distance of MetrStruct(# A,(discrete_dist A) #) is symmetric
proof
let a,
b be
Element of
MetrStruct(#
A,
(discrete_dist A) #);
METRIC_1:def 4 the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b) = the distance of MetrStruct(# A,(discrete_dist A) #) . (b,a)
hence
the
distance of
MetrStruct(#
A,
(discrete_dist A) #)
. (
a,
b)
= the
distance of
MetrStruct(#
A,
(discrete_dist A) #)
. (
b,
a)
;
verum
end;
A4:
the distance of MetrStruct(# A,(discrete_dist A) #) is triangle
proof
let a,
b,
c be
Element of
MetrStruct(#
A,
(discrete_dist A) #);
METRIC_1:def 5 the distance of MetrStruct(# A,(discrete_dist A) #) . (a,c) <= ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b)) + ( the distance of MetrStruct(# A,(discrete_dist A) #) . (b,c))
A5:
( the
distance of
MetrStruct(#
A,
(discrete_dist A) #)
. (
a,
b)
= 0 iff
a = b )
by Def10;
per cases
( ( a = b & a = c ) or ( a = b & a <> c ) or ( a = c & a <> b ) or ( b = c & a <> c ) or ( a <> b & a <> c & b <> c ) )
;
suppose A6:
(
a = c &
a <> b )
;
the distance of MetrStruct(# A,(discrete_dist A) #) . (a,c) <= ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b)) + ( the distance of MetrStruct(# A,(discrete_dist A) #) . (b,c))then A7:
the
distance of
MetrStruct(#
A,
(discrete_dist A) #)
. (
b,
c)
= 1
by Def10;
( the
distance of
MetrStruct(#
A,
(discrete_dist A) #)
. (
a,
c)
= 0 & the
distance of
MetrStruct(#
A,
(discrete_dist A) #)
. (
a,
b)
= 1 )
by A6, Def10;
hence
the
distance of
MetrStruct(#
A,
(discrete_dist A) #)
. (
a,
c)
<= ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b)) + ( the distance of MetrStruct(# A,(discrete_dist A) #) . (b,c))
by A7;
verum end; suppose A9:
(
a <> b &
a <> c &
b <> c )
;
the distance of MetrStruct(# A,(discrete_dist A) #) . (a,c) <= ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b)) + ( the distance of MetrStruct(# A,(discrete_dist A) #) . (b,c))then A10:
the
distance of
MetrStruct(#
A,
(discrete_dist A) #)
. (
b,
c)
= 1
by Def10;
( the
distance of
MetrStruct(#
A,
(discrete_dist A) #)
. (
a,
c)
= 1 & the
distance of
MetrStruct(#
A,
(discrete_dist A) #)
. (
a,
b)
= 1 )
by A9, Def10;
hence
the
distance of
MetrStruct(#
A,
(discrete_dist A) #)
. (
a,
c)
<= ( the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b)) + ( the distance of MetrStruct(# A,(discrete_dist A) #) . (b,c))
by A10;
verum end; end;
end;
the distance of MetrStruct(# A,(discrete_dist A) #) is Reflexive
by Def10;
hence
( DiscreteSpace A is Reflexive & DiscreteSpace A is discerning & DiscreteSpace A is symmetric & DiscreteSpace A is triangle )
by A1, A2, A4; verum