:: Basic Formal Properties of Triangular Norms and Conorms
:: by Adam Grabowski
::
:: Received June 27, 2017
:: Copyright (c) 2017-2025 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{ F₁() -> non empty real-membered set , F₂( Real, Real) -> set } :

ex f being BinOp of F₁() st
for a, b being Element of F₁() holds f . (a,b) = F₂(a,b)

provided

A2: for a, b being Element of F₁() holds F₂(a,b) in F₁()

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 b₁ being BinOp of [.0,1.] st
for a, b being Element of [.0,1.] holds b₁ . (a,b) = min (a,b)

proof end;

uniqueness
for b₁, b₂ being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds b₁ . (a,b) = min (a,b) ) & ( for a, b being Element of [.0,1.] holds b₂ . (a,b) = min (a,b) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem MinDef defines minnorm FUZNORM1:def 6 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = minnorm iff for a, b being Element of [.0,1.] holds b₁ . (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 quasi_total commutative associative monotonic with-1-identity for Element of bool [:[:[.0,1.],[.0,1.]:],[.0,1.]:];

existence
ex b₁ being BinOp of [.0,1.] st
( b₁ is commutative & b₁ is associative & b₁ is monotonic & b₁ 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 b₁ being BinOp of [.0,1.] st
for a, b being Element of [.0,1.] holds b₁ . (a,b) = max (a,b)

proof end;

uniqueness
for b₁, b₂ being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds b₁ . (a,b) = max (a,b) ) & ( for a, b being Element of [.0,1.] holds b₂ . (a,b) = max (a,b) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem MaxDef defines maxnorm FUZNORM1:def 7 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = maxnorm iff for a, b being Element of [.0,1.] holds b₁ . (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 quasi_total commutative associative monotonic with-0-identity for Element of bool [:[:[.0,1.],[.0,1.]:],[.0,1.]:];

existence
ex b₁ being BinOp of [.0,1.] st
( b₁ is commutative & b₁ is associative & b₁ is monotonic & b₁ 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 quasi_total 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 b₁ being commutative monotonic with-1-identity BinOp of [.0,1.] holds b₁ is with-0-annihilating by NormIs0;

cluster Function-like quasi_total 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 b₁ being commutative monotonic with-0-identity BinOp of [.0,1.] holds b₁ 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 b₁ being BinOp of [.0,1.] st
for a, b being Element of [.0,1.] holds b₁ . (a,b) = a * b

proof end;

uniqueness
for b₁, b₂ being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds b₁ . (a,b) = a * b ) & ( for a, b being Element of [.0,1.] holds b₂ . (a,b) = a * b ) holds
b₁ = b₂

proof end;

end;

:: deftheorem ProdDef defines prodnorm FUZNORM1:def 8 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = prodnorm iff for a, b being Element of [.0,1.] holds b₁ . (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 b₁ being BinOp of [.0,1.] st
for a, b being Element of [.0,1.] holds b₁ . (a,b) = (a + b) - (a * b)

proof end;

uniqueness
for b₁, b₂ being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds b₁ . (a,b) = (a + b) - (a * b) ) & ( for a, b being Element of [.0,1.] holds b₂ . (a,b) = (a + b) - (a * b) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem ProbSumDef defines probsum_conorm FUZNORM1:def 9 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = probsum_conorm iff for a, b being Element of [.0,1.] holds b₁ . (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 b₁ being BinOp of [.0,1.] st
for a, b being Element of [.0,1.] holds b₁ . (a,b) = max (0,((a + b) - 1))

proof end;

uniqueness
for b₁, b₂ being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds b₁ . (a,b) = max (0,((a + b) - 1)) ) & ( for a, b being Element of [.0,1.] holds b₂ . (a,b) = max (0,((a + b) - 1)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem LukNorm defines Lukasiewicz_norm FUZNORM1:def 10 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = Lukasiewicz_norm iff for a, b being Element of [.0,1.] holds b₁ . (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 b₁ being BinOp of [.0,1.] st
for a, b being Element of [.0,1.] holds
( ( max (a,b) = 1 implies b₁ . (a,b) = min (a,b) ) & ( max (a,b) <> 1 implies b₁ . (a,b) = 0 ) )

proof end;

uniqueness
for b₁, b₂ being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds
( ( max (a,b) = 1 implies b₁ . (a,b) = min (a,b) ) & ( max (a,b) <> 1 implies b₁ . (a,b) = 0 ) ) ) & ( for a, b being Element of [.0,1.] holds
( ( max (a,b) = 1 implies b₂ . (a,b) = min (a,b) ) & ( max (a,b) <> 1 implies b₂ . (a,b) = 0 ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Drastic2Def defines drastic_norm FUZNORM1:def 11 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = drastic_norm iff for a, b being Element of [.0,1.] holds
( ( max (a,b) = 1 implies b₁ . (a,b) = min (a,b) ) & ( max (a,b) <> 1 implies b₁ . (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 b₁ being BinOp of [.0,1.] st
for a, b being Element of [.0,1.] holds
( ( a + b > 1 implies b₁ . (a,b) = min (a,b) ) & ( a + b <= 1 implies b₁ . (a,b) = 0 ) )

proof end;

uniqueness
for b₁, b₂ being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds
( ( a + b > 1 implies b₁ . (a,b) = min (a,b) ) & ( a + b <= 1 implies b₁ . (a,b) = 0 ) ) ) & ( for a, b being Element of [.0,1.] holds
( ( a + b > 1 implies b₂ . (a,b) = min (a,b) ) & ( a + b <= 1 implies b₂ . (a,b) = 0 ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem NilminDef defines nilmin_norm FUZNORM1:def 12 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = nilmin_norm iff for a, b being Element of [.0,1.] holds
( ( a + b > 1 implies b₁ . (a,b) = min (a,b) ) & ( a + b <= 1 implies b₁ . (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 b₁ being BinOp of [.0,1.] st
for a, b being Element of [.0,1.] holds b₁ . (a,b) = (a * b) / ((a + b) - (a * b))

proof end;

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

proof end;

end;

:: deftheorem HamDef defines Hamacher_norm FUZNORM1:def 13 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = Hamacher_norm iff for a, b being Element of [.0,1.] holds b₁ . (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 b₁ being BinOp of [.0,1.] st
for a, b being Element of [.0,1.] holds
( ( min (a,b) = 0 implies b₁ . (a,b) = max (a,b) ) & ( min (a,b) <> 0 implies b₁ . (a,b) = 1 ) )

proof end;

uniqueness
for b₁, b₂ being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds
( ( min (a,b) = 0 implies b₁ . (a,b) = max (a,b) ) & ( min (a,b) <> 0 implies b₁ . (a,b) = 1 ) ) ) & ( for a, b being Element of [.0,1.] holds
( ( min (a,b) = 0 implies b₂ . (a,b) = max (a,b) ) & ( min (a,b) <> 0 implies b₂ . (a,b) = 1 ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Drastic2CDef defines drastic_conorm FUZNORM1:def 14 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = drastic_conorm iff for a, b being Element of [.0,1.] holds
( ( min (a,b) = 0 implies b₁ . (a,b) = max (a,b) ) & ( min (a,b) <> 0 implies b₁ . (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 b₁ being BinOp of [.0,1.] st
for a, b being Element of [.0,1.] holds b₁ . (a,b) = 1 - (t . ((1 - a),(1 - b)))

proof end;

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

proof end;

end;

:: deftheorem CoDef defines conorm FUZNORM1:def 15 :
for t, b₂ being BinOp of [.0,1.] holds
( b₂ = conorm t iff for a, b being Element of [.0,1.] holds b₂ . (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 b₁ being BinOp of [.0,1.] st
for a, b being Element of [.0,1.] holds
( ( a = b & b = 1 implies b₁ . (a,b) = 1 ) & ( ( a <> 1 or b <> 1 ) implies b₁ . (a,b) = ((a + b) - ((2 * a) * b)) / (1 - (a * b)) ) )

proof end;

uniqueness
for b₁, b₂ being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds
( ( a = b & b = 1 implies b₁ . (a,b) = 1 ) & ( ( a <> 1 or b <> 1 ) implies b₁ . (a,b) = ((a + b) - ((2 * a) * b)) / (1 - (a * b)) ) ) ) & ( for a, b being Element of [.0,1.] holds
( ( a = b & b = 1 implies b₂ . (a,b) = 1 ) & ( ( a <> 1 or b <> 1 ) implies b₂ . (a,b) = ((a + b) - ((2 * a) * b)) / (1 - (a * b)) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem HamCoDef defines Hamacher_conorm FUZNORM1:def 17 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = Hamacher_conorm iff for a, b being Element of [.0,1.] holds
( ( a = b & b = 1 implies b₁ . (a,b) = 1 ) & ( ( a <> 1 or b <> 1 ) implies b₁ . (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 b₁ being BinOp of [.0,1.] st
for a, b being Element of [.0,1.] holds
( ( a + b < 1 implies b₁ . (a,b) = max (a,b) ) & ( a + b >= 1 implies b₁ . (a,b) = 1 ) )

proof end;

uniqueness
for b₁, b₂ being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds
( ( a + b < 1 implies b₁ . (a,b) = max (a,b) ) & ( a + b >= 1 implies b₁ . (a,b) = 1 ) ) ) & ( for a, b being Element of [.0,1.] holds
( ( a + b < 1 implies b₂ . (a,b) = max (a,b) ) & ( a + b >= 1 implies b₂ . (a,b) = 1 ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem NilmaxDef defines nilmax_conorm FUZNORM1:def 18 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = nilmax_conorm iff for a, b being Element of [.0,1.] holds
( ( a + b < 1 implies b₁ . (a,b) = max (a,b) ) & ( a + b >= 1 implies b₁ . (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 b₁ being BinOp of [.0,1.] st
for a, b being Element of [.0,1.] holds b₁ . (a,b) = min ((a + b),1)

proof end;

uniqueness
for b₁, b₂ being BinOp of [.0,1.] st ( for a, b being Element of [.0,1.] holds b₁ . (a,b) = min ((a + b),1) ) & ( for a, b being Element of [.0,1.] holds b₂ . (a,b) = min ((a + b),1) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem LukConorm defines BoundedSum_conorm FUZNORM1:def 19 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = BoundedSum_conorm iff for a, b being Element of [.0,1.] holds b₁ . (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;