let t be t-norm; :: thesis:
set f1 = drastic_norm ;
for a, b being Element of [.0,1.] holds drastic_norm . (a,b) <= t . (a,b)
proof
let a, b be Element of [.0,1.]; :: thesis: drastic_norm . (a,b) <= t . (a,b)
per cases ( a = 1 or b = 1 or ( a <> 1 & b <> 1 ) ) ;
suppose A2: a = 1 ; :: thesis: drastic_norm . (a,b) <= t . (a,b)
reconsider aa = 1, bb = b as Element of [.0,1.] by XXREAL_1:1;
t . (aa,bb) = t . (bb,aa) by BINOP_1:def 2
.= b by IdDef ;
hence drastic_norm . (a,b) <= t . (a,b) by ; :: thesis: verum
end;
suppose A2: b = 1 ; :: thesis: drastic_norm . (a,b) <= t . (a,b)
reconsider aa = a, bb = 1 as Element of [.0,1.] by XXREAL_1:1;
drastic_norm . (aa,bb) = aa by DrasticDef;
hence drastic_norm . (a,b) <= t . (a,b) by ; :: thesis: verum
end;
suppose A2: ( a <> 1 & b <> 1 ) ; :: thesis: drastic_norm . (a,b) <= t . (a,b)
reconsider aa = a, bb = b as Element of [.0,1.] ;
drastic_norm . (aa,bb) = 0 by ;
hence drastic_norm . (a,b) <= t . (a,b) by XXREAL_1:1; :: thesis: verum
end;
end;
end;
hence drastic_norm <= t ; :: thesis: verum