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