let C1, C2, C3 be non empty set ; :: thesis: for f being RMembership_Func of C1,C2
for g, h being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
sup (rng (min f,(max g,h),x,z)) = max (sup (rng (min f,g,x,z))),(sup (rng (min f,h,x,z)))
let f be RMembership_Func of C1,C2; :: thesis: for g, h being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
sup (rng (min f,(max g,h),x,z)) = max (sup (rng (min f,g,x,z))),(sup (rng (min f,h,x,z)))
let g, h be RMembership_Func of C2,C3; :: thesis: for x, z being set st x in C1 & z in C3 holds
sup (rng (min f,(max g,h),x,z)) = max (sup (rng (min f,g,x,z))),(sup (rng (min f,h,x,z)))
let x, z be set ; :: thesis: ( x in C1 & z in C3 implies sup (rng (min f,(max g,h),x,z)) = max (sup (rng (min f,g,x,z))),(sup (rng (min f,h,x,z))) )
assume A1:
( x in C1 & z in C3 )
; :: thesis: sup (rng (min f,(max g,h),x,z)) = max (sup (rng (min f,g,x,z))),(sup (rng (min f,h,x,z)))
A2:
( dom (max (min f,g,x,z),(min f,h,x,z)) = C2 & dom (min f,(max g,h),x,z) = C2 )
by FUNCT_2:def 1;
A3:
for y being Element of C2 st y in C2 holds
(max (min f,g,x,z),(min f,h,x,z)) . y = (min f,(max g,h),x,z) . y
proof
let y be
Element of
C2;
:: thesis: ( y in C2 implies (max (min f,g,x,z),(min f,h,x,z)) . y = (min f,(max g,h),x,z) . y )
assume
y in C2
;
:: thesis: (max (min f,g,x,z),(min f,h,x,z)) . y = (min f,(max g,h),x,z) . y
A4:
[y,z] in [:C2,C3:]
by A1, ZFMISC_1:106;
(max (min f,g,x,z),(min f,h,x,z)) . y =
max ((min f,g,x,z) . y),
((min f,h,x,z) . y)
by FUZZY_1:def 5
.=
max ((min f,g,x,z) . y),
(min (f . [x,y]),(h . [y,z]))
by A1, Def2
.=
max (min (f . [x,y]),(g . [y,z])),
(min (f . [x,y]),(h . [y,z]))
by A1, Def2
.=
min (f . [x,y]),
(max (g . [y,z]),(h . [y,z]))
by XXREAL_0:38
.=
min (f . [x,y]),
((max g,h) . [y,z])
by A4, FUZZY_1:def 5
.=
(min f,(max g,h),x,z) . y
by A1, Def2
;
hence
(max (min f,g,x,z),(min f,h,x,z)) . y = (min f,(max g,h),x,z) . y
;
:: thesis: verum
end;
set F = min f,g,x,z;
set G = min f,h,x,z;
sup (rng (max (min f,g,x,z),(min f,h,x,z))) = max (sup (rng (min f,g,x,z))),(sup (rng (min f,h,x,z)))
proof
A5:
sup (rng (max (min f,g,x,z),(min f,h,x,z))) <= max (sup (rng (min f,g,x,z))),
(sup (rng (min f,h,x,z)))
proof
rng (max (min f,g,x,z),(min f,h,x,z)) is
bounded
by Th1;
then A6:
rng (max (min f,g,x,z),(min f,h,x,z)) is
bounded_above
by XXREAL_2:def 11;
A7:
for
s being
real number st
0 < s holds
ex
y being
set st
(
y in dom (max (min f,g,x,z),(min f,h,x,z)) &
(sup (rng (max (min f,g,x,z),(min f,h,x,z)))) - s < (max (min f,g,x,z),(min f,h,x,z)) . y )
proof
let s be
real number ;
:: thesis: ( 0 < s implies ex y being set st
( y in dom (max (min f,g,x,z),(min f,h,x,z)) & (sup (rng (max (min f,g,x,z),(min f,h,x,z)))) - s < (max (min f,g,x,z),(min f,h,x,z)) . y ) )
assume
0 < s
;
:: thesis: ex y being set st
( y in dom (max (min f,g,x,z),(min f,h,x,z)) & (sup (rng (max (min f,g,x,z),(min f,h,x,z)))) - s < (max (min f,g,x,z),(min f,h,x,z)) . y )
then consider r being
real number such that A8:
(
r in rng (max (min f,g,x,z),(min f,h,x,z)) &
(sup (rng (max (min f,g,x,z),(min f,h,x,z)))) - s < r )
by A6, SEQ_4:def 4;
consider y being
set such that A9:
(
y in dom (max (min f,g,x,z),(min f,h,x,z)) &
r = (max (min f,g,x,z),(min f,h,x,z)) . y )
by A8, FUNCT_1:def 5;
thus
ex
y being
set st
(
y in dom (max (min f,g,x,z),(min f,h,x,z)) &
(sup (rng (max (min f,g,x,z),(min f,h,x,z)))) - s < (max (min f,g,x,z),(min f,h,x,z)) . y )
by A8, A9;
:: thesis: verum
end;
for
s being
real number st
0 < s holds
(sup (rng (max (min f,g,x,z),(min f,h,x,z)))) - s < max (sup (rng (min f,g,x,z))),
(sup (rng (min f,h,x,z)))
proof
let s be
real number ;
:: thesis: ( 0 < s implies (sup (rng (max (min f,g,x,z),(min f,h,x,z)))) - s < max (sup (rng (min f,g,x,z))),(sup (rng (min f,h,x,z))) )
assume
0 < s
;
:: thesis: (sup (rng (max (min f,g,x,z),(min f,h,x,z)))) - s < max (sup (rng (min f,g,x,z))),(sup (rng (min f,h,x,z)))
then consider y being
set such that A10:
(
y in dom (max (min f,g,x,z),(min f,h,x,z)) &
(sup (rng (max (min f,g,x,z),(min f,h,x,z)))) - s < (max (min f,g,x,z),(min f,h,x,z)) . y )
by A7;
A11:
(max (min f,g,x,z),(min f,h,x,z)) . y = max ((min f,g,x,z) . y),
((min f,h,x,z) . y)
by A10, FUZZY_1:def 5;
(
(min f,g,x,z) . y <= sup (rng (min f,g,x,z)) &
(min f,h,x,z) . y <= sup (rng (min f,h,x,z)) )
proof
for
y being
set st
y in C2 holds
(
(min f,g,x,z) . y <= sup (rng (min f,g,x,z)) &
(min f,h,x,z) . y <= sup (rng (min f,h,x,z)) )
proof
let y be
set ;
:: thesis: ( y in C2 implies ( (min f,g,x,z) . y <= sup (rng (min f,g,x,z)) & (min f,h,x,z) . y <= sup (rng (min f,h,x,z)) ) )
assume
y in C2
;
:: thesis: ( (min f,g,x,z) . y <= sup (rng (min f,g,x,z)) & (min f,h,x,z) . y <= sup (rng (min f,h,x,z)) )
then
(
y in dom (min f,g,x,z) &
y in dom (min f,h,x,z) )
by FUNCT_2:def 1;
then A12:
(
(min f,g,x,z) . y in rng (min f,g,x,z) &
(min f,h,x,z) . y in rng (min f,h,x,z) )
by FUNCT_1:def 5;
(
rng (min f,g,x,z) is
bounded &
rng (min f,h,x,z) is
bounded )
by Th1;
then
(
rng (min f,g,x,z) is
bounded_above &
rng (min f,h,x,z) is
bounded_above )
by XXREAL_2:def 11;
hence
(
(min f,g,x,z) . y <= sup (rng (min f,g,x,z)) &
(min f,h,x,z) . y <= sup (rng (min f,h,x,z)) )
by A12, SEQ_4:def 4;
:: thesis: verum
end;
hence
(
(min f,g,x,z) . y <= sup (rng (min f,g,x,z)) &
(min f,h,x,z) . y <= sup (rng (min f,h,x,z)) )
by A10;
:: thesis: verum
end;
then
(max (min f,g,x,z),(min f,h,x,z)) . y <= max (sup (rng (min f,g,x,z))),
(sup (rng (min f,h,x,z)))
by A11, XXREAL_0:26;
hence
(sup (rng (max (min f,g,x,z),(min f,h,x,z)))) - s < max (sup (rng (min f,g,x,z))),
(sup (rng (min f,h,x,z)))
by A10, XXREAL_0:2;
:: thesis: verum
end;
then
for
s being
real number st
0 < s holds
(sup (rng (max (min f,g,x,z),(min f,h,x,z)))) - s <= max (sup (rng (min f,g,x,z))),
(sup (rng (min f,h,x,z)))
;
hence
sup (rng (max (min f,g,x,z),(min f,h,x,z))) <= max (sup (rng (min f,g,x,z))),
(sup (rng (min f,h,x,z)))
by XREAL_1:59;
:: thesis: verum
end;
A13:
for
y being
set st
y in C2 holds
(max (min f,g,x,z),(min f,h,x,z)) . y <= sup (rng (max (min f,g,x,z),(min f,h,x,z)))
proof
let y be
set ;
:: thesis: ( y in C2 implies (max (min f,g,x,z),(min f,h,x,z)) . y <= sup (rng (max (min f,g,x,z),(min f,h,x,z))) )
assume
y in C2
;
:: thesis: (max (min f,g,x,z),(min f,h,x,z)) . y <= sup (rng (max (min f,g,x,z),(min f,h,x,z)))
then
y in dom (max (min f,g,x,z),(min f,h,x,z))
by FUNCT_2:def 1;
then A14:
(max (min f,g,x,z),(min f,h,x,z)) . y in rng (max (min f,g,x,z),(min f,h,x,z))
by FUNCT_1:def 5;
rng (max (min f,g,x,z),(min f,h,x,z)) is
bounded
by Th1;
then
rng (max (min f,g,x,z),(min f,h,x,z)) is
bounded_above
by XXREAL_2:def 11;
hence
(max (min f,g,x,z),(min f,h,x,z)) . y <= sup (rng (max (min f,g,x,z),(min f,h,x,z)))
by A14, SEQ_4:def 4;
:: thesis: verum
end;
max (sup (rng (min f,g,x,z))),
(sup (rng (min f,h,x,z))) <= sup (rng (max (min f,g,x,z),(min f,h,x,z)))
proof
A15:
sup (rng (min f,g,x,z)) <= sup (rng (max (min f,g,x,z),(min f,h,x,z)))
proof
rng (min f,g,x,z) is
bounded
by Th1;
then A16:
rng (min f,g,x,z) is
bounded_above
by XXREAL_2:def 11;
A17:
for
s being
real number st
0 < s holds
ex
y being
set st
(
y in dom (min f,g,x,z) &
(sup (rng (min f,g,x,z))) - s < (min f,g,x,z) . y )
proof
let s be
real number ;
:: thesis: ( 0 < s implies ex y being set st
( y in dom (min f,g,x,z) & (sup (rng (min f,g,x,z))) - s < (min f,g,x,z) . y ) )
assume
0 < s
;
:: thesis: ex y being set st
( y in dom (min f,g,x,z) & (sup (rng (min f,g,x,z))) - s < (min f,g,x,z) . y )
then consider r being
real number such that A18:
(
r in rng (min f,g,x,z) &
(sup (rng (min f,g,x,z))) - s < r )
by A16, SEQ_4:def 4;
consider y being
set such that A19:
(
y in dom (min f,g,x,z) &
r = (min f,g,x,z) . y )
by A18, FUNCT_1:def 5;
thus
ex
y being
set st
(
y in dom (min f,g,x,z) &
(sup (rng (min f,g,x,z))) - s < (min f,g,x,z) . y )
by A18, A19;
:: thesis: verum
end;
for
s being
real number st
0 < s holds
(sup (rng (min f,g,x,z))) - s <= sup (rng (max (min f,g,x,z),(min f,h,x,z)))
proof
let s be
real number ;
:: thesis: ( 0 < s implies (sup (rng (min f,g,x,z))) - s <= sup (rng (max (min f,g,x,z),(min f,h,x,z))) )
assume
0 < s
;
:: thesis: (sup (rng (min f,g,x,z))) - s <= sup (rng (max (min f,g,x,z),(min f,h,x,z)))
then consider y being
set such that A20:
(
y in dom (min f,g,x,z) &
(sup (rng (min f,g,x,z))) - s < (min f,g,x,z) . y )
by A17;
(min f,g,x,z) . y <= max ((min f,g,x,z) . y),
((min f,h,x,z) . y)
by XXREAL_0:25;
then
(min f,g,x,z) . y <= (max (min f,g,x,z),(min f,h,x,z)) . y
by A20, FUZZY_1:def 5;
then A21:
(sup (rng (min f,g,x,z))) - s < (max (min f,g,x,z),(min f,h,x,z)) . y
by A20, XXREAL_0:2;
(max (min f,g,x,z),(min f,h,x,z)) . y <= sup (rng (max (min f,g,x,z),(min f,h,x,z)))
by A13, A20;
hence
(sup (rng (min f,g,x,z))) - s <= sup (rng (max (min f,g,x,z),(min f,h,x,z)))
by A21, XXREAL_0:2;
:: thesis: verum
end;
hence
sup (rng (min f,g,x,z)) <= sup (rng (max (min f,g,x,z),(min f,h,x,z)))
by XREAL_1:59;
:: thesis: verum
end;
sup (rng (min f,h,x,z)) <= sup (rng (max (min f,g,x,z),(min f,h,x,z)))
proof
rng (min f,h,x,z) is
bounded
by Th1;
then A22:
rng (min f,h,x,z) is
bounded_above
by XXREAL_2:def 11;
A23:
for
s being
real number st
0 < s holds
ex
y being
set st
(
y in dom (min f,h,x,z) &
(sup (rng (min f,h,x,z))) - s < (min f,h,x,z) . y )
proof
let s be
real number ;
:: thesis: ( 0 < s implies ex y being set st
( y in dom (min f,h,x,z) & (sup (rng (min f,h,x,z))) - s < (min f,h,x,z) . y ) )
assume
0 < s
;
:: thesis: ex y being set st
( y in dom (min f,h,x,z) & (sup (rng (min f,h,x,z))) - s < (min f,h,x,z) . y )
then consider r being
real number such that A24:
(
r in rng (min f,h,x,z) &
(sup (rng (min f,h,x,z))) - s < r )
by A22, SEQ_4:def 4;
consider y being
set such that A25:
(
y in dom (min f,h,x,z) &
r = (min f,h,x,z) . y )
by A24, FUNCT_1:def 5;
thus
ex
y being
set st
(
y in dom (min f,h,x,z) &
(sup (rng (min f,h,x,z))) - s < (min f,h,x,z) . y )
by A24, A25;
:: thesis: verum
end;
for
s being
real number st
0 < s holds
(sup (rng (min f,h,x,z))) - s <= sup (rng (max (min f,g,x,z),(min f,h,x,z)))
proof
let s be
real number ;
:: thesis: ( 0 < s implies (sup (rng (min f,h,x,z))) - s <= sup (rng (max (min f,g,x,z),(min f,h,x,z))) )
assume
0 < s
;
:: thesis: (sup (rng (min f,h,x,z))) - s <= sup (rng (max (min f,g,x,z),(min f,h,x,z)))
then consider y being
set such that A26:
(
y in dom (min f,h,x,z) &
(sup (rng (min f,h,x,z))) - s < (min f,h,x,z) . y )
by A23;
(min f,h,x,z) . y <= max ((min f,g,x,z) . y),
((min f,h,x,z) . y)
by XXREAL_0:25;
then
(min f,h,x,z) . y <= (max (min f,g,x,z),(min f,h,x,z)) . y
by A26, FUZZY_1:def 5;
then A27:
(sup (rng (min f,h,x,z))) - s < (max (min f,g,x,z),(min f,h,x,z)) . y
by A26, XXREAL_0:2;
(max (min f,g,x,z),(min f,h,x,z)) . y <= sup (rng (max (min f,g,x,z),(min f,h,x,z)))
by A13, A26;
hence
(sup (rng (min f,h,x,z))) - s <= sup (rng (max (min f,g,x,z),(min f,h,x,z)))
by A27, XXREAL_0:2;
:: thesis: verum
end;
hence
sup (rng (min f,h,x,z)) <= sup (rng (max (min f,g,x,z),(min f,h,x,z)))
by XREAL_1:59;
:: thesis: verum
end;
hence
max (sup (rng (min f,g,x,z))),
(sup (rng (min f,h,x,z))) <= sup (rng (max (min f,g,x,z),(min f,h,x,z)))
by A15, XXREAL_0:28;
:: thesis: verum
end;
hence
sup (rng (max (min f,g,x,z),(min f,h,x,z))) = max (sup (rng (min f,g,x,z))),
(sup (rng (min f,h,x,z)))
by A5, XXREAL_0:1;
:: thesis: verum
end;
hence
sup (rng (min f,(max g,h),x,z)) = max (sup (rng (min f,g,x,z))),(sup (rng (min f,h,x,z)))
by A2, A3, PARTFUN1:34; :: thesis: verum