let A be non empty set ; :: thesis: for L being lower-bounded LATTICE
for d being distance_function of A,L st d is onto holds
alpha d is one-to-one
let L be lower-bounded LATTICE; :: thesis: for d being distance_function of A,L st d is onto holds
alpha d is one-to-one
let d be distance_function of A,L; :: thesis: ( d is onto implies alpha d is one-to-one )
assume
d is onto
; :: thesis: alpha d is one-to-one
then A1:
rng d = the carrier of L
by FUNCT_2:def 3;
set f = alpha d;
for a, b being Element of L st (alpha d) . a = (alpha d) . b holds
a = b
proof
let a,
b be
Element of
L;
:: thesis: ( (alpha d) . a = (alpha d) . b implies a = b )
assume A2:
(alpha d) . a = (alpha d) . b
;
:: thesis: a = b
consider z1 being
set such that A3:
(
z1 in [:A,A:] &
d . z1 = a )
by A1, FUNCT_2:17;
consider x1,
y1 being
set such that A4:
(
x1 in A &
y1 in A &
z1 = [x1,y1] )
by A3, ZFMISC_1:def 2;
consider z2 being
set such that A5:
(
z2 in [:A,A:] &
d . z2 = b )
by A1, FUNCT_2:17;
consider x2,
y2 being
set such that A6:
(
x2 in A &
y2 in A &
z2 = [x2,y2] )
by A5, ZFMISC_1:def 2;
reconsider x1 =
x1,
y1 =
y1 as
Element of
A by A4;
reconsider x2 =
x2,
y2 =
y2 as
Element of
A by A6;
A7:
d . x1,
y1 = a
by A3, A4;
A8:
d . x2,
y2 = b
by A5, A6;
consider E1 being
Equivalence_Relation of
A such that A9:
(
E1 = (alpha d) . a & ( for
x,
y being
Element of
A holds
(
[x,y] in E1 iff
d . x,
y <= a ) ) )
by Def9;
consider E2 being
Equivalence_Relation of
A such that A10:
(
E2 = (alpha d) . b & ( for
x,
y being
Element of
A holds
(
[x,y] in E2 iff
d . x,
y <= b ) ) )
by Def9;
(
E1 = E2 &
[x1,y1] in E1 )
by A2, A7, A9, A10;
then A11:
a <= b
by A7, A10;
(
E1 = E2 &
[x2,y2] in E2 )
by A2, A8, A9, A10;
then
b <= a
by A8, A9;
hence
a = b
by A11, ORDERS_2:25;
:: thesis: verum
end;
hence
alpha d is one-to-one
by WAYBEL_1:def 1; :: thesis: verum