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) #); :: according to METRIC_1:def 4 :: thesis: the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b) = the distance of MetrStruct(# A,(discrete_dist A) #) . (b,a)
now :: thesis: the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b) = the distance of MetrStruct(# A,(discrete_dist A) #) . (b,a)
per cases ( a <> b or a = b ) ;
suppose A3: a <> b ; :: thesis: 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) = 1 by Def10
.= the distance of MetrStruct(# A,(discrete_dist A) #) . (b,a) by A3, Def10 ;
:: thesis: verum
end;
suppose a = b ; :: thesis: 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) ; :: thesis: verum
end;
end;
end;
hence the distance of MetrStruct(# A,(discrete_dist A) #) . (a,b) = the distance of MetrStruct(# A,(discrete_dist A) #) . (b,a) ; :: thesis: 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) #); :: according to METRIC_1:def 5 :: thesis: 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 ( a = b & a = c ) ; :: thesis: 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))
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 A5; :: thesis: verum
end;
suppose ( a = b & a <> c ) ; :: thesis: 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))
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 A5; :: thesis: verum
end;
suppose A6: ( a = c & a <> b ) ; :: thesis: 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; :: thesis: verum
end;
suppose A8: ( b = c & a <> c ) ; :: thesis: 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 the distance of MetrStruct(# A,(discrete_dist A) #) . (b,c) = 0 by 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 A8; :: thesis: verum
end;
suppose A9: ( a <> b & a <> c & b <> c ) ; :: thesis: 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; :: thesis: 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; :: thesis: verum