:: LFUZZY_0 semantic presentation

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 :

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 :

registration

cluster interval -> non empty real RelStr ;
coherence

proof end;

end;

registration

cluster empty -> real RelStr ;
coherence

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 non empty strict real interval RelStr ;
existence

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

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

proof end;

uniqueness by Th2;

end;

:: deftheorem Def3 defines RealPoset LFUZZY_0:def 3 :

registration

let X be non empty Subset of REAL ;
cluster RealPoset X -> non empty strict real ;
coherence

proof end;

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;

notation

let x, y be real number ;
synonym x <R= y for x <= y;
antonym y <R x for x <= y;
synonym y >R= x for x <= y;
antonym x >R y 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 <R= y iff x <<= y )

proof end;

registration

cluster real -> reflexive transitive antisymmetric RelStr ;
coherence

proof end;

end;

registration

cluster non empty real -> non empty reflexive transitive antisymmetric connected real RelStr ;
coherence

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 by SQUARE_1:49;

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 by SQUARE_1:38;

end;

registration

cluster non empty real -> non empty reflexive transitive antisymmetric connected with_suprema with_infima real RelStr ;
coherence ;

end;

theorem Th4: :: LFUZZY_0:4

for R being non empty real RelStr
for a, b being Element of R holds a "\/" b = max a,b

proof end;

theorem Th5: :: LFUZZY_0:5

for R being non empty real RelStr
for a, b being Element of R holds a "/\" b = min a,b

proof end;

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

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 reflexive transitive antisymmetric bounded connected with_suprema with_infima complete real interval RelStr ;
coherence

proof end;

end;

registration

cluster -> distributive RelStr ;
coherence

proof end;

end;

registration

cluster non empty interval -> non empty reflexive transitive antisymmetric bounded connected with_suprema with_infima complete distributive Heyting real interval RelStr ;
coherence

proof end;

end;

registration

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

proof end;

end;

registration

cluster RealPoset [.0,1.] -> non empty strict reflexive transitive antisymmetric bounded connected with_suprema with_infima complete distributive Heyting real interval ;
coherence

proof end;

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

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 ;

end;

:: deftheorem defines FuzzyLattice LFUZZY_0:def 4 :

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 Heyting constituted-Functions ;
coherence 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 by Lm2;

end;

:: deftheorem defines @ LFUZZY_0:def 5 :

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

end;

:: deftheorem defines @ LFUZZY_0:def 6 :

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

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

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 <R= 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 <R= (@ 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
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 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
FraenkelF'R'{ 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
FraenkelF6''R{ 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₅(x',y') where x' is Element of F₂() : P₁[x'] } ,F₁()) where y' is Element of F₃() : P₂[y'] } ,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 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;