:: by Adam Grabowski

::

:: Received February 26, 2020

:: Copyright (c) 2020-2021 Association of Mizar Users

registration

ex b_{1} being UnOp of [.0,1.] st

( b_{1} is bijective & b_{1} is increasing )
end;

cluster Relation-like [.0,1.] -defined [.0,1.] -valued Function-like non empty total quasi_total bijective complex-valued ext-real-valued real-valued increasing for Element of bool [:[.0,1.],[.0,1.]:];

existence ex b

( b

proof end;

registration

for b_{1} being UnOp of [.0,1.] st b_{1} is bijective & b_{1} is non-decreasing holds

b_{1} is increasing
;

for b_{1} being UnOp of [.0,1.] st b_{1} is bijective & b_{1} is increasing holds

b_{1} is non-decreasing
;

end;

cluster Function-like quasi_total bijective non-decreasing -> increasing for Element of bool [:[.0,1.],[.0,1.]:];

coherence for b

b

cluster Function-like quasi_total bijective increasing -> non-decreasing for Element of bool [:[.0,1.],[.0,1.]:];

coherence for b

b

registration

let f be bijective increasing UnOp of [.0,1.];

coherence

( f " is real-valued & f " is Function-like ) ;

end;
coherence

( f " is real-valued & f " is Function-like ) ;

registration
end;

RF220: for h being REAL -defined real-valued Function

for Y being set holds

( h | Y is increasing iff for r1, r2 being Real st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds

h . r1 < h . r2 )

proof end;

theorem :: FUZIMPL3:4

for f being one-to-one UnOp of [.0,1.]

for d being Element of [.0,1.] st d in rng f holds

(f ") . d in dom f

for d being Element of [.0,1.] st d in rng f holds

(f ") . d in dom f

proof end;

Cosik1: for f being bijective UnOp of [.0,1.] holds (f | [.0,1.]) " is REAL -defined

proof end;

FC9: for f being bijective increasing UnOp of [.0,1.] holds ((f | [.0,1.]) ") | (f .: [.0,1.]) is increasing

proof end;

registration
end;

theorem Rosnie: :: FUZIMPL3:6

for f being UnOp of [.0,1.] holds

( f is non-decreasing iff for a, b being Element of [.0,1.] st a <= b holds

f . a <= f . b )

( f is non-decreasing iff for a, b being Element of [.0,1.] st a <= b holds

f . a <= f . b )

proof end;

theorem NonInc: :: FUZIMPL3:7

for f being UnOp of [.0,1.] holds

( f is non-increasing iff for a, b being Element of [.0,1.] st a <= b holds

f . a >= f . b )

( f is non-increasing iff for a, b being Element of [.0,1.] st a <= b holds

f . a >= f . b )

proof end;

theorem Decreas: :: FUZIMPL3:8

for f being UnOp of [.0,1.] holds

( f is decreasing iff for a, b being Element of [.0,1.] st a < b holds

f . a > f . b )

( f is decreasing iff for a, b being Element of [.0,1.] st a < b holds

f . a > f . b )

proof end;

theorem RosnieI: :: FUZIMPL3:9

for f being UnOp of [.0,1.] holds

( f is increasing iff for a, b being Element of [.0,1.] st a < b holds

f . a < f . b )

( f is increasing iff for a, b being Element of [.0,1.] st a < b holds

f . a < f . b )

proof end;

registration

let f be bijective increasing UnOp of [.0,1.];

coherence

for b_{1} being UnOp of [.0,1.] st b_{1} = f " holds

( b_{1} is bijective & b_{1} is increasing )
;

end;
coherence

for b

( b

definition

{ f where f is bijective increasing UnOp of [.0,1.] : verum } is set ;

end;

func Theta -> set equals :: FUZIMPL3:def 1

{ f where f is bijective increasing UnOp of [.0,1.] : verum } ;

coherence { f where f is bijective increasing UnOp of [.0,1.] : verum } ;

{ f where f is bijective increasing UnOp of [.0,1.] : verum } is set ;

:: deftheorem defines Theta FUZIMPL3:def 1 :

Theta = { f where f is bijective increasing UnOp of [.0,1.] : verum } ;

Theta = { f where f is bijective increasing UnOp of [.0,1.] : verum } ;

definition

let f be BinOp of [.0,1.];

let h be bijective increasing UnOp of [.0,1.];

ex b_{1} being BinOp of [.0,1.] st

for x1, x2 being Element of [.0,1.] holds b_{1} . (x1,x2) = (h ") . (f . ((h . x1),(h . x2)))

for b_{1}, b_{2} being BinOp of [.0,1.] st ( for x1, x2 being Element of [.0,1.] holds b_{1} . (x1,x2) = (h ") . (f . ((h . x1),(h . x2))) ) & ( for x1, x2 being Element of [.0,1.] holds b_{2} . (x1,x2) = (h ") . (f . ((h . x1),(h . x2))) ) holds

b_{1} = b_{2}

end;
let h be bijective increasing UnOp of [.0,1.];

func ConjImpl (f,h) -> BinOp of [.0,1.] means :BIDef: :: FUZIMPL3:def 2

for x1, x2 being Element of [.0,1.] holds it . (x1,x2) = (h ") . (f . ((h . x1),(h . x2)));

existence for x1, x2 being Element of [.0,1.] holds it . (x1,x2) = (h ") . (f . ((h . x1),(h . x2)));

ex b

for x1, x2 being Element of [.0,1.] holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem BIDef defines ConjImpl FUZIMPL3:def 2 :

for f being BinOp of [.0,1.]

for h being bijective increasing UnOp of [.0,1.]

for b_{3} being BinOp of [.0,1.] holds

( b_{3} = ConjImpl (f,h) iff for x1, x2 being Element of [.0,1.] holds b_{3} . (x1,x2) = (h ") . (f . ((h . x1),(h . x2))) );

for f being BinOp of [.0,1.]

for h being bijective increasing UnOp of [.0,1.]

for b

( b

definition

let f, g be BinOp of [.0,1.];

end;
pred f,g are_conjugate means :: FUZIMPL3:def 3

ex h being bijective increasing UnOp of [.0,1.] st g = ConjImpl (f,h);

ex h being bijective increasing UnOp of [.0,1.] st g = ConjImpl (f,h);

:: deftheorem defines are_conjugate FUZIMPL3:def 3 :

for f, g being BinOp of [.0,1.] holds

( f,g are_conjugate iff ex h being bijective increasing UnOp of [.0,1.] st g = ConjImpl (f,h) );

for f, g being BinOp of [.0,1.] holds

( f,g are_conjugate iff ex h being bijective increasing UnOp of [.0,1.] st g = ConjImpl (f,h) );

registration

let I be Fuzzy_Implication;

let f be bijective non-decreasing UnOp of [.0,1.];

coherence

( ConjImpl (I,f) is decreasing_on_1st & ConjImpl (I,f) is increasing_on_2nd & ConjImpl (I,f) is 00-dominant & ConjImpl (I,f) is 11-dominant & ConjImpl (I,f) is 10-weak )

end;
let f be bijective non-decreasing UnOp of [.0,1.];

coherence

( ConjImpl (I,f) is decreasing_on_1st & ConjImpl (I,f) is increasing_on_2nd & ConjImpl (I,f) is 00-dominant & ConjImpl (I,f) is 11-dominant & ConjImpl (I,f) is 10-weak )

proof end;

theorem :: FUZIMPL3:11

for I being Fuzzy_Implication

for f being bijective increasing UnOp of [.0,1.] holds ConjImpl (I,f) is Fuzzy_Implication ;

for f being bijective increasing UnOp of [.0,1.] holds ConjImpl (I,f) is Fuzzy_Implication ;

registration

ex b_{1} being Fuzzy_Implication st

( b_{1} is satisfying_(NP) & b_{1} is satisfying_(OP) & b_{1} is satisfying_(EP) & b_{1} is satisfying_(IP) )
end;

cluster Relation-like [:[.K89(),1.],[.K89(),1.]:] -defined [.K89(),1.] -valued Function-like total quasi_total quasi_total complex-valued ext-real-valued real-valued decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak 01-dominant with_properties_of_fuzzy_implication with_properties_of_classical_implication satisfying_(LB) satisfying_(RB) satisfying_(NP) satisfying_(EP) satisfying_(IP) satisfying_(OP) for Element of bool [:[:[.K89(),1.],[.K89(),1.]:],[.K89(),1.]:];

existence ex b

( b

proof end;

theorem Prop136a: :: FUZIMPL3:12

for I being Fuzzy_Implication

for f being bijective increasing UnOp of [.0,1.] st I is satisfying_(NP) holds

ConjImpl (I,f) is satisfying_(NP)

for f being bijective increasing UnOp of [.0,1.] st I is satisfying_(NP) holds

ConjImpl (I,f) is satisfying_(NP)

proof end;

theorem Prop136b: :: FUZIMPL3:13

for I being Fuzzy_Implication

for f being bijective increasing UnOp of [.0,1.] st I is satisfying_(EP) holds

ConjImpl (I,f) is satisfying_(EP)

for f being bijective increasing UnOp of [.0,1.] st I is satisfying_(EP) holds

ConjImpl (I,f) is satisfying_(EP)

proof end;

theorem Prop136c: :: FUZIMPL3:14

for I being Fuzzy_Implication

for f being bijective increasing UnOp of [.0,1.] st I is satisfying_(IP) holds

ConjImpl (I,f) is satisfying_(IP)

for f being bijective increasing UnOp of [.0,1.] st I is satisfying_(IP) holds

ConjImpl (I,f) is satisfying_(IP)

proof end;

theorem Prop136d: :: FUZIMPL3:15

for I being Fuzzy_Implication

for f being bijective increasing UnOp of [.0,1.] st I is satisfying_(OP) holds

ConjImpl (I,f) is satisfying_(OP)

for f being bijective increasing UnOp of [.0,1.] st I is satisfying_(OP) holds

ConjImpl (I,f) is satisfying_(OP)

proof end;

registration

let I be satisfying_(NP) Fuzzy_Implication;

let f be bijective increasing UnOp of [.0,1.];

coherence

ConjImpl (I,f) is satisfying_(NP) by Prop136a;

end;
let f be bijective increasing UnOp of [.0,1.];

coherence

ConjImpl (I,f) is satisfying_(NP) by Prop136a;

registration

let I be satisfying_(EP) Fuzzy_Implication;

let f be bijective increasing UnOp of [.0,1.];

coherence

ConjImpl (I,f) is satisfying_(EP) by Prop136b;

end;
let f be bijective increasing UnOp of [.0,1.];

coherence

ConjImpl (I,f) is satisfying_(EP) by Prop136b;

registration

let I be satisfying_(IP) Fuzzy_Implication;

let f be bijective increasing UnOp of [.0,1.];

coherence

ConjImpl (I,f) is satisfying_(IP) by Prop136c;

end;
let f be bijective increasing UnOp of [.0,1.];

coherence

ConjImpl (I,f) is satisfying_(IP) by Prop136c;

registration

let I be satisfying_(OP) Fuzzy_Implication;

let f be bijective increasing UnOp of [.0,1.];

coherence

ConjImpl (I,f) is satisfying_(OP) by Prop136d;

end;
let f be bijective increasing UnOp of [.0,1.];

coherence

ConjImpl (I,f) is satisfying_(OP) by Prop136d;

theorem :: FUZIMPL3:16

for I being Fuzzy_Implication

for f being bijective increasing UnOp of [.0,1.] holds ConjImpl (I,f) = ((f ") * I) * [:f,f:]

for f being bijective increasing UnOp of [.0,1.] holds ConjImpl (I,f) = ((f ") * I) * [:f,f:]

proof end;

:: deftheorem N1Def defines satisfying_(N1) FUZIMPL3:def 4 :

for N being UnOp of [.0,1.] holds

( N is satisfying_(N1) iff ( N . 0 = 1 & N . 1 = 0 ) );

for N being UnOp of [.0,1.] holds

( N is satisfying_(N1) iff ( N . 0 = 1 & N . 1 = 0 ) );

:: deftheorem N2Def defines satisfying_(N2) FUZIMPL3:def 5 :

for N being UnOp of [.0,1.] holds

( N is satisfying_(N2) iff N is non-increasing );

for N being UnOp of [.0,1.] holds

( N is satisfying_(N2) iff N is non-increasing );

definition

ex b_{1} being UnOp of [.0,1.] st

for x being Element of [.0,1.] holds b_{1} . x = 1 - x

for b_{1}, b_{2} being UnOp of [.0,1.] st ( for x being Element of [.0,1.] holds b_{1} . x = 1 - x ) & ( for x being Element of [.0,1.] holds b_{2} . x = 1 - x ) holds

b_{1} = b_{2}
end;

func N_CC -> UnOp of [.0,1.] means :NDef: :: FUZIMPL3:def 6

for x being Element of [.0,1.] holds it . x = 1 - x;

existence for x being Element of [.0,1.] holds it . x = 1 - x;

ex b

for x being Element of [.0,1.] holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem NDef defines N_CC FUZIMPL3:def 6 :

for b_{1} being UnOp of [.0,1.] holds

( b_{1} = N_CC iff for x being Element of [.0,1.] holds b_{1} . x = 1 - x );

for b

( b

registration

ex b_{1} being UnOp of [.0,1.] st

( b_{1} is bijective & b_{1} is decreasing )
end;

cluster Relation-like [.0,1.] -defined [.0,1.] -valued Function-like non empty total quasi_total bijective complex-valued ext-real-valued real-valued decreasing for Element of bool [:[.0,1.],[.0,1.]:];

existence ex b

( b

proof end;

registration

ex b_{1} being UnOp of [.0,1.] st

( b_{1} is satisfying_(N1) & b_{1} is satisfying_(N2) )
end;

cluster Relation-like [.0,1.] -defined [.0,1.] -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued satisfying_(N1) satisfying_(N2) for Element of bool [:[.0,1.],[.0,1.]:];

existence ex b

( b

proof end;

definition

let f be UnOp of [.0,1.];

end;
attr f is continuous means :: FUZIMPL3:def 7

ex g being Function of I[01],I[01] st

( f = g & g is continuous );

ex g being Function of I[01],I[01] st

( f = g & g is continuous );

:: deftheorem defines continuous FUZIMPL3:def 7 :

for f being UnOp of [.0,1.] holds

( f is continuous iff ex g being Function of I[01],I[01] st

( f = g & g is continuous ) );

for f being UnOp of [.0,1.] holds

( f is continuous iff ex g being Function of I[01],I[01] st

( f = g & g is continuous ) );

:: deftheorem defines involutive FUZIMPL3:def 8 :

for N being UnOp of [.0,1.] holds

( N is involutive iff for x being Element of [.0,1.] holds N . (N . x) = x );

for N being UnOp of [.0,1.] holds

( N is involutive iff for x being Element of [.0,1.] holds N . (N . x) = x );

:: deftheorem defines satisfying_(N3) FUZIMPL3:def 9 :

for N being UnOp of [.0,1.] holds

( N is satisfying_(N3) iff N is decreasing );

for N being UnOp of [.0,1.] holds

( N is satisfying_(N3) iff N is decreasing );

:: deftheorem defines satisfying_(N4) FUZIMPL3:def 10 :

for N being UnOp of [.0,1.] holds

( N is satisfying_(N4) iff N is continuous );

for N being UnOp of [.0,1.] holds

( N is satisfying_(N4) iff N is continuous );

:: deftheorem defines satisfying_(N5) FUZIMPL3:def 11 :

for N being UnOp of [.0,1.] holds

( N is satisfying_(N5) iff N is involutive );

for N being UnOp of [.0,1.] holds

( N is satisfying_(N5) iff N is involutive );

:: deftheorem defines negation-strict FUZIMPL3:def 12 :

for N being UnOp of [.0,1.] holds

( N is negation-strict iff ( N is satisfying_(N3) & N is satisfying_(N4) ) );

for N being UnOp of [.0,1.] holds

( N is negation-strict iff ( N is satisfying_(N3) & N is satisfying_(N4) ) );

definition

let N be UnOp of [.0,1.];

end;
:: deftheorem defines negation-strong FUZIMPL3:def 13 :

for N being UnOp of [.0,1.] holds

( N is negation-strong iff N is satisfying_(N5) );

for N being UnOp of [.0,1.] holds

( N is negation-strong iff N is satisfying_(N5) );

:: deftheorem defines non-vanishing FUZIMPL3:def 14 :

for N being UnOp of [.0,1.] holds

( N is non-vanishing iff for x being Element of [.0,1.] holds

( N . x = 0 iff x = 1 ) );

for N being UnOp of [.0,1.] holds

( N is non-vanishing iff for x being Element of [.0,1.] holds

( N . x = 0 iff x = 1 ) );

:: deftheorem defines non-filling FUZIMPL3:def 15 :

for N being UnOp of [.0,1.] holds

( N is non-filling iff for x being Element of [.0,1.] holds

( N . x = 1 iff x = 0 ) );

for N being UnOp of [.0,1.] holds

( N is non-filling iff for x being Element of [.0,1.] holds

( N . x = 1 iff x = 0 ) );

definition

let I be BinOp of [.0,1.];

ex b_{1} being UnOp of [.0,1.] st

for x being Element of [.0,1.] holds b_{1} . x = I . (x,0)

for b_{1}, b_{2} being UnOp of [.0,1.] st ( for x being Element of [.0,1.] holds b_{1} . x = I . (x,0) ) & ( for x being Element of [.0,1.] holds b_{2} . x = I . (x,0) ) holds

b_{1} = b_{2}

end;
func FNegation I -> UnOp of [.0,1.] means :FNeg: :: FUZIMPL3:def 16

for x being Element of [.0,1.] holds it . x = I . (x,0);

existence for x being Element of [.0,1.] holds it . x = I . (x,0);

ex b

for x being Element of [.0,1.] holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem FNeg defines FNegation FUZIMPL3:def 16 :

for I being BinOp of [.0,1.]

for b_{2} being UnOp of [.0,1.] holds

( b_{2} = FNegation I iff for x being Element of [.0,1.] holds b_{2} . x = I . (x,0) );

for I being BinOp of [.0,1.]

for b

( b

:: Lemma 1.4.14

registration

let I be satisfying_(I1) satisfying_(I3) satisfying_(I5) BinOp of [.0,1.];

coherence

( FNegation I is satisfying_(N1) & FNegation I is satisfying_(N2) )

end;
coherence

( FNegation I is satisfying_(N1) & FNegation I is satisfying_(N2) )

proof end;

:: Definition 1.4.15

definition

ex b_{1} being UnOp of [.0,1.] st

for x being Element of [.0,1.] holds

( ( x = 0 implies b_{1} . x = 1 ) & ( x <> 0 implies b_{1} . x = 0 ) )

for b_{1}, b_{2} being UnOp of [.0,1.] st ( for x being Element of [.0,1.] holds

( ( x = 0 implies b_{1} . x = 1 ) & ( x <> 0 implies b_{1} . x = 0 ) ) ) & ( for x being Element of [.0,1.] holds

( ( x = 0 implies b_{2} . x = 1 ) & ( x <> 0 implies b_{2} . x = 0 ) ) ) holds

b_{1} = b_{2}

ex b_{1} being UnOp of [.0,1.] st

for x being Element of [.0,1.] holds

( ( x = 1 implies b_{1} . x = 0 ) & ( x <> 1 implies b_{1} . x = 1 ) )

for b_{1}, b_{2} being UnOp of [.0,1.] st ( for x being Element of [.0,1.] holds

( ( x = 1 implies b_{1} . x = 0 ) & ( x <> 1 implies b_{1} . x = 1 ) ) ) & ( for x being Element of [.0,1.] holds

( ( x = 1 implies b_{2} . x = 0 ) & ( x <> 1 implies b_{2} . x = 1 ) ) ) holds

b_{1} = b_{2}
end;

func NegationD1 -> UnOp of [.0,1.] means :D1Def: :: FUZIMPL3:def 17

for x being Element of [.0,1.] holds

( ( x = 0 implies it . x = 1 ) & ( x <> 0 implies it . x = 0 ) );

existence for x being Element of [.0,1.] holds

( ( x = 0 implies it . x = 1 ) & ( x <> 0 implies it . x = 0 ) );

ex b

for x being Element of [.0,1.] holds

( ( x = 0 implies b

proof end;

uniqueness for b

( ( x = 0 implies b

( ( x = 0 implies b

b

proof end;

func NegationD2 -> UnOp of [.0,1.] means :D2Def: :: FUZIMPL3:def 18

for x being Element of [.0,1.] holds

( ( x = 1 implies it . x = 0 ) & ( x <> 1 implies it . x = 1 ) );

existence for x being Element of [.0,1.] holds

( ( x = 1 implies it . x = 0 ) & ( x <> 1 implies it . x = 1 ) );

ex b

for x being Element of [.0,1.] holds

( ( x = 1 implies b

proof end;

uniqueness for b

( ( x = 1 implies b

( ( x = 1 implies b

b

proof end;

:: deftheorem D1Def defines NegationD1 FUZIMPL3:def 17 :

for b_{1} being UnOp of [.0,1.] holds

( b_{1} = NegationD1 iff for x being Element of [.0,1.] holds

( ( x = 0 implies b_{1} . x = 1 ) & ( x <> 0 implies b_{1} . x = 0 ) ) );

for b

( b

( ( x = 0 implies b

:: deftheorem D2Def defines NegationD2 FUZIMPL3:def 18 :

for b_{1} being UnOp of [.0,1.] holds

( b_{1} = NegationD2 iff for x being Element of [.0,1.] holds

( ( x = 1 implies b_{1} . x = 0 ) & ( x <> 1 implies b_{1} . x = 1 ) ) );

for b

( b

( ( x = 1 implies b

:: The Ordering of Fuzzy Negations

:: deftheorem defines <= FUZIMPL3:def 19 :

for f1, f2 being UnOp of [.0,1.] holds

( f1 <= f2 iff for a being Element of [.0,1.] holds f1 . a <= f2 . a );

for f1, f2 being UnOp of [.0,1.] holds

( f1 <= f2 iff for a being Element of [.0,1.] holds f1 . a <= f2 . a );

registration

coherence

( NegationD1 is satisfying_(N1) & NegationD1 is satisfying_(N2) )

( NegationD2 is satisfying_(N1) & NegationD2 is satisfying_(N2) )

end;
( NegationD1 is satisfying_(N1) & NegationD1 is satisfying_(N2) )

proof end;

coherence ( NegationD2 is satisfying_(N1) & NegationD2 is satisfying_(N2) )

proof end;

:: On Fuzzy Negations Generated by Fuzzy Implications

theorem :: FUZIMPL3:29

theorem Prop1417ii: :: FUZIMPL3:30

for I being satisfying_(EP) satisfying_(OP) BinOp of [.0,1.]

for x being Element of [.0,1.] holds x <= (FNegation I) . ((FNegation I) . x)

for x being Element of [.0,1.] holds x <= (FNegation I) . ((FNegation I) . x)

proof end;

theorem :: FUZIMPL3:31

for I being satisfying_(EP) satisfying_(OP) BinOp of [.0,1.] holds ((FNegation I) * (FNegation I)) * (FNegation I) = FNegation I

proof end;

:: deftheorem GreatDef defines _greater FUZIMPL3:def 20 :

for x, l being Real holds

( l is x _greater iff l > x );

for x, l being Real holds

( l is x _greater iff l > x );

definition

let l be Real;

assume A0: l > - 1 ;

ex b_{1} being UnOp of [.0,1.] st

for x being Element of [.0,1.] holds b_{1} . x = (1 - x) / (1 + (l * x))

for b_{1}, b_{2} being UnOp of [.0,1.] st ( for x being Element of [.0,1.] holds b_{1} . x = (1 - x) / (1 + (l * x)) ) & ( for x being Element of [.0,1.] holds b_{2} . x = (1 - x) / (1 + (l * x)) ) holds

b_{1} = b_{2}

end;
assume A0: l > - 1 ;

func SugenoNegation l -> UnOp of [.0,1.] means :DefSugeno: :: FUZIMPL3:def 21

for x being Element of [.0,1.] holds it . x = (1 - x) / (1 + (l * x));

existence for x being Element of [.0,1.] holds it . x = (1 - x) / (1 + (l * x));

ex b

for x being Element of [.0,1.] holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem DefSugeno defines SugenoNegation FUZIMPL3:def 21 :

for l being Real st l > - 1 holds

for b_{2} being UnOp of [.0,1.] holds

( b_{2} = SugenoNegation l iff for x being Element of [.0,1.] holds b_{2} . x = (1 - x) / (1 + (l * x)) );

for l being Real st l > - 1 holds

for b

( b

registration

let r be - 1 _greater Real;

coherence

( SugenoNegation r is satisfying_(N1) & SugenoNegation r is satisfying_(N2) )

end;
coherence

( SugenoNegation r is satisfying_(N1) & SugenoNegation r is satisfying_(N2) )

proof end;

definition

let f be UnOp of [.0,1.];

let h be bijective increasing UnOp of [.0,1.];

ex b_{1} being UnOp of [.0,1.] st

for x being Element of [.0,1.] holds b_{1} . x = (h ") . (f . (h . x))

for b_{1}, b_{2} being UnOp of [.0,1.] st ( for x being Element of [.0,1.] holds b_{1} . x = (h ") . (f . (h . x)) ) & ( for x being Element of [.0,1.] holds b_{2} . x = (h ") . (f . (h . x)) ) holds

b_{1} = b_{2}

end;
let h be bijective increasing UnOp of [.0,1.];

func ConjNeg (f,h) -> UnOp of [.0,1.] means :CNDef: :: FUZIMPL3:def 22

for x being Element of [.0,1.] holds it . x = (h ") . (f . (h . x));

existence for x being Element of [.0,1.] holds it . x = (h ") . (f . (h . x));

ex b

for x being Element of [.0,1.] holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem CNDef defines ConjNeg FUZIMPL3:def 22 :

for f being UnOp of [.0,1.]

for h being bijective increasing UnOp of [.0,1.]

for b_{3} being UnOp of [.0,1.] holds

( b_{3} = ConjNeg (f,h) iff for x being Element of [.0,1.] holds b_{3} . x = (h ") . (f . (h . x)) );

for f being UnOp of [.0,1.]

for h being bijective increasing UnOp of [.0,1.]

for b

( b

theorem :: FUZIMPL3:33

for I being Fuzzy_Negation

for f being bijective increasing UnOp of [.0,1.] holds ConjNeg (I,f) = ((f ") * I) * f

for f being bijective increasing UnOp of [.0,1.] holds ConjNeg (I,f) = ((f ") * I) * f

proof end;

definition

let f, g be UnOp of [.0,1.];

end;
pred f,g are_conjugate means :: FUZIMPL3:def 23

ex h being bijective increasing UnOp of [.0,1.] st g = ConjNeg (f,h);

ex h being bijective increasing UnOp of [.0,1.] st g = ConjNeg (f,h);

:: deftheorem defines are_conjugate FUZIMPL3:def 23 :

for f, g being UnOp of [.0,1.] holds

( f,g are_conjugate iff ex h being bijective increasing UnOp of [.0,1.] st g = ConjNeg (f,h) );

for f, g being UnOp of [.0,1.] holds

( f,g are_conjugate iff ex h being bijective increasing UnOp of [.0,1.] st g = ConjNeg (f,h) );

:: Proposition 1.4.8

registration

let N be Fuzzy_Negation;

let h be bijective increasing UnOp of [.0,1.];

coherence

( ConjNeg (N,h) is satisfying_(N1) & ConjNeg (N,h) is satisfying_(N2) )

end;
let h be bijective increasing UnOp of [.0,1.];

coherence

( ConjNeg (N,h) is satisfying_(N1) & ConjNeg (N,h) is satisfying_(N2) )

proof end;

theorem :: FUZIMPL3:34

for I being Fuzzy_Implication

for h being bijective increasing UnOp of [.0,1.] holds ConjNeg ((FNegation I),h) = FNegation (ConjImpl (I,h))

for h being bijective increasing UnOp of [.0,1.] holds ConjNeg ((FNegation I),h) = FNegation (ConjImpl (I,h))

proof end;