:: LFUZZY_0 semantic presentation

definition

let c₁ be RelStr ;
attr a₁ is real means :Def1: :: LFUZZY_0:def 1
( the carrier of a₁ c= REAL & ( for b₁, b₂ being real number st b₁ in the carrier of a₁ & b₂ in the carrier of a₁ holds
( [b₁,b₂] in the InternalRel of a₁ iff b₁ <= b₂ ) ) );

end;

:: deftheorem Def1 defines real LFUZZY_0:def 1 :

definition

let c₁ be RelStr ;
attr a₁ is interval means :Def2: :: LFUZZY_0:def 2
( a₁ is real & ex b₁, b₂ being real number st
( b₁ <= b₂ & the carrier of a₁ = [.b₁,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 b₁ being Subset of REAL ex b₂ being strict RelStr st
( the carrier of b₂ = b₁ & b₂ is real )

proof end;

registration

cluster non empty strict real interval RelStr ;
existence

proof end;

end;

theorem Th2: :: LFUZZY_0:2

for b₁, b₂ being real RelStr st the carrier of b₁ = the carrier of b₂ holds
RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #)

proof end;

registration

let c₁ be non empty real RelStr ;
cluster -> real Element of the carrier of a₁;
coherence

proof end;

end;

definition

let c₁ be Subset of REAL ;
func RealPoset c₁ -> strict real RelStr means :Def3: :: LFUZZY_0:def 3
the carrier of a₂ = a₁;
existence

proof end;

uniqueness by Th2;

end;

:: deftheorem Def3 defines RealPoset LFUZZY_0:def 3 :

registration

let c₁ be non empty Subset of REAL ;
cluster RealPoset a₁ -> non empty strict real ;
coherence

proof end;

end;

notation

let c₁ be RelStr ;
let c₂, c₃ be Element of c₁;
synonym c₂ <<= c₃ for c₂ <= c₃;
synonym c₃ >>= c₂ for c₂ <= c₃;
antonym c₂ ~<= c₃ for c₂ <= c₃;
antonym c₃ ~>= c₂ for c₂ <= c₃;

end;

notation

let c₁, c₂ be real number ;
synonym c₁ <R= c₂ for c₁ <= c₂;
antonym c₂ <R c₁ for c₁ <= c₂;
synonym c₂ >R= c₁ for c₁ <= c₂;
antonym c₁ >R c₂ for c₁ <= c₂;

end;

theorem Th3: :: LFUZZY_0:3

for b₁ being non empty real RelStr
for b₂, b₃ being Element of b₁ holds
( b₂ <R= b₃ iff b₂ <<= b₃ )

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 c₁ be non empty real RelStr ;
let c₂, c₃ be Element of c₁;
redefine func max as max c₂,c₃ -> Element of a₁;
coherence by SQUARE_1:49;

end;

definition

let c₁ be non empty real RelStr ;
let c₂, c₃ be Element of c₁;
redefine func min as min c₂,c₃ -> Element of a₁;
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 b₁ being non empty real RelStr
for b₂, b₃ being Element of b₁ holds b₂ "\/" b₃ = max b₂,b₃

proof end;

theorem Th5: :: LFUZZY_0:5

for b₁ being non empty real RelStr
for b₂, b₃ being Element of b₁ holds b₂ "/\" b₃ = min b₂,b₃

proof end;

theorem Th6: :: LFUZZY_0:6

for b₁ being non empty real RelStr holds
( ex b₂ being real number st
( b₂ in the carrier of b₁ & ( for b₃ being real number st b₃ in the carrier of b₁ holds
b₂ <= b₃ ) ) iff b₁ is lower-bounded )

proof end;

theorem Th7: :: LFUZZY_0:7

for b₁ being non empty real RelStr holds
( ex b₂ being real number st
( b₂ in the carrier of b₁ & ( for b₃ being real number st b₃ in the carrier of b₁ holds
b₂ >= b₃ ) ) iff b₁ is upper-bounded )

proof end;

registration

cluster non empty interval -> non empty bounded RelStr ;
coherence

proof end;

end;

theorem Th8: :: LFUZZY_0:8

for b₁ being non empty interval RelStr
for b₂ being set holds ex_sup_of b₂,b₁

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 b₁ being non empty set
for b₂ being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of b₁ st ( for b₃ being Element of b₁ holds b₂ . b₃ is sup-Semilattice ) holds
product b₂ is with_suprema

proof end;

theorem Th10: :: LFUZZY_0:10

for b₁ being non empty set
for b₂ being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of b₁ st ( for b₃ being Element of b₁ holds b₂ . b₃ is Semilattice ) holds
product b₂ is with_infima

proof end;

theorem Th11: :: LFUZZY_0:11

for b₁ being non empty set
for b₂ being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of b₁ st ( for b₃ being Element of b₁ holds b₂ . b₃ is Semilattice ) holds
for b₃, b₄ being Element of (product b₂)
for b₅ being Element of b₁ holds (b₃ "/\" b₄) . b₅ = (b₃ . b₅) "/\" (b₄ . b₅)

proof end;

theorem Th12: :: LFUZZY_0:12

for b₁ being non empty set
for b₂ being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of b₁ st ( for b₃ being Element of b₁ holds b₂ . b₃ is sup-Semilattice ) holds
for b₃, b₄ being Element of (product b₂)
for b₅ being Element of b₁ holds (b₃ "\/" b₄) . b₅ = (b₃ . b₅) "\/" (b₄ . b₅)

proof end;

theorem Th13: :: LFUZZY_0:13

for b₁ being non empty set
for b₂ being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of b₁ st ( for b₃ being Element of b₁ holds b₂ . b₃ is complete Heyting LATTICE ) holds
( product b₂ is complete & product b₂ is Heyting )

proof end;

registration

let c₁ be non empty set ;
let c₂ be complete Heyting LATTICE;
cluster a₂ |^ a₁ -> Heyting ;
coherence

proof end;

end;

definition

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

end;

:: deftheorem Def4 defines FuzzyLattice LFUZZY_0:def 4 :

theorem Th14: :: LFUZZY_0:14

for b₁ being non empty set holds the carrier of (FuzzyLattice b₁) = Funcs b₁,[.0,1.]

proof end;

Lemma18: for b₁ being non empty set holds FuzzyLattice b₁ is constituted-Functions

proof end;

registration

let c₁ be non empty set ;
cluster FuzzyLattice a₁ -> complete Heyting constituted-Functions ;
coherence by Lemma18;

end;

theorem Th15: :: LFUZZY_0:15

for b₁ being complete Heyting LATTICE
for b₂ being Subset of b₁
for b₃ being Element of b₁ holds ("\/" b₂,b₁) "/\" b₃ = "\/" { (b₄ "/\" b₃) where B is Element of b₁ : b₄ in b₂ } ,b₁

proof end;

Lemma20: for b₁ being non empty set
for b₂ being Element of (FuzzyLattice b₁) holds b₂ is Membership_Func of b₁

proof end;

definition

let c₁ be non empty set ;
let c₂ be Element of (FuzzyLattice c₁);
func @ c₂ -> Membership_Func of a₁ equals :: LFUZZY_0:def 5
a₂;
coherence by Lemma20;

end;

:: deftheorem Def5 defines @ LFUZZY_0:def 5 :

Lemma21: for b₁ being non empty set
for b₂ being Membership_Func of b₁ holds b₂ is Element of (FuzzyLattice b₁)

proof end;

definition

let c₁ be non empty set ;
let c₂ be Membership_Func of c₁;
func c₁,c₂ @ -> Element of (FuzzyLattice a₁) equals :: LFUZZY_0:def 6
a₂;
coherence by Lemma21;

end;

:: deftheorem Def6 defines @ LFUZZY_0:def 6 :

definition

let c₁ be non empty set ;
let c₂ be Membership_Func of c₁;
let c₃ be Element of c₁;
redefine func . as c₂ . c₃ -> Element of (RealPoset [.0,1.]);
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be Element of (FuzzyLattice c₁);
let c₃ be Element of c₁;
redefine func . as c₂ . c₃ -> Element of (RealPoset [.0,1.]);
coherence

proof end;

end;

theorem Th16: :: LFUZZY_0:16

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds
( ( for b₄ being Element of b₁ holds b₂ . b₄ <R= b₃ . b₄ ) iff b₁,b₂ @ <<= b₁,b₃ @ )

proof end;

theorem Th17: :: LFUZZY_0:17

for b₁ being non empty set
for b₂, b₃ being Element of (FuzzyLattice b₁) holds
( b₂ <<= b₃ iff for b₄ being Element of b₁ holds (@ b₂) . b₄ <R= (@ b₃) . b₄ )

proof end;

theorem Th18: :: LFUZZY_0:18

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds max b₂,b₃ = (b₁,b₂ @ ) "\/" (b₁,b₃ @ )

proof end;

theorem Th19: :: LFUZZY_0:19

for b₁ being non empty set
for b₂, b₃ being Element of (FuzzyLattice b₁) holds b₂ "\/" b₃ = max (@ b₂),(@ b₃)

proof end;

theorem Th20: :: LFUZZY_0:20

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds min b₂,b₃ = (b₁,b₂ @ ) "/\" (b₁,b₃ @ )

proof end;

theorem Th21: :: LFUZZY_0:21

for b₁ being non empty set
for b₂, b₃ being Element of (FuzzyLattice b₁) holds b₂ "/\" b₃ = min (@ b₂),(@ b₃)

proof end;

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

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

proof end;

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

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

proof end;

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

{ F₃(b₁,b₂) where B is Element of F₁(), B is Element of F₂() : P₁[b₁,b₂] } = { F₄(b₁,b₂) where B is Element of F₁(), B is Element of F₂() : P₁[b₁,b₂] }

provided

E25: for b₁ being Element of F₁()
for b₂ being Element of F₂() st P₁[b₁,b₂] holds
F₃(b₁,b₂) = F₄(b₁,b₂)

proof end;

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

{ F₃(b₁,b₂) where B is Element of F₁(), B is Element of F₂() : P₁[b₁,b₂] } = { F₄(b₁,b₂) where B is Element of F₁(), B is Element of F₂() : P₂[b₁,b₂] }

provided

E25: for b₁ being Element of F₁()
for b₂ being Element of F₂() holds
( P₁[b₁,b₂] iff P₂[b₁,b₂] ) and
E26: for b₁ being Element of F₁()
for b₂ being Element of F₂() st P₁[b₁,b₂] holds
F₃(b₁,b₂) = F₄(b₁,b₂)

proof end;

scheme :: LFUZZY_0:sch 5
s5{ 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₄(b₁,b₂) where B is Element of F₃() : P₂[b₂] } ,F₁()) where B is Element of F₂() : P₁[b₁] } ,F₁() = "\/" { ("\/" { F₅(b₂,b₁) where B is Element of F₂() : P₁[b₂] } ,F₁()) where B is Element of F₃() : P₂[b₁] } ,F₁()

provided

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

proof end;

Lemma25: for b₁ being Element of (RealPoset [.0,1.]) holds b₁ is Real

proof end;

Lemma26: for b₁, b₂, b₃ being non empty set
for b₄ being RMembership_Func of b₁,b₂
for b₅ being RMembership_Func of b₂,b₃
for b₆ being Element of b₁
for b₇ being Element of b₃ holds
( rng (min b₄,b₅,b₆,b₇) = { ((b₄ . [b₆,b₈]) "/\" (b₅ . [b₈,b₇])) where B is Element of b₂ : verum } & rng (min b₄,b₅,b₆,b₇) <> {} )

proof end;

theorem Th22: :: LFUZZY_0:22

for b₁, b₂, b₃ being non empty set
for b₄ being RMembership_Func of b₁,b₂
for b₅ being RMembership_Func of b₂,b₃
for b₆ being Element of b₁
for b₇ being Element of b₃ holds (b₄ (#) b₅) . [b₆,b₇] = "\/" { ((b₄ . [b₆,b₈]) "/\" (b₅ . [b₈,b₇])) where B is Element of b₂ : verum } ,(RealPoset [.0,1.])

proof end;

Lemma28: for b₁, b₂, b₃ being non empty set
for b₄ being RMembership_Func of b₁,b₂
for b₅ being RMembership_Func of b₂,b₃
for b₆ being Element of b₁
for b₇ being Element of b₃
for b₈ being Element of (RealPoset [.0,1.]) holds ((b₄ (#) b₅) . [b₆,b₇]) "/\" b₈ = "\/" { (((b₄ . [b₆,b₉]) "/\" (b₅ . [b₉,b₇])) "/\" b₈) where B is Element of b₂ : verum } ,(RealPoset [.0,1.])

proof end;

Lemma29: for b₁, b₂, b₃ being non empty set
for b₄ being RMembership_Func of b₁,b₂
for b₅ being RMembership_Func of b₂,b₃
for b₆ being Element of b₁
for b₇ being Element of b₃
for b₈ being Element of (RealPoset [.0,1.]) holds b₈ "/\" ((b₄ (#) b₅) . [b₆,b₇]) = "\/" { ((b₈ "/\" (b₄ . [b₆,b₉])) "/\" (b₅ . [b₉,b₇])) where B is Element of b₂ : verum } ,(RealPoset [.0,1.])

proof end;

theorem Th23: :: LFUZZY_0:23

for b₁, b₂, b₃, b₄ being non empty set
for b₅ being RMembership_Func of b₁,b₂
for b₆ being RMembership_Func of b₂,b₃
for b₇ being RMembership_Func of b₃,b₄ holds (b₅ (#) b₆) (#) b₇ = b₅ (#) (b₆ (#) b₇)

proof end;