set dn = conorm Lukasiewicz_norm;
set dc = BoundedSum_conorm ;
for a, b being Element of [.0,1.] holds BoundedSum_conorm . (a,b) = 1 - (Lukasiewicz_norm . ((1 - a),(1 - b)))
proof
let a,
b be
Element of
[.0,1.];
BoundedSum_conorm . (a,b) = 1 - (Lukasiewicz_norm . ((1 - a),(1 - b)))
A3:
( 1
- a in [.0,1.] & 1
- b in [.0,1.] )
by OpIn01;
BoundedSum_conorm . (
a,
b) =
min (
(a + b),1)
by LukConorm
.=
1
- (max (0,(((1 - a) + (1 - b)) - 1)))
by LukasiDual
.=
1
- (Lukasiewicz_norm . ((1 - a),(1 - b)))
by LukNorm, A3
;
hence
BoundedSum_conorm . (
a,
b)
= 1
- (Lukasiewicz_norm . ((1 - a),(1 - b)))
;
verum
end;
hence
conorm Lukasiewicz_norm = BoundedSum_conorm
by CoDef; verum