Journal of Formalized Mathematics
Volume 12, 2000
University of Bialystok
Copyright (c) 2000 Association of Mizar Users

### The Concept of Fuzzy Relation and Basic Properties of its Operation

by
Takashi Mitsuishi,
Katsumi Wasaki, and
Yasunari Shidama

Received September 15, 2000

MML identifier: FUZZY_3
[ Mizar article, MML identifier index ]

```environ

vocabulary RELAT_1, FUNCT_3, FUNCT_1, SQUARE_1, FUZZY_1, BOOLE, FUZZY_3,
FUNCT_2;
notation XBOOLE_0, ZFMISC_1, SUBSET_1, XREAL_0, RELSET_1, FUNCT_2, RFUNCT_1,
FUZZY_1;
constructors SEQ_1, RFUNCT_1, FUZZY_2, RCOMP_1, XCMPLX_0, MEMBERED;
clusters SUBSET_1, MEMBERED;

begin

reserve C1,C2 for non empty set;

definition let C be non empty set;
cluster -> quasi_total Membership_Func of C;
end;

definition let C1,C2 be non empty set;
mode RMembership_Func of C1,C2 is Membership_Func of [:C1,C2:];
end;

definition let C1,C2 be non empty set;
let h be RMembership_Func of C1,C2;
mode FuzzyRelation of C1,C2,h is FuzzySet of [:C1,C2:],h;
end;

reserve f,g for RMembership_Func of C1,C2;

begin :: Empty Fuzzy Set and Universal Fuzzy Set

definition let C1,C2 be non empty set;
mode Zero_Relation of C1,C2 is Empty_FuzzySet of [:C1,C2:];
mode Universe_Relation of C1,C2 is Universal_FuzzySet of [:C1,C2:];
end;

reserve X for Universe_Relation of C1,C2;
reserve O for Zero_Relation of C1,C2;

definition
let C1,C2 be non empty set;
func Zmf(C1,C2) -> RMembership_Func of C1,C2 equals
:: FUZZY_3:def 1
chi({},[:C1,C2:]);

func Umf(C1,C2) -> RMembership_Func of C1,C2 equals
:: FUZZY_3:def 2
chi([:C1,C2:],[:C1,C2:]);
end;

canceled 44;

theorem :: FUZZY_3:45
Zmf(C1,C2) = EMF [:C1,C2:];

theorem :: FUZZY_3:46
Umf(C1,C2) = UMF [:C1,C2:];

theorem :: FUZZY_3:47
O is FuzzyRelation of C1,C2,Zmf(C1,C2);

theorem :: FUZZY_3:48
X is FuzzyRelation of C1,C2,Umf(C1,C2);

canceled 3;

theorem :: FUZZY_3:52
for x be Element of [:C1,C2:],h be RMembership_Func of C1,C2 holds
(Zmf(C1,C2)).x <= h.x & h.x <= (Umf(C1,C2)).x;

theorem :: FUZZY_3:53
max(f,Umf(C1,C2)) = Umf(C1,C2) & min(f,Umf(C1,C2)) = f &
max(f,Zmf(C1,C2)) = f & min(f,Zmf(C1,C2)) = Zmf(C1,C2);

canceled 7;

theorem :: FUZZY_3:61
1_minus(Zmf(C1,C2)) = Umf(C1,C2) & 1_minus(Umf(C1,C2)) = Zmf(C1,C2);

canceled 59;

theorem :: FUZZY_3:121
min(f,1_minus g) = Zmf(C1,C2) implies
for c being Element of [:C1,C2:] holds f.c <= g.c;

canceled;

theorem :: FUZZY_3:123
min(f,g) = Zmf(C1,C2) implies min(f,1_minus g) = f;
```

Back to top