set dn = conorm nilmin_norm;
set dc = nilmax_conorm ;
for a, b being Element of [.0,1.] holds nilmax_conorm . (a,b) = 1 - (nilmin_norm . ((1 - a),(1 - b)))
proof
let a, b be Element of [.0,1.]; :: thesis: nilmax_conorm . (a,b) = 1 - (nilmin_norm . ((1 - a),(1 - b)))
A3: ( 1 - a in [.0,1.] & 1 - b in [.0,1.] ) by OpIn01;
per cases ( a + b < 1 or a + b >= 1 ) ;
suppose W0: a + b < 1 ; :: thesis: nilmax_conorm . (a,b) = 1 - (nilmin_norm . ((1 - a),(1 - b)))
then 2 - (a + b) > 2 - 1 by XREAL_1:10;
then W1: (1 - a) + (1 - b) > 1 ;
nilmax_conorm . (a,b) = max (a,b) by
.= 1 - (min ((1 - a),(1 - b))) by MaxMin
.= 1 - (nilmin_norm . ((1 - a),(1 - b))) by ;
hence nilmax_conorm . (a,b) = 1 - (nilmin_norm . ((1 - a),(1 - b))) ; :: thesis: verum
end;
suppose W0: a + b >= 1 ; :: thesis: nilmax_conorm . (a,b) = 1 - (nilmin_norm . ((1 - a),(1 - b)))
then 2 - (a + b) <= 2 - 1 by XREAL_1:10;
then W1: (1 - a) + (1 - b) <= 1 ;
nilmax_conorm . (a,b) = 1 - 0 by
.= 1 - (nilmin_norm . ((1 - a),(1 - b))) by ;
hence nilmax_conorm . (a,b) = 1 - (nilmin_norm . ((1 - a),(1 - b))) ; :: thesis: verum
end;
end;
end;
hence conorm nilmin_norm = nilmax_conorm by CoDef; :: thesis: verum