let C1, C2, C3 be non empty set ; :: thesis: for f being RMembership_Func of C1,C2
for x, z being set st x in C1 & z in C3 holds
sup (rng (min f,(Zmf C2,C3),x,z)) = (Zmf C1,C3) . [x,z]
let f be RMembership_Func of C1,C2; :: thesis: for x, z being set st x in C1 & z in C3 holds
sup (rng (min f,(Zmf C2,C3),x,z)) = (Zmf C1,C3) . [x,z]
let x, z be set ; :: thesis: ( x in C1 & z in C3 implies sup (rng (min f,(Zmf C2,C3),x,z)) = (Zmf C1,C3) . [x,z] )
assume A1:
( x in C1 & z in C3 )
; :: thesis: sup (rng (min f,(Zmf C2,C3),x,z)) = (Zmf C1,C3) . [x,z]
A2:
sup (rng (min f,(Zmf C2,C3),x,z)) <= (Zmf C1,C3) . [x,z]
proof
rng (min f,(Zmf C2,C3),x,z) is
bounded
by Th1;
then A3:
rng (min f,(Zmf C2,C3),x,z) is
bounded_above
by XXREAL_2:def 11;
for
s being
real number st
0 < s holds
(sup (rng (min f,(Zmf C2,C3),x,z))) - s <= (Zmf C1,C3) . [x,z]
proof
let s be
real number ;
:: thesis: ( 0 < s implies (sup (rng (min f,(Zmf C2,C3),x,z))) - s <= (Zmf C1,C3) . [x,z] )
assume
s > 0
;
:: thesis: (sup (rng (min f,(Zmf C2,C3),x,z))) - s <= (Zmf C1,C3) . [x,z]
then consider r being
real number such that A4:
(
r in rng (min f,(Zmf C2,C3),x,z) &
(sup (rng (min f,(Zmf C2,C3),x,z))) - s < r )
by A3, SEQ_4:def 4;
consider y being
set such that A5:
(
y in dom (min f,(Zmf C2,C3),x,z) &
r = (min f,(Zmf C2,C3),x,z) . y )
by A4, FUNCT_1:def 5;
A6:
(
[x,y] in [:C1,C2:] &
[y,z] in [:C2,C3:] &
[x,z] in [:C1,C3:] )
by A1, A5, ZFMISC_1:106;
A7:
0 <= f . [x,y]
by Th3;
r =
min (f . [x,y]),
((Zmf C2,C3) . [y,z])
by A1, A5, Def2
.=
min (f . [x,y]),
0
by A6, FUNCT_3:def 3
.=
0
by A7, XXREAL_0:def 9
.=
(Zmf C1,C3) . [x,z]
by A6, FUNCT_3:def 3
;
hence
(sup (rng (min f,(Zmf C2,C3),x,z))) - s <= (Zmf C1,C3) . [x,z]
by A4;
:: thesis: verum
end;
hence
sup (rng (min f,(Zmf C2,C3),x,z)) <= (Zmf C1,C3) . [x,z]
by XREAL_1:59;
:: thesis: verum
end;
sup (rng (min f,(Zmf C2,C3),x,z)) >= (Zmf C1,C3) . [x,z]
proof
A8:
rng (min f,(Zmf C2,C3),x,z) c= [.0 ,1.]
by RELAT_1:def 19;
reconsider A =
[.0 ,1.] as
closed-interval Subset of
REAL by INTEGRA1:def 1;
A = [.(inf A),(sup A).]
by INTEGRA1:5;
then A9:
(
0 = inf A & 1
= sup A )
by INTEGRA1:6;
A is
bounded_below
by INTEGRA1:3;
then A10:
inf A <= inf (rng (min f,(Zmf C2,C3),x,z))
by A8, SEQ_4:64;
rng (min f,(Zmf C2,C3),x,z) is
bounded
by Th1;
then A11:
inf (rng (min f,(Zmf C2,C3),x,z)) <= sup (rng (min f,(Zmf C2,C3),x,z))
by SEQ_4:24;
[x,z] in [:C1,C3:]
by A1, ZFMISC_1:106;
hence
sup (rng (min f,(Zmf C2,C3),x,z)) >= (Zmf C1,C3) . [x,z]
by A9, A10, A11, FUNCT_3:def 3;
:: thesis: verum
end;
hence
sup (rng (min f,(Zmf C2,C3),x,z)) = (Zmf C1,C3) . [x,z]
by A2, XXREAL_0:1; :: thesis: verum