:: On Fuzzy Negations and Laws of Contraposition. Lattice of Fuzzy Negations
:: by Adam Grabowski
::
:: Received November 21, 2023
:: Copyright (c) 2023-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XXREAL_1, REAL_1, XXREAL_0, FUZIMPL1, SUBSET_1, CARD_1,
TARSKI, ARYTM_1, ARYTM_3, POWER, FUNCT_1, XBOOLE_0, RELAT_1, BINOP_1,
FUZIMPL2, ORDINAL2, VALUED_0, FUNCT_2, FUZIMPL3, ZFMISC_1, BORSUK_1,
OPOSET_1, FUZIMPL4, LFUZZY_0, LATTICES, WAYBEL_0, REWRITE1, LATTICE2,
FUNCT_7, JGRAPH_2, TOPMETR, TREAL_1, VALUED_1, STRUCT_0, QC_LANG1,
FUZZY_1, YELLOW_0, NEWTON, CAT_1, RELAT_2, EQREL_1, REAL_LAT;
notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, XXREAL_0, NUMBERS, BINOP_1,
ZFMISC_1, VALUED_0, XREAL_0, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_3, RCOMP_1,
PARTFUN1, MEMBERED, POWER, FCONT_1, FUNCSDOM, STRUCT_0, PRE_TOPC,
ORDERS_2, BORSUK_1, LATTICES, LATTICE2, LATTICE3, LFUZZY_0, EUCLID,
TOPMETR, TMAP_1, TREAL_1, REAL_LAT, FUZIMPL1, FUZIMPL2, FUZIMPL3,
YELLOW_0, YELLOW_1, WAYBEL_0, WAYBEL_1, WAYBEL_3, COUSIN2, FUZZY_1;
constructors SEQ_4, TOPMETR, PREPOWER, POWER, FUZIMPL1, FUZIMPL2, FUNCT_3,
FUZIMPL3, LFUZZY_0, BORSUK_1, FCONT_1, TREAL_1, TMAP_1, ORDERS_1,
ORDERS_2, XXREAL_0, REAL_LAT, FUNCSDOM, STRUCT_0, WAYBEL_1, YELLOW_0,
YELLOW_1, COUSIN2, LATTICE3, ORDERS_3, WAYBEL_3, RELSET_1, FUZZY_1,
SETFAM_1, MEMBERED, XXREAL_2, BINOP_1, VALUED_0;
registrations XBOOLE_0, RELSET_1, XXREAL_0, XREAL_0, MEMBERED, ORDINAL1,
FUZNORM1, VALUED_0, NUMBERS, FUNCT_2, FOMODEL0, FUNCT_1, RELAT_1,
FUZIMPL2, BORSUK_1, FUZIMPL1, FUZIMPL3, LFUZZY_0, XXREAL_1, STRUCT_0,
YELLOW_0, YELLOW_1, WAYBEL_0, WAYBEL_1, SUBSET_1, REALSET1, ORDERS_1,
ORDERS_2, PRE_TOPC, TOPS_1, XXREAL_2, EUCLID, TOPMETR, LATTICE3,
WAYBEL_3, FUNCOP_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, VALUED_0, FUZIMPL1, FUZIMPL2, FUNCT_1;
equalities XCMPLX_0, BINOP_1, TREAL_1, EUCLID, SUBSET_1, LFUZZY_0;
expansions VALUED_0, FUZIMPL1;
theorems FUNCT_1, FUNCT_2, RELAT_1, POWER, XREAL_1, XXREAL_0, XXREAL_1,
FUZNORM1, FUZIMPL1, XBOOLE_0, ZFMISC_1, BINOP_1, FUZIMPL2, FUZIMPL3,
SUBSET_1, TOPMETR, TREAL_1, BORSUK_1, FCONT_1, YELLOW_0, YELLOW_1,
LFUZZY_0, XBOOLE_1, COUSIN2, REAL_LAT, FUNCOP_1, FUZZY_1;
schemes SCHEME1;
begin :: Laws of Contraposition
:: Definition 1.5.1
registration
cluster decreasing for Fuzzy_Negation;
existence
proof
set N = N_CC;
N_CC is decreasing;
hence thesis;
end;
end;
definition let N be Fuzzy_Negation;
let I be BinOp of [.0,1.]; :: note in Baczynski it should be FI
attr I is N-satisfying_CP means
for x,y being Element of [.0,1.] holds
I.(x,y) = I.(N.y,N.x);
end;
definition
let N be Fuzzy_Negation;
let I be BinOp of [.0,1.]; :: note in Baczynski it should be FI
attr I is N-satisfying_L-CP means
for x,y being Element of [.0,1.] holds
I.(N.x,y) = I.(N.y,x);
end;
definition
let N be Fuzzy_Negation;
let I be BinOp of [.0,1.]; :: note in Baczynski it should be FI
attr I is N-satisfying_R-CP means
for x,y being Element of [.0,1.] holds
I.(x,N.y) = I.(y,N.x);
end;
begin ::
theorem
N_CC = AffineMap (-1,1)|[.0,1.]
proof
set N = N_CC;
set f = AffineMap (-1,1)|[.0,1.];
A2: dom AffineMap (-1,1) = REAL by FUNCT_2:def 1;
AA: dom N = dom f by A2,FUNCT_2:def 1;
for x being object st x in dom N holds
f.x = N.x
proof
let x be object;
assume x in dom N; then
reconsider xx = x as Element of [.0,1.] by FUNCT_2:def 1;
f.x = AffineMap (-1,1).xx by FUNCT_1:49
.= (-1) * xx + 1 by FCONT_1:def 4
.= 1-xx
.= N.x by FUZIMPL3:def 6;
hence thesis;
end;
hence thesis by AA,FUNCT_1:2;
end;
registration
cluster N_CC -> continuous;
coherence
proof
reconsider g = L[01]((0,1)(#),(#)(0,1)) as Function of I[01],I[01]
by TOPMETR:20;
set t1 = (0,1)(#);
set t2 = (#)(0,1);
set f = L[01](t1,t2);
f = N_CC
proof
for x being Element of [.0,1.] holds f.x = N_CC.x
proof
let x be Element of [.0,1.];
reconsider xx = x as Element of Closed-Interval-TSpace (0,1)
by TOPMETR:18;
D1: t1 = 1 by TREAL_1:def 2;
f.x = (1 - xx) * t1 + xx * t2 by TREAL_1:def 3
.= (1 - xx) * t1 + xx * 0 by TREAL_1:def 1
.= N_CC.x by D1,FUZIMPL3:def 6;
hence thesis;
end;
hence thesis by FUNCT_2:63,BORSUK_1:40,TOPMETR:20;
end;
hence thesis by FUZIMPL3:def 7,TOPMETR:20, TREAL_1:8;
end;
end;
registration
cluster N_CC -> negation-strong;
coherence
proof
for x being Element of [.0,1.] holds
N_CC.(N_CC.x) = x
proof
let x be Element of [.0,1.];
A1: 1 - x in [.0,1.] by FUZNORM1:7;
N_CC.(N_CC.x) = (N_CC.(1-x)) by FUZIMPL3:def 6
.= (1-(1-x)) by A1,FUZIMPL3:def 6
.= x;
hence thesis;
end; then
N_CC is involutive by FUZIMPL3:def 8;
hence thesis by FUZIMPL3:def 11,def 13;
end;
end;
registration
cluster negation-strict for Fuzzy_Negation;
existence
proof
take N_CC;
N_CC is satisfying_(N3) satisfying_(N4)
by FUZIMPL3:def 9,def 10;
hence thesis by FUZIMPL3:def 12;
end;
cluster negation-strong for Fuzzy_Negation;
existence
proof
take N_CC;
thus thesis;
end;
end;
:: Every strong negation is strict
:: if N is negation-strict, then it is decreasing, so N is one-to-one
registration
cluster satisfying_(N3) -> decreasing for Fuzzy_Negation;
coherence by FUZIMPL3:def 9;
cluster decreasing -> satisfying_(N3) for Fuzzy_Negation;
coherence by FUZIMPL3:def 9;
end;
:: cluster FINSEQ_1 for increasing
registration
cluster -> REAL-defined real-valued for UnOp of [.0,1.];
coherence
proof
let f be UnOp of [.0,1.];
dom f = [.0,1.] by FUNCT_2:def 1;
hence thesis by RELAT_1:def 18;
end;
end;
registration
cluster REAL-defined decreasing -> one-to-one for real-valued Function;
coherence :: copied from FINSEQ_1 and rewritten for decreasing,
:: generalized from NAT- to REAL-defined
proof
let f be real-valued Function;
assume that
A0: f is REAL-defined and
A1: f is decreasing;
let x,y be object;
assume that
A2: x in dom f & y in dom f and
A3: f.x = f.y;
dom f c= REAL by A0,RELAT_1:def 18;
then reconsider x,y as Element of REAL by A2;
x <= y & x >= y by A1,A2,A3;
hence thesis by XXREAL_0:1;
end;
end;
registration
cluster decreasing -> one-to-one for UnOp of [.0,1.];
coherence;
end;
registration
cluster -> non-increasing for Fuzzy_Negation;
coherence by FUZIMPL3:def 5;
end;
registration
cluster negation-strict -> one-to-one for Fuzzy_Negation;
coherence
proof
let N be Fuzzy_Negation;
assume N is negation-strict; then
N is satisfying_(N3) by FUZIMPL3:def 12;
hence thesis;
end;
end;
theorem LemmaOne:
for R being Function st R~ is Function holds
R is one-to-one
proof
let R be Function;
assume
A0: R~ is Function;
assume not R is one-to-one; then
consider x1,x2 being object such that
A1: x1 in dom R & x2 in dom R & R.x1 = R.x2 & x1 <> x2 by FUNCT_1:def 4;
[x1,R.x1] in R by A1,FUNCT_1:def 2; then
A2: [R.x1,x1] in R~ by RELAT_1:def 7;
[x2,R.x2] in R by A1,FUNCT_1:def 2; then
[R.x2,x2] in R~ by RELAT_1:def 7;
hence thesis by A1,A2,A0,FUNCT_1:def 1;
end;
theorem
for N1,N2 being Fuzzy_Negation st N1~ = N2 holds
N1 is one-to-one by LemmaOne;
theorem LemmaOnto2:
for N1,N2 being Fuzzy_Negation st N1~ = N2 holds
N1 is onto
proof
let N1,N2 be Fuzzy_Negation;
assume N1~ = N2; then
AB: N1 = N2~; then
FF: N2 is one-to-one by LemmaOne;
for y being object st y in [.0,1.]
ex x being object st x in [.0,1.] & y = N1.x
proof
let y be object;
assume
A2: y in [.0,1.];
take x = N2.y;
N1 = N2" by AB,LemmaOne,FUNCT_1:def 5;
hence thesis by A2,FF,FUNCT_2:26,FUNCT_2:5;
end; then
rng N1 = [.0,1.] by FUNCT_2:10;
hence thesis by FUNCT_2:def 3;
end;
:: Proposition 1.5.2
theorem
for I being BinOp of [.0,1.],
N being negation-strict Fuzzy_Negation,
N1 being Fuzzy_Negation st N~ = N1 holds
I is N-satisfying_L-CP iff
I is N1-satisfying_R-CP
proof
let I be BinOp of [.0,1.],
N be negation-strict Fuzzy_Negation,
N1 be Fuzzy_Negation;
assume
A0: N~ = N1; then
N is onto by LemmaOnto2; then
A2: rng N = [.0,1.] by FUNCT_2:def 3;
DD: N" = N~ by FUNCT_1:def 5;
thus I is N-satisfying_L-CP implies I is N1-satisfying_R-CP
proof
assume
a1: I is N-satisfying_L-CP;
for x,y being Element of [.0,1.] holds
I.(x,N1.y) = I.(y,N1.x)
proof
let x,y be Element of [.0,1.];
I.(x,N1.y) = I.(N.(N1.x),N1.y) by A0,A2,FUNCT_1:35,DD
.= I.(N.(N1.y),N1.x) by a1
.= I.(y,N1.x) by A2,DD,A0,FUNCT_1:35;
hence thesis;
end;
hence I is N1-satisfying_R-CP;
end;
assume
a1: I is N1-satisfying_R-CP;
C1: dom N = [.0,1.] by FUNCT_2:def 1;
for x,y being Element of [.0,1.] holds
I.(N.x,y) = I.(N.y,x)
proof
let x,y be Element of [.0,1.];
B2: (N1 * N).y = y by A0,C1,FUNCT_1:34,DD;
(N1 * N).y = N1.(N.y) by C1,FUNCT_1:13; then
I.(N.x,y) = I.(N.y,N1.(N.x)) by a1,B2
.= I.(N.y,x) by A0,C1,FUNCT_1:34,DD;
hence thesis;
end;
hence I is N-satisfying_L-CP;
end;
begin
:: Proposition 1.5.3 (i) => (ii)
theorem Lemma15312:
for I being BinOp of [.0,1.],
N being negation-strong Fuzzy_Negation holds
I is N-satisfying_CP implies
I is N-satisfying_L-CP
proof
let I be BinOp of [.0,1.],
N be negation-strong Fuzzy_Negation;
assume
a0: I is N-satisfying_CP;
d1: N is involutive by FUZIMPL3:def 11,def 13;
for x,y being Element of [.0,1.] holds
I.(N.x,y) = I.(N.y,x)
proof
let x,y be Element of [.0,1.];
I.(N.x,y) = I.(N.y,N.(N.x)) by a0
.= I.(N.y,x) by d1,FUZIMPL3:def 8;
hence thesis;
end;
hence thesis;
end;
:: Proposition 1.5.3 (ii) => (iii)
theorem Lemma15323:
for I being BinOp of [.0,1.],
N being negation-strong Fuzzy_Negation holds
I is N-satisfying_L-CP implies
I is N-satisfying_R-CP
proof
let I be BinOp of [.0,1.],
N be negation-strong Fuzzy_Negation;
assume
a0: I is N-satisfying_L-CP;
d1: N is involutive by FUZIMPL3:def 11,def 13;
for x,y being Element of [.0,1.] holds
I.(x,N.y) = I.(y,N.x)
proof
let x,y be Element of [.0,1.];
I.(x,N.y) = I.(N.(N.x),N.y) by d1,FUZIMPL3:def 8
.= I.(N.(N.y),N.x) by a0
.= I.(y,N.x) by d1,FUZIMPL3:def 8;
hence thesis;
end;
hence thesis;
end;
:: Proposition 1.5.3 (iii) => (i)
theorem Lemma15331:
for I being BinOp of [.0,1.],
N being negation-strong Fuzzy_Negation holds
I is N-satisfying_R-CP implies
I is N-satisfying_CP
proof
let I be BinOp of [.0,1.],
N be negation-strong Fuzzy_Negation;
assume
a0: I is N-satisfying_R-CP;
d1: N is involutive by FUZIMPL3:def 11,def 13;
for x,y being Element of [.0,1.] holds
I.(x,y) = I.(N.y,N.x)
proof
let x,y be Element of [.0,1.];
I.(x,y) = I.(x,N.(N.y)) by d1,FUZIMPL3:def 8
.= I.(N.y,N.x) by a0;
hence thesis;
end;
hence thesis;
end;
:: Proposition 1.5.3 (i) <=> (ii)
theorem
for I being BinOp of [.0,1.],
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
for I being BinOp of [.0,1.],
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:
for I being BinOp of [.0,1.], :: for Fuzzy_Implication it is trivial
N being Fuzzy_Negation st
I is satisfying_(I1) N-satisfying_CP holds
I is satisfying_(I2)
proof
let I be BinOp of [.0,1.],
N be Fuzzy_Negation;
assume that
A0: I is satisfying_(I1) and
AA: I is N-satisfying_CP;
for x,y,z being Element of [.0,1.] st y <= z holds
I.(x,y) <= I.(x,z)
proof
let x,y,z be Element of [.0,1.];
assume y <= z; then
N.z <= N.y by FUZIMPL3:7; then
A1: I.(N.y,N.x) <= I.(N.z,N.x) by A0;
I.(x,y) = I.(N.y,N.x) by AA;
hence thesis by A1,AA;
end;
hence thesis;
end;
:: Lemma 1.5.4 (ii)
theorem Lemma154ii:
for I being BinOp of [.0,1.], :: for Fuzzy_Implication it is trivial
N being Fuzzy_Negation st
I is satisfying_(I2) N-satisfying_CP holds
I is satisfying_(I1)
proof
let I be BinOp of [.0,1.],
N be Fuzzy_Negation;
assume that
A0: I is satisfying_(I2) and
AA: I is N-satisfying_CP;
for x,y,z being Element of [.0,1.] st x <= y holds
I.(x,z) >= I.(y,z)
proof
let x,y,z be Element of [.0,1.];
assume x <= y; then
F0: N.y <= N.x by FUZIMPL3:7;
A3: I.(N.z,N.x) = I.(x,z) by AA;
I.(N.z,N.x) >= I.(N.z,N.y) by F0,A0;
hence thesis by A3,AA;
end;
hence thesis;
end;
:: Lemma 1.5.4 (iii)
theorem Lemma154iii:
for I being BinOp of [.0,1.], :: for Fuzzy_Implication it is trivial
N being Fuzzy_Negation st
I is satisfying_(LB) N-satisfying_CP holds
I is satisfying_(RB)
proof
let I be BinOp of [.0,1.],
N be Fuzzy_Negation;
assume that
A1: I is satisfying_(LB) and
A2: I is N-satisfying_CP;
let x be Element of [.0,1.];
A3: N.1 = 0 by FUZIMPL3:def 4;
1 in [.0,1.] by XXREAL_1:1; then
I.(x,1) = I.(N.1,N.x) by A2
.= 1 by A1,A3;
hence thesis;
end;
:: Lemma 1.5.4 (iv)
theorem Lemma154iv:
for I being BinOp of [.0,1.], :: for Fuzzy_Implication it is trivial
N being Fuzzy_Negation st
I is satisfying_(RB) N-satisfying_CP holds
I is satisfying_(LB)
proof
let I be BinOp of [.0,1.],
N be Fuzzy_Negation;
assume that
A1: I is satisfying_(RB) and
A2: I is N-satisfying_CP;
let y be Element of [.0,1.];
A4: 0 in [.0,1.] by XXREAL_1:1;
A3: N.0 = 1 by FUZIMPL3:def 4;
I.(0,y) = I.(N.y,N.0) by A2,A4
.= 1 by A1,A3;
hence thesis;
end;
:: Lemma 1.5.4 (v) a
theorem Lemma154va:
for I being BinOp of [.0,1.], :: for Fuzzy_Implication it is trivial
N being Fuzzy_Negation st
I is satisfying_(NP) N-satisfying_CP holds
N = FNegation I & FNegation I is negation-strong
proof
let I be BinOp of [.0,1.],
N be Fuzzy_Negation;
assume that
A1: I is satisfying_(NP) and
A2: I is N-satisfying_CP;
set NI = FNegation I;
A3: N.0 = 1 by FUZIMPL3:def 4;
B1: 0 in [.0,1.] by XXREAL_1:1;
B2: 1 in [.0,1.] by XXREAL_1:1;
for x being Element of [.0,1.] holds
NI.x = N.x
proof
let x be Element of [.0,1.];
NI.x = I.(x,0) by FUZIMPL3:def 16
.= I.(N.0,N.x) by B1,A2
.= N.x by A1,A3,FUZIMPL2:def 1;
hence thesis;
end;
hence
T1: N = NI by FUNCT_2:63; then
C1: NI.1 = 0 by FUZIMPL3:def 4;
for y being Element of [.0,1.] holds
y = NI.(NI.y)
proof
let y be Element of [.0,1.];
y = I.(1,y) by A1,FUZIMPL2:def 1
.= I.(NI.y,NI.1) by B2,A2,T1
.= NI.(NI.y) by C1,FUZIMPL3:def 16;
hence thesis;
end; then
NI is involutive by FUZIMPL3:def 8;
hence thesis by FUZIMPL3:def 13,def 11;
end;
:: Lemma 1.5.4 (v) b
theorem Lemma154vb:
for I being BinOp of [.0,1.], :: for Fuzzy_Implication it is trivial
N being Fuzzy_Negation st
I is satisfying_(NP) N-satisfying_CP holds
I is satisfying_(I3) satisfying_(I4) satisfying_(I5)
:: I4 and I5 obtained automatically
proof
let I be BinOp of [.0,1.],
N be Fuzzy_Negation;
assume that
A1: I is satisfying_(NP) and
A2: I is N-satisfying_CP;
T1: N = FNegation I & FNegation I is negation-strong
by A1,A2,Lemma154va;
0 in [.0,1.] by XXREAL_1:1; then
I.(0,0) = (FNegation I).0 by FUZIMPL3:def 16
.= 1 by T1,FUZIMPL3:def 4;
hence thesis by A1;
end;
:: Corollary 1.5.5
theorem
for I being BinOp of [.0,1.] st
I is satisfying_(NP) holds
FNegation I is not negation-strong implies
for N being Fuzzy_Negation holds
I is not N-satisfying_CP by Lemma154va;
:: Lemma 1.5.6 (i)
theorem Lemma156i:
for I being BinOp of [.0,1.],
N being negation-strong Fuzzy_Negation st
N = FNegation I holds
I is N-satisfying_CP implies
I is satisfying_(NP)
proof
let I be BinOp of [.0,1.],
N being negation-strong Fuzzy_Negation;
assume
A0: N = FNegation I;
assume
A1: I is N-satisfying_CP;
A2: N is involutive by FUZIMPL3:def 13,def 11;
for y being Element of [.0,1.] holds
I.(1,y) = y
proof
let y be Element of [.0,1.];
1 in [.0,1.] by XXREAL_1:1; then
I.(1,y) = I.(N.y,N.1) by A1
.= I.(N.y,0) by FUZIMPL3:def 4
.= N.(N.y) by A0,FUZIMPL3:def 16
.= y by A2,FUZIMPL3:def 8;
hence thesis;
end;
hence thesis by FUZIMPL2:def 1;
end;
:: Lemma 1.5.6 (ii)
theorem Lemma156ii:
for I being BinOp of [.0,1.],
N being negation-strong Fuzzy_Negation st
N = FNegation I holds
I is satisfying_(EP) implies
I is satisfying_(I3) satisfying_(I4) satisfying_(I5)
satisfying_(NP) N-satisfying_CP
proof
let I be BinOp of [.0,1.],
N being negation-strong Fuzzy_Negation;
assume
A0: N = FNegation I;
assume
A1: I is satisfying_(EP);
A2: N is involutive by FUZIMPL3:def 13,def 11;
for x,y being Element of [.0,1.] holds
I.(N.y,N.x) = I.(x,y)
proof
let x,y be Element of [.0,1.];
ZZ: N.y in [.0,1.] & 0 in [.0,1.] by XXREAL_1:1;
I.(N.y,N.x) = I.(N.y,I.(x,0)) by A0,FUZIMPL3:def 16
.= I.(x,I.(N.y,0)) by A1,FUZIMPL2:def 2,ZZ
.= I.(x,N.(N.y)) by FUZIMPL3:def 16,A0
.= I.(x,y) by A2,FUZIMPL3:def 8;
hence thesis;
end; then
T1: I is N-satisfying_CP; then
I is satisfying_(NP) by A0,Lemma156i;
hence thesis by T1,Lemma154vb;
end;
theorem Corr157i: :: Corollary 1.5.7 (i)
for I being BinOp of [.0,1.],
N being Fuzzy_Negation st
I is N-satisfying_CP holds
I is satisfying_(I1) iff I is satisfying_(I2)
by Lemma154i,Lemma154ii;
theorem :: Corollary 1.5.7 (ii)
for I being BinOp of [.0,1.],
N being Fuzzy_Negation st
I is N-satisfying_CP holds
I is satisfying_(LB) iff I is satisfying_(RB)
by Lemma154iii,Lemma154iv;
theorem :: Corollary 1.5.7 (iii)
for I being BinOp of [.0,1.],
N being Fuzzy_Negation st
I is N-satisfying_CP holds
N is negation-strong implies
(I is satisfying_(NP) iff N = FNegation I)
by Lemma154va,Lemma156i;
theorem :: Corollary 1.5.8
for I being BinOp of [.0,1.],
N being Fuzzy_Negation st
I is N-satisfying_CP satisfying_(I1) satisfying_(NP) holds
I in FI & FNegation I = N & N is negation-strong
proof
let I be BinOp of [.0,1.],
N be Fuzzy_Negation;
assume
A1: I is N-satisfying_CP satisfying_(I1) satisfying_(NP);
A4: I is satisfying_(I2) by A1,Corr157i;
I is satisfying_(I3) by A1,Lemma154vb;
hence I in FI by A1,A4,FUZIMPL1:def 15;
thus FNegation I = N by A1,Lemma154va;
hence thesis by A1,Lemma154va;
end;
theorem :: Corollary 1.5.9
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;
begin :: Some Further Examples of Fuzzy Implications
:: Example 1.5.10
:: (ii) I_4
definition :: Example 1.5.10 (i) - I_3 by Drewniak
func I_I3 -> BinOp of [.0,1.] means :II3Def:
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
proof
set C = [.0,1.];
defpred P[Real,Real] means $1 <> 0 & $2 = 0;
deffunc F(Element of C,Element of C) = In(0,C);
deffunc G(Element of C,Element of C) = In(1,C);
ex f being Function of [:C,C:],C st for c be Element of C,
d be Element of C st [c,d] in dom f holds
(P[c,d] implies f. [c,d] = F(c,d)) &
(not P [c,d] implies f. [c,d] = G(c,d)) from SCHEME1:sch 21; then
consider f being Function of [:C,C:],C such that
A1: for c be Element of C, d be Element of C st [c,d] in dom f holds
(P[c,d] implies f. [c,d] = F(c,d)) &
(not P [c,d] implies f. [c,d] = G(c,d));
take f;
A0: dom f = [:C,C:] by FUNCT_2:def 1;
let a,b be Element of C;
AA: [a,b] in dom f by A0,ZFMISC_1:87;
(a <> 0 & b = 0 implies f.(a,b) = 0) &
(a = 0 or b <> 0 implies f.(a,b) = 1)
proof
thus a <> 0 & b = 0 implies f.(a,b) = 0 by A1,AA;
assume a = 0 or b <> 0; then
f. [a,b] = G(a,b) by A1,AA
.= 1 by XXREAL_1:1,SUBSET_1:def 8;
hence thesis;
end;
hence thesis;
end;
uniqueness
proof
let f1,f2 be BinOp of [.0,1.] such that
A1: for a,b being Element of [.0,1.] holds
(a = 0 or b <> 0 implies f1.(a,b) = 1) &
(a <> 0 & b = 0 implies f1.(a,b) = 0) and
A2: for a,b being Element of [.0,1.] holds
(a = 0 or b <> 0 implies f2.(a,b) = 1) &
(a <> 0 & b = 0 implies f2.(a,b) = 0);
for a,b being set st a in [.0,1.] & b in [.0,1.] holds
f1.(a,b) = f2.(a,b)
proof
let a,b be set;
assume a in [.0,1.] & b in [.0,1.]; then
reconsider aa = a, bb = b as Element of [.0,1.];
per cases by XXREAL_1:1;
suppose
B0: aa > 0 & bb = 0; then
f1.(aa,bb) = 0 by A1
.= f2.(aa,bb) by A2,B0;
hence thesis;
end;
suppose
B0: aa > 0 & bb <> 0; then
f1.(aa,bb) = 1 by A1
.= f2.(aa,bb) by A2,B0;
hence thesis;
end;
suppose
B1: aa = 0; then
f1.(aa,bb) = 1 by A1
.= f2.(aa,bb) by A2,B1;
hence thesis;
end;
end;
hence thesis by BINOP_1:def 21;
end;
end;
registration
cluster I_I3 -> decreasing_on_1st increasing_on_2nd
00-dominant 11-dominant 10-weak;
coherence
proof
set f = I_I3;
b1: for x1,x2,y being Element of [.0,1.] st
x1 <= x2 holds f.(x1,y) >= f.(x2,y)
proof
let x1,x2,y be Element of [.0,1.];
assume Z1: x1 <= x2;
per cases;
suppose Z0: x2 = 0; then
x1 = 0 by Z1,XXREAL_1:1;
hence thesis by Z0;
end;
suppose x2 <> 0 & x1 <> 0 & y = 0; then
f.(x2,y) = 0 by II3Def;
hence thesis by XXREAL_1:1;
end;
suppose x2 <> 0 & x1 <> 0 & y <> 0; then
f.(x1,y) = 1 & f.(x2,y) = 1 by II3Def;
hence thesis;
end;
suppose x2 <> 0 & x1 = 0 & y = 0; then
f.(x1,y) = 1 & f.(x2,y) = 0 by II3Def;
hence thesis;
end;
suppose Z1: x2 <> 0 & x1 = 0 & y <> 0; then
f.(x2,y) = 1 by II3Def;
hence thesis by Z1,II3Def;
end;
end;
b2: for x,y1,y2 being Element of [.0,1.] st
y1 <= y2 holds f.(x,y1) <= f.(x,y2)
proof
let x,y1,y2 be Element of [.0,1.];
assume
SA: y1 <= y2;
per cases;
suppose x = 0; then
f.(x,y1) = 1 & f.(x,y2) = 1 by II3Def;
hence thesis;
end;
suppose Z1: x <> 0 & y1 <> 0; then
y2 > 0 by SA,XXREAL_1:1; then
f.(x,y1) = 1 & f.(x,y2) = 1 by Z1,II3Def;
hence thesis;
end;
suppose x <> 0 & y1 = 0 & y2 = 0;
hence thesis;
end;
suppose x <> 0 & y1 = 0 & y2 <> 0; then
f.(x,y1) = 0 & f.(x,y2) = 1 by II3Def;
hence thesis;
end;
end;
0 in [.0,1.] & 1 in [.0,1.] by XXREAL_1:1;
hence thesis by b1,b2,II3Def;
end;
end;
theorem FNegI3:
FNegation I_I3 = NegationD1
proof
set I = I_I3;
set f = FNegation I;
set g = NegationD1;
A1: 0 in [.0,1.] by XXREAL_1:1;
for x being Element of [.0,1.] holds f.x = g.x
proof
let x be Element of [.0,1.];
per cases;
suppose
B1: x = 0;
f.x = I.(x,0) by FUZIMPL3:def 16
.= 1 by II3Def,B1
.= g.x by FUZIMPL3:def 17,B1;
hence thesis;
end;
suppose
B1: x <> 0;
f.x = I.(x,0) by FUZIMPL3:def 16
.= 0 by A1,B1,II3Def
.= g.x by FUZIMPL3:def 17,B1;
hence thesis;
end;
end;
hence thesis by FUNCT_2:63;
end;
registration
cluster I_I3 -> satisfying_(EP) non satisfying_(NP);
coherence
proof
set I = I_I3;
ex y being Element of [.0,1.] st I.(1,y) <> y
proof
reconsider y = 1/2 as Element of [.0,1.] by XXREAL_1:1;
take y;
1 in [.0,1.] by XXREAL_1:1;
hence thesis by II3Def;
end; then
T1: I is non satisfying_(NP) by FUZIMPL2:def 1;
for x,y,z being Element of [.0,1.] holds I.(x,I.(y,z)) = I.(y,I.(x,z))
proof
let x,y,z be Element of [.0,1.];
per cases;
suppose z <> 0; then
D2: I.(y,z) = 1 & I.(x,z) = 1 by II3Def; then
I.(x,I.(y,z)) = 1 by II3Def
.= I.(y,I.(x,z)) by II3Def,D2;
hence thesis;
end;
suppose F1: z = 0 & y <> 0 & x <> 0; then
I.(y,z) = 0 & I.(x,z) = 0 by II3Def;
hence thesis by F1;
end;
suppose F1: z = 0 & y <> 0 & x = 0; then
I.(y,z) = 0 & I.(x,z) = 1 by II3Def;
hence thesis by F1,II3Def;
end;
suppose z = 0 & y = 0 & x = 0;
hence thesis;
end;
suppose F1: z = 0 & y = 0 & x <> 0; then
I.(y,z) = 1 by II3Def; then
I.(x,I.(y,z)) = 1 by II3Def
.= I.(y,I.(x,z)) by F1,II3Def;
hence thesis;
end;
end;
hence thesis by T1,FUZIMPL2:def 2;
end;
end;
registration
cluster I_I3 -> (FNegation I_I3)-satisfying_CP;
coherence
proof
set N = FNegation I_I3;
set I = I_I3;
for x,y being Element of [.0,1.] holds
I.(x,y) = I.(N.y,N.x)
proof
let x,y be Element of [.0,1.];
per cases;
suppose F1: x = 0;
F3: 1 in [.0,1.] by XXREAL_1:1;
thus I.(x,y) = 1 by II3Def,F1
.= I.(N.y,1) by II3Def,F3
.= I.(N.y,N.x) by F1,FUZIMPL3:def 4;
end;
suppose F1: y <> 0; then
F2: N.y = 0 by FNegI3,FUZIMPL3:def 17;
thus I.(x,y) = 1 by II3Def,F1
.= I.(N.y,N.x) by F2,II3Def;
end;
suppose F1: x <> 0 & y = 0; then
F3: N.y <> 0 & N.x = 0 by FNegI3,FUZIMPL3:def 17;
thus I.(x,y) = 0 by II3Def,F1
.= I.(N.y,N.x) by F3,II3Def;
end;
end;
hence thesis;
end;
end;
definition
func I_I4 -> BinOp of [.0,1.] means :II4Def:
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
proof
set C = [.0,1.];
defpred P[Real,Real] means $1 = 1 & $2 <> 1;
deffunc F(Element of C,Element of C) = In(0,C);
deffunc G(Element of C,Element of C) = In(1,C);
ex f being Function of [:C,C:],C st for c be Element of C,
d be Element of C st [c,d] in dom f holds
(P[c,d] implies f. [c,d] = F(c,d)) &
(not P [c,d] implies f. [c,d] = G(c,d)) from SCHEME1:sch 21; then
consider f being Function of [:C,C:],C such that
A1: for c be Element of C, d be Element of C st [c,d] in dom f holds
(P[c,d] implies f. [c,d] = F(c,d)) &
(not P [c,d] implies f. [c,d] = G(c,d));
take f;
A0: dom f = [:C,C:] by FUNCT_2:def 1;
let a,b be Element of C;
AA: [a,b] in dom f by A0,ZFMISC_1:87;
(a = 1 & b <> 1 implies f.(a,b) = 0) &
(a <> 1 or b = 1 implies f.(a,b) = 1)
proof
thus a = 1 & b <> 1 implies f.(a,b) = 0
proof
assume a = 1 & b <> 1; then
f. [a,b] = F(a,b) by A1,AA
.= 0 by SUBSET_1:def 8,XXREAL_1:1;
hence thesis;
end;
assume a <> 1 or b = 1; then
f. [a,b] = G(a,b) by A1,AA
.= 1 by XXREAL_1:1,SUBSET_1:def 8;
hence thesis;
end;
hence thesis;
end;
uniqueness
proof
let f1,f2 be BinOp of [.0,1.] such that
A1: for a,b being Element of [.0,1.] holds
(a <> 1 or b = 1 implies f1.(a,b) = 1) &
(a = 1 & b <> 1 implies f1.(a,b) = 0) and
A2: for a,b being Element of [.0,1.] holds
(a <> 1 or b = 1 implies f2.(a,b) = 1) &
(a = 1 & b <> 1 implies f2.(a,b) = 0);
for a,b being set st a in [.0,1.] & b in [.0,1.] holds
f1.(a,b) = f2.(a,b)
proof
let a,b be set;
assume a in [.0,1.] & b in [.0,1.]; then
reconsider aa = a, bb = b as Element of [.0,1.];
per cases;
suppose
B0: aa = 1 & bb < 1; then
f1.(aa,bb) = 0 by A1
.= f2.(aa,bb) by A2,B0;
hence thesis;
end;
suppose
B0: aa <> 1 or bb >= 1;
aa <> 1 or bb <= 1 by XXREAL_1:1; then
b0: aa <> 1 or bb = 1 by B0,XXREAL_0:1; then
f1.(aa,bb) = 1 by A1
.= f2.(aa,bb) by A2,b0;
hence thesis;
end;
end;
hence thesis by BINOP_1:def 21;
end;
end;
registration
cluster I_I4 -> decreasing_on_1st increasing_on_2nd
00-dominant 11-dominant 10-weak;
coherence
proof
set f = I_I4;
b1: for x1,x2,y being Element of [.0,1.] st
x1 <= x2 holds f.(x1,y) >= f.(x2,y)
proof
let x1,x2,y be Element of [.0,1.];
assume Z1: x1 <= x2;
per cases;
suppose Z0: x2 = 0; then
x1 = 0 by Z1,XXREAL_1:1;
hence thesis by Z0;
end;
suppose y = 1; then
f.(x1,y) = 1 & f.(x2,y) = 1 by II4Def;
hence thesis;
end;
suppose x1 <> 1; then
f.(x1,y) = 1 by II4Def;
hence thesis by XXREAL_1:1;
end;
suppose I1: x1 = 1 & y <> 1;
x2 <= 1 by XXREAL_1:1;
hence thesis by Z1,I1,XXREAL_0:1;
end;
end;
b2: for x,y1,y2 being Element of [.0,1.] st
y1 <= y2 holds f.(x,y1) <= f.(x,y2)
proof
let x,y1,y2 be Element of [.0,1.];
assume
SA: y1 <= y2;
per cases;
suppose x <> 1; then
f.(x,y1) = 1 & f.(x,y2) = 1 by II4Def;
hence thesis;
end;
suppose Z1: y1 = 1; then
y2 >= 1 & y2 <= 1 by SA,XXREAL_1:1;
hence thesis by Z1,XXREAL_0:1;
end;
suppose x = 1 & y1 <> 1 & y2 <> 1; then
f.(x,y1) = 0 & f.(x,y2) = 0 by II4Def;
hence thesis;
end;
suppose x = 1 & y1 <> 1 & y2 = 1; then
f.(x,y1) = 0 & f.(x,y2) = 1 by II4Def;
hence thesis;
end;
end;
0 in [.0,1.] & 1 in [.0,1.] by XXREAL_1:1;
hence thesis by b1,b2,II4Def;
end;
end;
theorem FNegD2:
FNegation I_I4 = NegationD2
proof
set I = I_I4;
set f = FNegation I;
set g = NegationD2;
A1: 0 in [.0,1.] by XXREAL_1:1;
for x being Element of [.0,1.] holds f.x = g.x
proof
let x be Element of [.0,1.];
x <= 1 by XXREAL_1:1; then
per cases by XXREAL_0:1;
suppose
B1: x < 1;
f.x = I.(x,0) by FUZIMPL3:def 16
.= 1 by II4Def,B1,A1
.= g.x by FUZIMPL3:def 18,B1;
hence thesis;
end;
suppose
B1: x = 1;
f.x = I.(x,0) by FUZIMPL3:def 16
.= 0 by A1,B1,II4Def
.= g.x by FUZIMPL3:def 18,B1;
hence thesis;
end;
end;
hence thesis by FUNCT_2:63;
end;
registration
cluster I_I4 -> satisfying_(EP) non satisfying_(NP);
coherence
proof
set I = I_I4;
ex y being Element of [.0,1.] st I.(1,y) <> y
proof
reconsider y = 1/2 as Element of [.0,1.] by XXREAL_1:1;
take y;
1 in [.0,1.] by XXREAL_1:1;
hence thesis by II4Def;
end; then
T1: I is non satisfying_(NP) by FUZIMPL2:def 1;
for x,y,z being Element of [.0,1.] holds I.(x,I.(y,z)) = I.(y,I.(x,z))
proof
let x,y,z be Element of [.0,1.];
per cases;
suppose D1: z = 1; then
I.(y,z) = 1 & I.(x,z) = 1 by II4Def;
hence thesis by D1;
end;
suppose
f2: z <> 1 & y <> 1 & x <> 1; then
I.(x,I.(y,z)) = 1 by II4Def
.= I.(y,I.(x,z)) by f2,II4Def;
hence thesis;
end;
suppose F1: z <> 1 & y <> 1 & x = 1; then
I.(y,z) = 1 & I.(x,z) = 0 by II4Def; then
I.(x,I.(y,z)) = 1 by II4Def
.= I.(y,I.(x,z)) by F1,II4Def;
hence thesis;
end;
suppose z <> 1 & y = 1 & x = 1;
hence thesis;
end;
suppose F1: z <> 1 & y = 1 & x <> 1; then
F3: I.(x,z) = 1 by II4Def;
I.(x,I.(y,z)) = 1 by II4Def,F1
.= I.(y,I.(x,z)) by F3,II4Def;
hence thesis;
end;
end;
hence thesis by T1,FUZIMPL2:def 2;
end;
end;
registration
cluster I_I4 -> (FNegation I_I4)-satisfying_CP;
coherence
proof
set N = FNegation I_I4;
set I = I_I4;
for x,y being Element of [.0,1.] holds
I.(x,y) = I.(N.y,N.x)
proof
let x,y be Element of [.0,1.];
per cases;
suppose F1: y = 1; then
F2: N.y = 0 by FUZIMPL3:def 4;
I.(x,y) = 1 by II4Def,F1
.= I.(N.y,N.x) by F2,II4Def;
hence thesis;
end;
suppose F1: x <> 1; then
F2: N.x = 1 by FNegD2,FUZIMPL3:def 18;
I.(x,y) = 1 by II4Def,F1
.= I.(N.y,N.x) by F2,II4Def;
hence thesis;
end;
suppose F1: x = 1 & y <> 1; then
F2: N.y = 1 by FNegD2,FUZIMPL3:def 18;
F3: N.y <> 0 & N.x = 0 by FNegD2,F1,FUZIMPL3:def 18;
I.(x,y) = 0 by II4Def,F1
.= I.(N.y,N.x) by F3,F2,II4Def;
hence thesis;
end;
end;
hence thesis;
end;
end;
:: Attribute satisfying CP wrt the natural negation
definition let I be Fuzzy_Implication;
attr I is satisfying_CP means
I is (FNegation I)-satisfying_CP;
attr I is satisfying_L-CP means
I is (FNegation I)-satisfying_L-CP;
attr I is satisfying_R-CP means
I is (FNegation I)-satisfying_R-CP;
end;
:: Table 1.9
LKIsCP:
I_LK is (N_CC)-satisfying_CP
proof
set N = N_CC;
set I = I_LK;
for x,y being Element of [.0,1.] holds
I.(x,y) = I.(N.y,N.x)
proof
let x,y be Element of [.0,1.];
I.(x,y) = min (1,1-(1-y)+(1-x)) by FUZIMPL1:def 14
.= min (1,1-N.y+(1-x)) by FUZIMPL3:def 6
.= min (1,1-N.y+N.x) by FUZIMPL3:def 6
.= I.(N.y,N.x) by FUZIMPL1:def 14;
hence thesis;
end;
hence thesis;
end;
LKIsLCP:
I_LK is (N_CC)-satisfying_L-CP
proof
set N = N_CC;
set I = I_LK;
for x,y being Element of [.0,1.] holds
I.(N.x,y) = I.(N.y,x)
proof
let x,y be Element of [.0,1.];
I.(N.x,y) = min (1,1-N.x+y) by FUZIMPL1:def 14
.= min (1,1-(1-x)+y) by FUZIMPL3:def 6
.= min (1,1-(1-y)+x)
.= min (1,1-N.y+x) by FUZIMPL3:def 6
.= I.(N.y,x) by FUZIMPL1:def 14;
hence thesis;
end;
hence thesis;
end;
LKIsRCP:
I_LK is (N_CC)-satisfying_R-CP
proof
set N = N_CC;
set I = I_LK;
for x,y being Element of [.0,1.] holds
I.(x,N.y) = I.(y,N.x)
proof
let x,y be Element of [.0,1.];
I.(x,N.y) = min (1,1-x+N.y) by FUZIMPL1:def 14
.= min (1,1-x+(1-y)) by FUZIMPL3:def 6
.= min (1,1-y+N.x) by FUZIMPL3:def 6
.= I.(y,N.x) by FUZIMPL1:def 14;
hence thesis;
end;
hence thesis;
end;
registration
cluster I_LK -> (N_CC)-satisfying_L-CP (N_CC)-satisfying_R-CP
(N_CC)-satisfying_CP;
coherence by LKIsRCP,LKIsLCP,LKIsCP;
end;
registration
cluster I_LK -> satisfying_L-CP satisfying_R-CP satisfying_CP;
coherence by FUZIMPL3:20;
end;
registration
cluster I_GD -> (NegationD1)-satisfying_R-CP;
coherence
proof
set N = NegationD1;
set I = I_GD;
for x,y being Element of [.0,1.] holds
I.(x,N.y) = I.(y,N.x)
proof
let x,y be Element of [.0,1.];
per cases;
suppose F1: x = 0; then
x <= N.y by XXREAL_1:1; then
I.(x,N.y) = 1 by FUZIMPL1:def 16
.= I.(y,1) by FUZIMPL1:8
.= I.(y,N.x) by F1,FUZIMPL3:def 4;
hence thesis;
end;
suppose F1: x <> 0 & y = 0; then
F2: N.x = 0 & N.y = 1 by FUZIMPL3:def 17;
I.(x,N.y) = 1 by F2,FUZIMPL1:8
.= I.(y,N.x) by F1,F2,FUZIMPL1:def 3;
hence thesis;
end;
suppose F1: x <> 0 & y <> 0; then
F2: N.x = 0 & N.y = 0 by FUZIMPL3:def 17;
F4: y > 0 by F1,XXREAL_1:1;
x > N.y by F1,F2,XXREAL_1:1; then
I.(x,N.y) = N.y by FUZIMPL1:def 16
.= I.(y,N.x) by F2,F4,FUZIMPL1:def 16;
hence thesis;
end;
end;
hence thesis;
end;
end;
registration
cluster I_GD -> satisfying_R-CP;
coherence by FUZIMPL3:21;
end;
IRCIsCP:
I_RC is (N_CC)-satisfying_CP
proof
set N = N_CC;
set I = I_RC;
for x,y being Element of [.0,1.] holds
I.(x,y) = I.(N.y,N.x)
proof
let x,y be Element of [.0,1.];
SA: N.x = 1 - x by FUZIMPL3:def 6;
SB: N.y = 1 - y by FUZIMPL3:def 6;
I.(x,y) = 1 - x + x * y by FUZIMPL1:def 17
.= 1 - N.y + N.y * N.x by SA,SB
.= I.(N.y,N.x) by FUZIMPL1:def 17;
hence thesis;
end;
hence thesis;
end;
IRCIsLCP:
I_RC is (N_CC)-satisfying_L-CP
proof
set N = N_CC;
set I = I_RC;
for x,y being Element of [.0,1.] holds
I.(N.x,y) = I.(N.y,x)
proof
let x,y be Element of [.0,1.];
SA: N.x = 1 - x by FUZIMPL3:def 6;
SB: N.y = 1 - y by FUZIMPL3:def 6;
I.(N.x,y) = 1 - N.x + N.x * y by FUZIMPL1:def 17
.= 1 - N.y + N.y * x by SA,SB
.= I.(N.y,x) by FUZIMPL1:def 17;
hence thesis;
end;
hence thesis;
end;
IRCIsRCP:
I_RC is (N_CC)-satisfying_R-CP
proof
set N = N_CC;
set I = I_RC;
for x,y being Element of [.0,1.] holds
I.(x,N.y) = I.(y,N.x)
proof
let x,y be Element of [.0,1.];
I.(x,N.y) = 1 - x + x * N.y by FUZIMPL1:def 17
.= 1 - x + x * (1 - y) by FUZIMPL3:def 6
.= 1 - y + y * (1 - x)
.= 1 - y + y * N.x by FUZIMPL3:def 6
.= I.(y,N.x) by FUZIMPL1:def 17;
hence thesis;
end;
hence thesis;
end;
registration
cluster I_RC -> (N_CC)-satisfying_CP
(N_CC)-satisfying_L-CP (N_CC)-satisfying_R-CP;
coherence by IRCIsCP,IRCIsLCP,IRCIsRCP;
end;
registration
cluster I_RC -> satisfying_CP satisfying_L-CP satisfying_R-CP;
coherence by FUZIMPL3:22;
end;
registration
cluster I_KD -> (N_CC)-satisfying_CP;
coherence
proof
set N = N_CC;
set I = I_KD;
for x,y being Element of [.0,1.] holds
I.(x,y) = I.(N.y,N.x)
proof
let x,y be Element of [.0,1.];
F6: 1 - N.y = 1 - (1 - y) by FUZIMPL3:def 6
.= y;
I.(x,y) = max (1-x,y) by FUZIMPL1:def 18
.= max (1-N.y,N.x) by F6,FUZIMPL3:def 6
.= I.(N.y,N.x) by FUZIMPL1:def 18;
hence thesis;
end;
hence thesis;
end;
end;
registration
cluster I_KD -> (N_CC)-satisfying_L-CP;
coherence
proof
set N = N_CC;
set I = I_KD;
for x,y being Element of [.0,1.] holds
I.(N.x,y) = I.(N.y,x)
proof
let x,y be Element of [.0,1.];
F5: 1 - N.x = 1 - (1 - x) by FUZIMPL3:def 6
.= x;
F6: 1 - N.y = 1 - (1 - y) by FUZIMPL3:def 6
.= y;
I.(N.x,y) = max (1-N.x,y) by FUZIMPL1:def 18
.= I.(N.y,x) by F5,F6,FUZIMPL1:def 18;
hence thesis;
end;
hence thesis;
end;
end;
registration
cluster I_KD -> (N_CC)-satisfying_R-CP;
coherence
proof
set N = N_CC;
set I = I_KD;
for x,y being Element of [.0,1.] holds
I.(x,N.y) = I.(y,N.x)
proof
let x,y be Element of [.0,1.];
I.(x,N.y) = max (1-x,N.y) by FUZIMPL1:def 18
.= max (1-x,1-y) by FUZIMPL3:def 6
.= max (1-y,N.x) by FUZIMPL3:def 6
.= I.(y,N.x) by FUZIMPL1:def 18;
hence thesis;
end;
hence thesis;
end;
end;
registration
cluster I_KD -> satisfying_CP satisfying_L-CP satisfying_R-CP;
coherence by FUZIMPL3:23;
end;
registration
cluster I_GG -> (NegationD1)-satisfying_R-CP;
coherence
proof
set N = NegationD1;
set I = I_GG;
for x,y being Element of [.0,1.] holds
I.(x,N.y) = I.(y,N.x)
proof
let x,y be Element of [.0,1.];
per cases;
suppose F1: x = 0; then
F2: N.x = 1 by FUZIMPL3:def 4;
x <= N.y by F1,XXREAL_1:1; then
I.(x,N.y) = 1 by FUZIMPL1:def 19
.= I.(y,N.x) by F2,FUZIMPL1:8;
hence thesis;
end;
suppose F1: x <> 0 & y = 0; then
F2: N.x = 0 & N.y = 1 by FUZIMPL3:def 17;
I.(x,N.y) = 1 by F2,FUZIMPL1:8
.= I.(y,N.x) by F1,F2,FUZIMPL1:def 3;
hence thesis;
end;
suppose F1: x <> 0 & y <> 0; then
F2: N.x = 0 & N.y = 0 by FUZIMPL3:def 17;
F3: 0 in [.0,1.] by XXREAL_1:1;
F4: y > 0 by F1,XXREAL_1:1;
x > N.y by F1,F2,XXREAL_1:1; then
I.(x,N.y) = (N.y) / x by FUZIMPL1:def 19
.= 0 / y by F2
.= I.(y,0) by F3,F4,FUZIMPL1:def 19
.= I.(y,N.x) by F1,FUZIMPL3:def 17;
hence thesis;
end;
end;
hence thesis;
end;
end;
registration
cluster I_GG -> satisfying_R-CP;
coherence by FUZIMPL3:24;
end;
IRSIsCP: I_RS is (N_CC)-satisfying_CP
proof
set N = N_CC;
set I = I_RS;
for x,y being Element of [.0,1.] holds
I.(x,y) = I.(N.y,N.x)
proof
let x,y be Element of [.0,1.];
per cases;
suppose A1: x <= y; then
1 - x >= 1 - y by XREAL_1:10; then
N.y <= 1 - x by FUZIMPL3:def 6; then
A2: N.y <= N.x by FUZIMPL3:def 6;
I.(x,y) = 1 by A1,FUZIMPL1:def 20
.= I.(N.y,N.x) by A2,FUZIMPL1:def 20;
hence thesis;
end;
suppose A1: x > y; then
1 - x < 1 - y by XREAL_1:10; then
N.x < 1 - y by FUZIMPL3:def 6; then
A2: N.x < N.y by FUZIMPL3:def 6;
I.(x,y) = 0 by A1,FUZIMPL1:def 20
.= I.(N.y,N.x) by A2,FUZIMPL1:def 20;
hence thesis;
end;
end;
hence thesis;
end;
theorem IRSIsLCP:
I_RS is (N_CC)-satisfying_L-CP
proof
set N = N_CC; set I = I_RS;
for x,y being Element of [.0,1.] holds I.(N.x,y) = I.(N.y,x)
proof
let x,y be Element of [.0,1.];
per cases;
suppose A1: N.x <= y; then
1 - x <= y by FUZIMPL3:def 6; then
1 - y <= x by XREAL_1:12; then
A2: N.y <= x by FUZIMPL3:def 6;
I.(N.x,y) = 1 by A1,FUZIMPL1:def 20
.= I.(N.y,x) by A2,FUZIMPL1:def 20;
hence thesis;
end;
suppose A1: N.x > y; then
1 - x > y by FUZIMPL3:def 6; then
1 - y > x by XREAL_1:12; then
A2: N.y > x by FUZIMPL3:def 6;
I.(N.x,y) = 0 by A1,FUZIMPL1:def 20
.= I.(N.y,x) by A2,FUZIMPL1:def 20;
hence thesis;
end;
end;
hence thesis;
end;
IRSIsRCP: I_RS is (N_CC)-satisfying_R-CP
proof
set N = N_CC;
set I = I_RS;
for x,y being Element of [.0,1.] holds
I.(x,N.y) = I.(y,N.x)
proof
let x,y be Element of [.0,1.];
per cases;
suppose A1: x <= N.y; then
x <= 1 - y by FUZIMPL3:def 6; then
1 - x >= y by XREAL_1:11; then
A2: N.x >= y by FUZIMPL3:def 6;
I.(x,N.y) = 1 by A1,FUZIMPL1:def 20
.= I.(y,N.x) by A2,FUZIMPL1:def 20;
hence thesis;
end;
suppose A1: x > N.y; then
x > 1 - y by FUZIMPL3:def 6; then
y > 1 - x by XREAL_1:11; then
A2: y > N.x by FUZIMPL3:def 6;
I.(x,N.y) = 0 by A1,FUZIMPL1:def 20
.= I.(y,N.x) by A2,FUZIMPL1:def 20;
hence thesis;
end;
end;
hence thesis;
end;
registration
cluster I_RS -> (N_CC)-satisfying_CP (N_CC)-satisfying_L-CP
(N_CC)-satisfying_R-CP;
coherence by IRSIsCP,IRSIsLCP,IRSIsRCP;
end;
theorem
for N being decreasing Fuzzy_Negation holds
I_RS is N-satisfying_CP
proof
let N be decreasing Fuzzy_Negation;
set I = I_RS;
for x,y being Element of [.0,1.] holds
I.(x,y) = I.(N.y,N.x)
proof
let x,y be Element of [.0,1.];
per cases;
suppose A1: x <= y; then
A2: N.y <= N.x by FUZIMPL3:7;
I.(x,y) = 1 by A1,FUZIMPL1:def 20
.= I.(N.y,N.x) by A2,FUZIMPL1:def 20;
hence thesis;
end;
suppose A1: x > y; then
A2: N.x < N.y by FUZIMPL3:8;
I.(x,y) = 0 by A1,FUZIMPL1:def 20
.= I.(N.y,N.x) by A2,FUZIMPL1:def 20;
hence thesis;
end;
end;
hence thesis;
end;
registration
cluster I_YG -> (NegationD1)-satisfying_R-CP;
coherence
proof
set N = NegationD1;
set I = I_YG;
for x,y being Element of [.0,1.] holds
I.(x,N.y) = I.(y,N.x)
proof
let x,y be Element of [.0,1.];
per cases by XXREAL_1:1;
suppose F1: x > 0 & y > 0; then
F2: N.x = 0 & N.y = 0 by FUZIMPL3:def 17;
I.(x,N.y) = (N.y) to_power x by F1,FUZIMPL1:def 21
.= 0 by F1,F2,POWER:def 2
.= 0 to_power y by F1,POWER:def 2
.= (N.x) to_power y by F1,FUZIMPL3:def 17
.= I.(y,N.x) by F1,FUZIMPL1:def 21;
hence thesis;
end;
suppose F1: x = 0 & y > 0; then
N.x = 1 & N.y = 0 by FUZIMPL3:def 17; then
I.(x,N.y) = 1 by F1,FUZIMPL1:def 21
.= 1 to_power y by POWER:26
.= (N.x) to_power y by F1,FUZIMPL3:def 17
.= I.(y,N.x) by FUZIMPL1:def 21,F1;
hence thesis;
end;
suppose F1: x > 0 & y = 0; then
F2: N.x = 0 & N.y = 1 by FUZIMPL3:def 17;
I.(x,N.y) = (N.y) to_power x by F1,FUZIMPL1:def 21
.= 1 by F2,POWER:26
.= I.(y,N.x) by F1,F2,FUZIMPL1:def 21;
hence thesis;
end;
suppose x = 0 & y = 0; then
F2: N.x = 1 & N.y = 1 by FUZIMPL3:def 17; then
I.(x,N.y) = (N.y) to_power x by FUZIMPL1:def 21
.= 1 by F2,POWER:26
.= (N.x) to_power y by F2,POWER:26
.= I.(y,N.x) by FUZIMPL1:def 21,F2;
hence thesis;
end;
end;
hence thesis;
end;
end;
registration
cluster I_YG -> satisfying_R-CP;
coherence by FUZIMPL3:26;
end;
registration
cluster I_WB -> (NegationD2)-satisfying_R-CP;
coherence
proof
set N = NegationD2;
set I = I_WB;
for x,y being Element of [.0,1.] holds
I.(x,N.y) = I.(y,N.x)
proof
let x,y be Element of [.0,1.];
x <= 1 by XXREAL_1:1; then
per cases by XXREAL_0:1;
suppose F1: x < 1; then
F2: N.x = 1 by FUZIMPL3:def 18;
I.(x,N.y) = 1 by F1,FUZIMPL1:def 22
.= I.(y,N.x) by F2,FUZIMPL1:8;
hence thesis;
end;
suppose F1: x = 1; then
I.(x,N.y) = N.y by FUZIMPL1:def 22
.= I.(y,0) by FUZIMPL3:def 16,27
.= I.(y,N.x) by F1,FUZIMPL3:def 18;
hence thesis;
end;
end;
hence thesis;
end;
end;
registration
cluster I_WB -> satisfying_R-CP;
coherence by FUZIMPL3:27;
end;
IFDIsCP:
I_FD is (N_CC)-satisfying_CP
proof
set N = N_CC;
set I = I_FD;
for x,y being Element of [.0,1.] holds
I.(x,y) = I.(N.y,N.x)
proof
let x,y be Element of [.0,1.];
per cases;
suppose A1: x <= y; then
1 - x >= 1 - y by XREAL_1:10; then
N.x >= 1 - y by FUZIMPL3:def 6; then
A2: N.x >= N.y by FUZIMPL3:def 6;
I.(x,y) = 1 by A1,FUZIMPL1:def 23
.= I.(N.y,N.x) by A2,FUZIMPL1:def 23;
hence thesis;
end;
suppose A1: x > y; then
1 - x < 1 - y by XREAL_1:10; then
N.x < 1 - y by FUZIMPL3:def 6; then
A2: N.x < N.y by FUZIMPL3:def 6;
A3: N.x = 1 - x & N.y = 1 - y by FUZIMPL3:def 6;
I.(x,y) = max (1-N.y,N.x) by A3,A1,FUZIMPL1:def 23
.= I.(N.y,N.x) by A2,FUZIMPL1:def 23;
hence thesis;
end;
end;
hence thesis;
end;
IFDIsLCP:
I_FD is (N_CC)-satisfying_L-CP
proof
set N = N_CC;
set I = I_FD;
for x,y being Element of [.0,1.] holds
I.(N.x,y) = I.(N.y,x)
proof
let x,y be Element of [.0,1.];
per cases;
suppose A1: x >= N.y; then
x >= 1 - y by FUZIMPL3:def 6; then
1 - x <= y by XREAL_1:12; then
N.x <= y by FUZIMPL3:def 6; then
I.(N.x,y) = 1 by FUZIMPL1:def 23
.= I.(N.y,x) by A1,FUZIMPL1:def 23;
hence thesis;
end;
suppose A1: x < N.y; then
x < 1 - y by FUZIMPL3:def 6; then
y < 1 - x by XREAL_1:12; then
A2: y < N.x by FUZIMPL3:def 6;
A3: N.x = 1 - x & N.y = 1 - y by FUZIMPL3:def 6;
I.(N.x,y) = max (1-N.x,y) by A2,FUZIMPL1:def 23
.= max (1-N.y,x) by A3
.= I.(N.y,x) by A1,FUZIMPL1:def 23;
hence thesis;
end;
end;
hence thesis;
end;
IFDIsRCP:
I_FD is (N_CC)-satisfying_R-CP
proof
set N = N_CC;
set I = I_FD;
for x,y being Element of [.0,1.] holds
I.(x,N.y) = I.(y,N.x)
proof
let x,y be Element of [.0,1.];
per cases;
suppose A1: x <= N.y; then
x <= 1 - y by FUZIMPL3:def 6; then
1 - x >= y by XREAL_1:11; then
A2: N.x >= y by FUZIMPL3:def 6;
I.(x,N.y) = 1 by A1,FUZIMPL1:def 23
.= I.(y,N.x) by A2,FUZIMPL1:def 23;
hence thesis;
end;
suppose A1: x > N.y; then
x > 1 - y by FUZIMPL3:def 6; then
y > 1 - x by XREAL_1:11; then
A2: y > N.x by FUZIMPL3:def 6;
I.(x,N.y) = max (1-x,N.y) by A1,FUZIMPL1:def 23
.= max (1-x,1-y) by FUZIMPL3:def 6
.= max (1-y,N.x) by FUZIMPL3:def 6
.= I.(y,N.x) by A2,FUZIMPL1:def 23;
hence thesis;
end;
end;
hence thesis;
end;
registration
cluster I_FD -> (N_CC)-satisfying_CP
(N_CC)-satisfying_L-CP (N_CC)-satisfying_R-CP;
coherence by IFDIsCP,IFDIsLCP,IFDIsRCP;
end;
registration
cluster I_FD -> satisfying_CP satisfying_L-CP satisfying_R-CP;
coherence by FUZIMPL3:28;
end;
begin :: Fuzzy Lattice Revisited
theorem :: Theorem 1.4.3, just for the illustration
FuzzyLattice [.0,1.] is complete Heyting distributive LATTICE;
theorem LemmaFuncs:
the set of all f where f is Fuzzy_Negation c= Funcs ([.0,1.],[.0,1.])
proof
let x be object;
assume x in the set of all f where f is Fuzzy_Negation; then
consider f being Fuzzy_Negation such that
A1: x = f;
thus thesis by A1,FUNCT_2:8;
end;
LemmaFunc:
for N being Fuzzy_Negation holds
N is Function of [.0,1.], REAL
proof
let N be Fuzzy_Negation;
rng N c= REAL by RELAT_1:def 19;
hence thesis by FUNCT_2:6;
end;
LemmaFunc2:
for N being Fuzzy_Negation holds
N in Funcs ([.0,1.], REAL)
proof
let N be Fuzzy_Negation;
N is Function of [.0,1.], REAL by LemmaFunc;
hence thesis by FUNCT_2:8;
end;
LemmaMaxRng:
for f,g being Function of [.0,1.], REAL holds
rng max (f,g) c= rng f \/ rng g
proof
let f,g be Function of [.0,1.], REAL;
let y be object;
assume y in rng max (f,g); then
consider x being object such that
A1: x in dom max (f,g) & y = (max (f,g)).x by FUNCT_1:def 3;
A3: dom max (f,g) = [.0,1.] by FUNCT_2:def 1;
dom f = [.0,1.] & dom g = [.0,1.] by FUNCT_2:def 1; then
A2: x in dom f & x in dom g by A1,FUNCT_2:def 1;
max (f,g).x = max (f.x,g.x) by A1,A3,COUSIN2:def 2; then
max (f,g).x = f.x or max (f,g).x = g.x by XXREAL_0:16; then
y in rng f or y in rng g by A1,A2,FUNCT_1:def 3;
hence thesis by XBOOLE_0:def 3;
end;
LemmaMinRng:
for f,g being Function of [.0,1.], REAL holds
rng min (f,g) c= rng f \/ rng g
proof
let f,g be Function of [.0,1.], REAL;
let y be object;
assume y in rng min (f,g); then
consider x being object such that
A1: x in dom min (f,g) & y = (min (f,g)).x by FUNCT_1:def 3;
A3: dom min (f,g) = [.0,1.] by FUNCT_2:def 1;
dom f = [.0,1.] & dom g = [.0,1.] by FUNCT_2:def 1; then
A2: x in dom f & x in dom g by A1,FUNCT_2:def 1;
min (f,g).x = min (f.x,g.x) by A1,A3,COUSIN2:def 1; then
min (f,g).x = f.x or min (f,g).x = g.x by XXREAL_0:15; then
y in rng f or y in rng g by A1,A2,FUNCT_1:def 3;
hence thesis by XBOOLE_0:def 3;
end;
definition let N1,N2 be Fuzzy_Negation;
func max (N1,N2) -> Fuzzy_Negation means :MaxFuz:
ex f,g being Function of [.0,1.], REAL st
f = N1 & g = N2 & it = max (f,g);
existence
proof
reconsider f = N1, g = N2 as Function of [.0,1.], REAL by LemmaFunc;
A1: rng max (f,g) c= rng f \/ rng g by LemmaMaxRng;
rng f c= [.0,1.] & rng g c= [.0,1.] by RELAT_1:def 19; then
rng f \/ rng g c= [.0,1.] by XBOOLE_1:8; then
rng max (f,g) c= [.0,1.] by A1,XBOOLE_1:1; then
::::::::::::::::::: Lemma!
reconsider EX = max (f,g) as UnOp of [.0,1.] by FUNCT_2:6;
B0: 0 in [.0,1.] & 1 in [.0,1.] by XXREAL_1:1;
B1: EX.0 = max (f.0,g.0) by B0,COUSIN2:def 2
.= max (1,N2.0) by FUZIMPL3:def 4
.= max (1,1) by FUZIMPL3:def 4
.= 1;
EX.1 = max (f.1,g.1) by B0,COUSIN2:def 2
.= max (0,N2.1) by FUZIMPL3:def 4
.= max (0,0) by FUZIMPL3:def 4
.= 0; then
C1: EX is satisfying_(N1) by B1,FUZIMPL3:def 4;
for a,b being Element of [.0,1.] st a <= b holds EX.a >= EX.b
proof
let a,b be Element of [.0,1.];
assume a <= b; then
f.a >= f.b & g.a >= g.b by FUZIMPL3:7; then
max (f.a,g.a) >= max (f.b,g.b) by XXREAL_0:26; then
max (f,g).a >= max (f.b,g.b) by COUSIN2:def 2;
hence thesis by COUSIN2:def 2;
end; then
reconsider EX as Fuzzy_Negation by C1,FUZIMPL3:def 5,7;
ex f,g being Function of [.0,1.], REAL st
f = N1 & g = N2 & EX = max (f,g);
hence thesis;
end;
uniqueness;
func min (N1,N2) -> Fuzzy_Negation means :MinFuz:
ex f,g being Function of [.0,1.], REAL st
f = N1 & g = N2 & it = min (f,g);
existence
proof
reconsider f = N1, g = N2 as Function of [.0,1.], REAL by LemmaFunc;
set EX = min (f,g);
A1: rng min (f,g) c= rng f \/ rng g by LemmaMinRng;
rng f c= [.0,1.] & rng g c= [.0,1.] by RELAT_1:def 19; then
rng f \/ rng g c= [.0,1.] by XBOOLE_1:8; then
rng min (f,g) c= [.0,1.] by A1,XBOOLE_1:1; then
::::::::::::::::::: Lemma!
reconsider EX as UnOp of [.0,1.] by FUNCT_2:6;
B0: 0 in [.0,1.] & 1 in [.0,1.] by XXREAL_1:1;
B1: EX.0 = min (f.0,g.0) by B0,COUSIN2:def 1
.= min (1,N2.0) by FUZIMPL3:def 4
.= min (1,1) by FUZIMPL3:def 4
.= 1;
EX.1 = min (f.1,g.1) by B0,COUSIN2:def 1
.= min (0,N2.1) by FUZIMPL3:def 4
.= min (0,0) by FUZIMPL3:def 4
.= 0; then
C1: EX is satisfying_(N1) by B1,FUZIMPL3:def 4;
for a,b being Element of [.0,1.] st a <= b holds EX.a >= EX.b
proof
let a,b be Element of [.0,1.];
assume a <= b; then
f.a >= f.b & g.a >= g.b by FUZIMPL3:7; then
min (f.a,g.a) >= min (f.b,g.b) by XXREAL_0:18; then
min (f,g).a >= min (f.b,g.b) by COUSIN2:def 1;
hence thesis by COUSIN2:def 1;
end; then
reconsider EX as Fuzzy_Negation by C1,FUZIMPL3:def 5,7;
ex f,g being Function of [.0,1.], REAL st
f = N1 & g = N2 & EX = min (f,g);
hence thesis;
end;
uniqueness;
end;
LemmaCarrier:
the carrier of ((RealPoset [.0,1.]) |^ [.0,1.]) =
Funcs ([.0,1.],[.0,1.])
proof
set Y = RealPoset [.0,1.];
the carrier of Y = [.0,1.] by LFUZZY_0:def 3;
hence thesis by YELLOW_1:28;
end;
definition
func Fuzzy_Negations -> strict full SubRelStr of
FuzzyLattice [.0,1.] means :FuzNegDef:
the carrier of it = the set of all f where f is Fuzzy_Negation;
existence
proof
set X = the set of all f where f is Fuzzy_Negation;
reconsider X as Subset of FuzzyLattice [.0,1.]
by LemmaCarrier,LemmaFuncs;
the carrier of subrelstr X = X by YELLOW_0:def 15;
hence thesis;
end;
uniqueness by YELLOW_0:57;
end;
registration
cluster Fuzzy_Negations -> non empty reflexive transitive antisymmetric;
coherence
proof
N_CC in the set of all f where f is Fuzzy_Negation;
hence thesis by FuzNegDef;
end;
end;
theorem
for f,g being Fuzzy_Negation holds
max(f,g) = (maxfuncreal [.0,1.]).(f,g)
proof
let f,g be Fuzzy_Negation;
set A = [.0,1.];
set fg = max (f,g);
set mfg = (maxfuncreal [.0,1.]).(f,g);
B1: dom fg = [.0,1.] by FUNCT_2:def 1;
AC: f in Funcs(A,REAL) & g in Funcs(A,REAL) & Funcs (A,REAL) <> {}
by LemmaFunc2;
mfg in Funcs (A,REAL) by AC,BINOP_1:17; then
consider f1 being Function such that
C1: mfg = f1 & dom f1 = A & rng f1 c= REAL by FUNCT_2:def 2;
for x being object st x in [.0,1.] holds
fg.x = mfg.x
proof
let x be object;
assume D0: x in [.0,1.];
consider f2,g2 being Function of [.0,1.], REAL such that
D1: f2 = f & g2 = g & fg = max (f2,g2) by MaxFuz;
dom f = A & rng f c= REAL &
dom g = A & rng g c= REAL by FUNCT_2:def 1,RELAT_1:def 19; then
reconsider fA = f, gA = g as Element of Funcs(A,REAL)
by FUNCT_2:def 2;
dom (maxreal.:(fA,gA)) = A by FUNCT_2:def 1; then
(maxreal.:(fA,gA)).x = maxreal.(fA.x,gA.x) by D0,FUNCOP_1:22
.= max (fA.x,gA.x) by REAL_LAT:def 2
.= fg.x by D1,D0,COUSIN2:def 2;
hence thesis by REAL_LAT:def 4;
end;
hence thesis by C1,B1,FUNCT_1:2;
end;
theorem MaxEqMax:
for f,g being Fuzzy_Negation,
ff, gg being Membership_Func of [.0,1.] st
f = ff & g = gg holds
max(f,g) = max (ff,gg)
proof
let f,g being Fuzzy_Negation,
ff, gg being Membership_Func of [.0,1.];
assume
A1: f = ff & g = gg;
consider f1,g1 being Function of [.0,1.], REAL such that
A2: f1 = f & g1 = g & max (f,g) = max (f1,g1) by MaxFuz;
reconsider ff1 = f1, gg1 = g1 as Membership_Func of [.0,1.] by A2;
for c being Element of [.0,1.] holds max(ff1,gg1).c = max(ff1.c,gg1.c)
by FUZZY_1:def 4;
hence thesis by A1,A2,COUSIN2:def 2;
end;
theorem MinEqMin:
for f,g being Fuzzy_Negation,
ff, gg being Membership_Func of [.0,1.] st
f = ff & g = gg holds
min (f,g) = min (ff,gg)
proof
let f,g being Fuzzy_Negation,
ff, gg being Membership_Func of [.0,1.];
assume
A1: f = ff & g = gg;
consider f1,g1 being Function of [.0,1.], REAL such that
A2: f1 = f & g1 = g & min (f,g) = min (f1,g1) by MinFuz;
reconsider ff1 = f1, gg1 = g1 as Membership_Func of [.0,1.] by A2;
for c being Element of [.0,1.] holds min(ff1,gg1).c = min(ff1.c,gg1.c)
by FUZZY_1:def 3;
hence thesis by A1,A2,COUSIN2:def 1;
end;
theorem
for f,g being Fuzzy_Negation holds
min(f,g) = (minfuncreal [.0,1.]).(f,g)
proof
let f,g be Fuzzy_Negation;
set A = [.0,1.];
set fg = min (f,g);
set mfg = (minfuncreal [.0,1.]).(f,g);
B1: dom fg = [.0,1.] by FUNCT_2:def 1;
f in Funcs(A,REAL) & g in Funcs(A,REAL) & Funcs (A,REAL) <> {}
by LemmaFunc2; then
(minfuncreal A).(f,g) in Funcs (A,REAL) by BINOP_1:17; then
consider f1 being Function such that
C1: mfg = f1 & dom f1 = A & rng f1 c= REAL by FUNCT_2:def 2;
for x being object st x in [.0,1.] holds
fg.x = mfg.x
proof
let x be object;
assume D0: x in [.0,1.];
consider f2,g2 being Function of [.0,1.], REAL such that
D1: f2 = f & g2 = g & fg = min (f2,g2) by MinFuz;
dom f = A & rng f c= REAL &
dom g = A & rng g c= REAL by FUNCT_2:def 1,RELAT_1:def 19; then
reconsider fA = f, gA = g as Element of Funcs(A,REAL)
by FUNCT_2:def 2;
dom (minreal.:(fA,gA)) = A by FUNCT_2:def 1; then
(minreal.:(fA,gA)).x = minreal.(fA.x,gA.x) by D0,FUNCOP_1:22
.= min (fA.x,gA.x) by REAL_LAT:def 1
.= fg.x by D1,D0,COUSIN2:def 1;
hence thesis by REAL_LAT:def 5;
end;
hence thesis by C1,B1,FUNCT_1:2;
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;
redefine func {a,b} -> Subset of L; :: redefines { (TARSKI, definition)
coherence by ZFMISC_1:32;
end;
registration
cluster Fuzzy_Negations -> join-inheriting;
coherence
proof
set L = FuzzyLattice [.0,1.];
set S = Fuzzy_Negations;
for x,y being Element of L st
x in the carrier of S & y in the carrier of S & ex_sup_of {x,y},L holds
sup {x,y} in the carrier of S
proof
let x,y be Element of L;
assume
S0: x in the carrier of S & y in the carrier of S &
ex_sup_of {x,y},L; then
x in the set of all f where f is Fuzzy_Negation by FuzNegDef; then
consider f being Fuzzy_Negation such that
S1: x = f;
y in the set of all f where f is Fuzzy_Negation by S0,FuzNegDef; then
consider g being Fuzzy_Negation such that
s1: y = g;
reconsider xx = x, yy = y as Fuzzy_Negation by S1,s1;
consider fxy being Function such that
F1: fxy = sup {x,y} & dom fxy = [.0,1.] & rng fxy c= [.0,1.]
by FUNCT_2:def 2,LemmaCarrier;
reconsider fxy as UnOp of [.0,1.] by F1,FUNCT_2:2;
T3: x "\/" y = max (@x,@y) by LFUZZY_0:19
.= max (xx,yy) by MaxEqMax;
fxy is Fuzzy_Negation by F1,T3,YELLOW_0:41; then
fxy in the set of all f where f is Fuzzy_Negation;
hence thesis by F1,FuzNegDef;
end;
hence thesis by YELLOW_0:def 17;
end;
cluster Fuzzy_Negations -> meet-inheriting;
coherence
proof
set L = FuzzyLattice [.0,1.];
set S = Fuzzy_Negations;
for x,y being Element of L st
x in the carrier of S & y in the carrier of S & ex_inf_of {x,y},L holds
inf {x,y} in the carrier of S
proof
let x,y be Element of L;
assume
S0: x in the carrier of S & y in the carrier of S &
ex_inf_of {x,y},L; then
x in the set of all f where f is Fuzzy_Negation by FuzNegDef; then
consider f being Fuzzy_Negation such that
S1: x = f;
y in the set of all f where f is Fuzzy_Negation by S0,FuzNegDef; then
consider g being Fuzzy_Negation such that
s1: y = g;
reconsider xx = x, yy = y as Fuzzy_Negation by S1,s1;
consider fxy being Function such that
F1: fxy = inf {x,y} & dom fxy = [.0,1.] & rng fxy c= [.0,1.]
by FUNCT_2:def 2,LemmaCarrier;
reconsider fxy as UnOp of [.0,1.] by F1,FUNCT_2:2;
T3: x "/\" y = min (@x,@y) by LFUZZY_0:21
.= min (xx,yy) by MinEqMin;
fxy is Fuzzy_Negation by F1,T3,YELLOW_0:40; then
fxy in the set of all f where f is Fuzzy_Negation;
hence thesis by F1,FuzNegDef;
end;
hence thesis by YELLOW_0:def 16;
end;
end;
theorem
for N1,N2 being Element of Fuzzy_Negations,
NN1,NN2 being Fuzzy_Negation st N1 = NN1 & N2 = NN2 holds
N1 "\/" N2 = max (NN1,NN2)
proof
let N1,N2 be Element of Fuzzy_Negations,
NN1,NN2 be Fuzzy_Negation;
assume
A0: N1 = NN1 & N2 = NN2;
reconsider s = N1, t = N2 as Element of FuzzyLattice [.0,1.]
by YELLOW_0:58;
A4: s "\/" t = N1 "\/" N2 by YELLOW_0:70;
s "\/" t = max(@s, @t) by LFUZZY_0:19;
hence thesis by A0,A4,MaxEqMax;
end;
theorem
for N1,N2 being Element of Fuzzy_Negations,
NN1,NN2 being Fuzzy_Negation st N1 = NN1 & N2 = NN2 holds
N1 "/\" N2 = min (NN1,NN2)
proof
let N1,N2 be Element of Fuzzy_Negations,
NN1,NN2 be Fuzzy_Negation;
assume
A0: N1 = NN1 & N2 = NN2;
reconsider s = N1, t = N2 as Element of FuzzyLattice [.0,1.]
by YELLOW_0:58;
A4: s "/\" t = N1 "/\" N2 by YELLOW_0:69;
s "/\" t = min(@s, @t) by LFUZZY_0:21;
hence thesis by A0,A4,MinEqMin;
end;