:: FUZZY_1 semantic presentation

theorem Th1: :: FUZZY_1:1

for b₁, b₂ being set holds rng (chi b₁,b₂) c= [.0,1.]

proof end;

definition

let c₁ be non empty set ;
mode Membership_Func of c₁ -> PartFunc of a₁, REAL means :Def1: :: FUZZY_1:def 1
( dom a₂ = a₁ & rng a₂ c= [.0,1.] );
existence

proof end;

end;

:: deftheorem Def1 defines Membership_Func FUZZY_1:def 1 :

theorem Th2: :: FUZZY_1:2

for b₁ being non empty set holds chi b₁,b₁ is Membership_Func of b₁

proof end;

registration

let c₁ be non empty set ;
cluster -> real-yielding Membership_Func of a₁;
coherence ;

end;

definition

let c₁, c₂ be real-yielding Function;
pred c₁ is_less_than c₂ means :Def2: :: FUZZY_1:def 2
( dom a₁ c= dom a₂ & ( for b₁ being set st b₁ in dom a₁ holds
a₁ . b₁ <= a₂ . b₁ ) );
reflexivity ;

end;

:: deftheorem Def2 defines is_less_than FUZZY_1:def 2 :

notation

let c₁ be non empty set ;
let c₂, c₃ be Membership_Func of c₁;
synonym c₂ c= c₃ for c₁ is_less_than c₂;

end;

definition

let c₁ be non empty set ;
let c₂, c₃ be Membership_Func of c₁;
redefine pred is_less_than as c₂ is_less_than c₃ means :Def3: :: FUZZY_1:def 3
for b₁ being Element of a₁ holds a₂ . b₁ <= a₃ . b₁;
compatibility

proof end;

end;

:: deftheorem Def3 defines is_less_than FUZZY_1:def 3 :

Lemma6: for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ st b₃ c= & b₂ c= holds
b₂ = b₃

proof end;

theorem Th3: :: FUZZY_1:3

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds
( b₂ = b₃ iff ( b₃ c= & b₂ c= ) ) by Lemma6;

theorem Th4: :: FUZZY_1:4

for b₁ being non empty set
for b₂ being Membership_Func of b₁ holds b₂ c= ;

theorem Th5: :: FUZZY_1:5

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ st b₃ c= & b₄ c= holds
b₄ c= ;

definition

let c₁ be non empty set ;
let c₂, c₃ be Membership_Func of c₁;
func min c₂,c₃ -> Membership_Func of a₁ means :Def4: :: FUZZY_1:def 4
for b₁ being Element of a₁ holds a₄ . b₁ = min (a₂ . b₁),(a₃ . b₁);
existence

proof end;

uniqueness

proof end;

idempotence ;
commutativity ;

end;

:: deftheorem Def4 defines min FUZZY_1:def 4 :

definition

let c₁ be non empty set ;
let c₂, c₃ be Membership_Func of c₁;
func max c₂,c₃ -> Membership_Func of a₁ means :Def5: :: FUZZY_1:def 5
for b₁ being Element of a₁ holds a₄ . b₁ = max (a₂ . b₁),(a₃ . b₁);
existence

proof end;

uniqueness

proof end;

idempotence ;
commutativity ;

end;

:: deftheorem Def5 defines max FUZZY_1:def 5 :

definition

let c₁ be non empty set ;
let c₂ be Membership_Func of c₁;
func 1_minus c₂ -> Membership_Func of a₁ means :Def6: :: FUZZY_1:def 6
for b₁ being Element of a₁ holds a₃ . b₁ = 1 - (a₂ . b₁);
existence

proof end;

uniqueness

proof end;

involutiveness

proof end;

end;

:: deftheorem Def6 defines 1_minus FUZZY_1:def 6 :

theorem Th6: :: FUZZY_1:6

for b₁ being non empty set
for b₂ being Element of b₁
for b₃, b₄ being Membership_Func of b₁ holds
( min (b₃ . b₂),(b₄ . b₂) = (min b₃,b₄) . b₂ & max (b₃ . b₂),(b₄ . b₂) = (max b₃,b₄) . b₂ ) by Def4, Def5;

theorem Th7: :: FUZZY_1:7

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ holds
( max b₂,b₂ = b₂ & min b₂,b₂ = b₂ & max b₂,b₂ = min b₂,b₂ & min b₃,b₄ = min b₄,b₃ & max b₃,b₄ = max b₄,b₃ ) ;

theorem Th8: :: FUZZY_1:8

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ holds
( max (max b₂,b₃),b₄ = max b₂,(max b₃,b₄) & min (min b₂,b₃),b₄ = min b₂,(min b₃,b₄) )

proof end;

theorem Th9: :: FUZZY_1:9

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds
( max b₂,(min b₂,b₃) = b₂ & min b₂,(max b₂,b₃) = b₂ )

proof end;

theorem Th10: :: FUZZY_1:10

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ holds
( min b₂,(max b₃,b₄) = max (min b₂,b₃),(min b₂,b₄) & max b₂,(min b₃,b₄) = min (max b₂,b₃),(max b₂,b₄) )

proof end;

theorem Th11: :: FUZZY_1:11

for b₁ being non empty set
for b₂ being Membership_Func of b₁ holds 1_minus (1_minus b₂) = b₂ ;

theorem Th12: :: FUZZY_1:12

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds
( 1_minus (max b₂,b₃) = min (1_minus b₂),(1_minus b₃) & 1_minus (min b₂,b₃) = max (1_minus b₂),(1_minus b₃) )

proof end;

theorem Th13: :: FUZZY_1:13

for b₁ being non empty set holds chi {} ,b₁ is Membership_Func of b₁

proof end;

definition

let c₁ be non empty set ;
func EMF c₁ -> Membership_Func of a₁ equals :: FUZZY_1:def 7
chi {} ,a₁;
correctness by Th13;

end;

:: deftheorem Def7 defines EMF FUZZY_1:def 7 :

definition

let c₁ be non empty set ;
func UMF c₁ -> Membership_Func of a₁ equals :: FUZZY_1:def 8
chi a₁,a₁;
correctness by Th2;

end;

:: deftheorem Def8 defines UMF FUZZY_1:def 8 :

theorem Th14: :: FUZZY_1:14

for b₁ being non empty set
for b₂, b₃ being Element of REAL
for b₄ being PartFunc of b₁, REAL st rng b₄ c= [.b₂,b₃.] & b₂ <= b₃ holds
for b₅ being Element of b₁ st b₅ in dom b₄ holds
( b₂ <= b₄ . b₅ & b₄ . b₅ <= b₃ )

proof end;

theorem Th15: :: FUZZY_1:15

for b₁ being non empty set
for b₂ being Membership_Func of b₁ holds b₂ c=

proof end;

theorem Th16: :: FUZZY_1:16

for b₁ being non empty set
for b₂ being Membership_Func of b₁ holds UMF b₁ c=

proof end;

theorem Th17: :: FUZZY_1:17

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being Membership_Func of b₁ holds
( (EMF b₁) . b₂ <= b₃ . b₂ & b₃ . b₂ <= (UMF b₁) . b₂ )

proof end;

theorem Th18: :: FUZZY_1:18

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds
( b₂ c= & max b₂,b₃ c= )

proof end;

theorem Th19: :: FUZZY_1:19

for b₁ being non empty set
for b₂ being Membership_Func of b₁ holds
( max b₂,(UMF b₁) = UMF b₁ & min b₂,(UMF b₁) = b₂ & max b₂,(EMF b₁) = b₂ & min b₂,(EMF b₁) = EMF b₁ )

proof end;

theorem Th20: :: FUZZY_1:20

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ st b₃ c= & b₃ c= holds
b₃ c=

proof end;

theorem Th21: :: FUZZY_1:21

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ st b₃ c= holds
max b₃,b₄ c=

proof end;

theorem Th22: :: FUZZY_1:22

for b₁ being non empty set
for b₂, b₃, b₄, b₅ being Membership_Func of b₁ st b₃ c= & b₅ c= holds
max b₃,b₅ c=

proof end;

theorem Th23: :: FUZZY_1:23

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ st b₃ c= holds
max b₂,b₃ = b₃

proof end;

theorem Th24: :: FUZZY_1:24

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds max b₂,b₃ c=

proof end;

theorem Th25: :: FUZZY_1:25

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ st b₃ c= & b₄ c= holds
min b₃,b₄ c=

proof end;

theorem Th26: :: FUZZY_1:26

for b₁, b₂, b₃, b₄ being Element of REAL st b₁ <= b₂ & b₃ <= b₄ holds
min b₁,b₃ <= min b₂,b₄

proof end;

theorem Th27: :: FUZZY_1:27

for b₁, b₂, b₃ being Element of REAL st b₁ <= b₂ holds
min b₁,b₃ <= min b₂,b₃ by Th26;

theorem Th28: :: FUZZY_1:28

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ st b₃ c= holds
min b₃,b₄ c=

proof end;

theorem Th29: :: FUZZY_1:29

for b₁ being non empty set
for b₂, b₃, b₄, b₅ being Membership_Func of b₁ st b₃ c= & b₅ c= holds
min b₃,b₅ c=

proof end;

theorem Th30: :: FUZZY_1:30

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ st b₃ c= holds
min b₂,b₃ = b₂

proof end;

theorem Th31: :: FUZZY_1:31

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ st b₃ c= & b₄ c= & min b₃,b₄ = EMF b₁ holds
b₂ = EMF b₁

proof end;

theorem Th32: :: FUZZY_1:32

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ st max (min b₂,b₃),(min b₂,b₄) = b₂ holds
max b₃,b₄ c=

proof end;

theorem Th33: :: FUZZY_1:33

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ st b₃ c= & min b₃,b₄ = EMF b₁ holds
min b₂,b₄ = EMF b₁

proof end;

theorem Th34: :: FUZZY_1:34

for b₁ being non empty set
for b₂ being Membership_Func of b₁ st EMF b₁ c= holds
b₂ = EMF b₁

proof end;

theorem Th35: :: FUZZY_1:35

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds
( max b₂,b₃ = EMF b₁ iff ( b₂ = EMF b₁ & b₃ = EMF b₁ ) )

proof end;

theorem Th36: :: FUZZY_1:36

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ holds
( b₂ = max b₃,b₄ iff ( b₂ c= & b₂ c= & ( for b₅ being Membership_Func of b₁ st b₅ c= & b₅ c= holds
b₅ c= ) ) )

proof end;

theorem Th37: :: FUZZY_1:37

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ holds
( b₂ = min b₃,b₄ iff ( b₃ c= & b₄ c= & ( for b₅ being Membership_Func of b₁ st b₃ c= & b₄ c= holds
b₂ c= ) ) )

proof end;

theorem Th38: :: FUZZY_1:38

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ st max b₃,b₄ c= & min b₂,b₄ = EMF b₁ holds
b₃ c=

proof end;

Lemma25: for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ st b₃ c= holds
1_minus b₂ c=

proof end;

theorem Th39: :: FUZZY_1:39

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds
( b₃ c= iff 1_minus b₂ c= )

proof end;

theorem Th40: :: FUZZY_1:40

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds
( 1_minus b₃ c= iff 1_minus b₂ c= )

proof end;

theorem Th41: :: FUZZY_1:41

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds 1_minus b₂ c=

proof end;

theorem Th42: :: FUZZY_1:42

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds 1_minus (min b₂,b₃) c=

proof end;

theorem Th43: :: FUZZY_1:43

for b₁ being non empty set
for b₂ being Element of b₁ holds
( (EMF b₁) . b₂ = 0 & (UMF b₁) . b₂ = 1 ) by FUNCT_3:def 3;

theorem Th44: :: FUZZY_1:44

for b₁ being non empty set holds
( 1_minus (EMF b₁) = UMF b₁ & 1_minus (UMF b₁) = EMF b₁ )

proof end;

definition

let c₁ be non empty set ;
let c₂, c₃ be Membership_Func of c₁;
func c₂ \+\ c₃ -> Membership_Func of a₁ equals :: FUZZY_1:def 9
max (min a₂,(1_minus a₃)),(min (1_minus a₂),a₃);
coherence ;
commutativity ;

end;

:: deftheorem Def9 defines \+\ FUZZY_1:def 9 :

theorem Th45: :: FUZZY_1:45

for b₁ being non empty set
for b₂ being Membership_Func of b₁ holds b₂ \+\ (EMF b₁) = b₂

proof end;

theorem Th46: :: FUZZY_1:46

for b₁ being non empty set
for b₂ being Membership_Func of b₁ holds b₂ \+\ (UMF b₁) = 1_minus b₂

proof end;

theorem Th47: :: FUZZY_1:47

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ holds min (min (max b₂,b₃),(max b₃,b₄)),(max b₄,b₂) = max (max (min b₂,b₃),(min b₃,b₄)),(min b₄,b₂)

proof end;

theorem Th48: :: FUZZY_1:48

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds 1_minus (b₂ \+\ b₃) c=

proof end;

theorem Th49: :: FUZZY_1:49

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds max b₂,b₃ c=

proof end;

theorem Th50: :: FUZZY_1:50

for b₁ being non empty set
for b₂ being Membership_Func of b₁ holds b₂ \+\ b₂ = min b₂,(1_minus b₂) ;

definition

let c₁ be non empty set ;
let c₂, c₃ be Membership_Func of c₁;
func ab_difMF c₂,c₃ -> Membership_Func of a₁ means :: FUZZY_1:def 10
for b₁ being Element of a₁ holds a₄ . b₁ = abs ((a₂ . b₁) - (a₃ . b₁));
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines ab_difMF FUZZY_1:def 10 :