set dn = conorm drastic_norm;
set dc = drastic_conorm ;
for a, b being Element of [.0,1.] holds drastic_conorm . (a,b) = 1 - (drastic_norm . ((1 - a),(1 - b)))
proof
let a, b be Element of [.0,1.]; :: thesis: drastic_conorm . (a,b) = 1 - (drastic_norm . ((1 - a),(1 - b)))
A3: ( 1 - a in [.0,1.] & 1 - b in [.0,1.] ) by OpIn01;
then we: ( 1 - a <= 1 & 1 - b <= 1 ) by XXREAL_1:1;
WE: ( 0 <= a & 0 <= b ) by XXREAL_1:1;
per cases ( ( a = 0 & b = 0 ) or ( a <> 0 & b <> 0 ) or ( b <> 0 & a = 0 ) or ( a <> 0 & b = 0 ) ) ;
suppose A0: ( a = 0 & b = 0 ) ; :: thesis: drastic_conorm . (a,b) = 1 - (drastic_norm . ((1 - a),(1 - b)))
then A1: min (a,b) = 0 ;
A2: max ((1 - a),(1 - b)) = 1 by A0;
drastic_conorm . (a,b) = max (a,b) by
.= 1 - (min ((1 - a),(1 - b))) by A0
.= 1 - (drastic_norm . ((1 - a),(1 - b))) by ;
hence drastic_conorm . (a,b) = 1 - (drastic_norm . ((1 - a),(1 - b))) ; :: thesis: verum
end;
suppose BB: ( a <> 0 & b <> 0 ) ; :: thesis: drastic_conorm . (a,b) = 1 - (drastic_norm . ((1 - a),(1 - b)))
then B0: min (a,b) <> 0 by XXREAL_0:15;
( 1 - a <> 1 & 1 - b <> 1 ) by BB;
then B1: max ((1 - a),(1 - b)) <> 1 by XXREAL_0:16;
drastic_conorm . (a,b) = 1 - 0 by
.= 1 - (drastic_norm . ((1 - a),(1 - b))) by ;
hence drastic_conorm . (a,b) = 1 - (drastic_norm . ((1 - a),(1 - b))) ; :: thesis: verum
end;
suppose BB: ( b <> 0 & a = 0 ) ; :: thesis: drastic_conorm . (a,b) = 1 - (drastic_norm . ((1 - a),(1 - b)))
then B0: min (a,b) = 0 by ;
B1: min ((1 - a),(1 - b)) = 1 - b by ;
B8: max ((1 - a),(1 - b)) = 1 by ;
drastic_conorm . (a,b) = max (a,b) by
.= 1 - (min ((1 - a),(1 - b))) by
.= 1 - (drastic_norm . ((1 - a),(1 - b))) by ;
hence drastic_conorm . (a,b) = 1 - (drastic_norm . ((1 - a),(1 - b))) ; :: thesis: verum
end;
suppose BB: ( a <> 0 & b = 0 ) ; :: thesis: drastic_conorm . (a,b) = 1 - (drastic_norm . ((1 - a),(1 - b)))
then B0: min (a,b) = 0 by ;
B1: min ((1 - a),(1 - b)) = 1 - a by ;
B8: max ((1 - a),(1 - b)) = 1 by ;
drastic_conorm . (a,b) = max (a,b) by
.= 1 - (min ((1 - a),(1 - b))) by
.= 1 - (drastic_norm . ((1 - a),(1 - b))) by ;
hence drastic_conorm . (a,b) = 1 - (drastic_norm . ((1 - a),(1 - b))) ; :: thesis: verum
end;
end;
end;
hence conorm drastic_norm = drastic_conorm by CoDef; :: thesis: verum