:: LFUZZY_1 semantic presentation

Lemma1: for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₃ <= b₄ holds
min b₁,b₃ <= min b₂,b₄

proof end;

registration

let c₁ be non empty set ;
cluster -> real-yielding Membership_Func of a₁;
coherence ;

end;

definition

let c₁, c₂ be non empty set ;
let c₃, c₄ be RMembership_Func of c₁,c₂;
redefine pred is_less_than as c₃ is_less_than c₄ means :Def1: :: LFUZZY_1:def 1
for b₁ being Element of a₁
for b₂ being Element of a₂ holds a₃ . [b₁,b₂] <= a₄ . [b₁,b₂];
compatibility

proof end;

end;

:: deftheorem Def1 defines is_less_than LFUZZY_1:def 1 :

theorem Th1: :: LFUZZY_1:1

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ st ( for b₄ being Element of b₁ holds b₂ . b₄ = b₃ . b₄ ) holds
b₂ = b₃

proof end;

theorem Th2: :: LFUZZY_1:2

for b₁, b₂ being non empty set
for b₃, b₄ being RMembership_Func of b₁,b₂ st ( for b₅ being Element of b₁
for b₆ being Element of b₂ holds b₃ . [b₅,b₆] = b₄ . [b₅,b₆] ) holds
b₃ = b₄

proof end;

theorem Th3: :: LFUZZY_1:3

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds
( b₂ = b₃ iff ( b₃ c= & b₂ c= ) )

proof end;

theorem Th4: :: LFUZZY_1:4

for b₁ being non empty set
for b₂ being Membership_Func of b₁ holds b₂ c= ;

theorem Th5: :: LFUZZY_1:5

for b₁ being non empty set
for b₂, b₃, b₄ being Membership_Func of b₁ st b₃ c= & b₄ c= holds
b₄ c=

proof end;

theorem Th6: :: LFUZZY_1:6

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

proof end;

definition

let c₁ be non empty set ;
let c₂, c₃ be Membership_Func of c₁;
redefine func min as min c₂,c₃ -> Membership_Func of a₁;
commutativity ;
redefine func max as max c₂,c₃ -> Membership_Func of a₁;
commutativity ;

end;

theorem Th7: :: LFUZZY_1:7

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds b₂ c=

proof end;

theorem Th8: :: LFUZZY_1:8

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ holds max b₂,b₃ c=

proof end;

definition

let c₁ be non empty set ;
let c₂ be RMembership_Func of c₁,c₁;
attr a₂ is reflexive means :Def2: :: LFUZZY_1:def 2
a₂ c= ;

end;

:: deftheorem Def2 defines reflexive LFUZZY_1:def 2 :

definition

let c₁ be non empty set ;
let c₂ be RMembership_Func of c₁,c₁;
redefine attr a₂ is reflexive means :Def3: :: LFUZZY_1:def 3
for b₁ being Element of a₁ holds a₂ . [b₁,b₁] = 1;
compatibility

proof end;

end;

:: deftheorem Def3 defines reflexive LFUZZY_1:def 3 :

definition

let c₁ be non empty set ;
let c₂ be RMembership_Func of c₁,c₁;
attr a₂ is symmetric means :Def4: :: LFUZZY_1:def 4
converse a₂ = a₂;

end;

:: deftheorem Def4 defines symmetric LFUZZY_1:def 4 :

definition

let c₁ be non empty set ;
let c₂ be RMembership_Func of c₁,c₁;
redefine attr a₂ is symmetric means :Def5: :: LFUZZY_1:def 5
for b₁, b₂ being Element of a₁ holds a₂ . [b₁,b₂] = a₂ . [b₂,b₁];
compatibility

proof end;

end;

:: deftheorem Def5 defines symmetric LFUZZY_1:def 5 :

definition

let c₁ be non empty set ;
let c₂ be RMembership_Func of c₁,c₁;
attr a₂ is transitive means :Def6: :: LFUZZY_1:def 6
a₂ c= ;

end;

:: deftheorem Def6 defines transitive LFUZZY_1:def 6 :

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

definition

let c₁ be non empty set ;
let c₂ be RMembership_Func of c₁,c₁;
redefine attr a₂ is transitive means :: LFUZZY_1:def 7
for b₁, b₂, b₃ being Element of a₁ holds (a₂ . [b₁,b₂]) "/\" (a₂ . [b₂,b₃]) <<= a₂ . [b₁,b₃];
compatibility

proof end;

end;

:: deftheorem Def7 defines transitive LFUZZY_1:def 7 :

definition

let c₁ be non empty set ;
let c₂ be RMembership_Func of c₁,c₁;
attr a₂ is antisymmetric means :Def8: :: LFUZZY_1:def 8
for b₁, b₂ being Element of a₁ st a₂ . [b₁,b₂] <> 0 & a₂ . [b₂,b₁] <> 0 holds
b₁ = b₂;

end;

:: deftheorem Def8 defines antisymmetric LFUZZY_1:def 8 :

definition

let c₁ be non empty set ;
let c₂ be RMembership_Func of c₁,c₁;
redefine attr a₂ is antisymmetric means :: LFUZZY_1:def 9
for b₁, b₂ being Element of a₁ st a₂ . [b₁,b₂] <> 0 & b₁ <> b₂ holds
a₂ . [b₂,b₁] = 0;
compatibility

proof end;

end;

:: deftheorem Def9 defines antisymmetric LFUZZY_1:def 9 :

registration

let c₁ be non empty set ;
cluster Imf a₁,a₁ -> reflexive symmetric transitive antisymmetric ;
coherence

proof end;

end;

registration

let c₁ be non empty set ;
cluster reflexive symmetric transitive antisymmetric Membership_Func of [:a₁,a₁:];
existence

proof end;

end;

theorem Th9: :: LFUZZY_1:9

for b₁ being non empty set
for b₂, b₃ being RMembership_Func of b₁,b₁ st b₂ is symmetric & b₃ is symmetric holds
converse (min b₂,b₃) = min b₂,b₃

proof end;

theorem Th10: :: LFUZZY_1:10

for b₁ being non empty set
for b₂, b₃ being RMembership_Func of b₁,b₁ st b₂ is symmetric & b₃ is symmetric holds
converse (max b₂,b₃) = max b₂,b₃

proof end;

registration

let c₁ be non empty set ;
let c₂, c₃ be symmetric RMembership_Func of c₁,c₁;
cluster min a₂,a₃ -> symmetric ;
coherence

proof end;

cluster max a₂,a₃ -> symmetric ;
coherence

proof end;

end;

theorem Th11: :: LFUZZY_1:11

for b₁ being non empty set
for b₂, b₃ being RMembership_Func of b₁,b₁ st b₂ is transitive & b₃ is transitive holds
min b₂,b₃ c=

proof end;

registration

let c₁ be non empty set ;
let c₂, c₃ be transitive RMembership_Func of c₁,c₁;
cluster min a₂,a₃ -> transitive ;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be non empty set ;
redefine func chi as chi c₁,c₂ -> Membership_Func of a₂;
coherence

proof end;

end;

theorem Th12: :: LFUZZY_1:12

for b₁ being non empty set
for b₂ being Relation of b₁ st b₂ is_reflexive_in b₁ holds
chi b₂,[:b₁,b₁:] is reflexive

proof end;

theorem Th13: :: LFUZZY_1:13

for b₁ being non empty set
for b₂ being Relation of b₁ st b₂ is antisymmetric holds
chi b₂,[:b₁,b₁:] is antisymmetric

proof end;

theorem Th14: :: LFUZZY_1:14

for b₁ being non empty set
for b₂ being Relation of b₁ st b₂ is symmetric holds
chi b₂,[:b₁,b₁:] is symmetric

proof end;

theorem Th15: :: LFUZZY_1:15

for b₁ being non empty set
for b₂ being Relation of b₁ st b₂ is transitive holds
chi b₂,[:b₁,b₁:] is transitive

proof end;

theorem Th16: :: LFUZZY_1:16

for b₁ being non empty set holds
( Zmf b₁,b₁ is symmetric & Zmf b₁,b₁ is antisymmetric & Zmf b₁,b₁ is transitive )

proof end;

theorem Th17: :: LFUZZY_1:17

for b₁ being non empty set holds
( Umf b₁,b₁ is symmetric & Umf b₁,b₁ is transitive & Umf b₁,b₁ is reflexive )

proof end;

theorem Th18: :: LFUZZY_1:18

for b₁ being non empty set
for b₂ being RMembership_Func of b₁,b₁ holds max b₂,(converse b₂) is symmetric

proof end;

theorem Th19: :: LFUZZY_1:19

for b₁ being non empty set
for b₂ being RMembership_Func of b₁,b₁ holds min b₂,(converse b₂) is symmetric

proof end;

theorem Th20: :: LFUZZY_1:20

for b₁ being non empty set
for b₂, b₃ being RMembership_Func of b₁,b₁ st b₃ is symmetric & b₃ c= holds
b₃ c=

proof end;

theorem Th21: :: LFUZZY_1:21

for b₁ being non empty set
for b₂, b₃ being RMembership_Func of b₁,b₁ st b₃ is symmetric & b₂ c= holds
min b₂,(converse b₂) c=

proof end;

definition

let c₁ be non empty set ;
let c₂ be RMembership_Func of c₁,c₁;
let c₃ be natural number ;
func c₃ iter c₂ -> RMembership_Func of a₁,a₁ means :Def10: :: LFUZZY_1:def 10
ex b₁ being Function of NAT , Funcs [:a₁,a₁:],[.0,1.] st
( a₄ = b₁ . a₃ & b₁ . 0 = Imf a₁,a₁ & ( for b₂ being natural number ex b₃ being RMembership_Func of a₁,a₁ st
( b₁ . b₂ = b₃ & b₁ . (b₂ + 1) = b₃ (#) a₂ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines iter LFUZZY_1:def 10 :

theorem Th22: :: LFUZZY_1:22

for b₁ being non empty set
for b₂ being RMembership_Func of b₁,b₁ holds (Imf b₁,b₁) (#) b₂ = b₂

proof end;

theorem Th23: :: LFUZZY_1:23

for b₁ being non empty set
for b₂ being RMembership_Func of b₁,b₁ holds b₂ (#) (Imf b₁,b₁) = b₂

proof end;

theorem Th24: :: LFUZZY_1:24

for b₁ being non empty set
for b₂ being RMembership_Func of b₁,b₁ holds 0 iter b₂ = Imf b₁,b₁

proof end;

theorem Th25: :: LFUZZY_1:25

for b₁ being non empty set
for b₂ being RMembership_Func of b₁,b₁ holds 1 iter b₂ = b₂

proof end;

theorem Th26: :: LFUZZY_1:26

for b₁ being non empty set
for b₂ being RMembership_Func of b₁,b₁
for b₃ being natural number holds (b₃ + 1) iter b₂ = (b₃ iter b₂) (#) b₂

proof end;

theorem Th27: :: LFUZZY_1:27

for b₁ being non empty set
for b₂ being RMembership_Func of b₁,b₁
for b₃, b₄ being natural number holds (b₃ + b₄) iter b₂ = (b₃ iter b₂) (#) (b₄ iter b₂)

proof end;

theorem Th28: :: LFUZZY_1:28

for b₁ being non empty set
for b₂ being RMembership_Func of b₁,b₁
for b₃, b₄ being natural number holds (b₃ * b₄) iter b₂ = b₃ iter (b₄ iter b₂)

proof end;

definition

let c₁ be non empty set ;
let c₂ be RMembership_Func of c₁,c₁;
func TrCl c₂ -> RMembership_Func of a₁,a₁ equals :: LFUZZY_1:def 11
"\/" { (b₁ iter a₂) where B is Nat : b₁ > 0 } ,(FuzzyLattice [:a₁,a₁:]);
coherence

proof end;

end;

:: deftheorem Def11 defines TrCl LFUZZY_1:def 11 :

theorem Th29: :: LFUZZY_1:29

for b₁ being non empty set
for b₂ being RMembership_Func of b₁,b₁
for b₃, b₄ being Element of b₁ holds (TrCl b₂) . [b₃,b₄] = "\/" (pi { (b₅ iter b₂) where B is Nat : b₅ > 0 } ,[b₃,b₄]),(RealPoset [.0,1.])

proof end;

theorem Th30: :: LFUZZY_1:30

for b₁ being non empty set
for b₂ being RMembership_Func of b₁,b₁ holds TrCl b₂ c=

proof end;

theorem Th31: :: LFUZZY_1:31

for b₁ being non empty set
for b₂ being RMembership_Func of b₁,b₁
for b₃ being natural number st b₃ > 0 holds
TrCl b₂ c=

proof end;

theorem Th32: :: LFUZZY_1:32

for b₁ being non empty set
for b₂ being Subset of (FuzzyLattice b₁)
for b₃ being Element of b₁ holds ("\/" b₂,(FuzzyLattice b₁)) . b₃ = "\/" (pi b₂,b₃),(RealPoset [.0,1.])

proof end;

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

proof end;

theorem Th33: :: LFUZZY_1:33

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;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

Lemma35: for b₁ being non empty set
for b₂ being RMembership_Func of b₁,b₁
for b₃ being Subset of (FuzzyLattice [:b₁,b₁:])
for b₄, b₅ being Element of b₁ holds { ((b₂ (#) (@ b₆)) . [b₄,b₅]) where B is Element of (FuzzyLattice [:b₁,b₁:]) : b₆ in b₃ } = pi { (b₂ (#) (@ b₆)) where B is Element of (FuzzyLattice [:b₁,b₁:]) : b₆ in b₃ } ,[b₄,b₅]

proof end;

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

proof end;

theorem Th34: :: LFUZZY_1:34

for b₁ being non empty set
for b₂ being RMembership_Func of b₁,b₁
for b₃ being Subset of (FuzzyLattice [:b₁,b₁:]) holds b₂ (#) (@ ("\/" b₃,(FuzzyLattice [:b₁,b₁:]))) = "\/" { (b₂ (#) (@ b₄)) where B is Element of (FuzzyLattice [:b₁,b₁:]) : b₄ in b₃ } ,(FuzzyLattice [:b₁,b₁:])

proof end;

theorem Th35: :: LFUZZY_1:35

for b₁ being non empty set
for b₂ being RMembership_Func of b₁,b₁
for b₃ being Subset of (FuzzyLattice [:b₁,b₁:]) holds (@ ("\/" b₃,(FuzzyLattice [:b₁,b₁:]))) (#) b₂ = "\/" { ((@ b₄) (#) b₂) where B is Element of (FuzzyLattice [:b₁,b₁:]) : b₄ in b₃ } ,(FuzzyLattice [:b₁,b₁:])

proof end;

theorem Th36: :: LFUZZY_1:36

for b₁ being non empty set
for b₂ being RMembership_Func of b₁,b₁ holds (TrCl b₂) (#) (TrCl b₂) = "\/" { ((b₃ iter b₂) (#) (b₄ iter b₂)) where B is Nat, B is Nat : ( b₃ > 0 & b₄ > 0 ) } ,(FuzzyLattice [:b₁,b₁:])

proof end;

registration

let c₁ be non empty set ;
let c₂ be RMembership_Func of c₁,c₁;
cluster TrCl a₂ -> transitive ;
coherence

proof end;

end;

theorem Th37: :: LFUZZY_1:37

for b₁ being non empty set
for b₂ being RMembership_Func of b₁,b₁
for b₃ being natural number st b₂ is transitive & b₃ > 0 holds
b₂ c=

proof end;

theorem Th38: :: LFUZZY_1:38

for b₁ being non empty set
for b₂ being RMembership_Func of b₁,b₁ st b₂ is transitive holds
b₂ = TrCl b₂

proof end;

theorem Th39: :: LFUZZY_1:39

for b₁ being non empty set
for b₂, b₃ being RMembership_Func of b₁,b₁
for b₄ being natural number st b₃ c= holds
b₄ iter b₃ c=

proof end;

theorem Th40: :: LFUZZY_1:40

for b₁ being non empty set
for b₂, b₃ being RMembership_Func of b₁,b₁ st b₃ is transitive & b₃ c= holds
b₃ c=

proof end;