set g = ConjImpl (I,f);
set X = [.0,1.];
V1:
for x1, x2, y being Element of [.0,1.] st x1 <= x2 holds
(ConjImpl (I,f)) . (x1,y) >= (ConjImpl (I,f)) . (x2,y)
proof
let x1,
x2,
y be
Element of
[.0,1.];
( x1 <= x2 implies (ConjImpl (I,f)) . (x1,y) >= (ConjImpl (I,f)) . (x2,y) )
set h =
((f | [.0,1.]) ") | (f .: [.0,1.]);
U1:
[.0,1.] = dom f
by FUNCT_2:def 1;
rng f = [.0,1.]
by FUNCT_2:def 3;
then Z8:
((f | [.0,1.]) ") | (f .: [.0,1.]) = (f ") | [.0,1.]
by U1, RELAT_1:113;
reconsider h =
((f | [.0,1.]) ") | (f .: [.0,1.]) as
UnOp of
[.0,1.] by Z8;
a0:
dom f = [.0,1.]
by FUNCT_2:def 1;
assume
x1 <= x2
;
(ConjImpl (I,f)) . (x1,y) >= (ConjImpl (I,f)) . (x2,y)
then B1:
f . x1 <= f . x2
by a0, VALUED_0:def 15;
A1:
(ConjImpl (I,f)) . (
x1,
y)
= (f ") . (I . ((f . x1),(f . y)))
by BIDef;
T1:
(ConjImpl (I,f)) . (
x2,
y)
= (f ") . (I . ((f . x2),(f . y)))
by BIDef;
I . (
(f . x1),
(f . y))
>= I . (
(f . x2),
(f . y))
by B1, FUZIMPL1:def 1;
hence
(ConjImpl (I,f)) . (
x1,
y)
>= (ConjImpl (I,f)) . (
x2,
y)
by A1, T1, Rosnie;
verum
end;
v2:
for x, y1, y2 being Element of [.0,1.] st y1 <= y2 holds
(ConjImpl (I,f)) . (x,y1) <= (ConjImpl (I,f)) . (x,y2)
proof
let x,
y1,
y2 be
Element of
[.0,1.];
( y1 <= y2 implies (ConjImpl (I,f)) . (x,y1) <= (ConjImpl (I,f)) . (x,y2) )
assume WW:
y1 <= y2
;
(ConjImpl (I,f)) . (x,y1) <= (ConjImpl (I,f)) . (x,y2)
reconsider h =
f " as
UnOp of
[.0,1.] ;
dom f = [.0,1.]
by FUNCT_2:def 1;
then B1:
f . y1 <= f . y2
by WW, VALUED_0:def 15;
A1:
(ConjImpl (I,f)) . (
x,
y2)
= (f ") . (I . ((f . x),(f . y2)))
by BIDef;
T1:
(ConjImpl (I,f)) . (
x,
y1)
= (f ") . (I . ((f . x),(f . y1)))
by BIDef;
I . (
(f . x),
(f . y1))
<= I . (
(f . x),
(f . y2))
by B1, FUZIMPL1:def 2;
hence
(ConjImpl (I,f)) . (
x,
y1)
<= (ConjImpl (I,f)) . (
x,
y2)
by A1, T1, Rosnie;
verum
end;
reconsider x1 = 0 , x2 = 1 as Element of [.0,1.] by XXREAL_1:1;
H2:
f . 0 = 0
by LemmaBound;
H3:
f . 1 = 1
by LemmaBound;
H5:
(f ") . 0 = 0
by LemmaBound;
v3: (ConjImpl (I,f)) . (x1,x1) =
(f ") . (I . ((f . x1),(f . x1)))
by BIDef
.=
(f ") . 1
by FUZIMPL1:def 3, H2
.=
1
by LemmaBound
;
v4: (ConjImpl (I,f)) . (x2,x2) =
(f ") . (I . ((f . x2),(f . x2)))
by BIDef
.=
(f ") . 1
by FUZIMPL1:def 4, H3
.=
1
by LemmaBound
;
(ConjImpl (I,f)) . (x2,x1) =
(f ") . (I . ((f . x2),(f . x1)))
by BIDef
.=
0
by H5, FUZIMPL1:def 5, H2, H3
;
hence
( ConjImpl (I,f) is decreasing_on_1st & ConjImpl (I,f) is increasing_on_2nd & ConjImpl (I,f) is 00-dominant & ConjImpl (I,f) is 11-dominant & ConjImpl (I,f) is 10-weak )
by V1, v2, v3, v4; verum