:: FUZZY_4 semantic presentation

registration

let c₁ be non empty set ;
let c₂ be Membership_Func of c₁;
cluster K11(a₂) -> non empty ;
coherence

proof end;

end;

theorem Th1: :: FUZZY_4:1

for b₁ being non empty set
for b₂ being Membership_Func of b₁ holds
( rng b₂ is bounded & ( for b₃ being set st b₃ in dom b₂ holds
b₂ . b₃ <= sup (rng b₂) ) & ( for b₃ being set st b₃ in dom b₂ holds
b₂ . b₃ >= inf (rng b₂) ) )

proof end;

theorem Th2: :: FUZZY_4:2

for b₁ being non empty set
for b₂, b₃ being Membership_Func of b₁ st ( for b₄ being set st b₄ in b₁ holds
b₂ . b₄ <= b₃ . b₄ ) holds
sup (rng b₂) <= sup (rng b₃)

proof end;

theorem Th3: :: FUZZY_4:3

for b₁, b₂ being non empty set
for b₃ being RMembership_Func of b₁,b₂
for b₄ being Element of [:b₁,b₂:] holds
( 0 <= b₃ . b₄ & b₃ . b₄ <= 1 )

proof end;

theorem Th4: :: FUZZY_4:4

for b₁, b₂ being non empty set
for b₃ being RMembership_Func of b₁,b₂
for b₄, b₅ being set st [b₄,b₅] in [:b₁,b₂:] holds
( 0 <= b₃ . [b₄,b₅] & b₃ . [b₄,b₅] <= 1 ) by Th3;

definition

let c₁, c₂ be non empty set ;
let c₃ be RMembership_Func of c₂,c₁;
func converse c₃ -> RMembership_Func of a₁,a₂ means :Def1: :: FUZZY_4:def 1
for b₁, b₂ being set st [b₁,b₂] in [:a₁,a₂:] holds
a₄ . [b₁,b₂] = a₃ . [b₂,b₁];
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines converse FUZZY_4:def 1 :

theorem Th5: :: FUZZY_4:5

for b₁, b₂ being non empty set
for b₃ being RMembership_Func of b₁,b₂ holds converse (converse b₃) = b₃

proof end;

theorem Th6: :: FUZZY_4:6

for b₁, b₂ being non empty set
for b₃ being RMembership_Func of b₁,b₂ holds 1_minus (converse b₃) = converse (1_minus b₃)

proof end;

theorem Th7: :: FUZZY_4:7

for b₁, b₂ being non empty set
for b₃, b₄ being RMembership_Func of b₁,b₂ holds converse (max b₃,b₄) = max (converse b₃),(converse b₄)

proof end;

theorem Th8: :: FUZZY_4:8

for b₁, b₂ being non empty set
for b₃, b₄ being RMembership_Func of b₁,b₂ holds converse (min b₃,b₄) = min (converse b₃),(converse b₄)

proof end;

theorem Th9: :: FUZZY_4:9

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

proof end;

theorem Th10: :: FUZZY_4:10

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

proof end;

theorem Th11: :: FUZZY_4:11

for b₁, b₂ being non empty set
for b₃, b₄ being RMembership_Func of b₁,b₂ holds converse (b₃ \ b₄) = (converse b₃) \ (converse b₄)

proof end;

theorem Th12: :: FUZZY_4:12

for b₁, b₂ being non empty set
for b₃, b₄ being RMembership_Func of b₁,b₂ holds converse (b₃ \+\ b₄) = (converse b₃) \+\ (converse b₄)

proof end;

definition

let c₁, c₂, c₃ be non empty set ;
let c₄ be RMembership_Func of c₁,c₂;
let c₅ be RMembership_Func of c₂,c₃;
let c₆, c₇ be set ;
assume E8: ( c₆ in c₁ & c₇ in c₃ ) ;
func min c₄,c₅,c₆,c₇ -> Membership_Func of a₂ means :Def2: :: FUZZY_4:def 2
for b₁ being Element of a₂ holds a₈ . b₁ = min (a₄ . [a₆,b₁]),(a₅ . [b₁,a₇]);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines min FUZZY_4:def 2 :

definition

let c₁, c₂, c₃ be non empty set ;
let c₄ be RMembership_Func of c₁,c₂;
let c₅ be RMembership_Func of c₂,c₃;
func c₄ (#) c₅ -> RMembership_Func of a₁,a₃ means :Def3: :: FUZZY_4:def 3
for b₁, b₂ being set st [b₁,b₂] in [:a₁,a₃:] holds
a₆ . [b₁,b₂] = sup (rng (min a₄,a₅,b₁,b₂));
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines (#) FUZZY_4:def 3 :

Lemma10: for b₁, b₂, b₃ being non empty set
for b₄ being RMembership_Func of b₁,b₂
for b₅, b₆ being RMembership_Func of b₂,b₃
for b₇, b₈ being set st b₇ in b₁ & b₈ in b₃ holds
sup (rng (min b₄,(max b₅,b₆),b₇,b₈)) = max (sup (rng (min b₄,b₅,b₇,b₈))),(sup (rng (min b₄,b₆,b₇,b₈)))

proof end;

theorem Th13: :: FUZZY_4:13

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

proof end;

Lemma11: for b₁, b₂, b₃ being non empty set
for b₄, b₅ being RMembership_Func of b₁,b₂
for b₆ being RMembership_Func of b₂,b₃
for b₇, b₈ being set st b₇ in b₁ & b₈ in b₃ holds
sup (rng (min (max b₄,b₅),b₆,b₇,b₈)) = max (sup (rng (min b₄,b₆,b₇,b₈))),(sup (rng (min b₅,b₆,b₇,b₈)))

proof end;

theorem Th14: :: FUZZY_4:14

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

proof end;

Lemma12: for b₁, b₂, b₃ being non empty set
for b₄ being RMembership_Func of b₁,b₂
for b₅, b₆ being RMembership_Func of b₂,b₃
for b₇, b₈ being set st b₇ in b₁ & b₈ in b₃ holds
sup (rng (min b₄,(min b₅,b₆),b₇,b₈)) <= min (sup (rng (min b₄,b₅,b₇,b₈))),(sup (rng (min b₄,b₆,b₇,b₈)))

proof end;

theorem Th15: :: FUZZY_4:15

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

proof end;

Lemma13: for b₁, b₂, b₃ being non empty set
for b₄, b₅ being RMembership_Func of b₁,b₂
for b₆ being RMembership_Func of b₂,b₃
for b₇, b₈ being set st b₇ in b₁ & b₈ in b₃ holds
sup (rng (min (min b₄,b₅),b₆,b₇,b₈)) <= min (sup (rng (min b₄,b₆,b₇,b₈))),(sup (rng (min b₅,b₆,b₇,b₈)))

proof end;

theorem Th16: :: FUZZY_4:16

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

proof end;

Lemma14: 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₆, b₇ being set st b₆ in b₁ & b₇ in b₃ holds
sup (rng (min (converse b₅),(converse b₄),b₇,b₆)) = sup (rng (min b₄,b₅,b₆,b₇))

proof end;

theorem Th17: :: FUZZY_4:17

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

proof end;

theorem Th18: :: FUZZY_4:18

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₃
for b₈, b₉ being set st b₈ in b₁ & b₉ in b₃ & ( for b₁₀ being set st b₁₀ in b₂ holds
( b₄ . [b₈,b₁₀] <= b₅ . [b₈,b₁₀] & b₆ . [b₁₀,b₉] <= b₇ . [b₁₀,b₉] ) ) holds
(b₄ (#) b₆) . [b₈,b₉] <= (b₅ (#) b₇) . [b₈,b₉]

proof end;

theorem Th19: :: FUZZY_4:19

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₁, c₂ be non empty set ;
func Imf c₁,c₂ -> RMembership_Func of a₁,a₂ means :: FUZZY_4:def 4
for b₁, b₂ being set st [b₁,b₂] in [:a₁,a₂:] holds
( ( b₁ = b₂ implies a₃ . [b₁,b₂] = 1 ) & ( not b₁ = b₂ implies a₃ . [b₁,b₂] = 0 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Imf FUZZY_4:def 4 :

theorem Th20: :: FUZZY_4:20

for b₁, b₂ being non empty set
for b₃ being Element of [:b₁,b₂:] holds
( (Zmf b₁,b₂) . b₃ = 0 & (Umf b₁,b₂) . b₃ = 1 )

proof end;

theorem Th21: :: FUZZY_4:21

for b₁, b₂ being non empty set
for b₃, b₄ being set st [b₃,b₄] in [:b₁,b₂:] holds
( (Zmf b₁,b₂) . [b₃,b₄] = 0 & (Umf b₁,b₂) . [b₃,b₄] = 1 ) by Th20;

Lemma17: for b₁, b₂, b₃ being non empty set
for b₄ being RMembership_Func of b₁,b₂
for b₅, b₆ being set st b₅ in b₃ & b₆ in b₂ holds
sup (rng (min (Zmf b₃,b₁),b₄,b₅,b₆)) = (Zmf b₃,b₂) . [b₅,b₆]

proof end;

theorem Th22: :: FUZZY_4:22

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

proof end;

Lemma19: for b₁, b₂, b₃ being non empty set
for b₄ being RMembership_Func of b₁,b₂
for b₅, b₆ being set st b₅ in b₁ & b₆ in b₃ holds
sup (rng (min b₄,(Zmf b₂,b₃),b₅,b₆)) = (Zmf b₁,b₃) . [b₅,b₆]

proof end;

theorem Th23: :: FUZZY_4:23

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

proof end;

theorem Th24: :: FUZZY_4:24

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

proof end;