:: Lattice of Fuzzy Sets
:: by Takashi Mitsuishi and Grzegorz Bancerek
::
:: Received August 12, 2003
:: Copyright (c) 2003-2011 Association of Mizar Users


begin

definition
let R be RelStr ;
attr R is real means :Def1: :: 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;

:: deftheorem Def1 defines real LFUZZY_0:def 1 :
for R being RelStr holds
( R is real iff ( 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 ) ) ) );

definition
let R be RelStr ;
attr R is interval means :Def2: :: LFUZZY_0:def 2
( R is real & ex a, b being real number st
( a <= b & the carrier of R = [.a,b.] ) );
end;

:: deftheorem Def2 defines interval LFUZZY_0:def 2 :
for R being RelStr holds
( R is interval iff ( R is real & ex a, b being real number st
( a <= b & the carrier of R = [.a,b.] ) ) );

registration
cluster interval -> non empty real RelStr ;
coherence
for b1 being RelStr st b1 is interval holds
( b1 is real & not b1 is empty )
proof end;
end;

registration
cluster empty -> real RelStr ;
coherence
for b1 being RelStr st b1 is empty holds
b1 is real
proof end;
end;

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

registration
cluster strict interval RelStr ;
existence
ex b1 being RelStr st
( b1 is interval & b1 is strict )
proof end;
end;

theorem Th2: :: LFUZZY_0:2
for R1, R2 being real RelStr st the carrier of R1 = the carrier of R2 holds
RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #)
proof end;

registration
let R be non empty real RelStr ;
cluster -> real Element of the carrier of R;
coherence
for b1 being Element of R holds b1 is real
proof end;
end;

definition
let X be Subset of REAL;
func RealPoset X -> strict real RelStr means :Def3: :: LFUZZY_0:def 3
 the carrier of it = X;
existence
ex b1 being strict real RelStr st the carrier of b1 = X
proof end;
uniqueness
for b1, b2 being strict real RelStr st the carrier of b1 = X & the carrier of b2 = X holds
b1 = b2 by Th2;
end;

:: deftheorem Def3 defines RealPoset LFUZZY_0:def 3 :
for X being Subset of REAL
for b2 being strict real RelStr holds
( b2 = RealPoset X iff the carrier of b2 = X );

registration
let X be non empty Subset of REAL;
cluster RealPoset X -> non empty strict real ;
coherence
not RealPoset X is empty by Def3;
end;

notation
let R be RelStr ;
let x, y be Element of R;
synonym x <<= y for x <= y;
synonym y >>= x for x <= y;
antonym x ~<= y for x <= y;
antonym y ~>= x for x <= y;
end;

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

registration
cluster real -> reflexive transitive antisymmetric RelStr ;
coherence
for b1 being RelStr st b1 is real holds
( b1 is reflexive & b1 is antisymmetric & b1 is transitive )
proof end;
end;

registration
cluster non empty real -> non empty connected real RelStr ;
coherence
for b1 being non empty real RelStr holds b1 is connected
proof end;
end;

definition
let R be non empty real RelStr ;
let x, y be Element of R;
:: original: max
redefine func max (x,y) -> Element of R;
coherence
max (x,y) is Element of R by XXREAL_0:16;
end;

definition
let R be non empty real RelStr ;
let x, y be Element of R;
:: original: min
redefine func min (x,y) -> Element of R;
coherence
min (x,y) is Element of R by XXREAL_0:15;
end;

registration
cluster non empty real -> non empty with_suprema with_infima real RelStr ;
coherence
for b1 being non empty real RelStr holds
( b1 is with_suprema & b1 is with_infima ) ;
end;

registration
let R be non empty real RelStr ;
let a, b be Element of R;
identify a "\/" b with max (a,b);
compatibility
a "\/" b = max (a,b)
proof end;
identify a "/\" b with min (a,b);
compatibility
a "/\" b = min (a,b)
proof end;
end;

theorem :: LFUZZY_0:4
for R being non empty real RelStr
for a, b being Element of R holds a "\/" b = max (a,b) ;

theorem :: LFUZZY_0:5
for R being non empty real RelStr
for a, b being Element of R holds a "/\" b = min (a,b) ;

theorem Th6: :: LFUZZY_0:6
for R being non empty real RelStr holds
( ex x being real number st
( x in the carrier of R & ( for y being real number st y in the carrier of R holds
x <= y ) ) iff R is lower-bounded )
proof end;

theorem Th7: :: LFUZZY_0:7
for R being non empty real RelStr holds
( ex x being real number st
( x in the carrier of R & ( for y being real number st y in the carrier of R holds
x >= y ) ) iff R is upper-bounded )
proof end;

registration
cluster non empty interval -> non empty bounded RelStr ;
coherence
for b1 being non empty RelStr st b1 is interval holds
b1 is bounded
proof end;
end;

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

registration
cluster non empty interval -> non empty complete interval RelStr ;
coherence
for b1 being non empty interval RelStr holds b1 is complete
proof end;
end;

registration
cluster non empty reflexive transitive antisymmetric connected -> distributive RelStr ;
coherence
for b1 being Chain holds b1 is distributive
proof end;
end;

registration
cluster non empty interval -> non empty Heyting interval RelStr ;
coherence
for b1 being non empty interval RelStr holds b1 is Heyting
proof end;
end;

registration
cluster K653(0,1) -> non empty ;
coherence
not [.0,1.] is empty
proof end;
end;

registration
cluster RealPoset [.0,1.] -> strict real interval ;
coherence
RealPoset [.0,1.] is interval
proof end;
end;

begin

theorem Th9: :: 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
proof end;

theorem Th10: :: 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
proof end;

theorem Th11: :: 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 ) holds
for f, g being Element of (product J)
for i being Element of I holds (f "/\" g) . i = (f . i) "/\" (g . i)
proof end;

theorem Th12: :: 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 ) holds
for f, g being Element of (product J)
for i being Element of I holds (f "\/" g) . i = (f . i) "\/" (g . i)
proof end;

theorem Th13: :: 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 complete Heyting LATTICE ) holds
( product J is complete & product J is Heyting )
proof end;

registration
let A be non empty set ;
let R be complete Heyting LATTICE;
cluster R |^ A -> Heyting ;
coherence
R |^ A is Heyting
proof end;
end;

begin

definition
let A be non empty set ;
func FuzzyLattice A -> complete Heyting LATTICE equals :: LFUZZY_0:def 4
(RealPoset [.0,1.]) |^ A;
coherence
(RealPoset [.0,1.]) |^ A is complete Heyting LATTICE ;
end;

:: deftheorem defines FuzzyLattice LFUZZY_0:def 4 :
for A being non empty set holds FuzzyLattice A = (RealPoset [.0,1.]) |^ A;

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

Lm1: for A being non empty set holds FuzzyLattice A is constituted-Functions
proof end;

registration
let A be non empty set ;
cluster FuzzyLattice A -> complete constituted-Functions Heyting ;
coherence
FuzzyLattice A is constituted-Functions by Lm1;
end;

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

Lm2: for X being non empty set
for a being Element of (FuzzyLattice X) holds a is Membership_Func of X
proof end;

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;
coherence
a is Membership_Func of X by Lm2;
end;

:: deftheorem defines @ LFUZZY_0:def 5 :
for X being non empty set
for a being Element of (FuzzyLattice X) holds @ a = a;

Lm3: for X being non empty set
for f being Membership_Func of X holds f is Element of (FuzzyLattice X)
proof 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;
coherence
f is Element of (FuzzyLattice X) by Lm3;
end;

:: deftheorem defines @ LFUZZY_0:def 6 :
for X being non empty set
for f being Membership_Func of X holds (X,f) @ = f;

definition
let X be non empty set ;
let f be Membership_Func of X;
let x be Element of X;
:: original: .
redefine func f . x -> Element of (RealPoset [.0,1.]);
coherence
f . x is Element of (RealPoset [.0,1.])
proof end;
end;

definition
let X, Y be non empty set ;
let f be RMembership_Func of X,Y;
let x be Element of X;
let y be Element of Y;
:: original: .
redefine func f . (x,y) -> Element of (RealPoset [.0,1.]);
coherence
f . (x,y) is Element of (RealPoset [.0,1.])
proof end;
end;

definition
let X be non empty set ;
let f be Element of (FuzzyLattice X);
let x be Element of X;
:: original: .
redefine func f . x -> Element of (RealPoset [.0,1.]);
coherence
f . x is Element of (RealPoset [.0,1.])
proof end;
end;

theorem Th16: :: LFUZZY_0:16
for C being non empty set
for f, g being Membership_Func of C holds
( ( for c being Element of C holds f . c <= g . c ) iff (C,f) @ <<= (C,g) @ )
proof end;

theorem :: LFUZZY_0:17
for C being non empty set
for s, t being Element of (FuzzyLattice C) holds
( s <<= t iff for c being Element of C holds (@ s) . c <= (@ t) . c )
proof end;

theorem Th18: :: LFUZZY_0:18
for C being non empty set
for f, g being Membership_Func of C holds max (f,g) = ((C,f) @) "\/" ((C,g) @)
proof end;

theorem :: LFUZZY_0:19
for C being non empty set
for s, t being Element of (FuzzyLattice C) holds s "\/" t = max ((@ s),(@ t))
proof end;

theorem Th20: :: LFUZZY_0:20
for C being non empty set
for f, g being Membership_Func of C holds min (f,g) = ((C,f) @) "/\" ((C,g) @)
proof end;

theorem :: LFUZZY_0:21
for C being non empty set
for s, t being Element of (FuzzyLattice C) holds s "/\" t = min ((@ s),(@ t))
proof end;

begin

scheme :: LFUZZY_0:sch 1
SupDistributivity{ F1() -> complete LATTICE, F2() -> non empty set , F3() -> non empty set , F4( set , set ) -> Element of F1(), P1[ set ], P2[ set ] } :
"\/" ( { ("\/" ( { F4(x,y) where y is Element of F3() : P2[y] } ,F1())) where x is Element of F2() : P1[x] } ,F1()) = "\/" ( { F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) } ,F1())
proof end;

scheme :: LFUZZY_0:sch 2
SupDistributivity9{ F1() -> complete LATTICE, F2() -> non empty set , F3() -> non empty set , F4( set , set ) -> Element of F1(), P1[ set ], P2[ set ] } :
"\/" ( { ("\/" ( { F4(x,y) where x is Element of F2() : P1[x] } ,F1())) where y is Element of F3() : P2[y] } ,F1()) = "\/" ( { F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) } ,F1())
proof end;

scheme :: LFUZZY_0:sch 3
FraenkelF9R9{ F1() -> non empty set , F2() -> non empty set , F3( set , set ) -> set , F4( set , set ) -> set , P1[ set , set ] } :
{ F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } = { F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P1[u2,v2] }
provided
A1: for u being Element of F1()
for v being Element of F2() st P1[u,v] holds
F3(u,v) = F4(u,v)
proof end;

scheme :: LFUZZY_0:sch 4
FraenkelF699R{ F1() -> non empty set , F2() -> non empty set , F3( set , set ) -> set , F4( set , set ) -> set , P1[ set , set ], P2[ set , set ] } :
{ F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } = { F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2] }
provided
A1: for u being Element of F1()
for v being Element of F2() holds
( P1[u,v] iff P2[u,v] ) and
A2: for u being Element of F1()
for v being Element of F2() st P1[u,v] holds
F3(u,v) = F4(u,v)
proof end;

scheme :: LFUZZY_0:sch 5
SupCommutativity{ F1() -> complete LATTICE, F2() -> non empty set , F3() -> non empty set , F4( set , set ) -> Element of F1(), F5( set , set ) -> Element of F1(), P1[ set ], P2[ set ] } :
"\/" ( { ("\/" ( { F4(x,y) where y is Element of F3() : P2[y] } ,F1())) where x is Element of F2() : P1[x] } ,F1()) = "\/" ( { ("\/" ( { F5(x9,y9) where x9 is Element of F2() : P1[x9] } ,F1())) where y9 is Element of F3() : P2[y9] } ,F1())
provided
A1: for x being Element of F2()
for y being Element of F3() st P1[x] & P2[y] holds
F4(x,y) = F5(x,y)
proof end;

Lm4: for x being Element of (RealPoset [.0,1.]) holds x is Real
proof end;

Lm5: 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
for z being Element of Z holds
( rng (min (R,S,x,z)) = { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} )
proof end;

theorem Th22: :: 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
for z being Element of Z holds (R (#) S) . (x,z) = "\/" ( { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } ,(RealPoset [.0,1.]))
proof end;

Lm6: 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
for z being Element of Z
for a being Element of (RealPoset [.0,1.]) holds ((R (#) S) . (x,z)) "/\" a = "\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } ,(RealPoset [.0,1.]))
proof end;

Lm7: 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
for z being Element of Z
for a being Element of (RealPoset [.0,1.]) holds a "/\" ((R (#) S) . (x,z)) = "\/" ( { ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum } ,(RealPoset [.0,1.]))
proof end;

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)
proof end;