let t be t-conorm; maxnorm <= t
set f1 = maxnorm ;
for a, b being Element of [.0,1.] holds maxnorm . (a,b) <= t . (a,b)
proof
let a,
b be
Element of
[.0,1.];
maxnorm . (a,b) <= t . (a,b)
reconsider aa =
a,
bb =
b as
Element of
[.0,1.] ;
A1:
maxnorm . (
a,
b)
= max (
aa,
bb)
by MaxDef;
reconsider cc =
0 as
Element of
[.0,1.] by XXREAL_1:1;
aa >= 0
by XXREAL_1:1;
then
t . (
aa,
bb)
>= t . (
cc,
bb)
by MonDef;
then
t . (
aa,
bb)
>= t . (
bb,
cc)
by BINOP_1:def 2;
then A3:
t . (
aa,
bb)
>= bb
by ZeroDef;
bb >= 0
by XXREAL_1:1;
then
t . (
aa,
bb)
>= t . (
aa,
cc)
by MonDef;
then
t . (
aa,
bb)
>= aa
by ZeroDef;
hence
maxnorm . (
a,
b)
<= t . (
a,
b)
by A1, XXREAL_0:28, A3;
verum
end;
hence
maxnorm <= t
; verum