let A be non empty set ; 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; 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; ( d is onto implies alpha d is one-to-one )
set f = alpha d;
assume
d is onto
; alpha d is one-to-one
then A1:
rng d = the carrier of L
by FUNCT_2:def 3;
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;
( (alpha d) . a = (alpha d) . b implies a = b )
assume A2:
(alpha d) . a = (alpha d) . b
;
a = b
consider z1 being
object such that A3:
z1 in [:A,A:]
and A4:
d . z1 = a
by A1, FUNCT_2:11;
consider x1,
y1 being
object such that A5:
(
x1 in A &
y1 in A )
and A6:
z1 = [x1,y1]
by A3, ZFMISC_1:def 2;
reconsider x1 =
x1,
y1 =
y1 as
Element of
A by A5;
consider z2 being
object such that A7:
z2 in [:A,A:]
and A8:
d . z2 = b
by A1, FUNCT_2:11;
consider x2,
y2 being
object such that A9:
(
x2 in A &
y2 in A )
and A10:
z2 = [x2,y2]
by A7, ZFMISC_1:def 2;
reconsider x2 =
x2,
y2 =
y2 as
Element of
A by A9;
consider E1 being
Equivalence_Relation of
A such that A11:
E1 = (alpha d) . a
and A12:
for
x,
y being
Element of
A holds
(
[x,y] in E1 iff
d . (
x,
y)
<= a )
by Def8;
consider E2 being
Equivalence_Relation of
A such that A13:
E2 = (alpha d) . b
and A14:
for
x,
y being
Element of
A holds
(
[x,y] in E2 iff
d . (
x,
y)
<= b )
by Def8;
A15:
d . (
x2,
y2)
= b
by A8, A10;
then
[x2,y2] in E2
by A14;
then A16:
b <= a
by A2, A15, A11, A12, A13;
A17:
d . (
x1,
y1)
= a
by A4, A6;
then
[x1,y1] in E1
by A12;
then
a <= b
by A2, A17, A11, A13, A14;
hence
a = b
by A16, ORDERS_2:2;
verum
end;
hence
alpha d is one-to-one
by WAYBEL_1:def 1; verum