:: On Fuzzy Negations Generated by Fuzzy Implications
::
:: 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
existence
ex b1 being UnOp of [.0,1.] st
( b1 is bijective & b1 is increasing )
proof end;
end;

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

registration
let f be bijective increasing UnOp of [.0,1.];
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.];
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 b1 being UnOp of [.0,1.] st b1 = f " holds
( b1 is bijective & b1 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 b1 being BinOp of [.0,1.] st
for x1, x2 being Element of [.0,1.] holds b1 . (x1,x2) = (h ") . (f . ((h . x1),(h . x2)))
proof end;
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for x1, x2 being Element of [.0,1.] holds b1 . (x1,x2) = (h ") . (f . ((h . x1),(h . x2))) ) & ( for x1, x2 being Element of [.0,1.] holds b2 . (x1,x2) = (h ") . (f . ((h . x1),(h . x2))) ) holds
b1 = b2
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 b3 being BinOp of [.0,1.] holds
( b3 = ConjImpl (f,h) iff for x1, x2 being Element of [.0,1.] holds b3 . (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.];
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
existence
ex b1 being Fuzzy_Implication st
( b1 is satisfying_(NP) & b1 is satisfying_(OP) & b1 is satisfying_(EP) & b1 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 b1 being UnOp of [.0,1.] st
for x being Element of [.0,1.] holds b1 . x = 1 - x
proof end;
uniqueness
for b1, b2 being UnOp of [.0,1.] st ( for x being Element of [.0,1.] holds b1 . x = 1 - x ) & ( for x being Element of [.0,1.] holds b2 . x = 1 - x ) holds
b1 = b2
proof end;
end;

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

registration
coherence
proof end;
end;

registration
coherence
( N_CC is bijective & N_CC is decreasing )
proof end;
end;

registration
existence
ex b1 being UnOp of [.0,1.] st
( b1 is bijective & b1 is decreasing )
proof end;
end;

registration
existence
ex b1 being UnOp of [.0,1.] st
( b1 is satisfying_(N1) & b1 is satisfying_(N2) )
proof end;
end;

definition end;

definition
let f be UnOp of [.0,1.];
attr f is continuous means :: FUZIMPL3:def 7
ex g being Function of I,I 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,I 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 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 b1 being UnOp of [.0,1.] st
for x being Element of [.0,1.] holds b1 . x = I . (x,0)
proof end;
uniqueness
for b1, b2 being UnOp of [.0,1.] st ( for x being Element of [.0,1.] holds b1 . x = I . (x,0) ) & ( for x being Element of [.0,1.] holds b2 . x = I . (x,0) ) holds
b1 = b2
proof end;
end;

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

:: Lemma 1.4.14
registration
let I be satisfying_(I1) satisfying_(I3) satisfying_(I5) BinOp of [.0,1.];
coherence
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 b1 being UnOp of [.0,1.] st
for x being Element of [.0,1.] holds
( ( x = 0 implies b1 . x = 1 ) & ( x <> 0 implies b1 . x = 0 ) )
proof end;
uniqueness
for b1, b2 being UnOp of [.0,1.] st ( for x being Element of [.0,1.] holds
( ( x = 0 implies b1 . x = 1 ) & ( x <> 0 implies b1 . x = 0 ) ) ) & ( for x being Element of [.0,1.] holds
( ( x = 0 implies b2 . x = 1 ) & ( x <> 0 implies b2 . x = 0 ) ) ) holds
b1 = b2
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 b1 being UnOp of [.0,1.] st
for x being Element of [.0,1.] holds
( ( x = 1 implies b1 . x = 0 ) & ( x <> 1 implies b1 . x = 1 ) )
proof end;
uniqueness
for b1, b2 being UnOp of [.0,1.] st ( for x being Element of [.0,1.] holds
( ( x = 1 implies b1 . x = 0 ) & ( x <> 1 implies b1 . x = 1 ) ) ) & ( for x being Element of [.0,1.] holds
( ( x = 1 implies b2 . x = 0 ) & ( x <> 1 implies b2 . x = 1 ) ) ) holds
b1 = b2
proof end;
end;

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

:: deftheorem D2Def defines NegationD2 FUZIMPL3:def 18 :
for b1 being UnOp of [.0,1.] holds
( b1 = NegationD2 iff for x being Element of [.0,1.] holds
( ( x = 1 implies b1 . x = 0 ) & ( x <> 1 implies b1 . 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
coherence
proof end;
coherence
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
proof end;

theorem :: FUZIMPL3:21
proof end;

theorem :: FUZIMPL3:22
proof end;

theorem :: FUZIMPL3:23
proof end;

theorem :: FUZIMPL3:24
proof end;

theorem :: FUZIMPL3:25
proof end;

theorem :: FUZIMPL3:26
proof end;

theorem :: FUZIMPL3:27
proof end;

theorem :: FUZIMPL3:28
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 <= () . (() . x)
proof end;

theorem :: FUZIMPL3:31
for I being satisfying_(EP) satisfying_(OP) BinOp of [.0,1.] holds (() * ()) * () = 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 b1 being Real st b1 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 b1 being UnOp of [.0,1.] st
for x being Element of [.0,1.] holds b1 . x = (1 - x) / (1 + (l * x))
proof end;
uniqueness
for b1, b2 being UnOp of [.0,1.] st ( for x being Element of [.0,1.] holds b1 . x = (1 - x) / (1 + (l * x)) ) & ( for x being Element of [.0,1.] holds b2 . x = (1 - x) / (1 + (l * x)) ) holds
b1 = b2
proof end;
end;

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

theorem :: FUZIMPL3:32
proof end;

registration
let r be - 1 _greater Real;
coherence
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 b1 being UnOp of [.0,1.] st
for x being Element of [.0,1.] holds b1 . x = (h ") . (f . (h . x))
proof end;
uniqueness
for b1, b2 being UnOp of [.0,1.] st ( for x being Element of [.0,1.] holds b1 . x = (h ") . (f . (h . x)) ) & ( for x being Element of [.0,1.] holds b2 . x = (h ") . (f . (h . x)) ) holds
b1 = b2
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 b3 being UnOp of [.0,1.] holds
( b3 = ConjNeg (f,h) iff for x being Element of [.0,1.] holds b3 . 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.];
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 ((),h) = FNegation (ConjImpl (I,h))
proof end;