:: On Fuzzy Negations Generated by Fuzzy Implications
:: by Adam Grabowski
::
:: Received February 26, 2020
:: Copyright (c) 2020-2021 Association of Mizar Users

theorem LemmaImp: :: FUZIMPL3:1

for x, r being Real st 0 <= x & x <= 1 & r > - 1 holds
(x * r) + 1 > 0

proof end;

theorem Wazne1: :: FUZIMPL3:2

for z being Real st z in [.0,1.] & z <> 0 holds
ex w being Element of [.0,1.] st w < z

proof end;

theorem Wazne2: :: FUZIMPL3:3

for z being Real st z in [.0,1.] & z <> 1 holds
ex w being Element of [.0,1.] st w > z

proof end;

registration

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₁ being UnOp of [.0,1.] st
( b₁ is bijective & b₁ is increasing )

proof end;

end;

registration

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

coherence
for b₁ being UnOp of [.0,1.] st b₁ is bijective & b₁ is non-decreasing holds
b₁ is increasing ;

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

coherence
for b₁ being UnOp of [.0,1.] st b₁ is bijective & b₁ is increasing holds
b₁ is non-decreasing ;

end;

registration

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

cluster f " -> real-valued ;

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

end;

registration

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

cluster (f | [.0,1.]) " -> real-valued ;

coherence
(f | [.0,1.]) " is real-valued ;

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

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;

theorem LemmaIncreas: :: FUZIMPL3:5

for f being bijective increasing UnOp of [.0,1.] holds f " is increasing

proof end;

registration

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

cluster f " -> increasing ;

coherence
f " is increasing by LemmaIncreas;

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 )

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 )

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 )

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 )

proof end;

theorem LemmaBound: :: FUZIMPL3:10

for f being bijective increasing UnOp of [.0,1.] holds
( f . 0 = 0 & f . 1 = 1 )

proof end;

registration

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

cluster f " -> bijective increasing for UnOp of [.0,1.];

coherence
for b₁ being UnOp of [.0,1.] st b₁ = f " holds
( b₁ is bijective & b₁ is increasing ) ;

end;

definition

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 } is set ;

end;

:: deftheorem defines Theta FUZIMPL3:def 1 :
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.];

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
ex b₁ being BinOp of [.0,1.] st
for x1, x2 being Element of [.0,1.] holds b₁ . (x1,x2) = (h ") . (f . ((h . x1),(h . x2)))

proof end;

uniqueness
for b₁, b₂ being BinOp of [.0,1.] st ( for x1, x2 being Element of [.0,1.] holds b₁ . (x1,x2) = (h ") . (f . ((h . x1),(h . x2))) ) & ( for x1, x2 being Element of [.0,1.] holds b₂ . (x1,x2) = (h ") . (f . ((h . x1),(h . x2))) ) holds
b₁ = b₂

proof end;

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₃ being BinOp of [.0,1.] holds
( b₃ = ConjImpl (f,h) iff for x1, x2 being Element of [.0,1.] holds b₃ . (x1,x2) = (h ") . (f . ((h . x1),(h . x2))) );

definition

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

pred f,g are_conjugate means :: FUZIMPL3:def 3
ex h being bijective increasing UnOp of [.0,1.] st g = ConjImpl (f,h);

end;

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

registration

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

cluster ConjImpl (I,f) -> decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak ;

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;

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 ;

registration

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₁ being Fuzzy_Implication st
( b₁ is satisfying_(NP) & b₁ is satisfying_(OP) & b₁ is satisfying_(EP) & b₁ is satisfying_(IP) )

proof end;

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)

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)

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)

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)

proof end;

registration

let I be satisfying_(NP) Fuzzy_Implication;
let f be bijective increasing UnOp of [.0,1.];

cluster ConjImpl (I,f) -> satisfying_(NP) ;

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

end;

registration

let I be satisfying_(EP) Fuzzy_Implication;
let f be bijective increasing UnOp of [.0,1.];

cluster ConjImpl (I,f) -> satisfying_(EP) ;

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

end;

registration

let I be satisfying_(IP) Fuzzy_Implication;
let f be bijective increasing UnOp of [.0,1.];

cluster ConjImpl (I,f) -> satisfying_(IP) ;

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

end;

registration

let I be satisfying_(OP) Fuzzy_Implication;
let f be bijective increasing UnOp of [.0,1.];

cluster ConjImpl (I,f) -> satisfying_(OP) ;

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

end;

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:]

proof end;

definition

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

attr N is satisfying_(N1) means :N1Def: :: FUZIMPL3:def 4
( N . 0 = 1 & N . 1 = 0 );

attr N is satisfying_(N2) means :N2Def: :: FUZIMPL3:def 5
N is non-increasing ;

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 ) );

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

definition

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
ex b₁ being UnOp of [.0,1.] st
for x being Element of [.0,1.] holds b₁ . x = 1 - x

proof end;

uniqueness
for b₁, b₂ being UnOp of [.0,1.] st ( for x being Element of [.0,1.] holds b₁ . x = 1 - x ) & ( for x being Element of [.0,1.] holds b₂ . x = 1 - x ) holds
b₁ = b₂

proof end;

end;

:: deftheorem NDef defines N_CC FUZIMPL3:def 6 :
for b₁ being UnOp of [.0,1.] holds
( b₁ = N_CC iff for x being Element of [.0,1.] holds b₁ . x = 1 - x );

registration

cluster N_CC -> satisfying_(N1) satisfying_(N2) ;

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

proof end;

end;

registration

cluster N_CC -> bijective decreasing ;

coherence
( N_CC is bijective & N_CC is decreasing )

proof end;

end;

registration

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₁ being UnOp of [.0,1.] st
( b₁ is bijective & b₁ is decreasing )

proof end;

end;

registration

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₁ being UnOp of [.0,1.] st
( b₁ is satisfying_(N1) & b₁ is satisfying_(N2) )

proof end;

end;

definition

mode Fuzzy_Negation is satisfying_(N1) satisfying_(N2) UnOp of [.0,1.];

end;

definition

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

attr f is continuous means :: FUZIMPL3:def 7
ex g being Function of I[01],I[01] st
( f = g & g is continuous );

end;

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

definition

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

attr N is involutive means :: FUZIMPL3:def 8
for x being Element of [.0,1.] holds N . (N . x) = x;

end;

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

definition

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

attr N is satisfying_(N3) means :: FUZIMPL3:def 9
N is decreasing ;

attr N is satisfying_(N4) means :: FUZIMPL3:def 10
N is continuous ;

attr N is satisfying_(N5) means :: FUZIMPL3:def 11
N is involutive ;

end;

:: deftheorem defines satisfying_(N3) FUZIMPL3:def 9 :
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 );

:: deftheorem defines satisfying_(N5) FUZIMPL3:def 11 :
for N being UnOp of [.0,1.] holds
( N is satisfying_(N5) iff N is involutive );

definition

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

attr N is negation-strict means :: FUZIMPL3:def 12
( N is satisfying_(N3) & N is satisfying_(N4) );

end;

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

definition

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

attr N is negation-strong means :: FUZIMPL3:def 13
N is satisfying_(N5) ;

attr N is non-vanishing means :: FUZIMPL3:def 14
for x being Element of [.0,1.] holds
( N . x = 0 iff x = 1 );

attr N is non-filling means :: FUZIMPL3:def 15
for x being Element of [.0,1.] holds
( N . x = 1 iff x = 0 );

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) );

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

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

theorem :: FUZIMPL3:17

for f being bijective decreasing UnOp of [.0,1.] holds
( f . 0 = 1 & f . 1 = 0 )

proof end;

definition

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

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
ex b₁ being UnOp of [.0,1.] st
for x being Element of [.0,1.] holds b₁ . x = I . (x,0)

proof end;

uniqueness
for b₁, b₂ being UnOp of [.0,1.] st ( for x being Element of [.0,1.] holds b₁ . x = I . (x,0) ) & ( for x being Element of [.0,1.] holds b₂ . x = I . (x,0) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem FNeg defines FNegation FUZIMPL3:def 16 :
for I being BinOp of [.0,1.]
for b₂ being UnOp of [.0,1.] holds
( b₂ = FNegation I iff for x being Element of [.0,1.] holds b₂ . x = I . (x,0) );

:: Lemma 1.4.14

registration

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

cluster FNegation I -> satisfying_(N1) satisfying_(N2) ;

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

proof end;

end;

:: Definition 1.4.15

theorem :: FUZIMPL3:18

for I being Fuzzy_Implication holds FNegation I is Fuzzy_Negation ;

definition

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
ex b₁ being UnOp of [.0,1.] st
for x being Element of [.0,1.] holds
( ( x = 0 implies b₁ . x = 1 ) & ( x <> 0 implies b₁ . x = 0 ) )

proof end;

uniqueness
for b₁, b₂ being UnOp of [.0,1.] st ( for x being Element of [.0,1.] holds
( ( x = 0 implies b₁ . x = 1 ) & ( x <> 0 implies b₁ . x = 0 ) ) ) & ( for x being Element of [.0,1.] holds
( ( x = 0 implies b₂ . x = 1 ) & ( x <> 0 implies b₂ . x = 0 ) ) ) holds
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
ex b₁ being UnOp of [.0,1.] st
for x being Element of [.0,1.] holds
( ( x = 1 implies b₁ . x = 0 ) & ( x <> 1 implies b₁ . x = 1 ) )

proof end;

uniqueness
for b₁, b₂ being UnOp of [.0,1.] st ( for x being Element of [.0,1.] holds
( ( x = 1 implies b₁ . x = 0 ) & ( x <> 1 implies b₁ . x = 1 ) ) ) & ( for x being Element of [.0,1.] holds
( ( x = 1 implies b₂ . x = 0 ) & ( x <> 1 implies b₂ . x = 1 ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem D1Def defines NegationD1 FUZIMPL3:def 17 :
for b₁ being UnOp of [.0,1.] holds
( b₁ = NegationD1 iff for x being Element of [.0,1.] holds
( ( x = 0 implies b₁ . x = 1 ) & ( x <> 0 implies b₁ . x = 0 ) ) );

:: deftheorem D2Def defines NegationD2 FUZIMPL3:def 18 :
for b₁ being UnOp of [.0,1.] holds
( b₁ = NegationD2 iff for x being Element of [.0,1.] holds
( ( x = 1 implies b₁ . x = 0 ) & ( x <> 1 implies b₁ . x = 1 ) ) );

:: The Ordering of Fuzzy Negations

definition

let f1, f2 be UnOp of [.0,1.];

pred f1 <= f2 means :: FUZIMPL3:def 19
for a being Element of [.0,1.] holds f1 . a <= f2 . a;

end;

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

registration

cluster NegationD1 -> satisfying_(N1) satisfying_(N2) ;

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

proof end;

cluster NegationD2 -> satisfying_(N1) satisfying_(N2) ;

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

proof end;

end;

theorem :: FUZIMPL3:19

for N being Fuzzy_Negation holds
( NegationD1 <= N & N <= NegationD2 )

proof end;

:: On Fuzzy Negations Generated by Fuzzy Implications

theorem :: FUZIMPL3:20

FNegation I_LK = N_CC

proof end;

theorem :: FUZIMPL3:21

FNegation I_GD = NegationD1

proof end;

theorem :: FUZIMPL3:22

FNegation I_RC = N_CC

proof end;

theorem :: FUZIMPL3:23

FNegation I_KD = N_CC

proof end;

theorem :: FUZIMPL3:24

FNegation I_GG = NegationD1

proof end;

theorem :: FUZIMPL3:25

FNegation I_RS = NegationD1

proof end;

theorem :: FUZIMPL3:26

FNegation I_YG = NegationD1

proof end;

theorem :: FUZIMPL3:27

FNegation I_WB = NegationD2

proof end;

theorem :: FUZIMPL3:28

FNegation I_FD = N_CC

proof end;

theorem :: FUZIMPL3:29

for I being satisfying_(EP) satisfying_(OP) BinOp of [.0,1.] holds FNegation I is Fuzzy_Negation ;

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)

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;

definition

let x, l be Real;

attr l is x _greater means :GreatDef: :: FUZIMPL3:def 20
l > x;

end;

:: deftheorem GreatDef defines _greater FUZIMPL3:def 20 :
for x, l being Real holds
( l is x _greater iff l > x );

registration

cluster V31() ext-real V38() - 1 _greater for object ;

existence
ex b₁ being Real st b₁ is - 1 _greater

proof end;

end;

definition

let l be Real;
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
ex b₁ being UnOp of [.0,1.] st
for x being Element of [.0,1.] holds b₁ . x = (1 - x) / (1 + (l * x))

proof end;

uniqueness
for b₁, b₂ being UnOp of [.0,1.] st ( for x being Element of [.0,1.] holds b₁ . x = (1 - x) / (1 + (l * x)) ) & ( for x being Element of [.0,1.] holds b₂ . x = (1 - x) / (1 + (l * x)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem DefSugeno defines SugenoNegation FUZIMPL3:def 21 :
for l being Real st l > - 1 holds
for b₂ being UnOp of [.0,1.] holds
( b₂ = SugenoNegation l iff for x being Element of [.0,1.] holds b₂ . x = (1 - x) / (1 + (l * x)) );

theorem :: FUZIMPL3:32

N_CC = SugenoNegation 0

proof end;

registration

let r be - 1 _greater Real;

cluster SugenoNegation r -> satisfying_(N1) satisfying_(N2) ;

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

proof end;

end;

definition

let f be UnOp of [.0,1.];
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
ex b₁ being UnOp of [.0,1.] st
for x being Element of [.0,1.] holds b₁ . x = (h ") . (f . (h . x))

proof end;

uniqueness
for b₁, b₂ being UnOp of [.0,1.] st ( for x being Element of [.0,1.] holds b₁ . x = (h ") . (f . (h . x)) ) & ( for x being Element of [.0,1.] holds b₂ . x = (h ") . (f . (h . x)) ) holds
b₁ = b₂

proof end;

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₃ being UnOp of [.0,1.] holds
( b₃ = ConjNeg (f,h) iff for x being Element of [.0,1.] holds b₃ . x = (h ") . (f . (h . x)) );

theorem :: FUZIMPL3:33

for I being Fuzzy_Negation
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.];

pred f,g are_conjugate means :: FUZIMPL3:def 23
ex h being bijective increasing UnOp of [.0,1.] st g = ConjNeg (f,h);

end;

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

:: Proposition 1.4.8

registration

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

cluster ConjNeg (N,h) -> satisfying_(N1) satisfying_(N2) ;

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

proof end;

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))

proof end;