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

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 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 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 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 st
( a <= b & the carrier of R = [.a,b.] ) ) );

registration

cluster interval -> non empty real for RelStr ;

coherence
for b₁ being RelStr st b₁ is interval holds
( b₁ is real & not b₁ is empty ) by XXREAL_1:1;

end;

registration

cluster empty -> real for RelStr ;

coherence
for b₁ being RelStr st b₁ is empty holds
b₁ is real

proof end;

end;

theorem Th1: :: LFUZZY_0:1

for X being real-membered set ex R being strict RelStr st
( the carrier of R = X & R is real )

proof end;

registration

cluster strict interval for RelStr ;

existence
ex b₁ being RelStr st
( b₁ is interval & b₁ 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 for Element of the carrier of R;

coherence
for b₁ being Element of R holds b₁ is real

proof end;

end;

definition

let X be real-membered set ;

func RealPoset X -> strict real RelStr means :Def3: :: LFUZZY_0:def 3
the carrier of it = X;

existence
ex b₁ being strict real RelStr st the carrier of b₁ = X

proof end;

uniqueness
for b₁, b₂ being strict real RelStr st the carrier of b₁ = X & the carrier of b₂ = X holds
b₁ = b₂ by Th2;

end;

:: deftheorem Def3 defines RealPoset LFUZZY_0:def 3 :
for X being real-membered set
for b₂ being strict real RelStr holds
( b₂ = RealPoset X iff the carrier of b₂ = X );

registration

let X be non empty real-membered set ;

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 for RelStr ;

coherence
for b₁ being RelStr st b₁ is real holds
( b₁ is reflexive & b₁ is antisymmetric & b₁ is transitive )

proof end;

end;

registration

cluster non empty real -> non empty connected real for RelStr ;

coherence
for b₁ being non empty real RelStr holds b₁ 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 for RelStr ;

coherence
for b₁ being non empty real RelStr holds
( b₁ is with_suprema & b₁ 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 st
( x in the carrier of R & ( for y being Real 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 st
( x in the carrier of R & ( for y being Real 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 for RelStr ;

coherence
for b₁ being non empty RelStr st b₁ is interval holds
b₁ 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 for RelStr ;

coherence
for b₁ being non empty interval RelStr holds b₁ is complete

proof end;

end;

registration

cluster non empty reflexive transitive antisymmetric connected -> distributive for RelStr ;

coherence
for b₁ being Chain holds b₁ is distributive

proof end;

end;

registration

cluster non empty interval -> non empty Heyting interval for RelStr ;

coherence
for b₁ being non empty interval RelStr holds b₁ is Heyting

proof end;

end;

registration

cluster K587(0,1) -> non empty ;

coherence
not [.0,1.] is empty by MEASURE5:14;

end;

registration

cluster RealPoset [.0,1.] -> strict real interval ;

coherence
RealPoset [.0,1.] is interval by Def3;

end;

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;

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;

scheme :: LFUZZY_0:sch 1
SupDistributivity{ F₁() -> complete LATTICE, F₂() -> non empty set , F₃() -> non empty set , F₄( set , set ) -> Element of F₁(), P₁[ set ], P₂[ set ] } :

"\/" ( { ("\/" ( { F₄(x,y) where y is Element of F₃() : P₂[y] } ,F₁())) where x is Element of F₂() : P₁[x] } ,F₁()) = "\/" ( { F₄(x,y) where x is Element of F₂(), y is Element of F₃() : ( P₁[x] & P₂[y] ) } ,F₁())

proof end;

scheme :: LFUZZY_0:sch 2
SupDistributivity9{ F₁() -> complete LATTICE, F₂() -> non empty set , F₃() -> non empty set , F₄( set , set ) -> Element of F₁(), P₁[ set ], P₂[ set ] } :

"\/" ( { ("\/" ( { F₄(x,y) where x is Element of F₂() : P₁[x] } ,F₁())) where y is Element of F₃() : P₂[y] } ,F₁()) = "\/" ( { F₄(x,y) where x is Element of F₂(), y is Element of F₃() : ( P₁[x] & P₂[y] ) } ,F₁())

proof end;

scheme :: LFUZZY_0:sch 3
FraenkelF9R9{ F₁() -> non empty set , F₂() -> non empty set , F₃( set , set ) -> set , F₄( set , set ) -> set , P₁[ set , set ] } :

{ F₃(u1,v1) where u1 is Element of F₁(), v1 is Element of F₂() : P₁[u1,v1] } = { F₄(u2,v2) where u2 is Element of F₁(), v2 is Element of F₂() : P₁[u2,v2] }

provided

A1: for u being Element of F₁()
for v being Element of F₂() st P₁[u,v] holds
F₃(u,v) = F₄(u,v)

proof end;

scheme :: LFUZZY_0:sch 4
FraenkelF699R{ F₁() -> non empty set , F₂() -> non empty set , F₃( set , set ) -> set , F₄( set , set ) -> set , P₁[ set , set ], P₂[ set , set ] } :

{ F₃(u1,v1) where u1 is Element of F₁(), v1 is Element of F₂() : P₁[u1,v1] } = { F₄(u2,v2) where u2 is Element of F₁(), v2 is Element of F₂() : P₂[u2,v2] }

provided

A1: for u being Element of F₁()
for v being Element of F₂() holds
( P₁[u,v] iff P₂[u,v] ) and
A2: for u being Element of F₁()
for v being Element of F₂() st P₁[u,v] holds
F₃(u,v) = F₄(u,v)

proof end;

scheme :: LFUZZY_0:sch 5
SupCommutativity{ F₁() -> complete LATTICE, F₂() -> non empty set , F₃() -> non empty set , F₄( set , set ) -> Element of F₁(), F₅( set , set ) -> Element of F₁(), P₁[ set ], P₂[ set ] } :

"\/" ( { ("\/" ( { F₄(x,y) where y is Element of F₃() : P₂[y] } ,F₁())) where x is Element of F₂() : P₁[x] } ,F₁()) = "\/" ( { ("\/" ( { F₅(x9,y9) where x9 is Element of F₂() : P₁[x9] } ,F₁())) where y9 is Element of F₃() : P₂[y9] } ,F₁())

provided

A1: for x being Element of F₂()
for y being Element of F₃() st P₁[x] & P₂[y] holds
F₄(x,y) = F₅(x,y)

proof end;

Lm4: 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;

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
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;

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 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;