let A be non empty set ; for L being lower-bounded LATTICE
for d being distance_function of A,L holds alpha d is meet-preserving
let L be lower-bounded LATTICE; for d being distance_function of A,L holds alpha d is meet-preserving
let d be distance_function of A,L; alpha d is meet-preserving
let a, b be Element of L; WAYBEL_0:def 34 alpha d preserves_inf_of {a,b}
set f = alpha d;
A1:
ex_inf_of (alpha d) .: {a,b}, EqRelLATT A
by YELLOW_0:17;
consider E3 being Equivalence_Relation of A such that
A2:
E3 = (alpha d) . (a "/\" b)
and
A3:
for x, y being Element of A holds
( [x,y] in E3 iff d . (x,y) <= a "/\" b )
by Def8;
consider E2 being Equivalence_Relation of A such that
A4:
E2 = (alpha d) . b
and
A5:
for x, y being Element of A holds
( [x,y] in E2 iff d . (x,y) <= b )
by Def8;
consider E1 being Equivalence_Relation of A such that
A6:
E1 = (alpha d) . a
and
A7:
for x, y being Element of A holds
( [x,y] in E1 iff d . (x,y) <= a )
by Def8;
A8:
for x, y being Element of A holds
( [x,y] in E1 /\ E2 iff [x,y] in E3 )
proof
let x,
y be
Element of
A;
( [x,y] in E1 /\ E2 iff [x,y] in E3 )
hereby ( [x,y] in E3 implies [x,y] in E1 /\ E2 )
assume A9:
[x,y] in E1 /\ E2
;
[x,y] in E3then
[x,y] in E2
by XBOOLE_0:def 4;
then A10:
d . (
x,
y)
<= b
by A5;
[x,y] in E1
by A9, XBOOLE_0:def 4;
then
d . (
x,
y)
<= a
by A7;
then
d . (
x,
y)
<= a "/\" b
by A10, YELLOW_0:23;
hence
[x,y] in E3
by A3;
verum
end;
assume
[x,y] in E3
;
[x,y] in E1 /\ E2
then A11:
d . (
x,
y)
<= a "/\" b
by A3;
a "/\" b <= b
by YELLOW_0:23;
then
d . (
x,
y)
<= b
by A11, ORDERS_2:3;
then A12:
[x,y] in E2
by A5;
a "/\" b <= a
by YELLOW_0:23;
then
d . (
x,
y)
<= a
by A11, ORDERS_2:3;
then
[x,y] in E1
by A7;
hence
[x,y] in E1 /\ E2
by A12, XBOOLE_0:def 4;
verum
end;
A13:
for x, y being object holds
( [x,y] in E1 /\ E2 iff [x,y] in E3 )
proof
let x,
y be
object ;
( [x,y] in E1 /\ E2 iff [x,y] in E3 )
(field E1) /\ (field E2) =
A /\ (field E2)
by EQREL_1:9
.=
A /\ A
by EQREL_1:9
.=
A
;
then A14:
field (E1 /\ E2) c= A
by RELAT_1:19;
hereby ( [x,y] in E3 implies [x,y] in E1 /\ E2 )
end;
assume A16:
[x,y] in E3
;
[x,y] in E1 /\ E2
field E3 = A
by EQREL_1:9;
then reconsider x9 =
x,
y9 =
y as
Element of
A by A16, RELAT_1:15;
[x9,y9] in E1 /\ E2
by A8, A16;
hence
[x,y] in E1 /\ E2
;
verum
end;
dom (alpha d) = the carrier of L
by FUNCT_2:def 1;
then inf ((alpha d) .: {a,b}) =
inf {((alpha d) . a),((alpha d) . b)}
by FUNCT_1:60
.=
((alpha d) . a) "/\" ((alpha d) . b)
by YELLOW_0:40
.=
E1 /\ E2
by A6, A4, Th8
.=
(alpha d) . (a "/\" b)
by A2, A13, RELAT_1:def 2
.=
(alpha d) . (inf {a,b})
by YELLOW_0:40
;
hence
alpha d preserves_inf_of {a,b}
by A1; verum