set f = Lukasiewicz_implication ;
A1:
( 0 in [.0,1.] & 1 in [.0,1.] )
by XXREAL_1:1;
b1:
for x1, x2, y being Element of [.0,1.] st x1 <= x2 holds
Lukasiewicz_implication . (x1,y) >= Lukasiewicz_implication . (x2,y)
proof
let x1,
x2,
y be
Element of
[.0,1.];
( x1 <= x2 implies Lukasiewicz_implication . (x1,y) >= Lukasiewicz_implication . (x2,y) )
assume U1:
x1 <= x2
;
Lukasiewicz_implication . (x1,y) >= Lukasiewicz_implication . (x2,y)
U2:
Lukasiewicz_implication . (
x1,
y)
= min (1,
((1 - x1) + y))
by Luk;
U3:
Lukasiewicz_implication . (
x2,
y)
= min (1,
((1 - x2) + y))
by Luk;
1
- x1 >= 1
- x2
by U1, XREAL_1:13;
then
(1 - x1) + y >= (1 - x2) + y
by XREAL_1:7;
hence
Lukasiewicz_implication . (
x1,
y)
>= Lukasiewicz_implication . (
x2,
y)
by U2, U3, XXREAL_0:18;
verum
end;
b3:
for x, y1, y2 being Element of [.0,1.] st y1 <= y2 holds
Lukasiewicz_implication . (x,y1) <= Lukasiewicz_implication . (x,y2)
proof
let x,
y1,
y2 be
Element of
[.0,1.];
( y1 <= y2 implies Lukasiewicz_implication . (x,y1) <= Lukasiewicz_implication . (x,y2) )
assume
y1 <= y2
;
Lukasiewicz_implication . (x,y1) <= Lukasiewicz_implication . (x,y2)
then
(1 - x) + y1 <= (1 - x) + y2
by XREAL_1:7;
then U1:
min (1,
((1 - x) + y2))
>= min (1,
((1 - x) + y1))
by XXREAL_0:18;
Lukasiewicz_implication . (
x,
y1)
= min (1,
((1 - x) + y1))
by Luk;
hence
Lukasiewicz_implication . (
x,
y1)
<= Lukasiewicz_implication . (
x,
y2)
by U1, Luk;
verum
end;
bb:
min (1,((1 - 1) + 0)) = 0
by XXREAL_0:def 9;
min (1,((1 - 0) + 0)) = 1
;
hence
( Lukasiewicz_implication is decreasing_on_1st & Lukasiewicz_implication is increasing_on_2nd & Lukasiewicz_implication is 00-dominant & Lukasiewicz_implication is 11-dominant & Lukasiewicz_implication is 10-weak )
by b1, b3, A1, Luk, bb; verum