fuzzy_1.miz
begin
reserve x,y,y1,y2 for
set;
reserve C for non
empty
set;
reserve c for
Element of C;
registration
let x, y;
cluster (
chi (x,y)) ->
[.
0 , 1.]
-valued;
coherence
proof
1
in
[.
0 , 1.] &
0
in
[.
0 , 1.] by
XXREAL_1: 1;
then (
rng (
chi (x,y)))
c=
{
0 , 1} &
{
0 , 1}
c=
[.
0 , 1.] by
FUNCT_3: 39,
ZFMISC_1: 32;
hence (
rng (
chi (x,y)))
c=
[.
0 , 1.] by
XBOOLE_1: 1;
end;
end
registration
let C;
cluster
[.
0 , 1.]
-valued for
Function of C,
REAL ;
existence
proof
take (
chi (C,C));
thus (
rng (
chi (C,C)))
c=
[.
0 , 1.] by
RELAT_1:def 19;
end;
end
definition
let C;
mode
Membership_Func of C is
[.
0 , 1.]
-valued
Function of C,
REAL ;
end
theorem ::
FUZZY_1:1
(
chi (C,C)) is
Membership_Func of C;
reserve f,h,g,h1 for
Membership_Func of C;
registration
let X be non
empty
set;
cluster ->
real-valued for
Membership_Func of X;
coherence ;
end
definition
let f,g be
real-valued
Function;
::
FUZZY_1:def1
pred f
is_less_than g means (
dom f)
c= (
dom g) & for x be
set st x
in (
dom f) holds (f
. x)
<= (g
. x);
reflexivity ;
end
notation
let X be non
empty
set;
let f,g be
Membership_Func of X;
synonym f
c= g for f
is_less_than g;
end
definition
let X be non
empty
set;
let f,g be
Membership_Func of X;
:: original:
is_less_than
redefine
::
FUZZY_1:def2
pred f
is_less_than g means
:
Def2: for x be
Element of X holds (f
. x)
<= (g
. x);
compatibility
proof
thus f
is_less_than g iff for x be
Element of X holds (f
. x)
<= (g
. x)
proof
hereby
assume
A1: f
is_less_than g;
thus for x be
Element of X holds (f
. x)
<= (g
. x)
proof
let x be
Element of X;
(
dom f)
= X by
FUNCT_2:def 1;
hence thesis by
A1;
end;
end;
assume for x be
Element of X holds (f
. x)
<= (g
. x);
then (
dom g)
= X & for x be
set st x
in (
dom f) holds (f
. x)
<= (g
. x) by
FUNCT_2:def 1;
hence thesis;
end;
end;
end
Lm1: f
c= g & g
c= f implies f
= g
proof
set A = f, B = g;
assume
A1: A
c= B & B
c= A;
A2: for c be
Element of C st c
in C holds (f
. c)
= (g
. c)
proof
let c be
Element of C;
(f
. c)
<= (g
. c) & (g
. c)
<= (f
. c) by
A1;
hence thesis by
XXREAL_0: 1;
end;
C
= (
dom f) & C
= (
dom g) by
FUNCT_2:def 1;
hence thesis by
A2,
PARTFUN1: 5;
end;
theorem ::
FUZZY_1:2
f
= g iff f
c= g & g
c= f by
Lm1;
theorem ::
FUZZY_1:3
f
c= f;
theorem ::
FUZZY_1:4
f
c= g & g
c= h implies g
c= h;
begin
reconsider jj = 1 as
Element of
REAL by
XREAL_0:def 1;
definition
let C be non
empty
set;
let h,g be
Membership_Func of C;
::
FUZZY_1:def3
func
min (h,g) ->
Membership_Func of C means
:
Def3: for c be
Element of C holds (it
. c)
= (
min ((h
. c),(g
. c)));
existence
proof
defpred
P[
object,
object] means $2
= (
min ((h
. $1),(g
. $1)));
A1: for x,y1,y2 be
object st x
in C &
P[x, y1] &
P[x, y2] holds y1
= y2;
A2: for x,y be
object st x
in C &
P[x, y] holds y
in
REAL by
XREAL_0:def 1;
consider IT be
PartFunc of C,
REAL such that
A3: (for x be
object holds x
in (
dom IT) iff x
in C & ex y be
object st
P[x, y]) & for x be
object st x
in (
dom IT) holds
P[x, (IT
. x)] from
PARTFUN1:sch 2(
A2,
A1);
for x be
object st x
in C holds x
in (
dom IT)
proof
let x be
object;
(
min ((h
. x),(g
. x))) is
set by
TARSKI: 1;
hence thesis by
A3;
end;
then C
c= (
dom IT) by
TARSKI:def 3;
then
A5: (
dom IT)
= C by
XBOOLE_0:def 10;
then
A6: for c be
Element of C holds (IT
. c)
= (
min ((h
. c),(g
. c))) by
A3;
A7: (
rng h)
c=
[.
0 , 1.] by
RELAT_1:def 19;
A8: (
rng g)
c=
[.
0 , 1.] by
RELAT_1:def 19;
for y be
object st y
in (
rng IT) holds y
in
[.
0 , 1.]
proof
reconsider A =
[.
0 , jj.] as non
empty
closed_interval
Subset of
REAL by
MEASURE5: 14;
let y be
object;
assume y
in (
rng IT);
then
consider x be
Element of C such that
A9: x
in (
dom IT) and
A10: y
= (IT
. x) by
PARTFUN1: 3;
A11: (h
. x)
>= (
min ((h
. x),(g
. x))) by
XXREAL_0: 17;
A12: A
=
[.(
lower_bound A), (
upper_bound A).] by
INTEGRA1: 4;
then
A13:
0
= (
lower_bound A) by
INTEGRA1: 5;
A14: x
in C;
then x
in (
dom h) by
FUNCT_2:def 1;
then
A15: (h
. x)
in (
rng h) by
FUNCT_1:def 3;
A16: 1
= (
upper_bound A) by
A12,
INTEGRA1: 5;
then (h
. x)
<= 1 by
A7,
A15,
INTEGRA2: 1;
then (
min ((h
. x),(g
. x)))
<= 1 by
A11,
XXREAL_0: 2;
then
A17: (IT
. x)
<= 1 by
A3,
A9;
x
in (
dom g) by
A14,
FUNCT_2:def 1;
then (g
. x)
in (
rng g) by
FUNCT_1:def 3;
then
A18:
0
<= (g
. x) by
A8,
A13,
INTEGRA2: 1;
0
<= (h
. x) by
A7,
A13,
A15,
INTEGRA2: 1;
then
0
<= (
min ((h
. x),(g
. x))) by
A18,
XXREAL_0: 20;
then
0
<= (IT
. x) by
A3,
A9;
hence thesis by
A10,
A13,
A16,
A17,
INTEGRA2: 1;
end;
then
A19: (
rng IT)
c=
[.
0 , 1.] by
TARSKI:def 3;
IT is
total by
A5,
PARTFUN1:def 2;
then IT is
Membership_Func of C by
A19,
RELAT_1:def 19;
hence thesis by
A6;
end;
uniqueness
proof
let F,G be
Membership_Func of C;
assume that
A20: for c be
Element of C holds (F
. c)
= (
min ((h
. c),(g
. c))) and
A21: for c be
Element of C holds (G
. c)
= (
min ((h
. c),(g
. c)));
A22: for c be
Element of C st c
in C holds (F
. c)
= (G
. c)
proof
let c be
Element of C;
(F
. c)
= (
min ((h
. c),(g
. c))) by
A20;
hence thesis by
A21;
end;
C
= (
dom F) & C
= (
dom G) by
FUNCT_2:def 1;
hence thesis by
A22,
PARTFUN1: 5;
end;
idempotence ;
commutativity ;
end
definition
let C be non
empty
set;
let h,g be
Membership_Func of C;
::
FUZZY_1:def4
func
max (h,g) ->
Membership_Func of C means
:
Def4: for c be
Element of C holds (it
. c)
= (
max ((h
. c),(g
. c)));
existence
proof
defpred
P[
object,
object] means $2
= (
max ((h
. $1),(g
. $1)));
A1: for x,y1,y2 be
object st x
in C &
P[x, y1] &
P[x, y2] holds y1
= y2;
A2: for x,y be
object st x
in C &
P[x, y] holds y
in
REAL by
XREAL_0:def 1;
consider IT be
PartFunc of C,
REAL such that
A3: (for x be
object holds x
in (
dom IT) iff x
in C & ex y be
object st
P[x, y]) & for x be
object st x
in (
dom IT) holds
P[x, (IT
. x)] from
PARTFUN1:sch 2(
A2,
A1);
for x be
object st x
in C holds x
in (
dom IT)
proof
let x be
object;
(
max ((h
. x),(g
. x))) is
set by
TARSKI: 1;
hence thesis by
A3;
end;
then C
c= (
dom IT) by
TARSKI:def 3;
then
A5: (
dom IT)
= C by
XBOOLE_0:def 10;
then
A6: for c be
Element of C holds (IT
. c)
= (
max ((h
. c),(g
. c))) by
A3;
A7: (
rng h)
c=
[.
0 , 1.] by
RELAT_1:def 19;
A8: (
rng g)
c=
[.
0 , 1.] by
RELAT_1:def 19;
for y be
object st y
in (
rng IT) holds y
in
[.
0 , 1.]
proof
reconsider A =
[.
0 , jj.] as non
empty
closed_interval
Subset of
REAL by
MEASURE5: 14;
let y be
object;
assume y
in (
rng IT);
then
consider x be
Element of C such that
A9: x
in (
dom IT) and
A10: y
= (IT
. x) by
PARTFUN1: 3;
A11: A
=
[.(
lower_bound A), (
upper_bound A).] by
INTEGRA1: 4;
then
A12:
0
= (
lower_bound A) by
INTEGRA1: 5;
A13: x
in C;
then x
in (
dom h) by
FUNCT_2:def 1;
then
A14: (h
. x)
in (
rng h) by
FUNCT_1:def 3;
then
0
<= (h
. x) by
A7,
A12,
INTEGRA2: 1;
then
0
<= (
max ((h
. x),(g
. x))) by
XXREAL_0: 30;
then
A15:
0
<= (IT
. x) by
A3,
A9;
A16: 1
= (
upper_bound A) by
A11,
INTEGRA1: 5;
x
in (
dom g) by
A13,
FUNCT_2:def 1;
then (g
. x)
in (
rng g) by
FUNCT_1:def 3;
then
A17: (g
. x)
<= 1 by
A8,
A16,
INTEGRA2: 1;
(h
. x)
<= 1 by
A7,
A16,
A14,
INTEGRA2: 1;
then (
max ((h
. x),(g
. x)))
<= 1 by
A17,
XXREAL_0: 28;
then (IT
. x)
<= 1 by
A3,
A9;
hence thesis by
A10,
A12,
A16,
A15,
INTEGRA2: 1;
end;
then
A18: (
rng IT)
c=
[.
0 , 1.] by
TARSKI:def 3;
IT is
total by
A5,
PARTFUN1:def 2;
then IT is
Membership_Func of C by
A18,
RELAT_1:def 19;
hence thesis by
A6;
end;
uniqueness
proof
let F,G be
Membership_Func of C;
assume that
A19: for c be
Element of C holds (F
. c)
= (
max ((h
. c),(g
. c))) and
A20: for c be
Element of C holds (G
. c)
= (
max ((h
. c),(g
. c)));
A21: for c be
Element of C st c
in C holds (F
. c)
= (G
. c)
proof
let c be
Element of C;
(F
. c)
= (
max ((h
. c),(g
. c))) by
A19;
hence thesis by
A20;
end;
C
= (
dom F) & C
= (
dom G) by
FUNCT_2:def 1;
hence thesis by
A21,
PARTFUN1: 5;
end;
idempotence ;
commutativity ;
end
definition
let C be non
empty
set;
let h be
Membership_Func of C;
::
FUZZY_1:def5
func
1_minus h ->
Membership_Func of C means
:
Def5: for c be
Element of C holds (it
. c)
= (1
- (h
. c));
existence
proof
deffunc
F(
set) = (
In ((1
- (h
. $1)),
REAL ));
defpred
P[
set] means $1
in (
dom h);
consider IT be
PartFunc of C,
REAL such that
A1: (for x be
Element of C holds x
in (
dom IT) iff
P[x]) & for x be
Element of C st x
in (
dom IT) holds (IT
. x)
=
F(x) from
SEQ_1:sch 3;
for x be
object st x
in C holds x
in (
dom IT)
proof
let x be
object;
A2: (
dom h)
= C by
FUNCT_2:def 1;
assume x
in C;
hence thesis by
A1,
A2;
end;
then C
c= (
dom IT) by
TARSKI:def 3;
then
A3: (
dom IT)
= C by
XBOOLE_0:def 10;
then
A4: for c be
Element of C holds (IT
. c)
=
F(c) by
A1;
A5: (
rng h)
c=
[.
0 , 1.] by
RELAT_1:def 19;
for y be
object st y
in (
rng IT) holds y
in
[.
0 , 1.]
proof
reconsider A =
[.
0 , jj.] as non
empty
closed_interval
Subset of
REAL by
MEASURE5: 14;
let y be
object;
assume y
in (
rng IT);
then
consider x be
Element of C such that
A6: x
in (
dom IT) and
A7: y
= (IT
. x) by
PARTFUN1: 3;
A8: A
=
[.(
lower_bound A), (
upper_bound A).] by
INTEGRA1: 4;
then
A9:
0
= (
lower_bound A) by
INTEGRA1: 5;
x
in C;
then x
in (
dom h) by
FUNCT_2:def 1;
then
A10: (h
. x)
in (
rng h) by
FUNCT_1:def 3;
then
0
<= (h
. x) by
A5,
A9,
INTEGRA2: 1;
then (
0
+ 1)
<= (1
+ (h
. x)) by
XREAL_1: 6;
then
F(x)
<= 1 by
XREAL_1: 20;
then
A11: (IT
. x)
<= 1 by
A1,
A6;
A12: 1
= (
upper_bound A) by
A8,
INTEGRA1: 5;
then (h
. x)
<= 1 by
A5,
A10,
INTEGRA2: 1;
then
0
<=
F(x) by
XREAL_1: 48;
then
0
<= (IT
. x) by
A1,
A6;
hence thesis by
A7,
A9,
A12,
A11,
INTEGRA2: 1;
end;
then
A13: (
rng IT)
c=
[.
0 , 1.] by
TARSKI:def 3;
IT is
total by
A3,
PARTFUN1:def 2;
then
reconsider IT as
Membership_Func of C by
A13,
RELAT_1:def 19;
take IT;
let c be
Element of C;
(IT
. c)
=
F(c) by
A4;
hence thesis;
end;
uniqueness
proof
let F,G be
Membership_Func of C;
assume that
A14: for c be
Element of C holds (F
. c)
= (1
- (h
. c)) and
A15: for c be
Element of C holds (G
. c)
= (1
- (h
. c));
A16: for c be
Element of C st c
in C holds (F
. c)
= (G
. c)
proof
let c be
Element of C;
(F
. c)
= (1
- (h
. c)) by
A14;
hence thesis by
A15;
end;
C
= (
dom F) & C
= (
dom G) by
FUNCT_2:def 1;
hence thesis by
A16,
PARTFUN1: 5;
end;
involutiveness
proof
let h1,h2 be
Membership_Func of C;
assume
A17: for c be
Element of C holds (h1
. c)
= (1
- (h2
. c));
let c be
Element of C;
thus (h2
. c)
= (1
- (1
- (h2
. c)))
.= (1
- (h1
. c)) by
A17;
end;
end
theorem ::
FUZZY_1:5
(
min ((h
. c),(g
. c)))
= ((
min (h,g))
. c) & (
max ((h
. c),(g
. c)))
= ((
max (h,g))
. c) by
Def3,
Def4;
theorem ::
FUZZY_1:6
(
max (h,h))
= h & (
min (h,h))
= h & (
max (h,h))
= (
min (h,h)) & (
min (f,g))
= (
min (g,f)) & (
max (f,g))
= (
max (g,f));
theorem ::
FUZZY_1:7
Th7: (
max ((
max (f,g)),h))
= (
max (f,(
max (g,h)))) & (
min ((
min (f,g)),h))
= (
min (f,(
min (g,h))))
proof
A1: C
= (
dom (
min ((
min (f,g)),h))) & C
= (
dom (
min (f,(
min (g,h))))) by
FUNCT_2:def 1;
A2: for x be
Element of C st x
in C holds ((
max ((
max (f,g)),h))
. x)
= ((
max (f,(
max (g,h))))
. x)
proof
let x be
Element of C;
((
max ((
max (f,g)),h))
. x)
= (
max (((
max (f,g))
. x),(h
. x))) by
Def4
.= (
max ((
max ((f
. x),(g
. x))),(h
. x))) by
Def4
.= (
max ((f
. x),(
max ((g
. x),(h
. x))))) by
XXREAL_0: 34
.= (
max ((f
. x),((
max (g,h))
. x))) by
Def4
.= ((
max (f,(
max (g,h))))
. x) by
Def4;
hence thesis;
end;
A3: for x be
Element of C st x
in C holds ((
min ((
min (f,g)),h))
. x)
= ((
min (f,(
min (g,h))))
. x)
proof
let x be
Element of C;
((
min ((
min (f,g)),h))
. x)
= (
min (((
min (f,g))
. x),(h
. x))) by
Def3
.= (
min ((
min ((f
. x),(g
. x))),(h
. x))) by
Def3
.= (
min ((f
. x),(
min ((g
. x),(h
. x))))) by
XXREAL_0: 33
.= (
min ((f
. x),((
min (g,h))
. x))) by
Def3
.= ((
min (f,(
min (g,h))))
. x) by
Def3;
hence thesis;
end;
C
= (
dom (
max ((
max (f,g)),h))) & C
= (
dom (
max (f,(
max (g,h))))) by
FUNCT_2:def 1;
hence thesis by
A1,
A2,
A3,
PARTFUN1: 5;
end;
theorem ::
FUZZY_1:8
Th8: (
max (f,(
min (f,g))))
= f & (
min (f,(
max (f,g))))
= f
proof
A1: C
= (
dom (
min (f,(
max (f,g))))) by
FUNCT_2:def 1;
A2: for x be
Element of C st x
in C holds ((
max (f,(
min (f,g))))
. x)
= (f
. x)
proof
let x be
Element of C;
((
max (f,(
min (f,g))))
. x)
= (
max ((f
. x),((
min (f,g))
. x))) by
Def4
.= (
max ((f
. x),(
min ((f
. x),(g
. x))))) by
Def3
.= (f
. x) by
XXREAL_0: 36;
hence thesis;
end;
A3: for x be
Element of C st x
in C holds ((
min (f,(
max (f,g))))
. x)
= (f
. x)
proof
let x be
Element of C;
((
min (f,(
max (f,g))))
. x)
= (
min ((f
. x),((
max (f,g))
. x))) by
Def3
.= (
min ((f
. x),(
max ((f
. x),(g
. x))))) by
Def4
.= (f
. x) by
XXREAL_0: 35;
hence thesis;
end;
C
= (
dom (
max (f,(
min (f,g))))) & C
= (
dom f) by
FUNCT_2:def 1;
hence thesis by
A1,
A2,
A3,
PARTFUN1: 5;
end;
theorem ::
FUZZY_1:9
Th9: (
min (f,(
max (g,h))))
= (
max ((
min (f,g)),(
min (f,h)))) & (
max (f,(
min (g,h))))
= (
min ((
max (f,g)),(
max (f,h))))
proof
A1: C
= (
dom (
max (f,(
min (g,h))))) & C
= (
dom (
min ((
max (f,g)),(
max (f,h))))) by
FUNCT_2:def 1;
A2: for x be
Element of C st x
in C holds ((
min (f,(
max (g,h))))
. x)
= ((
max ((
min (f,g)),(
min (f,h))))
. x)
proof
let x be
Element of C;
((
min (f,(
max (g,h))))
. x)
= (
min ((f
. x),((
max (g,h))
. x))) by
Def3
.= (
min ((f
. x),(
max ((g
. x),(h
. x))))) by
Def4
.= (
max ((
min ((f
. x),(g
. x))),(
min ((f
. x),(h
. x))))) by
XXREAL_0: 38
.= (
max (((
min (f,g))
. x),(
min ((f
. x),(h
. x))))) by
Def3
.= (
max (((
min (f,g))
. x),((
min (f,h))
. x))) by
Def3
.= ((
max ((
min (f,g)),(
min (f,h))))
. x) by
Def4;
hence thesis;
end;
A3: for x be
Element of C st x
in C holds ((
max (f,(
min (g,h))))
. x)
= ((
min ((
max (f,g)),(
max (f,h))))
. x)
proof
let x be
Element of C;
((
max (f,(
min (g,h))))
. x)
= (
max ((f
. x),((
min (g,h))
. x))) by
Def4
.= (
max ((f
. x),(
min ((g
. x),(h
. x))))) by
Def3
.= (
min ((
max ((f
. x),(g
. x))),(
max ((f
. x),(h
. x))))) by
XXREAL_0: 39
.= (
min (((
max (f,g))
. x),(
max ((f
. x),(h
. x))))) by
Def4
.= (
min (((
max (f,g))
. x),((
max (f,h))
. x))) by
Def4
.= ((
min ((
max (f,g)),(
max (f,h))))
. x) by
Def3;
hence thesis;
end;
C
= (
dom (
min (f,(
max (g,h))))) & C
= (
dom (
max ((
min (f,g)),(
min (f,h))))) by
FUNCT_2:def 1;
hence thesis by
A1,
A2,
A3,
PARTFUN1: 5;
end;
::$Canceled
theorem ::
FUZZY_1:11
Th10: (
1_minus (
max (f,g)))
= (
min ((
1_minus f),(
1_minus g))) & (
1_minus (
min (f,g)))
= (
max ((
1_minus f),(
1_minus g)))
proof
A1: C
= (
dom (
1_minus (
min (f,g)))) & C
= (
dom (
max ((
1_minus f),(
1_minus g)))) by
FUNCT_2:def 1;
A2: for x be
Element of C st x
in C holds ((
1_minus (
max (f,g)))
. x)
= ((
min ((
1_minus f),(
1_minus g)))
. x)
proof
let x be
Element of C;
A3: ((
1_minus (
max (f,g)))
. x)
= (1
- ((
max (f,g))
. x)) by
Def5
.= (1
- (
max ((f
. x),(g
. x)))) by
Def4
.= (1
- ((((f
. x)
+ (g
. x))
+
|.((f
. x)
- (g
. x)).|)
/ 2)) by
COMPLEX1: 74;
((
min ((
1_minus f),(
1_minus g)))
. x)
= (
min (((
1_minus f)
. x),((
1_minus g)
. x))) by
Def3
.= (
min ((1
- (f
. x)),((
1_minus g)
. x))) by
Def5
.= (
min ((1
- (f
. x)),(1
- (g
. x)))) by
Def5
.= ((((1
- (f
. x))
+ (1
- (g
. x)))
-
|.((1
- (f
. x))
- (1
- (g
. x))).|)
/ 2) by
COMPLEX1: 73
.= ((((2
- (f
. x))
- (g
. x))
-
|.(
- ((f
. x)
- (g
. x))).|)
/ 2)
.= (((2
- ((f
. x)
+ (g
. x)))
-
|.((f
. x)
- (g
. x)).|)
/ 2) by
COMPLEX1: 52
.= (1
- ((((f
. x)
+ (g
. x))
+
|.((f
. x)
- (g
. x)).|)
/ 2));
hence thesis by
A3;
end;
A4: for x be
Element of C st x
in C holds ((
1_minus (
min (f,g)))
. x)
= ((
max ((
1_minus f),(
1_minus g)))
. x)
proof
let x be
Element of C;
A5: ((
1_minus (
min (f,g)))
. x)
= (1
- ((
min (f,g))
. x)) by
Def5
.= (1
- (
min ((f
. x),(g
. x)))) by
Def3
.= (1
- ((((f
. x)
+ (g
. x))
-
|.((f
. x)
- (g
. x)).|)
/ 2)) by
COMPLEX1: 73;
((
max ((
1_minus f),(
1_minus g)))
. x)
= (
max (((
1_minus f)
. x),((
1_minus g)
. x))) by
Def4
.= (
max ((1
- (f
. x)),((
1_minus g)
. x))) by
Def5
.= (
max ((1
- (f
. x)),(1
- (g
. x)))) by
Def5
.= ((((1
- (f
. x))
+ (1
- (g
. x)))
+
|.((1
- (f
. x))
- (1
- (g
. x))).|)
/ 2) by
COMPLEX1: 74
.= ((((2
- (f
. x))
- (g
. x))
+
|.(
- ((f
. x)
- (g
. x))).|)
/ 2)
.= (((2
- ((f
. x)
+ (g
. x)))
+
|.((f
. x)
- (g
. x)).|)
/ 2) by
COMPLEX1: 52
.= (1
- ((((f
. x)
+ (g
. x))
-
|.((f
. x)
- (g
. x)).|)
/ 2));
hence thesis by
A5;
end;
C
= (
dom (
1_minus (
max (f,g)))) & C
= (
dom (
min ((
1_minus f),(
1_minus g)))) by
FUNCT_2:def 1;
hence thesis by
A1,
A2,
A4,
PARTFUN1: 5;
end;
begin
theorem ::
FUZZY_1:12
(
chi (
{} ,C)) is
Membership_Func of C;
definition
let C be non
empty
set;
::
FUZZY_1:def6
func
EMF (C) ->
Membership_Func of C equals (
chi (
{} ,C));
correctness ;
end
definition
let C be non
empty
set;
::
FUZZY_1:def7
func
UMF (C) ->
Membership_Func of C equals (
chi (C,C));
correctness ;
end
theorem ::
FUZZY_1:13
Th12: for a,b be
Element of
REAL , f be
PartFunc of C,
REAL st (
rng f)
c=
[.a, b.] & a
<= b holds for x be
Element of C st x
in (
dom f) holds a
<= (f
. x) & (f
. x)
<= b
proof
let a,b be
Element of
REAL ;
let f be
PartFunc of C,
REAL ;
assume that
A1: (
rng f)
c=
[.a, b.] and
A2: a
<= b;
for x be
Element of C st x
in (
dom f) holds a
<= (f
. x) & (f
. x)
<= b
proof
reconsider A =
[.a, b.] as non
empty
closed_interval
Subset of
REAL by
A2,
MEASURE5: 14;
let x be
Element of C;
A
=
[.(
lower_bound A), (
upper_bound A).] by
INTEGRA1: 4;
then
A3: a
= (
lower_bound A) & b
= (
upper_bound A) by
INTEGRA1: 5;
assume x
in (
dom f);
then (f
. x)
in (
rng f) by
FUNCT_1:def 3;
hence thesis by
A1,
A3,
INTEGRA2: 1;
end;
hence thesis;
end;
theorem ::
FUZZY_1:14
Th13: (
EMF C)
c= f
proof
let x be
Element of C;
A1: (
rng f)
c=
[.
0 , jj.] by
RELAT_1:def 19;
(
dom f)
= C & ((
EMF C)
. x)
=
0 by
FUNCT_2:def 1,
FUNCT_3:def 3;
hence thesis by
A1,
Th12;
end;
theorem ::
FUZZY_1:15
Th14: f
c= (
UMF C)
proof
let x be
Element of C;
A1:
0
in
REAL by
XREAL_0:def 1;
A2: (
rng f)
c=
[.
0 , 1.] by
RELAT_1:def 19;
(
dom f)
= C & ((
UMF C)
. x)
= 1 by
FUNCT_2:def 1,
FUNCT_3:def 3;
hence thesis by
A2,
Th12,
A1;
end;
theorem ::
FUZZY_1:16
Th15: for x be
Element of C, h be
Membership_Func of C holds ((
EMF C)
. x)
<= (h
. x) & (h
. x)
<= ((
UMF C)
. x) by
Th13,
Th14,
Def2;
theorem ::
FUZZY_1:17
Th16: (
min (f,g))
c= f & f
c= (
max (f,g))
proof
thus (
min (f,g))
c= f
proof
let x be
Element of C;
((
min (f,g))
. x)
= (
min ((f
. x),(g
. x))) by
Def3;
hence thesis by
XXREAL_0: 17;
end;
let x be
Element of C;
((
max (f,g))
. x)
= (
max ((f
. x),(g
. x))) by
Def4;
hence thesis by
XXREAL_0: 25;
end;
theorem ::
FUZZY_1:18
Th17: (
max (f,(
UMF C)))
= (
UMF C) & (
min (f,(
UMF C)))
= f & (
max (f,(
EMF C)))
= f & (
min (f,(
EMF C)))
= (
EMF C)
proof
A1: C
= (
dom (
max (f,(
EMF C)))) & C
= (
dom (
min (f,(
EMF C)))) by
FUNCT_2:def 1;
A2: for x be
Element of C st x
in C holds ((
min (f,(
UMF C)))
. x)
= (f
. x)
proof
let x be
Element of C;
A3: (f
. x)
<= ((
UMF C)
. x) by
Th15;
((
min (f,(
UMF C)))
. x)
= (
min ((f
. x),((
UMF C)
. x))) by
Def3
.= (f
. x) by
A3,
XXREAL_0:def 9;
hence thesis;
end;
A4: for x be
Element of C st x
in C holds ((
min (f,(
EMF C)))
. x)
= ((
EMF C)
. x)
proof
let x be
Element of C;
A5: ((
EMF C)
. x)
<= (f
. x) by
Th15;
((
min (f,(
EMF C)))
. x)
= (
min ((f
. x),((
EMF C)
. x))) by
Def3
.= ((
EMF C)
. x) by
A5,
XXREAL_0:def 9;
hence thesis;
end;
A6: for x be
Element of C st x
in C holds ((
max (f,(
EMF C)))
. x)
= (f
. x)
proof
let x be
Element of C;
A7: ((
EMF C)
. x)
<= (f
. x) by
Th15;
((
max (f,(
EMF C)))
. x)
= (
max ((f
. x),((
EMF C)
. x))) by
Def4
.= (f
. x) by
A7,
XXREAL_0:def 10;
hence thesis;
end;
(
max (f,(
UMF C)))
c= (
UMF C) & (
UMF C)
c= (
max (f,(
UMF C))) by
Th14,
Th16;
hence (
max (f,(
UMF C)))
= (
UMF C) by
Lm1;
A8: C
= (
dom (
EMF C)) by
FUNCT_2:def 1;
C
= (
dom (
min (f,(
UMF C)))) & C
= (
dom f) by
FUNCT_2:def 1;
hence thesis by
A2,
A6,
A1,
A8,
A4,
PARTFUN1: 5;
end;
theorem ::
FUZZY_1:19
Th18: f
c= h & g
c= h implies (
max (f,g))
c= h
proof
assume
A1: f
c= h & g
c= h;
let x be
Element of C;
A2: (
max ((f
. x),(g
. x)))
= ((
max (f,g))
. x) by
Def4;
(f
. x)
<= (h
. x) & (g
. x)
<= (h
. x) by
A1;
hence thesis by
A2,
XXREAL_0: 28;
end;
theorem ::
FUZZY_1:20
f
c= g implies (
max (f,h))
c= (
max (g,h))
proof
assume
A1: f
c= g;
let x be
Element of C;
(f
. x)
<= (g
. x) by
A1;
then (
max ((f
. x),(h
. x)))
<= (
max ((g
. x),(h
. x))) by
XXREAL_0: 26;
then (
max ((f
. x),(h
. x)))
<= ((
max (g,h))
. x) by
Def4;
hence thesis by
Def4;
end;
theorem ::
FUZZY_1:21
f
c= g & h
c= h1 implies (
max (f,h))
c= (
max (g,h1))
proof
assume
A1: f
c= g & h
c= h1;
let x be
Element of C;
(f
. x)
<= (g
. x) & (h
. x)
<= (h1
. x) by
A1;
then (
max ((f
. x),(h
. x)))
<= (
max ((g
. x),(h1
. x))) by
XXREAL_0: 26;
then ((
max (f,h))
. x)
<= (
max ((g
. x),(h1
. x))) by
Def4;
hence thesis by
Def4;
end;
theorem ::
FUZZY_1:22
f
c= g implies (
max (f,g))
= g
proof
assume f
c= g;
then
A1: (
max (f,g))
c= g by
Th18;
g
c= (
max (f,g)) by
Th16;
hence thesis by
A1,
Lm1;
end;
theorem ::
FUZZY_1:23
(
min (f,g))
c= (
max (f,g))
proof
let x be
Element of C;
(
min ((f
. x),(g
. x)))
<= (f
. x) & (f
. x)
<= (
max ((f
. x),(g
. x))) by
XXREAL_0: 17,
XXREAL_0: 25;
then (
min ((f
. x),(g
. x)))
<= (
max ((f
. x),(g
. x))) by
XXREAL_0: 2;
then (
min ((f
. x),(g
. x)))
<= ((
max (f,g))
. x) by
Def4;
hence thesis by
Def3;
end;
theorem ::
FUZZY_1:24
Th23: h
c= f & h
c= g implies h
c= (
min (f,g))
proof
assume
A1: h
c= f & h
c= g;
let x be
Element of C;
(h
. x)
<= (f
. x) & (h
. x)
<= (g
. x) by
A1;
then (h
. x)
<= (
min ((f
. x),(g
. x))) by
XXREAL_0: 20;
hence thesis by
Def3;
end;
theorem ::
FUZZY_1:25
f
c= g implies (
min (f,h))
c= (
min (g,h))
proof
assume
A1: f
c= g;
let x be
Element of C;
(f
. x)
<= (g
. x) by
A1;
then (
min ((f
. x),(h
. x)))
<= (
min ((g
. x),(h
. x))) by
XXREAL_0: 18;
then ((
min (f,h))
. x)
<= (
min ((g
. x),(h
. x))) by
Def3;
hence thesis by
Def3;
end;
theorem ::
FUZZY_1:26
f
c= g & h
c= h1 implies (
min (f,h))
c= (
min (g,h1))
proof
assume
A1: f
c= g & h
c= h1;
let x be
Element of C;
(f
. x)
<= (g
. x) & (h
. x)
<= (h1
. x) by
A1;
then (
min ((f
. x),(h
. x)))
<= (
min ((g
. x),(h1
. x))) by
XXREAL_0: 18;
then ((
min (f,h))
. x)
<= (
min ((g
. x),(h1
. x))) by
Def3;
hence thesis by
Def3;
end;
theorem ::
FUZZY_1:27
Th26: f
c= g implies (
min (f,g))
= f
proof
assume
A1: f
c= g;
A2: for x be
Element of C st x
in C holds ((
min (f,g))
. x)
= (f
. x)
proof
let x be
Element of C;
(f
. x)
<= (g
. x) by
A1;
then (f
. x)
= (
min ((f
. x),(g
. x))) by
XXREAL_0:def 9
.= ((
min (f,g))
. x) by
Def3;
hence thesis;
end;
C
= (
dom (
min (f,g))) & C
= (
dom f) by
FUNCT_2:def 1;
hence thesis by
A2,
PARTFUN1: 5;
end;
theorem ::
FUZZY_1:28
f
c= g & f
c= h & (
min (g,h))
= (
EMF C) implies f
= (
EMF C)
proof
assume that
A1: f
c= g & f
c= h and
A2: (
min (g,h))
= (
EMF C);
A3: for x be
Element of C st x
in C holds (f
. x)
= ((
EMF C)
. x)
proof
let x be
Element of C;
(f
. x)
<= (g
. x) & (f
. x)
<= (h
. x) by
A1;
then (f
. x)
<= (
min ((g
. x),(h
. x))) by
XXREAL_0: 20;
then
A4: (f
. x)
<= ((
min (g,h))
. x) by
Def3;
((
EMF C)
. x)
<= (f
. x) by
Th15;
hence thesis by
A2,
A4,
XXREAL_0: 1;
end;
C
= (
dom f) & C
= (
dom (
EMF C)) by
FUNCT_2:def 1;
hence thesis by
A3,
PARTFUN1: 5;
end;
theorem ::
FUZZY_1:29
(
max ((
min (f,g)),(
min (f,h))))
= f implies f
c= (
max (g,h))
proof
assume
A1: (
max ((
min (f,g)),(
min (f,h))))
= f;
let x be
Element of C;
((
max ((
min (f,g)),(
min (f,h))))
. x)
= (
max (((
min (f,g))
. x),((
min (f,h))
. x))) by
Def4
.= (
max (((
min (f,g))
. x),(
min ((f
. x),(h
. x))))) by
Def3
.= (
max ((
min ((f
. x),(g
. x))),(
min ((f
. x),(h
. x))))) by
Def3
.= (
min ((f
. x),(
max ((g
. x),(h
. x))))) by
XXREAL_0: 38;
then (f
. x)
<= (
max ((g
. x),(h
. x))) by
A1,
XXREAL_0:def 9;
hence thesis by
Def4;
end;
theorem ::
FUZZY_1:30
f
c= g & (
min (g,h))
= (
EMF C) implies (
min (f,h))
= (
EMF C)
proof
assume that
A1: f
c= g and
A2: (
min (g,h))
= (
EMF C);
A3: for x be
Element of C st x
in C holds ((
min (f,h))
. x)
= ((
EMF C)
. x)
proof
let x be
Element of C;
(f
. x)
<= (g
. x) by
A1;
then (
min ((f
. x),(h
. x)))
<= (
min ((g
. x),(h
. x))) by
XXREAL_0: 18;
then (
min ((f
. x),(h
. x)))
<= ((
min (g,h))
. x) by
Def3;
then
A4: ((
min (f,h))
. x)
<= ((
min (g,h))
. x) by
Def3;
((
EMF C)
. x)
<= ((
min (f,h))
. x) by
Th15;
hence thesis by
A2,
A4,
XXREAL_0: 1;
end;
C
= (
dom (
min (f,h))) & C
= (
dom (
EMF C)) by
FUNCT_2:def 1;
hence thesis by
A3,
PARTFUN1: 5;
end;
theorem ::
FUZZY_1:31
f
c= (
EMF C) implies f
= (
EMF C)
proof
(
EMF C)
c= f by
Th13;
hence thesis by
Lm1;
end;
theorem ::
FUZZY_1:32
(
max (f,g))
= (
EMF C) iff f
= (
EMF C) & g
= (
EMF C)
proof
thus (
max (f,g))
= (
EMF C) implies f
= (
EMF C) & g
= (
EMF C)
proof
assume
A1: (
max (f,g))
= (
EMF C);
A2: for x be
Element of C st x
in C holds (f
. x)
= ((
EMF C)
. x)
proof
let x be
Element of C;
(
max ((f
. x),(g
. x)))
= ((
EMF C)
. x) by
A1,
Def4;
then
A3: (f
. x)
<= ((
EMF C)
. x) by
XXREAL_0: 25;
((
EMF C)
. x)
<= (f
. x) by
Th15;
hence thesis by
A3,
XXREAL_0: 1;
end;
A4: for x be
Element of C st x
in C holds (g
. x)
= ((
EMF C)
. x)
proof
let x be
Element of C;
(
max ((f
. x),(g
. x)))
= ((
EMF C)
. x) by
A1,
Def4;
then
A5: (g
. x)
<= ((
EMF C)
. x) by
XXREAL_0: 25;
((
EMF C)
. x)
<= (g
. x) by
Th15;
hence thesis by
A5,
XXREAL_0: 1;
end;
C
= (
dom f) & C
= (
dom (
EMF C)) by
FUNCT_2:def 1;
hence f
= (
EMF C) by
A2,
PARTFUN1: 5;
C
= (
dom g) & C
= (
dom (
EMF C)) by
FUNCT_2:def 1;
hence g
= (
EMF C) by
A4,
PARTFUN1: 5;
end;
assume f
= (
EMF C) & g
= (
EMF C);
hence thesis;
end;
theorem ::
FUZZY_1:33
f
= (
max (g,h)) iff g
c= f & h
c= f & for h1 st g
c= h1 & h
c= h1 holds f
c= h1
proof
hereby
assume
A1: f
= (
max (g,h));
hence g
c= f & h
c= f by
Th16;
let h1;
assume
A2: g
c= h1 & h
c= h1;
thus f
c= h1
proof
let x be
Element of C;
(g
. x)
<= (h1
. x) & (h
. x)
<= (h1
. x) by
A2;
then (
max ((g
. x),(h
. x)))
<= (h1
. x) by
XXREAL_0: 28;
hence thesis by
A1,
Def4;
end;
end;
assume that
A3: g
c= f & h
c= f and
A4: for h1 st g
c= h1 & h
c= h1 holds f
c= h1;
g
c= (
max (g,h)) & h
c= (
max (g,h)) by
Th16;
then
A5: f
c= (
max (g,h)) by
A4;
(
max (g,h))
c= f by
A3,
Th18;
hence thesis by
A5,
Lm1;
end;
theorem ::
FUZZY_1:34
f
= (
min (g,h)) iff f
c= g & f
c= h & for h1 st h1
c= g & h1
c= h holds h1
c= f
proof
hereby
assume
A1: f
= (
min (g,h));
hence f
c= g & f
c= h by
Th16;
let h1;
assume
A2: h1
c= g & h1
c= h;
thus h1
c= f
proof
let x be
Element of C;
(h1
. x)
<= (g
. x) & (h1
. x)
<= (h
. x) by
A2;
then (
min ((g
. x),(h
. x)))
>= (h1
. x) by
XXREAL_0: 20;
hence thesis by
A1,
Def3;
end;
end;
assume that
A3: f
c= g & f
c= h and
A4: for h1 st h1
c= g & h1
c= h holds h1
c= f;
(
min (g,h))
c= g & (
min (g,h))
c= h by
Th16;
then
A5: (
min (g,h))
c= f by
A4;
f
c= (
min (g,h)) by
A3,
Th23;
hence thesis by
A5,
Lm1;
end;
theorem ::
FUZZY_1:35
f
c= (
max (g,h)) & (
min (f,h))
= (
EMF C) implies f
c= g
proof
assume that
A1: f
c= (
max (g,h)) and
A2: (
min (f,h))
= (
EMF C);
let x be
Element of C;
(
min (f,(
max (g,h))))
= f by
A1,
Th26;
then f
= (
max ((
min (f,g)),(
min (f,h)))) by
Th9
.= (
min (f,g)) by
A2,
Th17;
then (f
. x)
= (
min ((f
. x),(g
. x))) by
Def3;
hence thesis by
XXREAL_0:def 9;
end;
Lm2: f
c= g implies (
1_minus g)
c= (
1_minus f)
proof
assume
A1: f
c= g;
let x be
Element of C;
(f
. x)
<= (g
. x) by
A1;
then (1
- (g
. x))
<= (1
- (f
. x)) by
XREAL_1: 10;
then ((
1_minus g)
. x)
<= (1
- (f
. x)) by
Def5;
hence thesis by
Def5;
end;
theorem ::
FUZZY_1:36
Th35: f
c= g iff (
1_minus g)
c= (
1_minus f)
proof
(
1_minus (
1_minus f))
= f & (
1_minus (
1_minus g))
= g;
hence thesis by
Lm2;
end;
theorem ::
FUZZY_1:37
f
c= (
1_minus g) implies g
c= (
1_minus f)
proof
(
1_minus (
1_minus f))
= f;
hence thesis by
Th35;
end;
theorem ::
FUZZY_1:38
(
1_minus (
max (f,g)))
c= (
1_minus f) by
Th16,
Th35;
theorem ::
FUZZY_1:39
(
1_minus f)
c= (
1_minus (
min (f,g))) by
Th16,
Th35;
theorem ::
FUZZY_1:40
Th39: (
1_minus (
EMF C))
= (
UMF C) & (
1_minus (
UMF C))
= (
EMF C)
proof
A1: for x be
Element of C st x
in C holds ((
1_minus (
EMF C))
. x)
= ((
UMF C)
. x)
proof
let x be
Element of C;
((
1_minus (
EMF C))
. x)
= (1
- ((
EMF C)
. x)) by
Def5
.= (1
-
0 ) by
FUNCT_3:def 3
.= 1;
hence thesis by
FUNCT_3:def 3;
end;
C
= (
dom (
1_minus (
EMF C))) & C
= (
dom (
UMF C)) by
FUNCT_2:def 1;
hence (
1_minus (
EMF C))
= (
UMF C) by
A1,
PARTFUN1: 5;
A2: for x be
Element of C st x
in C holds ((
1_minus (
UMF C))
. x)
= ((
EMF C)
. x)
proof
let x be
Element of C;
((
1_minus (
UMF C))
. x)
= (1
- ((
UMF C)
. x)) by
Def5
.= (1
- 1) by
FUNCT_3:def 3
.=
0 ;
hence thesis by
FUNCT_3:def 3;
end;
C
= (
dom (
1_minus (
UMF C))) & C
= (
dom (
EMF C)) by
FUNCT_2:def 1;
hence thesis by
A2,
PARTFUN1: 5;
end;
definition
let C be non
empty
set;
let h,g be
Membership_Func of C;
::
FUZZY_1:def8
func h
\+\ g ->
Membership_Func of C equals (
max ((
min (h,(
1_minus g))),(
min ((
1_minus h),g))));
coherence ;
commutativity ;
end
theorem ::
FUZZY_1:41
(f
\+\ (
EMF C))
= f
proof
thus (f
\+\ (
EMF C))
= (
max ((
min (f,(
UMF C))),(
min ((
1_minus f),(
EMF C))))) by
Th39
.= (
max (f,(
min ((
1_minus f),(
EMF C))))) by
Th17
.= (
max (f,(
EMF C))) by
Th17
.= f by
Th17;
end;
theorem ::
FUZZY_1:42
(f
\+\ (
UMF C))
= (
1_minus f)
proof
thus (f
\+\ (
UMF C))
= (
max ((
min (f,(
EMF C))),(
min ((
1_minus f),(
UMF C))))) by
Th39
.= (
max ((
EMF C),(
min ((
1_minus f),(
UMF C))))) by
Th17
.= (
min ((
1_minus f),(
UMF C))) by
Th17
.= (
1_minus f) by
Th17;
end;
theorem ::
FUZZY_1:43
(
min ((
min ((
max (f,g)),(
max (g,h)))),(
max (h,f))))
= (
max ((
max ((
min (f,g)),(
min (g,h)))),(
min (h,f))))
proof
thus (
min ((
min ((
max (f,g)),(
max (g,h)))),(
max (h,f))))
= (
max ((
min ((
min ((
max (f,g)),(
max (g,h)))),h)),(
min ((
min ((
max (f,g)),(
max (g,h)))),f)))) by
Th9
.= (
max ((
min ((
max (f,g)),(
min ((
max (g,h)),h)))),(
min ((
min ((
max (f,g)),(
max (g,h)))),f)))) by
Th7
.= (
max ((
min ((
max (f,g)),(
min ((
max (h,g)),h)))),(
min ((
min ((
max (f,g)),f)),(
max (g,h)))))) by
Th7
.= (
max ((
min ((
max (f,g)),h)),(
min ((
min ((
max (f,g)),f)),(
max (g,h)))))) by
Th8
.= (
max ((
min ((
max (f,g)),h)),(
min (f,(
max (g,h)))))) by
Th8
.= (
max ((
min (h,(
max (f,g)))),(
max ((
min (f,g)),(
min (f,h)))))) by
Th9
.= (
max ((
max ((
min (f,g)),(
min (f,h)))),(
max ((
min (h,f)),(
min (h,g)))))) by
Th9
.= (
max ((
max ((
max ((
min (f,g)),(
min (f,h)))),(
min (f,h)))),(
min (h,g)))) by
Th7
.= (
max ((
max ((
min (f,g)),(
max ((
min (f,h)),(
min (f,h)))))),(
min (h,g)))) by
Th7
.= (
max ((
max ((
min (f,g)),(
min (g,h)))),(
min (h,f)))) by
Th7;
end;
theorem ::
FUZZY_1:44
(
max ((
min (f,g)),(
min ((
1_minus f),(
1_minus g)))))
c= (
1_minus (f
\+\ g))
proof
set f1 = (
1_minus f), g1 = (
1_minus g);
let x be
Element of C;
(
1_minus (f
\+\ g))
= (
min ((
1_minus (
min (f,g1))),(
1_minus (
min (f1,g))))) by
Th10
.= (
min ((
max (f1,(
1_minus g1))),(
1_minus (
min (f1,g))))) by
Th10
.= (
min ((
max (f1,g)),(
max ((
1_minus f1),g1)))) by
Th10
.= (
max ((
min ((
max (f1,g)),f)),(
min ((
max (f1,g)),g1)))) by
Th9
.= (
max ((
max ((
min (f,f1)),(
min (f,g)))),(
min ((
max (f1,g)),g1)))) by
Th9
.= (
max ((
max ((
min (f,f1)),(
min (f,g)))),(
max ((
min (g1,f1)),(
min (g1,g)))))) by
Th9
.= (
max ((
max ((
max ((
min (f,g)),(
min (f,f1)))),(
min (g1,f1)))),(
min (g1,g)))) by
Th7
.= (
max ((
max ((
max ((
min (g1,f1)),(
min (f,g)))),(
min (f,f1)))),(
min (g1,g)))) by
Th7
.= (
max ((
max ((
min (g1,f1)),(
min (f,g)))),(
max ((
min (f,f1)),(
min (g1,g)))))) by
Th7;
then ((
1_minus (f
\+\ g))
. x)
= (
max (((
max ((
min (f,g)),(
min (f1,g1))))
. x),((
max ((
min (f,f1)),(
min (g1,g))))
. x))) by
Def4;
hence thesis by
XXREAL_0: 25;
end;
theorem ::
FUZZY_1:45
(
max ((f
\+\ g),(
min (f,g))))
c= (
max (f,g))
proof
set f1 = (
1_minus f), g1 = (
1_minus g);
let x be
Element of C;
(
max ((f
\+\ g),(
min (f,g))))
= (
max ((
min (f,g1)),(
max ((
min (f1,g)),(
min (f,g)))))) by
Th7
.= (
max ((
min (f,g1)),(
min ((
max ((
min (f1,g)),f)),(
max (g,(
min (f1,g)))))))) by
Th9
.= (
max ((
min (f,g1)),(
min ((
max ((
min (f1,g)),f)),g)))) by
Th8
.= (
min ((
max ((
min (f,g1)),(
max (f,(
min (f1,g)))))),(
max ((
min (f,g1)),g)))) by
Th9
.= (
min ((
max ((
max (f,(
min (f,g1)))),(
min (f1,g)))),(
max ((
min (f,g1)),g)))) by
Th7
.= (
min ((
max (f,(
min (f1,g)))),(
max ((
min (f,g1)),g)))) by
Th8
.= (
min ((
min ((
max (f,f1)),(
max (f,g)))),(
max (g,(
min (f,g1)))))) by
Th9
.= (
min ((
min ((
max (f,f1)),(
max (f,g)))),(
min ((
max (g,f)),(
max (g,g1)))))) by
Th9
.= (
min ((
min ((
min ((
max (f,f1)),(
max (f,g)))),(
max (g,f)))),(
max (g,g1)))) by
Th7
.= (
min ((
min ((
max (f,f1)),(
min ((
max (f,g)),(
max (f,g)))))),(
max (g,g1)))) by
Th7
.= (
min ((
max (f,g)),(
min ((
max (f,f1)),(
max (g,g1)))))) by
Th7;
then ((
max ((f
\+\ g),(
min (f,g))))
. x)
= (
min (((
max (f,g))
. x),((
min ((
max (f,f1)),(
max (g,g1))))
. x))) by
Def3;
hence thesis by
XXREAL_0: 17;
end;
theorem ::
FUZZY_1:46
(f
\+\ f)
= (
min (f,(
1_minus f)));
definition
let C be non
empty
set;
let h,g be
Membership_Func of C;
::
FUZZY_1:def9
func
ab_difMF (h,g) ->
Membership_Func of C means for c be
Element of C holds (it
. c)
=
|.((h
. c)
- (g
. c)).|;
existence
proof
defpred
P[
object,
object] means $2
=
|.((h
. $1)
- (g
. $1)).|;
A1: for x,y1,y2 be
object st x
in C &
P[x, y1] &
P[x, y2] holds y1
= y2;
A2: for x,y be
object st x
in C &
P[x, y] holds y
in
REAL by
XREAL_0:def 1;
consider IT be
PartFunc of C,
REAL such that
A3: (for x be
object holds x
in (
dom IT) iff x
in C & ex y be
object st
P[x, y]) & for x be
object st x
in (
dom IT) holds
P[x, (IT
. x)] from
PARTFUN1:sch 2(
A2,
A1);
for x be
object st x
in C holds x
in (
dom IT)
proof
let x be
object;
|.((h
. x)
- (g
. x)).| is
set by
TARSKI: 1;
hence thesis by
A3;
end;
then C
c= (
dom IT) by
TARSKI:def 3;
then
A5: (
dom IT)
= C by
XBOOLE_0:def 10;
then
A6: for c be
Element of C holds (IT
. c)
=
|.((h
. c)
- (g
. c)).| by
A3;
A7: (
rng g)
c=
[.
0 , 1.] by
RELAT_1:def 19;
A8: (
rng h)
c=
[.
0 , 1.] by
RELAT_1:def 19;
for y be
object st y
in (
rng IT) holds y
in
[.
0 , 1.]
proof
reconsider A =
[.
0 , jj.] as non
empty
closed_interval
Subset of
REAL by
MEASURE5: 14;
let y be
object;
assume y
in (
rng IT);
then
consider x be
Element of C such that
A9: x
in (
dom IT) and
A10: y
= (IT
. x) by
PARTFUN1: 3;
0
<=
|.((h
. x)
- (g
. x)).| by
COMPLEX1: 46;
then
A11:
0
<= (IT
. x) by
A3,
A9;
A12: A
=
[.(
lower_bound A), (
upper_bound A).] by
INTEGRA1: 4;
then
A13:
0
= (
lower_bound A) by
INTEGRA1: 5;
A14: x
in C;
then x
in (
dom h) by
FUNCT_2:def 1;
then
A15: (h
. x)
in (
rng h) by
FUNCT_1:def 3;
x
in (
dom g) by
A14,
FUNCT_2:def 1;
then
A16: (g
. x)
in (
rng g) by
FUNCT_1:def 3;
then
0
<= (g
. x) by
A7,
A13,
INTEGRA2: 1;
then
A17: (1
-
0 )
>= (1
- (g
. x)) by
XREAL_1: 10;
A18: 1
= (
upper_bound A) by
A12,
INTEGRA1: 5;
then (g
. x)
<= 1 by
A7,
A16,
INTEGRA2: 1;
then
A19: (
- (g
. x))
>= (
- 1) by
XREAL_1: 24;
0
<= (h
. x) by
A8,
A13,
A15,
INTEGRA2: 1;
then (
0
- (g
. x))
<= ((h
. x)
- (g
. x)) by
XREAL_1: 9;
then
A20: (
- 1)
<= ((h
. x)
- (g
. x)) by
A19,
XXREAL_0: 2;
(h
. x)
<= 1 by
A8,
A18,
A15,
INTEGRA2: 1;
then ((h
. x)
- (g
. x))
<= (1
- (g
. x)) by
XREAL_1: 9;
then ((h
. x)
- (g
. x))
<= 1 by
A17,
XXREAL_0: 2;
then
|.((h
. x)
- (g
. x)).|
<= 1 by
A20,
ABSVALUE: 5;
then (IT
. x)
<= 1 by
A3,
A9;
hence thesis by
A10,
A13,
A18,
A11,
INTEGRA2: 1;
end;
then
A21: (
rng IT)
c=
[.
0 , 1.] by
TARSKI:def 3;
IT is
total by
A5,
PARTFUN1:def 2;
then IT is
Membership_Func of C by
A21,
RELAT_1:def 19;
hence thesis by
A6;
end;
uniqueness
proof
let F,G be
Membership_Func of C;
assume that
A22: for c be
Element of C holds (F
. c)
=
|.((h
. c)
- (g
. c)).| and
A23: for c be
Element of C holds (G
. c)
=
|.((h
. c)
- (g
. c)).|;
A24: for c be
Element of C st c
in C holds (F
. c)
= (G
. c)
proof
let c be
Element of C;
(F
. c)
=
|.((h
. c)
- (g
. c)).| by
A22;
hence thesis by
A23;
end;
C
= (
dom F) & C
= (
dom G) by
FUNCT_2:def 1;
hence thesis by
A24,
PARTFUN1: 5;
end;
end