let C be non empty set ; for f, h, g being Membership_Func of C holds (max (f,g)) ++ (max (f,h)) c=
let f, h, g be Membership_Func of C; (max (f,g)) ++ (max (f,h)) c=
let c be Element of C; FUZZY_1:def 2 (max (f,(g ++ h))) . c <= ((max (f,g)) ++ (max (f,h))) . c
A1: ((max (f,g)) ++ (max (f,h))) . c =
(((max (f,g)) . c) + ((max (f,h)) . c)) - (((max (f,g)) . c) * ((max (f,h)) . c))
by Def3
.=
((max ((f . c),(g . c))) + ((max (f,h)) . c)) - (((max (f,g)) . c) * ((max (f,h)) . c))
by FUZZY_1:5
.=
((max ((f . c),(g . c))) + (max ((f . c),(h . c)))) - (((max (f,g)) . c) * ((max (f,h)) . c))
by FUZZY_1:5
.=
((max ((f . c),(g . c))) + (max ((f . c),(h . c)))) - ((max ((f . c),(g . c))) * ((max (f,h)) . c))
by FUZZY_1:5
.=
((max ((f . c),(g . c))) + (max ((f . c),(h . c)))) - ((max ((f . c),(g . c))) * (max ((f . c),(h . c))))
by FUZZY_1:5
;
A2:
max ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= ((max ((f . c),(g . c))) + (max ((f . c),(h . c)))) - ((max ((f . c),(g . c))) * (max ((f . c),(h . c))))
proof
per cases
( ( max ((f . c),(g . c)) = f . c & max ((f . c),(h . c)) = f . c ) or ( max ((f . c),(g . c)) = f . c & max ((f . c),(h . c)) = h . c ) or ( max ((f . c),(g . c)) = g . c & max ((f . c),(h . c)) = f . c ) or ( max ((f . c),(g . c)) = g . c & max ((f . c),(h . c)) = h . c ) )
by XXREAL_0:16;
suppose A3:
(
max (
(f . c),
(g . c))
= f . c &
max (
(f . c),
(h . c))
= f . c )
;
max ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= ((max ((f . c),(g . c))) + (max ((f . c),(h . c)))) - ((max ((f . c),(g . c))) * (max ((f . c),(h . c))))
(1_minus g) . c >= 0
by Th1;
then A4:
1
- (g . c) >= 0
by FUZZY_1:def 5;
h . c <= f . c
by A3, XXREAL_0:def 10;
then
1
- (h . c) >= 1
- (f . c)
by XREAL_1:10;
then A5:
(1 - (g . c)) * (1 - (f . c)) <= (1 - (g . c)) * (1 - (h . c))
by A4, XREAL_1:64;
(1_minus f) . c >= 0
by Th1;
then A6:
1
- (f . c) >= 0
by FUZZY_1:def 5;
f ++ f c=
by Th28;
then
(f ++ f) . c >= f . c
;
then A7:
((f . c) + (f . c)) - ((f . c) * (f . c)) >= f . c
by Def3;
g . c <= f . c
by A3, XXREAL_0:def 10;
then
1
- (g . c) >= 1
- (f . c)
by XREAL_1:10;
then
(1 - (f . c)) * (1 - (f . c)) <= (1 - (g . c)) * (1 - (f . c))
by A6, XREAL_1:64;
then
(1 - (f . c)) * (1 - (f . c)) <= (1 - (g . c)) * (1 - (h . c))
by A5, XXREAL_0:2;
then
1
- ((1 - (f . c)) * (1 - (f . c))) >= 1
- ((1 - (g . c)) * (1 - (h . c)))
by XREAL_1:10;
hence
max (
(f . c),
(1 - ((1 - (g . c)) * (1 - (h . c)))))
<= ((max ((f . c),(g . c))) + (max ((f . c),(h . c)))) - ((max ((f . c),(g . c))) * (max ((f . c),(h . c))))
by A3, A7, XXREAL_0:28;
verum end; suppose A8:
(
max (
(f . c),
(g . c))
= f . c &
max (
(f . c),
(h . c))
= h . c )
;
max ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= ((max ((f . c),(g . c))) + (max ((f . c),(h . c)))) - ((max ((f . c),(g . c))) * (max ((f . c),(h . c))))
(1_minus f) . c >= 0
by Th1;
then A9:
1
- (f . c) >= 0
by FUZZY_1:def 5;
h . c >= 0
by Th1;
then
0 * (h . c) <= (h . c) * (1 - (f . c))
by A9, XREAL_1:64;
then A10:
0 + (f . c) <= ((h . c) * (1 - (f . c))) + (f . c)
by XREAL_1:6;
(1_minus h) . c >= 0
by Th1;
then A11:
1
- (h . c) >= 0
by FUZZY_1:def 5;
g . c <= f . c
by A8, XXREAL_0:def 10;
then
1
- (f . c) <= 1
- (g . c)
by XREAL_1:10;
then
(1 - (f . c)) * (1 - (h . c)) <= (1 - (g . c)) * (1 - (h . c))
by A11, XREAL_1:64;
then
1
- ((1 - (f . c)) * (1 - (h . c))) >= 1
- ((1 - (g . c)) * (1 - (h . c)))
by XREAL_1:10;
hence
max (
(f . c),
(1 - ((1 - (g . c)) * (1 - (h . c)))))
<= ((max ((f . c),(g . c))) + (max ((f . c),(h . c)))) - ((max ((f . c),(g . c))) * (max ((f . c),(h . c))))
by A8, A10, XXREAL_0:28;
verum end; suppose A12:
(
max (
(f . c),
(g . c))
= g . c &
max (
(f . c),
(h . c))
= f . c )
;
max ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= ((max ((f . c),(g . c))) + (max ((f . c),(h . c)))) - ((max ((f . c),(g . c))) * (max ((f . c),(h . c))))
(1_minus f) . c >= 0
by Th1;
then A13:
1
- (f . c) >= 0
by FUZZY_1:def 5;
g . c >= 0
by Th1;
then
0 * (g . c) <= (g . c) * (1 - (f . c))
by A13, XREAL_1:64;
then A14:
0 + (f . c) <= ((g . c) * (1 - (f . c))) + (f . c)
by XREAL_1:6;
(1_minus g) . c >= 0
by Th1;
then A15:
1
- (g . c) >= 0
by FUZZY_1:def 5;
h . c <= f . c
by A12, XXREAL_0:def 10;
then
1
- (f . c) <= 1
- (h . c)
by XREAL_1:10;
then
(1 - (f . c)) * (1 - (g . c)) <= (1 - (h . c)) * (1 - (g . c))
by A15, XREAL_1:64;
then
1
- ((1 - (f . c)) * (1 - (g . c))) >= 1
- ((1 - (h . c)) * (1 - (g . c)))
by XREAL_1:10;
hence
max (
(f . c),
(1 - ((1 - (g . c)) * (1 - (h . c)))))
<= ((max ((f . c),(g . c))) + (max ((f . c),(h . c)))) - ((max ((f . c),(g . c))) * (max ((f . c),(h . c))))
by A12, A14, XXREAL_0:28;
verum end; suppose A16:
(
max (
(f . c),
(g . c))
= g . c &
max (
(f . c),
(h . c))
= h . c )
;
max ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c))))) <= ((max ((f . c),(g . c))) + (max ((f . c),(h . c)))) - ((max ((f . c),(g . c))) * (max ((f . c),(h . c))))
(1_minus g) . c >= 0
by Th1;
then A17:
1
- (g . c) >= 0
by FUZZY_1:def 5;
h . c >= f . c
by A16, XXREAL_0:def 10;
then
1
- (h . c) <= 1
- (f . c)
by XREAL_1:10;
then A18:
(1 - (g . c)) * (1 - (f . c)) >= (1 - (g . c)) * (1 - (h . c))
by A17, XREAL_1:64;
(1_minus f) . c >= 0
by Th1;
then A19:
1
- (f . c) >= 0
by FUZZY_1:def 5;
g . c >= f . c
by A16, XXREAL_0:def 10;
then
1
- (g . c) <= 1
- (f . c)
by XREAL_1:10;
then
(1 - (f . c)) * (1 - (f . c)) >= (1 - (g . c)) * (1 - (f . c))
by A19, XREAL_1:64;
then
(1 - (f . c)) * (1 - (f . c)) >= (1 - (g . c)) * (1 - (h . c))
by A18, XXREAL_0:2;
then
1
- ((1 - (f . c)) * (1 - (f . c))) <= 1
- ((1 - (g . c)) * (1 - (h . c)))
by XREAL_1:10;
then A20:
(f ++ f) . c <= 1
- ((1 - (g . c)) * (1 - (h . c)))
by Th49;
f ++ f c=
by Th28;
then
(f ++ f) . c >= f . c
;
then
f . c <= 1
- ((1 - (g . c)) * (1 - (h . c)))
by A20, XXREAL_0:2;
hence
max (
(f . c),
(1 - ((1 - (g . c)) * (1 - (h . c)))))
<= ((max ((f . c),(g . c))) + (max ((f . c),(h . c)))) - ((max ((f . c),(g . c))) * (max ((f . c),(h . c))))
by A16, XXREAL_0:28;
verum end; end;
end;
(max (f,(g ++ h))) . c =
max ((f . c),((g ++ h) . c))
by FUZZY_1:5
.=
max ((f . c),(1 - ((1 - (g . c)) * (1 - (h . c)))))
by Th49
;
hence
(max (f,(g ++ h))) . c <= ((max (f,g)) ++ (max (f,h))) . c
by A1, A2; verum