The Mizar abstract of LFUZZY

Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users
The abstract of the Mizar article:: Lattice of Fuzzy Sets
by
Takashi Mitsuishi, and
Grzegorz Bancerek
Received August 12, 2003
MML identifier: LFUZZY_0
[ Mizar article, MML identifier index ]
environ

 vocabulary LFUZZY_0, ORDERS_1, ARYTM, RELAT_2, LATTICES, RCOMP_1, FUNCT_1,
      RELAT_1, QC_LANG1, FUZZY_3, SEQ_1, TARSKI, FUZZY_1, GROUP_1, LATTICE2,
      LATTICE3, WAYBEL_0, MEASURE5, SQUARE_1, BOOLE, YELLOW_0, SEQ_2, INTEGRA1,
      SEQ_4, PRE_TOPC, BHSP_3, ORDINAL2, YELLOW_1, PBOOLE, FUNCT_2, PARTFUN1,
      MONOID_0, CARD_3, WAYBEL_3, WAYBEL_1, FUNCOP_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_2, DOMAIN_1,
      ORDINAL1, PARTFUN1, SUBSET_1, NUMBERS, XREAL_0, REAL_1, SQUARE_1, SEQ_1,
      SEQ_4, RCOMP_1, RELSET_1, STRUCT_0, ORDERS_1, PRE_TOPC, PBOOLE, MONOID_0,
      LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_1, WAYBEL_3, FUZZY_1,
      FUZZY_3, FUZZY_4, INTEGRA1, PRE_CIRC;
 constructors XCMPLX_0, SQUARE_1, INTEGRA1, WAYBEL_2, YELLOW10, PSCOMP_1,
      WAYBEL_3, FUZZY_4, DOMAIN_1, ORDERS_3, PRE_CIRC, MONOID_0;
 clusters SUBSET_1, LATTICE3, XREAL_0, YELLOW14, RELSET_1, ORDERS_4, STRUCT_0,
      MONOID_0, WAYBEL_2, WAYBEL10, WAYBEL17, WAYBEL_3, MEMBERED;
 requirements BOOLE, SUBSET, NUMERALS, REAL;


begin :: Posets of Real Numbers

definition
  let R be RelStr;
  attr R is real means
:: LFUZZY_0:def 1

   the carrier of R c= REAL &
   for x,y being real number st x in the carrier of R & y in the carrier of R
    holds [x,y] in the InternalRel of R iff x <= y;
end;

definition
  let R be RelStr;
  attr R is interval means
:: LFUZZY_0:def 2

   R is real & ex a,b being real number st a <= b & the carrier of R = [.a,b.];
end;

definition
  cluster interval -> real non empty RelStr;
end;

definition
  cluster empty -> real RelStr;
end;

theorem :: LFUZZY_0:1
  for X being Subset of REAL
  ex R being strict RelStr st
   the carrier of R = X & R is real;

definition
  cluster interval strict RelStr;
end;

theorem :: LFUZZY_0:2
  for R1,R2 being real RelStr
   st the carrier of R1 = the carrier of R2
   holds the RelStr of R1 = the RelStr of R2;

definition
  let R be non empty real RelStr;
  cluster -> real Element of R;
end;

definition
 let X be Subset of REAL;
 func RealPoset X -> real strict RelStr means
:: LFUZZY_0:def 3

  the carrier of it = X;
end;

definition
  let X be non empty Subset of REAL;
  cluster RealPoset X -> non empty;
end;

definition
  let R be RelStr;
  let x,y be Element of R;
  redefine pred x <= y;
   synonym x <<= y; synonym y >>= x; antonym x ~<= y; antonym y ~>= x;
end;

definition
  let x,y be real number;
  redefine pred x <= y;
   synonym x <R= y; antonym y <R x; synonym y >R= x; antonym x >R y;
end;

theorem :: LFUZZY_0:3
 for R being non empty real RelStr
 for x,y being Element of R
  holds x <R= y iff x <<= y;

definition
  cluster real -> reflexive antisymmetric transitive RelStr;
end;

definition
  cluster -> connected (real non empty RelStr);
end;

definition
 let R be non empty real RelStr;
 let x,y be Element of R;
 redefine func max(x,y) -> Element of R;
end;

definition
 let R be non empty real RelStr;
 let x,y be Element of R;
 redefine func min(x,y) -> Element of R;
end;

definition
  cluster -> with_suprema with_infima (real non empty RelStr);
end;

reserve X for non empty Subset of REAL,
   x,y,z,w for real number,
   R for real non empty RelStr,
   a,b,c for Element of R;

theorem :: LFUZZY_0:4
  a"\/"b = max(a,b);

theorem :: LFUZZY_0:5
  a"/\"b = min(a,b);

theorem :: LFUZZY_0:6
  (ex x st x in the carrier of R & for y st y in the carrier of R holds x <= y)
    iff R is lower-bounded;

theorem :: LFUZZY_0:7
  (ex x st x in the carrier of R & for y st y in the carrier of R holds x >= y)
    iff R is upper-bounded;

definition
  cluster interval -> bounded (non empty RelStr);
end;

theorem :: LFUZZY_0:8
for R being interval non empty RelStr, X being set holds
ex_sup_of X,R;

definition
  cluster -> complete (interval non empty RelStr);
end;

definition
  cluster -> distributive Chain;
end;

definition
  cluster -> Heyting (interval non empty RelStr);
end;

definition
  cluster [.0,1 .] -> non empty;
end;

definition
  cluster RealPoset [.0,1 .] -> interval;
end;

begin :: Product of Heyting Lattices

theorem :: LFUZZY_0:9
 for I being non empty set
 for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I
  st for i being Element of I holds J.i is sup-Semilattice
 holds product J is with_suprema;

theorem :: LFUZZY_0:10
 for I being non empty set
 for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I
  st for i being Element of I holds J.i is Semilattice
 holds product J is with_infima;

theorem :: LFUZZY_0:11
  for I being non empty set
  for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I
   st for i being Element of I holds J.i is Semilattice
  for f,g being Element of product J, i being Element of I
   holds (f "/\" g).i = (f.i) "/\" (g.i);

theorem :: LFUZZY_0:12
  for I being non empty set
  for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I
   st for i being Element of I holds J.i is sup-Semilattice
  for f,g being Element of product J, i being Element of I
   holds (f "\/" g).i = (f.i) "\/" (g.i);

theorem :: LFUZZY_0:13
  for I being non empty set
  for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I
   st for i being Element of I holds J.i is Heyting complete LATTICE
   holds product J is complete Heyting;

definition
   let A be non empty set;
   let R be complete Heyting LATTICE;
   cluster R |^ A -> Heyting;
end;

begin :: Lattice of Fuzzy Sets

definition
   let A be non empty set;
   func FuzzyLattice A -> Heyting complete LATTICE equals
:: LFUZZY_0:def 4

   (RealPoset [. 0,1 .]) |^ A;
end;

theorem :: LFUZZY_0:14
  for A being non empty set holds
    the carrier of FuzzyLattice A = Funcs(A, [. 0, 1 .]);

definition
   let A be non empty set;
   cluster FuzzyLattice A -> constituted-Functions;
end;

theorem :: LFUZZY_0:15
for R being complete Heyting LATTICE,
X being Subset of R,
y be Element of R holds
"\/"(X,R) "/\" y = "\/"({x "/\" y where x is Element of R: x in X},R);

definition
  let X be non empty set;
  let a be Element of FuzzyLattice X;
  func @a -> Membership_Func of X equals
:: LFUZZY_0:def 5
a;
end;

definition
  let X be non empty set;
  let f be Membership_Func of X;
  func (X,f)@ -> Element of FuzzyLattice X equals
:: LFUZZY_0:def 6
f;
end;

definition
  let X be non empty set;
  let f be Membership_Func of X;
  let x be Element of X;
  redefine func f.x -> Element of RealPoset [. 0,1 .];
end;

definition
  let X be non empty set;
  let f be Element of FuzzyLattice X;
  let x be Element of X;
  redefine func f.x -> Element of RealPoset [. 0,1 .];
end;

reserve C for non empty set, c for Element of C,
   f,g for Membership_Func of C,
   s,t for Element of FuzzyLattice C;

theorem :: LFUZZY_0:16
  (for c holds f.c <R= g.c) iff (C,f)@ <<= (C,g)@;

theorem :: LFUZZY_0:17
  s <<= t iff for c holds @s.c <R= @t.c;

theorem :: LFUZZY_0:18
  max(f,g) = (C,f)@ "\/" (C,g)@;

theorem :: LFUZZY_0:19
 s "\/" t = max(@s, @t);

theorem :: LFUZZY_0:20
  min(f,g) = (C,f)@ "/\" (C,g)@;

theorem :: LFUZZY_0:21
 s "/\" t = min(@s, @t);

begin :: Associativity of composition of fuzzy relations

scheme SupDistributivity { L() -> complete LATTICE,
  X, Y() -> non empty set,  F(set,set) -> Element of L(), P,Q[set]}:
  "\/"({ "\/"({F(x,y) where y is Element of Y(): Q[y]}, L())
         where x is Element of X(): P[x] }, L())
  = "\/"({F(x,y) where x is Element of X(), y is Element of Y():
   P[x] & Q[y]}, L());

scheme SupDistributivity' { L() -> complete LATTICE,
  X, Y() -> non empty set, F(set,set) -> Element of L(), P,Q[set]}:
  "\/"({ "\/"({F(x,y) where x is Element of X(): P[x]},L())
         where y is Element of Y(): Q[y] }, L())
  = "\/"({F(x,y) where x is Element of X(), y is Element of Y():
        P[x] & Q[y]}, L());

scheme FraenkelF'R'{ A() -> non empty set,B() -> non empty set,
F1, F2(set,set) -> set, P[set,set]  } :
    { F1(u1,v1) where u1 is (Element of A()), v1 is Element of B() : P[u1,v1] }
  = { F2(u2,v2) where u2 is (Element of A()), v2 is Element of B() : P[u2,v2] }
 provided
for u being (Element of A()), v being Element of B()
      st P[u,v] holds F1(u,v) = F2(u,v);

scheme FraenkelF6''R
 { A() -> non empty set, B() -> non empty set,
   F1, F2(set,set) -> set, P[set,set], Q[set,set] } :
    { F1(u1,v1) where u1 is (Element of A()), v1 is Element of B() : P[u1,v1] }
  = { F2(u2,v2) where u2 is (Element of A()), v2 is Element of B() : Q[u2,v2] }
 provided
for u being (Element of A()), v being Element of B()
      holds P[u,v] iff Q[u,v]
  and
for u being (Element of A()), v being Element of B()
     st P[u,v] holds F1(u,v) = F2(u,v);

scheme SupCommutativity { L() -> complete LATTICE, X, Y() -> non empty set,
  F1, F2(set,set) -> Element of L(), P,Q[set]}:
    "\/"({ "\/"({F1(x,y) where y is Element of Y(): Q[y]}, L())
           where x is Element of X(): P[x] }, L())
  = "\/"({ "\/"({F2(x',y') where x' is Element of X(): P[x']}, L())
           where y' is Element of Y(): Q[y'] }, L())
  provided
  for x being Element of X(), y being Element of Y() st P[x] & Q[y]
   holds F1(x,y) = F2(x,y);

theorem :: LFUZZY_0:22
  for X,Y,Z being non empty set
  for R being RMembership_Func of X,Y
  for S being RMembership_Func of Y,Z
  for x being Element of X, z being Element of Z
   holds  (R (#) S). [x,z] = "\/"({R. [x,y] "/\" S. [y,z]
      where y is Element of Y: not contradiction}, RealPoset [. 0,1 .]);

theorem :: LFUZZY_0:23
  for X,Y,Z,W being non empty set
  for R being RMembership_Func of X,Y
  for S being RMembership_Func of Y,Z
  for T being RMembership_Func of Z,W
   holds (R (#) S) (#) T = R (#) (S (#) T);
The abstract of the Mizar article:

Lattice of Fuzzy Sets
