:: On Fuzzy Negations and Laws of Contraposition. Lattice of Fuzzy Negations
:: by Adam Grabowski
::
:: Received November 21, 2023
:: Copyright (c) 2023-2025 Association of Mizar Users

:: Definition 1.5.1

registration

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

existence
ex b₁ being Fuzzy_Negation st b₁ is decreasing

proof end;

end;

definition

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

attr I is N -satisfying_CP means :: FUZIMPL4:def 1
for x, y being Element of [.0,1.] holds I . (x,y) = I . ((N . y),(N . x));

end;

:: deftheorem defines -satisfying_CP FUZIMPL4:def 1 :
for N being Fuzzy_Negation
for I being BinOp of [.0,1.] holds
( I is N -satisfying_CP iff for x, y being Element of [.0,1.] holds I . (x,y) = I . ((N . y),(N . x)) );

definition

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

attr I is N -satisfying_L-CP means :: FUZIMPL4:def 2
for x, y being Element of [.0,1.] holds I . ((N . x),y) = I . ((N . y),x);

end;

:: deftheorem defines -satisfying_L-CP FUZIMPL4:def 2 :
for N being Fuzzy_Negation
for I being BinOp of [.0,1.] holds
( I is N -satisfying_L-CP iff for x, y being Element of [.0,1.] holds I . ((N . x),y) = I . ((N . y),x) );

definition

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

attr I is N -satisfying_R-CP means :: FUZIMPL4:def 3
for x, y being Element of [.0,1.] holds I . (x,(N . y)) = I . (y,(N . x));

end;

:: deftheorem defines -satisfying_R-CP FUZIMPL4:def 3 :
for N being Fuzzy_Negation
for I being BinOp of [.0,1.] holds
( I is N -satisfying_R-CP iff for x, y being Element of [.0,1.] holds I . (x,(N . y)) = I . (y,(N . x)) );

theorem :: FUZIMPL4:1

N_CC = (AffineMap ((- 1),1)) | [.0,1.]

proof end;

registration

cluster N_CC -> continuous ;

coherence
N_CC is continuous

proof end;

end;

registration

cluster N_CC -> negation-strong ;

coherence
N_CC is negation-strong

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) negation-strict for Element of bool [:[.0,1.],[.0,1.]:];

existence
ex b₁ being Fuzzy_Negation st b₁ is negation-strict

proof 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) negation-strong for Element of bool [:[.0,1.],[.0,1.]:];

existence
ex b₁ being Fuzzy_Negation st b₁ is negation-strong

proof end;

end;

:: Every strong negation is strict
:: if N is negation-strict, then it is decreasing, so N is one-to-one

registration

cluster Function-like quasi_total satisfying_(N1) satisfying_(N2) satisfying_(N3) -> decreasing for Element of bool [:[.0,1.],[.0,1.]:];

coherence
for b₁ being Fuzzy_Negation st b₁ is satisfying_(N3) holds
b₁ is decreasing by FUZIMPL3:def 9;

cluster Function-like quasi_total decreasing satisfying_(N1) satisfying_(N2) -> satisfying_(N3) for Element of bool [:[.0,1.],[.0,1.]:];

coherence
for b₁ being Fuzzy_Negation st b₁ is decreasing holds
b₁ is satisfying_(N3) by FUZIMPL3:def 9;

end;

:: cluster FINSEQ_1 for increasing

registration

cluster Function-like quasi_total -> REAL -defined real-valued for Element of bool [:[.0,1.],[.0,1.]:];

coherence
for b₁ being UnOp of [.0,1.] holds
( b₁ is REAL -defined & b₁ is real-valued )

proof end;

end;

registration

cluster Relation-like REAL -defined Function-like real-valued decreasing -> one-to-one real-valued for set ;

coherence
for b₁ being real-valued Function st b₁ is REAL -defined & b₁ is decreasing holds
b₁ is one-to-one

proof end;

end;

registration

cluster Function-like quasi_total decreasing -> one-to-one for Element of bool [:[.0,1.],[.0,1.]:];

coherence
for b₁ being UnOp of [.0,1.] st b₁ is decreasing holds
b₁ is one-to-one ;

end;

registration

cluster Function-like quasi_total satisfying_(N1) satisfying_(N2) -> non-increasing for Element of bool [:[.0,1.],[.0,1.]:];

coherence
for b₁ being Fuzzy_Negation holds b₁ is non-increasing by FUZIMPL3:def 5;

end;

registration

cluster Function-like quasi_total satisfying_(N1) satisfying_(N2) negation-strict -> one-to-one for Element of bool [:[.0,1.],[.0,1.]:];

coherence
for b₁ being Fuzzy_Negation st b₁ is negation-strict holds
b₁ is one-to-one

proof end;

end;

theorem LemmaOne: :: FUZIMPL4:2

for R being Function st R ~ is Function holds
R is one-to-one

proof end;

theorem :: FUZIMPL4:3

for N1, N2 being Fuzzy_Negation st N1 ~ = N2 holds
N1 is one-to-one by LemmaOne;

theorem LemmaOnto2: :: FUZIMPL4:4

for N1, N2 being Fuzzy_Negation st N1 ~ = N2 holds
N1 is onto

proof end;

:: Proposition 1.5.2

theorem :: FUZIMPL4:5

for I being BinOp of [.0,1.]
for N being negation-strict Fuzzy_Negation
for N1 being Fuzzy_Negation st N ~ = N1 holds
( I is N -satisfying_L-CP iff I is N1 -satisfying_R-CP )

proof end;

:: Proposition 1.5.3 (i) => (ii)

theorem Lemma15312: :: FUZIMPL4:6

for I being BinOp of [.0,1.]
for N being negation-strong Fuzzy_Negation st I is N -satisfying_CP holds
I is N -satisfying_L-CP

proof end;

:: Proposition 1.5.3 (ii) => (iii)

theorem Lemma15323: :: FUZIMPL4:7

for I being BinOp of [.0,1.]
for N being negation-strong Fuzzy_Negation st I is N -satisfying_L-CP holds
I is N -satisfying_R-CP

proof end;

:: Proposition 1.5.3 (iii) => (i)

theorem Lemma15331: :: FUZIMPL4:8

for I being BinOp of [.0,1.]
for N being negation-strong Fuzzy_Negation st I is N -satisfying_R-CP holds
I is N -satisfying_CP

proof end;

:: Proposition 1.5.3 (i) <=> (ii)

theorem :: FUZIMPL4:9

for I being BinOp of [.0,1.]
for N being negation-strong Fuzzy_Negation holds
( I is N -satisfying_CP iff I is N -satisfying_L-CP ) by Lemma15312, Lemma15323, Lemma15331;

:: Proposition 1.5.3 (i) <=> (iii)

theorem :: FUZIMPL4:10

for I being BinOp of [.0,1.]
for N being negation-strong Fuzzy_Negation holds
( I is N -satisfying_CP iff I is N -satisfying_R-CP ) by Lemma15312, Lemma15323, Lemma15331;

:: Lemma 1.5.4 (i)

theorem Lemma154i: :: FUZIMPL4:11

for I being BinOp of [.0,1.]
for N being Fuzzy_Negation st I is satisfying_(I1) & I is N -satisfying_CP holds
I is satisfying_(I2)

proof end;

:: Lemma 1.5.4 (ii)

theorem Lemma154ii: :: FUZIMPL4:12

for I being BinOp of [.0,1.]
for N being Fuzzy_Negation st I is satisfying_(I2) & I is N -satisfying_CP holds
I is satisfying_(I1)

proof end;

:: Lemma 1.5.4 (iii)

theorem Lemma154iii: :: FUZIMPL4:13

for I being BinOp of [.0,1.]
for N being Fuzzy_Negation st I is satisfying_(LB) & I is N -satisfying_CP holds
I is satisfying_(RB)

proof end;

:: Lemma 1.5.4 (iv)

theorem Lemma154iv: :: FUZIMPL4:14

for I being BinOp of [.0,1.]
for N being Fuzzy_Negation st I is satisfying_(RB) & I is N -satisfying_CP holds
I is satisfying_(LB)

proof end;

:: Lemma 1.5.4 (v) a

theorem Lemma154va: :: FUZIMPL4:15

for I being BinOp of [.0,1.]
for N being Fuzzy_Negation st I is satisfying_(NP) & I is N -satisfying_CP holds
( N = FNegation I & FNegation I is negation-strong )

proof end;

:: Lemma 1.5.4 (v) b

theorem Lemma154vb: :: FUZIMPL4:16

for I being BinOp of [.0,1.]
for N being Fuzzy_Negation st I is satisfying_(NP) & I is N -satisfying_CP holds
( I is satisfying_(I3) & I is satisfying_(I4) & I is satisfying_(I5) )

proof end;

:: Corollary 1.5.5

theorem :: FUZIMPL4:17

for I being BinOp of [.0,1.] st I is satisfying_(NP) & not FNegation I is negation-strong holds
for N being Fuzzy_Negation holds not I is N -satisfying_CP by Lemma154va;

:: Lemma 1.5.6 (i)

theorem Lemma156i: :: FUZIMPL4:18

for I being BinOp of [.0,1.]
for N being negation-strong Fuzzy_Negation st N = FNegation I & I is N -satisfying_CP holds
I is satisfying_(NP)

proof end;

:: Lemma 1.5.6 (ii)

theorem Lemma156ii: :: FUZIMPL4:19

for I being BinOp of [.0,1.]
for N being negation-strong Fuzzy_Negation st N = FNegation I & I is satisfying_(EP) holds
( I is satisfying_(I3) & I is satisfying_(I4) & I is satisfying_(I5) & I is satisfying_(NP) & I is N -satisfying_CP )

proof end;

theorem Corr157i: :: FUZIMPL4:20

for I being BinOp of [.0,1.]
for N being Fuzzy_Negation st I is N -satisfying_CP holds
( I is satisfying_(I1) iff I is satisfying_(I2) ) by Lemma154i, Lemma154ii;

theorem :: FUZIMPL4:21

for I being BinOp of [.0,1.]
for N being Fuzzy_Negation st I is N -satisfying_CP holds
( I is satisfying_(LB) iff I is satisfying_(RB) ) by Lemma154iii, Lemma154iv;

theorem :: FUZIMPL4:22

for I being BinOp of [.0,1.]
for N being Fuzzy_Negation st I is N -satisfying_CP & N is negation-strong holds
( I is satisfying_(NP) iff N = FNegation I ) by Lemma154va, Lemma156i;

theorem :: FUZIMPL4:23

for I being BinOp of [.0,1.]
for N being Fuzzy_Negation st I is N -satisfying_CP & I is satisfying_(I1) & I is satisfying_(NP) holds
( I in FI & FNegation I = N & N is negation-strong )

proof end;

theorem :: FUZIMPL4:24

for I being satisfying_(NP) satisfying_(EP) Fuzzy_Implication holds
( FNegation I is negation-strong iff I is FNegation I -satisfying_CP ) by Lemma154va, Lemma156ii;

:: Example 1.5.10
:: (ii) I_4

definition

:: Example 1.5.10
:: (ii) I_4

func I_I3 -> BinOp of [.0,1.] means :II3Def: :: FUZIMPL4:def 4
for x, y being Element of [.0,1.] holds
( ( ( x = 0 or y <> 0 ) implies it . (x,y) = 1 ) & ( x <> 0 & y = 0 implies it . (x,y) = 0 ) );

existence
ex b₁ being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds
( ( ( x = 0 or y <> 0 ) implies b₁ . (x,y) = 1 ) & ( x <> 0 & y = 0 implies b₁ . (x,y) = 0 ) )

proof end;

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

proof end;

end;

:: deftheorem II3Def defines I_I3 FUZIMPL4:def 4 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = I_I3 iff for x, y being Element of [.0,1.] holds
( ( ( x = 0 or y <> 0 ) implies b₁ . (x,y) = 1 ) & ( x <> 0 & y = 0 implies b₁ . (x,y) = 0 ) ) );

registration

cluster I_I3 -> decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak ;

coherence
( I_I3 is decreasing_on_1st & I_I3 is increasing_on_2nd & I_I3 is 00-dominant & I_I3 is 11-dominant & I_I3 is 10-weak )

proof end;

end;

theorem FNegI3: :: FUZIMPL4:25

FNegation I_I3 = NegationD1

proof end;

registration

cluster I_I3 -> non satisfying_(NP) satisfying_(EP) ;

coherence
( I_I3 is satisfying_(EP) & not I_I3 is satisfying_(NP) )

proof end;

end;

registration

cluster I_I3 -> FNegation I_I3 -satisfying_CP ;

coherence
I_I3 is FNegation I_I3 -satisfying_CP

proof end;

end;

definition

func I_I4 -> BinOp of [.0,1.] means :II4Def: :: FUZIMPL4:def 5
for x, y being Element of [.0,1.] holds
( ( ( x <> 1 or y = 1 ) implies it . (x,y) = 1 ) & ( x = 1 & y <> 1 implies it . (x,y) = 0 ) );

existence
ex b₁ being BinOp of [.0,1.] st
for x, y being Element of [.0,1.] holds
( ( ( x <> 1 or y = 1 ) implies b₁ . (x,y) = 1 ) & ( x = 1 & y <> 1 implies b₁ . (x,y) = 0 ) )

proof end;

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

proof end;

end;

:: deftheorem II4Def defines I_I4 FUZIMPL4:def 5 :
for b₁ being BinOp of [.0,1.] holds
( b₁ = I_I4 iff for x, y being Element of [.0,1.] holds
( ( ( x <> 1 or y = 1 ) implies b₁ . (x,y) = 1 ) & ( x = 1 & y <> 1 implies b₁ . (x,y) = 0 ) ) );

registration

cluster I_I4 -> decreasing_on_1st increasing_on_2nd 00-dominant 11-dominant 10-weak ;

coherence
( I_I4 is decreasing_on_1st & I_I4 is increasing_on_2nd & I_I4 is 00-dominant & I_I4 is 11-dominant & I_I4 is 10-weak )

proof end;

end;

theorem FNegD2: :: FUZIMPL4:26

FNegation I_I4 = NegationD2

proof end;

registration

cluster I_I4 -> non satisfying_(NP) satisfying_(EP) ;

coherence
( I_I4 is satisfying_(EP) & not I_I4 is satisfying_(NP) )

proof end;

end;

registration

cluster I_I4 -> FNegation I_I4 -satisfying_CP ;

coherence
I_I4 is FNegation I_I4 -satisfying_CP

proof end;

end;

:: Attribute satisfying CP wrt the natural negation

definition

let I be Fuzzy_Implication;

attr I is satisfying_CP means :: FUZIMPL4:def 6
I is FNegation I -satisfying_CP ;

attr I is satisfying_L-CP means :: FUZIMPL4:def 7
I is FNegation I -satisfying_L-CP ;

attr I is satisfying_R-CP means :: FUZIMPL4:def 8
I is FNegation I -satisfying_R-CP ;

end;

:: deftheorem defines satisfying_CP FUZIMPL4:def 6 :
for I being Fuzzy_Implication holds
( I is satisfying_CP iff I is FNegation I -satisfying_CP );

:: deftheorem defines satisfying_L-CP FUZIMPL4:def 7 :
for I being Fuzzy_Implication holds
( I is satisfying_L-CP iff I is FNegation I -satisfying_L-CP );

:: deftheorem defines satisfying_R-CP FUZIMPL4:def 8 :
for I being Fuzzy_Implication holds
( I is satisfying_R-CP iff I is FNegation I -satisfying_R-CP );

LKIsCP: I_LK is N_CC -satisfying_CP

proof end;

LKIsLCP: I_LK is N_CC -satisfying_L-CP

proof end;

LKIsRCP: I_LK is N_CC -satisfying_R-CP

proof end;

registration

cluster Lukasiewicz_implication -> N_CC -satisfying_CP N_CC -satisfying_L-CP N_CC -satisfying_R-CP ;

coherence
( I_LK is N_CC -satisfying_L-CP & I_LK is N_CC -satisfying_R-CP & I_LK is N_CC -satisfying_CP ) by LKIsRCP, LKIsLCP, LKIsCP;

end;

registration

cluster Lukasiewicz_implication -> satisfying_CP satisfying_L-CP satisfying_R-CP ;

coherence
( I_LK is satisfying_L-CP & I_LK is satisfying_R-CP & I_LK is satisfying_CP ) by FUZIMPL3:20;

end;

registration

cluster Goedel_implication -> NegationD1 -satisfying_R-CP ;

coherence
I_GD is NegationD1 -satisfying_R-CP

proof end;

end;

registration

cluster Goedel_implication -> satisfying_R-CP ;

coherence
I_GD is satisfying_R-CP by FUZIMPL3:21;

end;

IRCIsCP: I_RC is N_CC -satisfying_CP

proof end;

IRCIsLCP: I_RC is N_CC -satisfying_L-CP

proof end;

IRCIsRCP: I_RC is N_CC -satisfying_R-CP

proof end;

registration

cluster Reichenbach_implication -> N_CC -satisfying_CP N_CC -satisfying_L-CP N_CC -satisfying_R-CP ;

coherence
( I_RC is N_CC -satisfying_CP & I_RC is N_CC -satisfying_L-CP & I_RC is N_CC -satisfying_R-CP ) by IRCIsCP, IRCIsLCP, IRCIsRCP;

end;

registration

cluster Reichenbach_implication -> satisfying_CP satisfying_L-CP satisfying_R-CP ;

coherence
( I_RC is satisfying_CP & I_RC is satisfying_L-CP & I_RC is satisfying_R-CP ) by FUZIMPL3:22;

end;

registration

cluster Kleene-Dienes_implication -> N_CC -satisfying_CP ;

coherence
I_KD is N_CC -satisfying_CP

proof end;

end;

registration

cluster Kleene-Dienes_implication -> N_CC -satisfying_L-CP ;

coherence
I_KD is N_CC -satisfying_L-CP

proof end;

end;

registration

cluster Kleene-Dienes_implication -> N_CC -satisfying_R-CP ;

coherence
I_KD is N_CC -satisfying_R-CP

proof end;

end;

registration

cluster Kleene-Dienes_implication -> satisfying_CP satisfying_L-CP satisfying_R-CP ;

coherence
( I_KD is satisfying_CP & I_KD is satisfying_L-CP & I_KD is satisfying_R-CP ) by FUZIMPL3:23;

end;

registration

cluster Goguen_implication -> NegationD1 -satisfying_R-CP ;

coherence
I_GG is NegationD1 -satisfying_R-CP

proof end;

end;

registration

cluster Goguen_implication -> satisfying_R-CP ;

coherence
I_GG is satisfying_R-CP by FUZIMPL3:24;

end;

IRSIsCP: I_RS is N_CC -satisfying_CP

proof end;

theorem IRSIsLCP: :: FUZIMPL4:27

I_RS is N_CC -satisfying_L-CP

proof end;

IRSIsRCP: I_RS is N_CC -satisfying_R-CP

proof end;

registration

cluster Rescher_implication -> N_CC -satisfying_CP N_CC -satisfying_L-CP N_CC -satisfying_R-CP ;

coherence
( I_RS is N_CC -satisfying_CP & I_RS is N_CC -satisfying_L-CP & I_RS is N_CC -satisfying_R-CP ) by IRSIsCP, IRSIsLCP, IRSIsRCP;

end;

theorem :: FUZIMPL4:28

for N being decreasing Fuzzy_Negation holds I_RS is N -satisfying_CP

proof end;

registration

cluster Yager_implication -> NegationD1 -satisfying_R-CP ;

coherence
I_YG is NegationD1 -satisfying_R-CP

proof end;

end;

registration

cluster Yager_implication -> satisfying_R-CP ;

coherence
I_YG is satisfying_R-CP by FUZIMPL3:26;

end;

registration

cluster Weber_implication -> NegationD2 -satisfying_R-CP ;

coherence
I_WB is NegationD2 -satisfying_R-CP

proof end;

end;

registration

cluster Weber_implication -> satisfying_R-CP ;

coherence
I_WB is satisfying_R-CP by FUZIMPL3:27;

end;

IFDIsCP: I_FD is N_CC -satisfying_CP

proof end;

IFDIsLCP: I_FD is N_CC -satisfying_L-CP

proof end;

IFDIsRCP: I_FD is N_CC -satisfying_R-CP

proof end;

registration

cluster Fodor_implication -> N_CC -satisfying_CP N_CC -satisfying_L-CP N_CC -satisfying_R-CP ;

coherence
( I_FD is N_CC -satisfying_CP & I_FD is N_CC -satisfying_L-CP & I_FD is N_CC -satisfying_R-CP ) by IFDIsCP, IFDIsLCP, IFDIsRCP;

end;

registration

cluster Fodor_implication -> satisfying_CP satisfying_L-CP satisfying_R-CP ;

coherence
( I_FD is satisfying_CP & I_FD is satisfying_L-CP & I_FD is satisfying_R-CP ) by FUZIMPL3:28;

end;

theorem :: FUZIMPL4:29

FuzzyLattice [.0,1.] is complete distributive Heyting LATTICE ;

theorem LemmaFuncs: :: FUZIMPL4:30

{ f where f is Fuzzy_Negation : verum } c= Funcs ([.0,1.],[.0,1.])

proof end;

LemmaFunc: for N being Fuzzy_Negation holds N is Function of [.0,1.],REAL

proof end;

LemmaFunc2: for N being Fuzzy_Negation holds N in Funcs ([.0,1.],REAL)

proof end;

LemmaMaxRng: for f, g being Function of [.0,1.],REAL holds rng (max (f,g)) c= (rng f) \/ (rng g)

proof end;

LemmaMinRng: for f, g being Function of [.0,1.],REAL holds rng (min (f,g)) c= (rng f) \/ (rng g)

proof end;

definition

let N1, N2 be Fuzzy_Negation;

func max (N1,N2) -> Fuzzy_Negation means :MaxFuz: :: FUZIMPL4:def 9
ex f, g being Function of [.0,1.],REAL st
( f = N1 & g = N2 & it = max (f,g) );

existence
ex b₁ being Fuzzy_Negation ex f, g being Function of [.0,1.],REAL st
( f = N1 & g = N2 & b₁ = max (f,g) )

proof end;

uniqueness
for b₁, b₂ being Fuzzy_Negation st ex f, g being Function of [.0,1.],REAL st
( f = N1 & g = N2 & b₁ = max (f,g) ) & ex f, g being Function of [.0,1.],REAL st
( f = N1 & g = N2 & b₂ = max (f,g) ) holds
b₁ = b₂ ;

func min (N1,N2) -> Fuzzy_Negation means :MinFuz: :: FUZIMPL4:def 10
ex f, g being Function of [.0,1.],REAL st
( f = N1 & g = N2 & it = min (f,g) );

existence
ex b₁ being Fuzzy_Negation ex f, g being Function of [.0,1.],REAL st
( f = N1 & g = N2 & b₁ = min (f,g) )

proof end;

uniqueness
for b₁, b₂ being Fuzzy_Negation st ex f, g being Function of [.0,1.],REAL st
( f = N1 & g = N2 & b₁ = min (f,g) ) & ex f, g being Function of [.0,1.],REAL st
( f = N1 & g = N2 & b₂ = min (f,g) ) holds
b₁ = b₂ ;

end;

:: deftheorem MaxFuz defines max FUZIMPL4:def 9 :
for N1, N2, b₃ being Fuzzy_Negation holds
( b₃ = max (N1,N2) iff ex f, g being Function of [.0,1.],REAL st
( f = N1 & g = N2 & b₃ = max (f,g) ) );

:: deftheorem MinFuz defines min FUZIMPL4:def 10 :
for N1, N2, b₃ being Fuzzy_Negation holds
( b₃ = min (N1,N2) iff ex f, g being Function of [.0,1.],REAL st
( f = N1 & g = N2 & b₃ = min (f,g) ) );

LemmaCarrier: the carrier of ((RealPoset [.0,1.]) |^ [.0,1.]) = Funcs ([.0,1.],[.0,1.])

proof end;

definition

func Fuzzy_Negations -> strict full SubRelStr of FuzzyLattice [.0,1.] means :FuzNegDef: :: FUZIMPL4:def 11
the carrier of it = { f where f is Fuzzy_Negation : verum } ;

existence
ex b₁ being strict full SubRelStr of FuzzyLattice [.0,1.] st the carrier of b₁ = { f where f is Fuzzy_Negation : verum }

proof end;

uniqueness
for b₁, b₂ being strict full SubRelStr of FuzzyLattice [.0,1.] st the carrier of b₁ = { f where f is Fuzzy_Negation : verum } & the carrier of b₂ = { f where f is Fuzzy_Negation : verum } holds
b₁ = b₂ by YELLOW_0:57;

end;

:: deftheorem FuzNegDef defines Fuzzy_Negations FUZIMPL4:def 11 :
for b₁ being strict full SubRelStr of FuzzyLattice [.0,1.] holds
( b₁ = Fuzzy_Negations iff the carrier of b₁ = { f where f is Fuzzy_Negation : verum } );

registration

cluster Fuzzy_Negations -> non empty strict reflexive transitive antisymmetric full ;

coherence
( not Fuzzy_Negations is empty & Fuzzy_Negations is reflexive & Fuzzy_Negations is transitive & Fuzzy_Negations is antisymmetric )

proof end;

end;

theorem :: FUZIMPL4:31

for f, g being Fuzzy_Negation holds max (f,g) = (maxfuncreal [.0,1.]) . (f,g)

proof end;

theorem MaxEqMax: :: FUZIMPL4:32

for f, g being Fuzzy_Negation
for ff, gg being Membership_Func of [.0,1.] st f = ff & g = gg holds
max (f,g) = max (ff,gg)

proof end;

theorem MinEqMin: :: FUZIMPL4:33

for f, g being Fuzzy_Negation
for ff, gg being Membership_Func of [.0,1.] st f = ff & g = gg holds
min (f,g) = min (ff,gg)

proof end;

theorem :: FUZIMPL4:34

for f, g being Fuzzy_Negation holds min (f,g) = (minfuncreal [.0,1.]) . (f,g)

proof end;

::: The following formalize more or less the same notions of max, remove:
::: func max from FUZZY_1:def 4
::: func max from COUSIN2
::: func maxfuncreal from REAL_LAT
::: Also dual notions are repeated

definition

let L be non empty 1-sorted ;
let a, b be Element of L;
:: original: {
redefine func {a,b} -> Subset of L;
coherence
{a,b} is Subset of L by ZFMISC_1:32;

end;

registration

cluster Fuzzy_Negations -> strict full join-inheriting ;

coherence
Fuzzy_Negations is join-inheriting

proof end;

cluster Fuzzy_Negations -> strict full meet-inheriting ;

coherence
Fuzzy_Negations is meet-inheriting

proof end;

end;

theorem :: FUZIMPL4:35

for N1, N2 being Element of Fuzzy_Negations
for NN1, NN2 being Fuzzy_Negation st N1 = NN1 & N2 = NN2 holds
N1 "\/" N2 = max (NN1,NN2)

proof end;

theorem :: FUZIMPL4:36

for N1, N2 being Element of Fuzzy_Negations
for NN1, NN2 being Fuzzy_Negation st N1 = NN1 & N2 = NN2 holds
N1 "/\" N2 = min (NN1,NN2)

proof end;