:: FUZZY_4 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

registration
let C1 be non empty set ;
let F be Membership_Func of C1;
cluster K11(F) -> non empty ;
coherence
not rng F is empty
proof end;
end;

theorem Th1: :: FUZZY_4:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1 being non empty set
for F being Membership_Func of C1 holds
( rng F is bounded & ( for x being set st x in dom F holds
F . x <= sup (rng F) ) & ( for x being set st x in dom F holds
F . x >= inf (rng F) ) )
proof end;

theorem :: FUZZY_4:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1 being non empty set
for F, G being Membership_Func of C1 st ( for x being set st x in C1 holds
F . x <= G . x ) holds
sup (rng F) <= sup (rng G)
proof end;

theorem Th3: :: FUZZY_4:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1, C2 being non empty set
for f being RMembership_Func of C1,C2
for c being Element of [:C1,C2:] holds
( 0 <= f . c & f . c <= 1 )
proof end;

theorem :: FUZZY_4:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1, C2 being non empty set
for f being RMembership_Func of C1,C2
for x, y being set st [x,y] in [:C1,C2:] holds
( 0 <= f . [x,y] & f . [x,y] <= 1 ) by Th3;

definition
let C1, C2 be non empty set ;
let h be RMembership_Func of C2,C1;
func converse h -> RMembership_Func of C1,C2 means :Def1: :: FUZZY_4:def 1
for x, y being set st [x,y] in [:C1,C2:] holds
it . [x,y] = h . [y,x];
existence
ex b1 being RMembership_Func of C1,C2 st
for x, y being set st [x,y] in [:C1,C2:] holds
b1 . [x,y] = h . [y,x]
proof end;
uniqueness
for b1, b2 being RMembership_Func of C1,C2 st ( for x, y being set st [x,y] in [:C1,C2:] holds
b1 . [x,y] = h . [y,x] ) & ( for x, y being set st [x,y] in [:C1,C2:] holds
b2 . [x,y] = h . [y,x] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines converse FUZZY_4:def 1 :
for C1, C2 being non empty set
for h being RMembership_Func of C2,C1
for b4 being RMembership_Func of C1,C2 holds
( b4 = converse h iff for x, y being set st [x,y] in [:C1,C2:] holds
b4 . [x,y] = h . [y,x] );

theorem :: FUZZY_4:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1, C2 being non empty set
for f being RMembership_Func of C1,C2 holds converse (converse f) = f
proof end;

theorem Th6: :: FUZZY_4:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1, C2 being non empty set
for f being RMembership_Func of C1,C2 holds 1_minus (converse f) = converse (1_minus f)
proof end;

theorem Th7: :: FUZZY_4:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1, C2 being non empty set
for f, g being RMembership_Func of C1,C2 holds converse (max f,g) = max (converse f),(converse g)
proof end;

theorem Th8: :: FUZZY_4:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1, C2 being non empty set
for f, g being RMembership_Func of C1,C2 holds converse (min f,g) = min (converse f),(converse g)
proof end;

theorem Th9: :: FUZZY_4:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1, C2 being non empty set
for f, g being RMembership_Func of C1,C2
for x, y being set st x in C1 & y in C2 & f . [x,y] <= g . [x,y] holds
(converse f) . [y,x] <= (converse g) . [y,x]
proof end;

theorem :: FUZZY_4:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1, C2 being non empty set
for f, g being RMembership_Func of C1,C2 st g c= holds
converse g c=
proof end;

theorem :: FUZZY_4:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1, C2 being non empty set
for f, g being RMembership_Func of C1,C2 holds converse (f \ g) = (converse f) \ (converse g)
proof end;

theorem :: FUZZY_4:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1, C2 being non empty set
for f, g being RMembership_Func of C1,C2 holds converse (f \+\ g) = (converse f) \+\ (converse g)
proof end;

definition
let C1, C2, C3 be non empty set ;
let h be RMembership_Func of C1,C2;
let g be RMembership_Func of C2,C3;
let x, z be set ;
assume A1: ( x in C1 & z in C3 ) ;
func min h,g,x,z -> Membership_Func of C2 means :Def2: :: FUZZY_4:def 2
for y being Element of C2 holds it . y = min (h . [x,y]),(g . [y,z]);
existence
ex b1 being Membership_Func of C2 st
for y being Element of C2 holds b1 . y = min (h . [x,y]),(g . [y,z])
proof end;
uniqueness
for b1, b2 being Membership_Func of C2 st ( for y being Element of C2 holds b1 . y = min (h . [x,y]),(g . [y,z]) ) & ( for y being Element of C2 holds b2 . y = min (h . [x,y]),(g . [y,z]) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines min FUZZY_4:def 2 :
for C1, C2, C3 being non empty set
for h being RMembership_Func of C1,C2
for g being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
for b8 being Membership_Func of C2 holds
( b8 = min h,g,x,z iff for y being Element of C2 holds b8 . y = min (h . [x,y]),(g . [y,z]) );

definition
let C1, C2, C3 be non empty set ;
let h be RMembership_Func of C1,C2;
let g be RMembership_Func of C2,C3;
func h (#) g -> RMembership_Func of C1,C3 means :Def3: :: FUZZY_4:def 3
for x, z being set st [x,z] in [:C1,C3:] holds
it . [x,z] = sup (rng (min h,g,x,z));
existence
ex b1 being RMembership_Func of C1,C3 st
for x, z being set st [x,z] in [:C1,C3:] holds
b1 . [x,z] = sup (rng (min h,g,x,z))
proof end;
uniqueness
for b1, b2 being RMembership_Func of C1,C3 st ( for x, z being set st [x,z] in [:C1,C3:] holds
b1 . [x,z] = sup (rng (min h,g,x,z)) ) & ( for x, z being set st [x,z] in [:C1,C3:] holds
b2 . [x,z] = sup (rng (min h,g,x,z)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines (#) FUZZY_4:def 3 :
for C1, C2, C3 being non empty set
for h being RMembership_Func of C1,C2
for g being RMembership_Func of C2,C3
for b6 being RMembership_Func of C1,C3 holds
( b6 = h (#) g iff for x, z being set st [x,z] in [:C1,C3:] holds
b6 . [x,z] = sup (rng (min h,g,x,z)) );

Lm1: for C1, C2, C3 being non empty set
for f being RMembership_Func of C1,C2
for g, h being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
sup (rng (min f,(max g,h),x,z)) = max (sup (rng (min f,g,x,z))),(sup (rng (min f,h,x,z)))
proof end;

theorem :: FUZZY_4:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1, C2, C3 being non empty set
for f being RMembership_Func of C1,C2
for g, h being RMembership_Func of C2,C3 holds f (#) (max g,h) = max (f (#) g),(f (#) h)
proof end;

Lm2: for C1, C2, C3 being non empty set
for f, g being RMembership_Func of C1,C2
for h being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
sup (rng (min (max f,g),h,x,z)) = max (sup (rng (min f,h,x,z))),(sup (rng (min g,h,x,z)))
proof end;

theorem :: FUZZY_4:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1, C2, C3 being non empty set
for f, g being RMembership_Func of C1,C2
for h being RMembership_Func of C2,C3 holds (max f,g) (#) h = max (f (#) h),(g (#) h)
proof end;

Lm3: for C1, C2, C3 being non empty set
for f being RMembership_Func of C1,C2
for g, h being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
sup (rng (min f,(min g,h),x,z)) <= min (sup (rng (min f,g,x,z))),(sup (rng (min f,h,x,z)))
proof end;

theorem :: FUZZY_4:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1, C2, C3 being non empty set
for f being RMembership_Func of C1,C2
for g, h being RMembership_Func of C2,C3 holds min (f (#) g),(f (#) h) c=
proof end;

Lm4: for C1, C2, C3 being non empty set
for f, g being RMembership_Func of C1,C2
for h being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
sup (rng (min (min f,g),h,x,z)) <= min (sup (rng (min f,h,x,z))),(sup (rng (min g,h,x,z)))
proof end;

theorem :: FUZZY_4:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1, C2, C3 being non empty set
for f, g being RMembership_Func of C1,C2
for h being RMembership_Func of C2,C3 holds min (f (#) h),(g (#) h) c=
proof end;

Lm5: for C1, C2, C3 being non empty set
for f being RMembership_Func of C1,C2
for g being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
sup (rng (min (converse g),(converse f),z,x)) = sup (rng (min f,g,x,z))
proof end;

theorem :: FUZZY_4:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1, C2, C3 being non empty set
for f being RMembership_Func of C1,C2
for g being RMembership_Func of C2,C3 holds converse (f (#) g) = (converse g) (#) (converse f)
proof end;

theorem Th18: :: FUZZY_4:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1, C2, C3 being non empty set
for f, g being RMembership_Func of C1,C2
for h, k being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 & ( for y being set st y in C2 holds
( f . [x,y] <= g . [x,y] & h . [y,z] <= k . [y,z] ) ) holds
(f (#) h) . [x,z] <= (g (#) k) . [x,z]
proof end;

theorem :: FUZZY_4:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1, C2, C3 being non empty set
for f, g being RMembership_Func of C1,C2
for h, k being RMembership_Func of C2,C3 st g c= & k c= holds
g (#) k c=
proof end;

definition
let C1, C2 be non empty set ;
func Imf C1,C2 -> RMembership_Func of C1,C2 means :: FUZZY_4:def 4
for x, y being set st [x,y] in [:C1,C2:] holds
( ( x = y implies it . [x,y] = 1 ) & ( not x = y implies it . [x,y] = 0 ) );
existence
ex b1 being RMembership_Func of C1,C2 st
for x, y being set st [x,y] in [:C1,C2:] holds
( ( x = y implies b1 . [x,y] = 1 ) & ( not x = y implies b1 . [x,y] = 0 ) )
proof end;
uniqueness
for b1, b2 being RMembership_Func of C1,C2 st ( for x, y being set st [x,y] in [:C1,C2:] holds
( ( x = y implies b1 . [x,y] = 1 ) & ( not x = y implies b1 . [x,y] = 0 ) ) ) & ( for x, y being set st [x,y] in [:C1,C2:] holds
( ( x = y implies b2 . [x,y] = 1 ) & ( not x = y implies b2 . [x,y] = 0 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines Imf FUZZY_4:def 4 :
for C1, C2 being non empty set
for b3 being RMembership_Func of C1,C2 holds
( b3 = Imf C1,C2 iff for x, y being set st [x,y] in [:C1,C2:] holds
( ( x = y implies b3 . [x,y] = 1 ) & ( not x = y implies b3 . [x,y] = 0 ) ) );

theorem Th20: :: FUZZY_4:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1, C2 being non empty set
for c being Element of [:C1,C2:] holds
( (Zmf C1,C2) . c = 0 & (Umf C1,C2) . c = 1 )
proof end;

theorem :: FUZZY_4:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1, C2 being non empty set
for x, y being set st [x,y] in [:C1,C2:] holds
( (Zmf C1,C2) . [x,y] = 0 & (Umf C1,C2) . [x,y] = 1 ) by Th20;

Lm6: for C2, C3, C1 being non empty set
for f being RMembership_Func of C2,C3
for x, z being set st x in C1 & z in C3 holds
sup (rng (min (Zmf C1,C2),f,x,z)) = (Zmf C1,C3) . [x,z]
proof end;

theorem Th22: :: FUZZY_4:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C2, C3, C1 being non empty set
for f being RMembership_Func of C2,C3 holds (Zmf C1,C2) (#) f = Zmf C1,C3
proof end;

Lm7: for C1, C2, C3 being non empty set
for f being RMembership_Func of C1,C2
for x, z being set st x in C1 & z in C3 holds
sup (rng (min f,(Zmf C2,C3),x,z)) = (Zmf C1,C3) . [x,z]
proof end;

theorem Th23: :: FUZZY_4:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1, C2, C3 being non empty set
for f being RMembership_Func of C1,C2 holds f (#) (Zmf C2,C3) = Zmf C1,C3
proof end;

theorem :: FUZZY_4:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C1 being non empty set
for f being RMembership_Func of C1,C1 holds f (#) (Zmf C1,C1) = (Zmf C1,C1) (#) f
proof end;