:: by Takashi Mitsuishi and Grzegorz Bancerek

::

:: Received August 12, 2003

:: Copyright (c) 2003-2019 Association of Mizar Users

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

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

:: 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.] ) ) );

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

coherence

for b_{1} being RelStr st b_{1} is interval holds

( b_{1} is real & not b_{1} is empty )
by XXREAL_1:1;

end;
for b

( b

registration
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 #)

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 ;

coherence

for b_{1} being Element of R holds b_{1} is real

end;
coherence

for b

proof end;

definition

let X be real-membered set ;

existence

ex b_{1} being strict real RelStr st the carrier of b_{1} = X

for b_{1}, b_{2} being strict real RelStr st the carrier of b_{1} = X & the carrier of b_{2} = X holds

b_{1} = b_{2}
by Th2;

end;
existence

ex b

proof end;

uniqueness for b

b

:: deftheorem Def3 defines RealPoset LFUZZY_0:def 3 :

for X being real-membered set

for b_{2} being strict real RelStr holds

( b_{2} = RealPoset X iff the carrier of b_{2} = X );

for X being real-membered set

for b

( b

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

registration

coherence

for b_{1} being RelStr st b_{1} is real holds

( b_{1} is reflexive & b_{1} is antisymmetric & b_{1} is transitive )

end;
for b

( b

proof end;

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

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

registration

coherence

for b_{1} being non empty real RelStr holds

( b_{1} is with_suprema & b_{1} is with_infima )
;

end;
for b

( b

registration

let R be non empty real RelStr ;

let a, b be Element of R;

compatibility

a "\/" b = max (a,b)

a "/\" b = min (a,b)

end;
let a, b be Element of R;

compatibility

a "\/" b = max (a,b)

proof end;

compatibility a "/\" b = min (a,b)

proof end;

theorem :: LFUZZY_0:4

theorem :: LFUZZY_0:5

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 )

( 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 )

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

registration
end;

registration
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

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

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)

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)

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 )

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

definition
end;

:: deftheorem defines FuzzyLattice LFUZZY_0:def 4 :

for A being non empty set holds FuzzyLattice A = (RealPoset [.0,1.]) |^ A;

for A being non empty set holds FuzzyLattice A = (RealPoset [.0,1.]) |^ A;

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

proof end;

registration
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)

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

coherence

a is Membership_Func of X by Lm2;

end;
let a be Element of (FuzzyLattice X);

coherence

a is Membership_Func of X by Lm2;

:: deftheorem defines @ LFUZZY_0:def 5 :

for X being non empty set

for a being Element of (FuzzyLattice X) holds @ a = a;

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;

coherence

f is Element of (FuzzyLattice X) by Lm3;

end;
let f be Membership_Func of X;

coherence

f is Element of (FuzzyLattice X) by Lm3;

:: deftheorem defines @ LFUZZY_0:def 6 :

for X being non empty set

for f being Membership_Func of X holds (X,f) @ = f;

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.])

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

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.])

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

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.])

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

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) @ )

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 )

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) @)

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

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) @)

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

for s, t being Element of (FuzzyLattice C) holds s "/\" t = min ((@ s),(@ t))

proof end;

scheme :: LFUZZY_0:sch 1

SupDistributivity{ F_{1}() -> complete LATTICE, F_{2}() -> non empty set , F_{3}() -> non empty set , F_{4}( set , set ) -> Element of F_{1}(), P_{1}[ set ], P_{2}[ set ] } :

SupDistributivity{ F

"\/" ( { ("\/" ( { F_{4}(x,y) where y is Element of F_{3}() : P_{2}[y] } ,F_{1}())) where x is Element of F_{2}() : P_{1}[x] } ,F_{1}()) = "\/" ( { F_{4}(x,y) where x is Element of F_{2}(), y is Element of F_{3}() : ( P_{1}[x] & P_{2}[y] ) } ,F_{1}())

proof end;

scheme :: LFUZZY_0:sch 2

SupDistributivity9{ F_{1}() -> complete LATTICE, F_{2}() -> non empty set , F_{3}() -> non empty set , F_{4}( set , set ) -> Element of F_{1}(), P_{1}[ set ], P_{2}[ set ] } :

SupDistributivity9{ F

"\/" ( { ("\/" ( { F_{4}(x,y) where x is Element of F_{2}() : P_{1}[x] } ,F_{1}())) where y is Element of F_{3}() : P_{2}[y] } ,F_{1}()) = "\/" ( { F_{4}(x,y) where x is Element of F_{2}(), y is Element of F_{3}() : ( P_{1}[x] & P_{2}[y] ) } ,F_{1}())

proof end;

scheme :: LFUZZY_0:sch 3

FraenkelF9R9{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}( set , set ) -> set , F_{4}( set , set ) -> set , P_{1}[ set , set ] } :

FraenkelF9R9{ F

{ F_{3}(u1,v1) where u1 is Element of F_{1}(), v1 is Element of F_{2}() : P_{1}[u1,v1] } = { F_{4}(u2,v2) where u2 is Element of F_{1}(), v2 is Element of F_{2}() : P_{1}[u2,v2] }

provided
A1:
for u being Element of F_{1}()

for v being Element of F_{2}() st P_{1}[u,v] holds

F_{3}(u,v) = F_{4}(u,v)

for v being Element of F

F

proof end;

scheme :: LFUZZY_0:sch 4

FraenkelF699R{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}( set , set ) -> set , F_{4}( set , set ) -> set , P_{1}[ set , set ], P_{2}[ set , set ] } :

FraenkelF699R{ F

{ F_{3}(u1,v1) where u1 is Element of F_{1}(), v1 is Element of F_{2}() : P_{1}[u1,v1] } = { F_{4}(u2,v2) where u2 is Element of F_{1}(), v2 is Element of F_{2}() : P_{2}[u2,v2] }

provided
A1:
for u being Element of F_{1}()

for v being Element of F_{2}() holds

( P_{1}[u,v] iff P_{2}[u,v] )
and

A2: for u being Element of F_{1}()

for v being Element of F_{2}() st P_{1}[u,v] holds

F_{3}(u,v) = F_{4}(u,v)

for v being Element of F

( P

A2: for u being Element of F

for v being Element of F

F

proof end;

scheme :: LFUZZY_0:sch 5

SupCommutativity{ F_{1}() -> complete LATTICE, F_{2}() -> non empty set , F_{3}() -> non empty set , F_{4}( set , set ) -> Element of F_{1}(), F_{5}( set , set ) -> Element of F_{1}(), P_{1}[ set ], P_{2}[ set ] } :

SupCommutativity{ F

"\/" ( { ("\/" ( { F_{4}(x,y) where y is Element of F_{3}() : P_{2}[y] } ,F_{1}())) where x is Element of F_{2}() : P_{1}[x] } ,F_{1}()) = "\/" ( { ("\/" ( { F_{5}(x9,y9) where x9 is Element of F_{2}() : P_{1}[x9] } ,F_{1}())) where y9 is Element of F_{3}() : P_{2}[y9] } ,F_{1}())

provided
A1:
for x being Element of F_{2}()

for y being Element of F_{3}() st P_{1}[x] & P_{2}[y] holds

F_{4}(x,y) = F_{5}(x,y)

for y being Element of F

F

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.]))

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)

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;