set f = Lukasiewicz_norm ;
A1:
for a, b being Element of [.0,1.] holds Lukasiewicz_norm . (a,b) = Lukasiewicz_norm . (b,a)
C1:
for a, b, c being Element of [.0,1.] holds Lukasiewicz_norm . ((Lukasiewicz_norm . (a,b)),c) = Lukasiewicz_norm . (a,(Lukasiewicz_norm . (b,c)))
proof
let a,
b,
c be
Element of
[.0,1.];
Lukasiewicz_norm . ((Lukasiewicz_norm . (a,b)),c) = Lukasiewicz_norm . (a,(Lukasiewicz_norm . (b,c)))
set B =
max (
0,
((a + b) - 1));
set C =
max (
0,
((b + c) - 1));
G1:
max (
0,
((a + b) - 1))
in [.0,1.]
by Lemma2;
G2:
max (
0,
((b + c) - 1))
in [.0,1.]
by Lemma2;
Lukasiewicz_norm . (
(Lukasiewicz_norm . (a,b)),
c) =
Lukasiewicz_norm . (
(max (0,((a + b) - 1))),
c)
by LukNorm
.=
max (
0,
(((max (0,((a + b) - 1))) + c) - 1))
by LukNorm, G1
.=
max (
0,
((a + (max (0,((b + c) - 1)))) - 1))
by Lemma3
.=
Lukasiewicz_norm . (
a,
(max (0,((b + c) - 1))))
by LukNorm, G2
.=
Lukasiewicz_norm . (
a,
(Lukasiewicz_norm . (b,c)))
by LukNorm
;
hence
Lukasiewicz_norm . (
(Lukasiewicz_norm . (a,b)),
c)
= Lukasiewicz_norm . (
a,
(Lukasiewicz_norm . (b,c)))
;
verum
end;
D1:
for a, b, c, d being Element of [.0,1.] st a <= c & b <= d holds
Lukasiewicz_norm . (a,b) <= Lukasiewicz_norm . (c,d)
proof
let a,
b,
c,
d be
Element of
[.0,1.];
( a <= c & b <= d implies Lukasiewicz_norm . (a,b) <= Lukasiewicz_norm . (c,d) )
assume
(
a <= c &
b <= d )
;
Lukasiewicz_norm . (a,b) <= Lukasiewicz_norm . (c,d)
then
a + b <= c + d
by XREAL_1:7;
then
(a + b) - 1
<= (c + d) - 1
by XREAL_1:9;
then
max (
0,
((a + b) - 1))
<= max (
0,
((c + d) - 1))
by XXREAL_0:26;
then
max (
0,
((a + b) - 1))
<= Lukasiewicz_norm . (
c,
d)
by LukNorm;
hence
Lukasiewicz_norm . (
a,
b)
<= Lukasiewicz_norm . (
c,
d)
by LukNorm;
verum
end;
for a being Element of [.0,1.] holds Lukasiewicz_norm . (a,1) = a
hence
( Lukasiewicz_norm is commutative & Lukasiewicz_norm is associative & Lukasiewicz_norm is monotonic & Lukasiewicz_norm is with-1-identity )
by BINOP_1:def 2, BINOP_1:def 3, A1, C1, D1; verum