set dn = conorm Hamacher_norm;
set dc = Hamacher_conorm ;
for a, b being Element of [.0,1.] holds Hamacher_conorm . (a,b) = 1 - (Hamacher_norm . ((1 - a),(1 - b)))
proof
let a, b be Element of [.0,1.]; :: thesis: Hamacher_conorm . (a,b) = 1 - (Hamacher_norm . ((1 - a),(1 - b)))
AB: 0 in [.0,1.] by XXREAL_1:1;
A3: ( 1 - a in [.0,1.] & 1 - b in [.0,1.] ) by OpIn01;
WE: ( 0 <= a & a <= 1 & 0 <= b & b <= 1 ) by XXREAL_1:1;
per cases ( a <> 1 or b <> 1 or ( a = b & b = 1 ) ) ;
suppose Aa: ( a <> 1 or b <> 1 ) ; :: thesis: Hamacher_conorm . (a,b) = 1 - (Hamacher_norm . ((1 - a),(1 - b)))
then AA: 1 - (a * b) <> 0 by ;
Hamacher_conorm . (a,b) = ((a + b) - ((2 * a) * b)) / (1 - (a * b)) by
.= ((1 * (((1 - a) + (1 - b)) - ((1 - a) * (1 - b)))) - ((1 - a) * (1 - b))) / (((1 - a) + (1 - b)) - ((1 - a) * (1 - b)))
.= 1 - (((1 - a) * (1 - b)) / (((1 - a) + (1 - b)) - ((1 - a) * (1 - b)))) by
.= 1 - (Hamacher_norm . ((1 - a),(1 - b))) by ;
hence Hamacher_conorm . (a,b) = 1 - (Hamacher_norm . ((1 - a),(1 - b))) ; :: thesis: verum
end;
suppose T1: ( a = b & b = 1 ) ; :: thesis: Hamacher_conorm . (a,b) = 1 - (Hamacher_norm . ((1 - a),(1 - b)))
then Hamacher_norm . ((1 - a),(1 - b)) = () / (() - ()) by
.= 0 ;
hence Hamacher_conorm . (a,b) = 1 - (Hamacher_norm . ((1 - a),(1 - b))) by ; :: thesis: verum
end;
end;
end;
hence conorm Hamacher_norm = Hamacher_conorm by CoDef; :: thesis: verum