:: Basic Formal Properties of Triangular Norms and Conorms
:: by Adam Grabowski
::
:: Received June 27, 2017
:: Copyright (c) 2017-2021 Association of Mizar Users


registration
cluster K276(0,1) -> non empty ;
coherence
not [.0,1.] is empty by XXREAL_1:1;
end;

theorem MinIn01: :: FUZNORM1:1
for a, b being Element of [.0,1.] holds min (a,b) in [.0,1.]
proof end;

theorem MaxIn01: :: FUZNORM1:2
for a, b being Element of [.0,1.] holds max (a,b) in [.0,1.]
proof end;

theorem Lemma1: :: FUZNORM1:3
for a, b being Element of [.0,1.] holds a * b in [.0,1.]
proof end;

theorem Lemma2: :: FUZNORM1:4
for a, b being Element of [.0,1.] holds max (0,((a + b) - 1)) in [.0,1.]
proof end;

theorem Lemma2a: :: FUZNORM1:5
for a, b being Element of [.0,1.] holds min ((a + b),1) in [.0,1.]
proof end;

theorem Lemma3: :: FUZNORM1:6
for a, b, c being Element of [.0,1.] holds max (0,(((max (0,((a + b) - 1))) + c) - 1)) = max (0,((a + (max (0,((b + c) - 1)))) - 1))
proof end;

theorem OpIn01: :: FUZNORM1:7
for a being Element of [.0,1.] holds 1 - a in [.0,1.]
proof end;

theorem abMinab01: :: FUZNORM1:8
for a, b being Element of [.0,1.] holds (a + b) - (a * b) in [.0,1.]
proof end;

theorem HamIn01: :: FUZNORM1:9
for a, b being Element of [.0,1.] holds (a * b) / ((a + b) - (a * b)) in [.0,1.]
proof end;

theorem DiffMax: :: FUZNORM1:10
for a, b being Element of [.0,1.] st max (a,b) <> 1 holds
( a <> 1 & b <> 1 )
proof end;

theorem Lemacik: :: FUZNORM1:11
for x, y being Element of [.0,1.] st x * y = x + y holds
x = 0
proof end;

theorem MaxMin: :: FUZNORM1:12
for a, b being Element of [.0,1.] holds max (a,b) = 1 - (min ((1 - a),(1 - b)))
proof end;

theorem LukasiDual: :: FUZNORM1:13
for a, b being Element of [.0,1.] holds min ((a + b),1) = 1 - (max (0,(((1 - a) + (1 - b)) - 1)))
proof end;

theorem HamCoIn01: :: FUZNORM1:14
for a, b being Element of [.0,1.] holds ((a + b) - ((2 * a) * b)) / (1 - (a * b)) in [.0,1.]
proof end;

registration
let f be BinOp of [.0,1.];
let a, b be Real;
cluster f . (a,b) -> real ;
coherence
f . (a,b) is real
proof end;
end;

theorem NormIn01: :: FUZNORM1:15
for a, b being Real
for t being BinOp of [.0,1.] holds t . (a,b) in [.0,1.]
proof end;

theorem CoIn01: :: FUZNORM1:16
for f being BinOp of [.0,1.]
for a, b being Real holds 1 - (f . ((1 - a),(1 - b))) in [.0,1.]
proof end;

theorem MES57: :: FUZNORM1:17
for x, y, k being Real st k <= 0 holds
( k * (min (x,y)) = max ((k * x),(k * y)) & k * (max (x,y)) = min ((k * x),(k * y)) )
proof end;

definition
let A be real-membered set ;
let f be BinOp of A;
attr f is monotonic means :MonDef: :: FUZNORM1:def 1
 for a, b, c, d being Element of A st a <= c & b <= d holds
f . (a,b) <= f . (c,d);
attr f is with-1-identity means :IdDef: :: FUZNORM1:def 2
 for a being Element of A holds f . (a,1) = a;
attr f is with-1-annihilating means :: FUZNORM1:def 3
 for a being Element of A holds f . (a,1) = 1;
attr f is with-0-identity means :ZeroDef: :: FUZNORM1:def 4
 for a being Element of A holds f . (a,0) = a;
attr f is with-0-annihilating means :: FUZNORM1:def 5
 for a being Element of A holds f . (a,0) = 0 ;
end;

:: deftheorem MonDef defines monotonic FUZNORM1:def 1 :
for A being real-membered set
for f being BinOp of A holds
( f is monotonic iff for a, b, c, d being Element of A st a <= c & b <= d holds
f . (a,b) <= f . (c,d) );

:: deftheorem IdDef defines with-1-identity FUZNORM1:def 2 :
for A being real-membered set
for f being BinOp of A holds
( f is with-1-identity iff for a being Element of A holds f . (a,1) = a );

:: deftheorem defines with-1-annihilating FUZNORM1:def 3 :
for A being real-membered set
for f being BinOp of A holds
( f is with-1-annihilating iff for a being Element of A holds f . (a,1) = 1 );

:: deftheorem ZeroDef defines with-0-identity FUZNORM1:def 4 :
for A being real-membered set
for f being BinOp of A holds
( f is with-0-identity iff for a being Element of A holds f . (a,0) = a );

:: deftheorem defines with-0-annihilating FUZNORM1:def 5 :
for A being real-membered set
for f being BinOp of A holds
( f is with-0-annihilating iff for a being Element of A holds f . (a,0) = 0 );

scheme :: FUZNORM1:sch 1
ExBinOp{ F1() -> non empty real-membered set , F2( Real, Real) -> set } :
ex f being BinOp of F1() st
for a, b being Element of F1() holds f . (a,b) = F2(a,b)
provided
A2: for a, b being Element of F1() holds F2(a,b) in F1()
proof end;

definition
func minnorm -> BinOp of [.0,1.] means :MinDef: :: FUZNORM1:def 6
 for a, b being Element of [.0,1.] holds it . (a,b) = min (a,b);
existence
ex b1 being BinOp of [.0,1.] st
for a, b being Element of [.0,1.] holds b1 . (a,b) = min (a,b)
proof end;
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds b1 . (a,b) = min (a,b) ) & ( for a, b being Element of [.0,1.] holds b2 . (a,b) = min (a,b) ) holds
b1 = b2
proof end;
end;

:: deftheorem MinDef defines minnorm FUZNORM1:def 6 :
for b1 being BinOp of [.0,1.] holds
( b1 = minnorm iff for a, b being Element of [.0,1.] holds b1 . (a,b) = min (a,b) );

registration
cluster minnorm -> commutative associative monotonic with-1-identity ;
coherence
( minnorm is commutative & minnorm is associative & minnorm is monotonic & minnorm is with-1-identity )
proof end;
end;

registration
cluster Relation-like [:[.0,1.],[.0,1.]:] -defined [.0,1.] -valued Function-like V30([:[.0,1.],[.0,1.]:],[.0,1.]) commutative associative monotonic with-1-identity for Element of bool [:[:[.0,1.],[.0,1.]:],[.0,1.]:];
existence
ex b1 being BinOp of [.0,1.] st
( b1 is commutative & b1 is associative & b1 is monotonic & b1 is with-1-identity )
proof end;
end;

definition
mode t-norm is commutative associative monotonic with-1-identity BinOp of [.0,1.];
end;

definition
func maxnorm -> BinOp of [.0,1.] means :MaxDef: :: FUZNORM1:def 7
 for a, b being Element of [.0,1.] holds it . (a,b) = max (a,b);
existence
ex b1 being BinOp of [.0,1.] st
for a, b being Element of [.0,1.] holds b1 . (a,b) = max (a,b)
proof end;
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds b1 . (a,b) = max (a,b) ) & ( for a, b being Element of [.0,1.] holds b2 . (a,b) = max (a,b) ) holds
b1 = b2
proof end;
end;

:: deftheorem MaxDef defines maxnorm FUZNORM1:def 7 :
for b1 being BinOp of [.0,1.] holds
( b1 = maxnorm iff for a, b being Element of [.0,1.] holds b1 . (a,b) = max (a,b) );

registration
cluster maxnorm -> commutative associative monotonic with-0-identity ;
coherence
( maxnorm is commutative & maxnorm is associative & maxnorm is monotonic & maxnorm is with-0-identity )
proof end;
end;

registration
cluster Relation-like [:[.0,1.],[.0,1.]:] -defined [.0,1.] -valued Function-like V30([:[.0,1.],[.0,1.]:],[.0,1.]) commutative associative monotonic with-0-identity for Element of bool [:[:[.0,1.],[.0,1.]:],[.0,1.]:];
existence
ex b1 being BinOp of [.0,1.] st
( b1 is commutative & b1 is associative & b1 is monotonic & b1 is with-0-identity )
proof end;
end;

definition
mode t-conorm is commutative associative monotonic with-0-identity BinOp of [.0,1.];
end;

theorem NormIs0: :: FUZNORM1:18
for t being commutative monotonic with-1-identity BinOp of [.0,1.]
for a being Element of [.0,1.] holds t . (a,0) = 0
proof end;

theorem ConormIs1: :: FUZNORM1:19
for t being commutative monotonic with-0-identity BinOp of [.0,1.]
for a being Element of [.0,1.] holds t . (a,1) = 1
proof end;

registration
cluster Function-like V30([:[.0,1.],[.0,1.]:],[.0,1.]) commutative monotonic with-1-identity -> commutative monotonic with-1-identity with-0-annihilating for Element of bool [:[:[.0,1.],[.0,1.]:],[.0,1.]:];
coherence
for b1 being commutative monotonic with-1-identity BinOp of [.0,1.] holds b1 is with-0-annihilating by NormIs0;
cluster Function-like V30([:[.0,1.],[.0,1.]:],[.0,1.]) commutative monotonic with-0-identity -> commutative monotonic with-1-annihilating with-0-identity for Element of bool [:[:[.0,1.],[.0,1.]:],[.0,1.]:];
coherence
for b1 being commutative monotonic with-0-identity BinOp of [.0,1.] holds b1 is with-1-annihilating by ConormIs1;
end;

definition
func prodnorm -> BinOp of [.0,1.] means :ProdDef: :: FUZNORM1:def 8
 for a, b being Element of [.0,1.] holds it . (a,b) = a * b;
existence
ex b1 being BinOp of [.0,1.] st
for a, b being Element of [.0,1.] holds b1 . (a,b) = a * b
proof end;
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds b1 . (a,b) = a * b ) & ( for a, b being Element of [.0,1.] holds b2 . (a,b) = a * b ) holds
b1 = b2
proof end;
end;

:: deftheorem ProdDef defines prodnorm FUZNORM1:def 8 :
for b1 being BinOp of [.0,1.] holds
( b1 = prodnorm iff for a, b being Element of [.0,1.] holds b1 . (a,b) = a * b );

registration
cluster prodnorm -> commutative associative monotonic with-1-identity ;
coherence
( prodnorm is commutative & prodnorm is associative & prodnorm is monotonic & prodnorm is with-1-identity )
proof end;
end;

definition
func probsum_conorm -> BinOp of [.0,1.] means :ProbSumDef: :: FUZNORM1:def 9
 for a, b being Element of [.0,1.] holds it . (a,b) = (a + b) - (a * b);
existence
ex b1 being BinOp of [.0,1.] st
for a, b being Element of [.0,1.] holds b1 . (a,b) = (a + b) - (a * b)
proof end;
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds b1 . (a,b) = (a + b) - (a * b) ) & ( for a, b being Element of [.0,1.] holds b2 . (a,b) = (a + b) - (a * b) ) holds
b1 = b2
proof end;
end;

:: deftheorem ProbSumDef defines probsum_conorm FUZNORM1:def 9 :
for b1 being BinOp of [.0,1.] holds
( b1 = probsum_conorm iff for a, b being Element of [.0,1.] holds b1 . (a,b) = (a + b) - (a * b) );

definition
func Lukasiewicz_norm -> BinOp of [.0,1.] means :LukNorm: :: FUZNORM1:def 10
 for a, b being Element of [.0,1.] holds it . (a,b) = max (0,((a + b) - 1));
existence
ex b1 being BinOp of [.0,1.] st
for a, b being Element of [.0,1.] holds b1 . (a,b) = max (0,((a + b) - 1))
proof end;
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds b1 . (a,b) = max (0,((a + b) - 1)) ) & ( for a, b being Element of [.0,1.] holds b2 . (a,b) = max (0,((a + b) - 1)) ) holds
b1 = b2
proof end;
end;

:: deftheorem LukNorm defines Lukasiewicz_norm FUZNORM1:def 10 :
for b1 being BinOp of [.0,1.] holds
( b1 = Lukasiewicz_norm iff for a, b being Element of [.0,1.] holds b1 . (a,b) = max (0,((a + b) - 1)) );

registration
cluster Lukasiewicz_norm -> commutative associative monotonic with-1-identity ;
coherence
( Lukasiewicz_norm is commutative & Lukasiewicz_norm is associative & Lukasiewicz_norm is monotonic & Lukasiewicz_norm is with-1-identity )
proof end;
end;

definition
func drastic_norm -> BinOp of [.0,1.] means :Drastic2Def: :: FUZNORM1:def 11
 for a, b being Element of [.0,1.] holds
( ( max (a,b) = 1 implies it . (a,b) = min (a,b) ) & ( max (a,b) <> 1 implies it . (a,b) = 0 ) );
existence
ex b1 being BinOp of [.0,1.] st
for a, b being Element of [.0,1.] holds
( ( max (a,b) = 1 implies b1 . (a,b) = min (a,b) ) & ( max (a,b) <> 1 implies b1 . (a,b) = 0 ) )
proof end;
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds
( ( max (a,b) = 1 implies b1 . (a,b) = min (a,b) ) & ( max (a,b) <> 1 implies b1 . (a,b) = 0 ) ) ) & ( for a, b being Element of [.0,1.] holds
( ( max (a,b) = 1 implies b2 . (a,b) = min (a,b) ) & ( max (a,b) <> 1 implies b2 . (a,b) = 0 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Drastic2Def defines drastic_norm FUZNORM1:def 11 :
for b1 being BinOp of [.0,1.] holds
( b1 = drastic_norm iff for a, b being Element of [.0,1.] holds
( ( max (a,b) = 1 implies b1 . (a,b) = min (a,b) ) & ( max (a,b) <> 1 implies b1 . (a,b) = 0 ) ) );

theorem DrasticDef: :: FUZNORM1:20
for a, b being Element of [.0,1.] holds
( ( a = 1 implies drastic_norm . (a,b) = b ) & ( b = 1 implies drastic_norm . (a,b) = a ) & ( a <> 1 & b <> 1 implies drastic_norm . (a,b) = 0 ) )
proof end;

registration
cluster drastic_norm -> commutative associative monotonic with-1-identity ;
coherence
( drastic_norm is commutative & drastic_norm is associative & drastic_norm is with-1-identity & drastic_norm is monotonic )
proof end;
end;

definition
func nilmin_norm -> BinOp of [.0,1.] means :NilminDef: :: FUZNORM1:def 12
 for a, b being Element of [.0,1.] holds
( ( a + b > 1 implies it . (a,b) = min (a,b) ) & ( a + b <= 1 implies it . (a,b) = 0 ) );
existence
ex b1 being BinOp of [.0,1.] st
for a, b being Element of [.0,1.] holds
( ( a + b > 1 implies b1 . (a,b) = min (a,b) ) & ( a + b <= 1 implies b1 . (a,b) = 0 ) )
proof end;
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds
( ( a + b > 1 implies b1 . (a,b) = min (a,b) ) & ( a + b <= 1 implies b1 . (a,b) = 0 ) ) ) & ( for a, b being Element of [.0,1.] holds
( ( a + b > 1 implies b2 . (a,b) = min (a,b) ) & ( a + b <= 1 implies b2 . (a,b) = 0 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem NilminDef defines nilmin_norm FUZNORM1:def 12 :
for b1 being BinOp of [.0,1.] holds
( b1 = nilmin_norm iff for a, b being Element of [.0,1.] holds
( ( a + b > 1 implies b1 . (a,b) = min (a,b) ) & ( a + b <= 1 implies b1 . (a,b) = 0 ) ) );

registration
cluster nilmin_norm -> commutative associative monotonic with-1-identity ;
coherence
( nilmin_norm is commutative & nilmin_norm is associative & nilmin_norm is with-1-identity & nilmin_norm is monotonic )
proof end;
end;

definition
func Hamacher_norm -> BinOp of [.0,1.] means :HamDef: :: FUZNORM1:def 13
 for a, b being Element of [.0,1.] holds it . (a,b) = (a * b) / ((a + b) - (a * b));
existence
ex b1 being BinOp of [.0,1.] st
for a, b being Element of [.0,1.] holds b1 . (a,b) = (a * b) / ((a + b) - (a * b))
proof end;
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds b1 . (a,b) = (a * b) / ((a + b) - (a * b)) ) & ( for a, b being Element of [.0,1.] holds b2 . (a,b) = (a * b) / ((a + b) - (a * b)) ) holds
b1 = b2
proof end;
end;

:: deftheorem HamDef defines Hamacher_norm FUZNORM1:def 13 :
for b1 being BinOp of [.0,1.] holds
( b1 = Hamacher_norm iff for a, b being Element of [.0,1.] holds b1 . (a,b) = (a * b) / ((a + b) - (a * b)) );

registration
cluster Hamacher_norm -> commutative associative monotonic with-1-identity ;
coherence
( Hamacher_norm is commutative & Hamacher_norm is associative & Hamacher_norm is with-1-identity & Hamacher_norm is monotonic )
proof end;
end;

definition
func drastic_conorm -> BinOp of [.0,1.] means :Drastic2CDef: :: FUZNORM1:def 14
 for a, b being Element of [.0,1.] holds
( ( min (a,b) = 0 implies it . (a,b) = max (a,b) ) & ( min (a,b) <> 0 implies it . (a,b) = 1 ) );
existence
ex b1 being BinOp of [.0,1.] st
for a, b being Element of [.0,1.] holds
( ( min (a,b) = 0 implies b1 . (a,b) = max (a,b) ) & ( min (a,b) <> 0 implies b1 . (a,b) = 1 ) )
proof end;
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds
( ( min (a,b) = 0 implies b1 . (a,b) = max (a,b) ) & ( min (a,b) <> 0 implies b1 . (a,b) = 1 ) ) ) & ( for a, b being Element of [.0,1.] holds
( ( min (a,b) = 0 implies b2 . (a,b) = max (a,b) ) & ( min (a,b) <> 0 implies b2 . (a,b) = 1 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Drastic2CDef defines drastic_conorm FUZNORM1:def 14 :
for b1 being BinOp of [.0,1.] holds
( b1 = drastic_conorm iff for a, b being Element of [.0,1.] holds
( ( min (a,b) = 0 implies b1 . (a,b) = max (a,b) ) & ( min (a,b) <> 0 implies b1 . (a,b) = 1 ) ) );

definition
let t be BinOp of [.0,1.];
func conorm t -> BinOp of [.0,1.] means :CoDef: :: FUZNORM1:def 15
 for a, b being Element of [.0,1.] holds it . (a,b) = 1 - (t . ((1 - a),(1 - b)));
existence
ex b1 being BinOp of [.0,1.] st
for a, b being Element of [.0,1.] holds b1 . (a,b) = 1 - (t . ((1 - a),(1 - b)))
proof end;
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds b1 . (a,b) = 1 - (t . ((1 - a),(1 - b))) ) & ( for a, b being Element of [.0,1.] holds b2 . (a,b) = 1 - (t . ((1 - a),(1 - b))) ) holds
b1 = b2
proof end;
end;

:: deftheorem CoDef defines conorm FUZNORM1:def 15 :
for t, b2 being BinOp of [.0,1.] holds
( b2 = conorm t iff for a, b being Element of [.0,1.] holds b2 . (a,b) = 1 - (t . ((1 - a),(1 - b))) );

registration
let t be t-norm;
cluster conorm t -> commutative associative monotonic with-0-identity ;
coherence
( conorm t is monotonic & conorm t is commutative & conorm t is associative & conorm t is with-0-identity )
proof end;
end;

theorem :: FUZNORM1:21
maxnorm = conorm minnorm
proof end;

theorem :: FUZNORM1:22
for t being BinOp of [.0,1.] holds conorm (conorm t) = t
proof end;

definition
let f1, f2 be BinOp of [.0,1.];
pred f1 <= f2 means :: FUZNORM1:def 16
 for a, b being Element of [.0,1.] holds f1 . (a,b) <= f2 . (a,b);
end;

:: deftheorem defines <= FUZNORM1:def 16 :
for f1, f2 being BinOp of [.0,1.] holds
( f1 <= f2 iff for a, b being Element of [.0,1.] holds f1 . (a,b) <= f2 . (a,b) );

theorem :: FUZNORM1:23
for t being t-norm holds drastic_norm <= t
proof end;

theorem :: FUZNORM1:24
for t being t-norm holds t <= minnorm
proof end;

theorem :: FUZNORM1:25
for t1, t2 being t-norm st t1 <= t2 holds
conorm t2 <= conorm t1
proof end;

definition
func Hamacher_conorm -> BinOp of [.0,1.] means :HamCoDef: :: FUZNORM1:def 17
 for a, b being Element of [.0,1.] holds
( ( a = b & b = 1 implies it . (a,b) = 1 ) & ( ( a <> 1 or b <> 1 ) implies it . (a,b) = ((a + b) - ((2 * a) * b)) / (1 - (a * b)) ) );
existence
ex b1 being BinOp of [.0,1.] st
for a, b being Element of [.0,1.] holds
( ( a = b & b = 1 implies b1 . (a,b) = 1 ) & ( ( a <> 1 or b <> 1 ) implies b1 . (a,b) = ((a + b) - ((2 * a) * b)) / (1 - (a * b)) ) )
proof end;
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds
( ( a = b & b = 1 implies b1 . (a,b) = 1 ) & ( ( a <> 1 or b <> 1 ) implies b1 . (a,b) = ((a + b) - ((2 * a) * b)) / (1 - (a * b)) ) ) ) & ( for a, b being Element of [.0,1.] holds
( ( a = b & b = 1 implies b2 . (a,b) = 1 ) & ( ( a <> 1 or b <> 1 ) implies b2 . (a,b) = ((a + b) - ((2 * a) * b)) / (1 - (a * b)) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem HamCoDef defines Hamacher_conorm FUZNORM1:def 17 :
for b1 being BinOp of [.0,1.] holds
( b1 = Hamacher_conorm iff for a, b being Element of [.0,1.] holds
( ( a = b & b = 1 implies b1 . (a,b) = 1 ) & ( ( a <> 1 or b <> 1 ) implies b1 . (a,b) = ((a + b) - ((2 * a) * b)) / (1 - (a * b)) ) ) );

theorem CoHam: :: FUZNORM1:26
conorm Hamacher_norm = Hamacher_conorm
proof end;

registration
cluster Hamacher_conorm -> commutative associative monotonic with-0-identity ;
coherence
( Hamacher_conorm is commutative & Hamacher_conorm is associative & Hamacher_conorm is with-0-identity & Hamacher_conorm is monotonic ) by CoHam;
end;

theorem :: FUZNORM1:27
conorm drastic_norm = drastic_conorm
proof end;

theorem ConormProd: :: FUZNORM1:28
conorm prodnorm = probsum_conorm
proof end;

registration
cluster probsum_conorm -> commutative associative monotonic with-0-identity ;
coherence
( probsum_conorm is commutative & probsum_conorm is associative & probsum_conorm is with-0-identity & probsum_conorm is monotonic ) by ConormProd;
end;

definition
func nilmax_conorm -> BinOp of [.0,1.] means :NilmaxDef: :: FUZNORM1:def 18
 for a, b being Element of [.0,1.] holds
( ( a + b < 1 implies it . (a,b) = max (a,b) ) & ( a + b >= 1 implies it . (a,b) = 1 ) );
existence
ex b1 being BinOp of [.0,1.] st
for a, b being Element of [.0,1.] holds
( ( a + b < 1 implies b1 . (a,b) = max (a,b) ) & ( a + b >= 1 implies b1 . (a,b) = 1 ) )
proof end;
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds
( ( a + b < 1 implies b1 . (a,b) = max (a,b) ) & ( a + b >= 1 implies b1 . (a,b) = 1 ) ) ) & ( for a, b being Element of [.0,1.] holds
( ( a + b < 1 implies b2 . (a,b) = max (a,b) ) & ( a + b >= 1 implies b2 . (a,b) = 1 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem NilmaxDef defines nilmax_conorm FUZNORM1:def 18 :
for b1 being BinOp of [.0,1.] holds
( b1 = nilmax_conorm iff for a, b being Element of [.0,1.] holds
( ( a + b < 1 implies b1 . (a,b) = max (a,b) ) & ( a + b >= 1 implies b1 . (a,b) = 1 ) ) );

theorem ConormNilmin: :: FUZNORM1:29
conorm nilmin_norm = nilmax_conorm
proof end;

registration
cluster nilmax_conorm -> commutative associative monotonic with-0-identity ;
coherence
( nilmax_conorm is commutative & nilmax_conorm is associative & nilmax_conorm is with-0-identity & nilmax_conorm is monotonic ) by ConormNilmin;
end;

definition
func BoundedSum_conorm -> BinOp of [.0,1.] means :LukConorm: :: FUZNORM1:def 19
 for a, b being Element of [.0,1.] holds it . (a,b) = min ((a + b),1);
existence
ex b1 being BinOp of [.0,1.] st
for a, b being Element of [.0,1.] holds b1 . (a,b) = min ((a + b),1)
proof end;
uniqueness
for b1, b2 being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds b1 . (a,b) = min ((a + b),1) ) & ( for a, b being Element of [.0,1.] holds b2 . (a,b) = min ((a + b),1) ) holds
b1 = b2
proof end;
end;

:: deftheorem LukConorm defines BoundedSum_conorm FUZNORM1:def 19 :
for b1 being BinOp of [.0,1.] holds
( b1 = BoundedSum_conorm iff for a, b being Element of [.0,1.] holds b1 . (a,b) = min ((a + b),1) );

theorem ConormLukasiewicz: :: FUZNORM1:30
conorm Lukasiewicz_norm = BoundedSum_conorm
proof end;

registration
cluster BoundedSum_conorm -> commutative associative monotonic with-0-identity ;
coherence
( BoundedSum_conorm is commutative & BoundedSum_conorm is associative & BoundedSum_conorm is with-0-identity & BoundedSum_conorm is monotonic ) by ConormLukasiewicz;
end;

theorem :: FUZNORM1:31
for t being t-conorm holds maxnorm <= t
proof end;

theorem :: FUZNORM1:32
for t being t-conorm holds t <= drastic_conorm
proof end;