:: Formal Development of Rough Inclusion Functions
:: by Adam Grabowski
::
:: Received August 29, 2019
:: Copyright (c) 2019-2021 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 STRUCT_0, ORDERS_2, RELAT_1, TARSKI, ZFMISC_1, XBOOLE_0,
SUBSET_1, FUNCT_1, ROUGHS_1, ROUGHS_2, ROUGHS_5, ROUGHIF1, FINSET_1,
CARD_1, REAL_1, NUMBERS, ARYTM_3, XXREAL_0, XXREAL_1, ARYTM_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, BINOP_1, ENUMSET1, ORDINAL1,
XCMPLX_0, XXREAL_0, FINSET_1, CARD_1, XREAL_0, PARTFUN1, FUNCT_2,
RCOMP_1, STRUCT_0, ORDERS_2, ROUGHS_1, ROUGHS_2, ROUGHS_5;
constructors REALSET2, ROUGHS_1, ROUGHS_2, RCOMP_1, RVSUM_1, ROUGHS_5;
registrations XBOOLE_0, SUBSET_1, FINSET_1, NAT_1, STRUCT_0, ORDERS_2,
ROUGHS_1, CARD_1, ORDINAL1, XXREAL_0, XREAL_0, MEMBERED, FUZNORM1,
XCMPLX_0;
requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM;
equalities SUBSET_1, STRUCT_0, ROUGHS_5;
expansions TARSKI, XBOOLE_0;
theorems XBOOLE_1, SUBSET_1, ZFMISC_1, CARD_1, XXREAL_1, NAT_1, XREAL_1,
XCMPLX_1, CARD_2, BINOP_1, ENUMSET1, PRE_TOPC, TDLAT_1, ROUGHS_5,
XXREAL_0;
schemes BINOP_1;
begin :: Preliminaries
theorem Lemacik:
for a,b,c being Real st a <= b & b > 0 & c >= 0
holds a / b <= (a + c) / (b + c)
proof
let a,b,c be Real;
assume
A1: a <= b & b > 0 & c >= 0; then
a * c <= b * c by XREAL_1:64; then
a * b + a * c <= a * b + b * c by XREAL_1:6; then
a * (b + c) <= b * (a + c);
hence thesis by XREAL_1:102,A1;
end;
registration
cluster strict finite for Approximation_Space;
existence
proof
set R = RelStr (# {{}}, id {{}} #);
take R;
thus thesis;
end;
end;
registration let R be finite 1-sorted;
cluster -> finite for Subset of R;
coherence;
end;
reserve R for 1-sorted;
reserve X,Y for Subset of R;
theorem LemmaSet:
X c= Y iff X` \/ Y = [#]R
proof
thus X c= Y implies X` \/ Y = [#]R
proof
assume X c= Y; then
X \ Y = {} by XBOOLE_1:37; then
(X \ Y)` = [#]R;
hence thesis by SUBSET_1:14;
end;
assume X` \/ Y = [#]R; then
(X \ Y)`` = ({}R)`` by SUBSET_1:14;
hence thesis by XBOOLE_1:37;
end;
reserve R for finite 1-sorted;
reserve X,Y for Subset of R;
theorem LemmaCard:
card (X \/ Y) = card Y iff X c= Y
proof
X c= X \/ Y & Y c= X \/ Y by XBOOLE_1:7;
hence card (X \/ Y) = card Y implies X c= Y by CARD_2:102;
assume X c= Y;
hence thesis by XBOOLE_1:12;
end;
theorem LemmaCard2:
card (X` \/ Y) = card [#]R implies X` \/ Y = [#]R by CARD_2:102;
registration let R be non empty 1-sorted;
let X be Subset of R;
reduce [#]R \/ X to [#]R;
reducibility by XBOOLE_1:12;
reduce [#]R /\ X to X;
reducibility by XBOOLE_1:28;
end;
begin :: Standard Rough Inclusion Function
reserve R for finite Approximation_Space;
reserve X,Y,Z,W for Subset of R;
definition let R be finite Approximation_Space;
let X,Y be Subset of R;
func kappa (X,Y) -> Element of [.0,1.] equals :KappaDef:
card (X /\ Y) / card X if X <> {}
otherwise 1;
coherence
proof
AA: card (X /\ Y) <= card X by NAT_1:43,XBOOLE_1:17;
card (X /\ Y) / card X <= 1 by AA,XREAL_1:185;
hence thesis by XXREAL_1:1;
end;
consistency;
end;
theorem
kappa ({}R,X) = 1 by KappaDef;
theorem Prop1a: :: Proposition 1 a)
kappa (X,Y) = 1 iff X c= Y
proof
per cases;
suppose
A1: X <> {};
thus kappa (X,Y) = 1 implies X c= Y
proof
assume kappa (X,Y) = 1; then
card (X /\ Y) / card X = 1 by KappaDef,A1; then
card (X /\ Y) = card X by XCMPLX_1:58; then
X /\ Y = X by CARD_2:102,XBOOLE_1:17;
hence thesis by XBOOLE_1:17;
end;
assume X c= Y; then
X /\ Y = X by XBOOLE_1:28; then
kappa (X,Y) = card X / card X by A1,KappaDef;
hence thesis by XCMPLX_1:60,A1;
end;
suppose
X = {};
hence thesis by KappaDef;
end;
end;
theorem Prop1b: :: Proposition 1 b)
Y c= Z implies kappa (X,Y) <= kappa (X,Z)
proof
assume
A0: Y c= Z;
per cases;
suppose
A1: X <> {};
card (X /\ Y) <= card (X /\ Z) by NAT_1:43,A0,XBOOLE_1:26; then
card (X /\ Y) / card X <= card (X /\ Z) / card X by XREAL_1:72; then
kappa (X,Y) <= card (X /\ Z) / card X by A1,KappaDef;
hence thesis by A1,KappaDef;
end;
suppose X = {}; then
kappa (X,Y) = 1 & kappa (X,Z) = 1 by KappaDef;
hence thesis;
end;
end;
theorem :: Proposition 1 c)
Z c= Y c= X implies kappa (X,Z) <= kappa (Y,Z)
proof
assume
AA: Z c= Y c= X;
per cases;
suppose
A1: X <> {} & Y <> {}; then
kappa (Y,Z) = card (Y /\ Z) / card Y by KappaDef; then
F1: kappa (Y,Z) = card Z / card Y by AA,XBOOLE_1:28;
Z c= X by AA; then
e2: X /\ Z = Z by XBOOLE_1:28;
kappa (X,Z) = card Z / card X by e2,A1,KappaDef;
hence thesis by A1,XREAL_1:118,F1,AA,NAT_1:43;
end;
suppose X = {} & Y <> {};
hence thesis by AA;
end;
suppose X = {} & Y = {};
hence thesis;
end;
suppose X <> {} & Y = {}; then
kappa (Y,Z) = 1 by KappaDef;
hence thesis by XXREAL_1:1;
end;
end;
theorem Prop1d: :: binary variant of Proposition 1 d)
kappa (X, Y \/ Z) <= kappa (X,Y) + kappa (X,Z)
proof
per cases;
suppose
A0: X <> {}; then
A1: kappa (X, Y \/ Z) = card (X /\ (Y \/ Z)) / card X by KappaDef;
A2: kappa (X, Y) = card (X /\ Y) / card X by A0,KappaDef;
A3: kappa (X, Z) = card (X /\ Z) / card X by A0,KappaDef;
X /\ (Y \/ Z) = (X /\ Y) \/ (X /\ Z) by XBOOLE_1:23; then
card (X /\ (Y \/ Z)) / card X <=
(card (X /\ Y) + card (X /\ Z)) / card X by XREAL_1:72,CARD_2:43;
hence thesis by A2,A3,A1,XCMPLX_1:62;
end;
suppose
A2: X = {}; then
A3: kappa (X, Y \/ Z) = 1 by KappaDef;
kappa (X, Y) = 1 & kappa (X, Z) = 1 by A2,KappaDef;
hence thesis by A3;
end;
end;
theorem Prop1e: :: binary variant of Proposition 1 e)
X <> {} & Y misses Z implies
kappa (X,Y \/ Z) = kappa (X,Y) + kappa (X,Z)
proof
assume
A0: X <> {} & Y misses Z; then
A1: kappa (X,Y \/ Z) = card (X /\ (Y \/ Z)) / card X by KappaDef
.= card ((X /\ Y) \/ (X /\ Z)) / card X by XBOOLE_1:23;
A2: kappa (X,Y) = card (X /\ Y) / card X &
kappa (X,Z) = card (X /\ Z) / card X by A0,KappaDef;
card ((X /\ Y) \/ (X /\ Z)) = card (X /\ Y) + card (X /\ Z)
by CARD_2:40,A0,XBOOLE_1:76;
hence thesis by A2,A1,XCMPLX_1:62;
end;
begin :: Rough Inclusion Functions
definition let R be 1-sorted;
mode preRoughInclusionFunction of R is
Function of [:bool the carrier of R, bool the carrier of R:],
[.0,1.];
end;
definition let R be 1-sorted;
mode preRIF of R is preRoughInclusionFunction of R;
end;
scheme BinOpEq {R() -> non empty 1-sorted,
F(Subset of R(), Subset of R()) -> Element of [.0,1.]} :
for f1, f2 being preRIF of R() st
(for x,y being Subset of R() holds f1.(x,y) = F(x,y)) &
(for x,y being Subset of R() holds f2.(x,y) = F(x,y)) holds
f1 = f2
proof
let f1, f2 be preRIF of R() such that
A1: (for x,y being Subset of R() holds f1.(x,y) = F(x,y)) and
A2: (for x,y being Subset of R() holds f2.(x,y) = F(x,y));
for x,y being Element of bool the carrier of R() holds
f2.(x,y) = f1.(x,y)
proof
let x,y be Element of bool the carrier of R();
f1.(x,y) = F(x,y) by A1
.= f2.(x,y) by A2;
hence thesis;
end;
hence thesis by BINOP_1:2;
end;
definition let R be finite Approximation_Space;
func kappa R -> preRIF of R means :DefKappa:
for x,y being Subset of R holds it.(x,y) = kappa (x,y);
existence
proof
deffunc F(Subset of R,Subset of R) = kappa ($1,$2);
ex f being preRIF of R st
for x,y being Element of bool the carrier of R holds
f.(x,y) = F(x,y) from BINOP_1:sch 4; then
consider f being
Function of [:bool the carrier of R, bool the carrier of R:],
[.0,1.] such that
A1: for x,y being Element of bool the carrier of R holds
f.(x,y) = F(x,y);
take f;
thus thesis by A1;
end;
uniqueness
proof
deffunc F(Subset of R,Subset of R) = kappa($1,$2);
for f1, f2 being preRIF of R st
(for x,y being Subset of R holds f1.(x,y) = F(x,y)) &
(for x,y being Subset of R holds f2.(x,y) = F(x,y)) holds
f1 = f2 from BinOpEq;
hence thesis;
end;
end;
begin :: Defining Two New RIFs
definition let R be finite Approximation_Space;
let X,Y be Subset of R;
func kappa_1 (X,Y) -> Element of [.0,1.] equals :Kappa1:
card Y / card (X \/ Y) if X \/ Y <> {}
otherwise 1;
coherence
proof
card Y / card (X \/ Y) in [.0,1.]
proof
card Y <= card (X \/ Y) by NAT_1:43,XBOOLE_1:7; then
card Y / card (X \/ Y) <= 1 by XREAL_1:183;
hence thesis by XXREAL_1:1;
end;
hence thesis by XXREAL_1:1;
end;
consistency;
func kappa_2 (X,Y) -> Element of [.0,1.] equals
card (X` \/ Y) / card ([#]R);
coherence
proof
card (X` \/ Y) / card ([#]R) in [.0,1.]
proof
card (X` \/ Y) / card ([#]R) <= 1 by XREAL_1:183,NAT_1:43;
hence thesis by XXREAL_1:1;
end;
hence thesis;
end;
end;
definition let R be finite Approximation_Space;
func kappa_1 R -> preRIF of R means :DefKappa1:
for x,y being Subset of R holds it.(x,y) = kappa_1 (x,y);
existence
proof
deffunc F(Subset of R,Subset of R) = kappa_1 ($1,$2);
ex f being Function of [:bool the carrier of R, bool the carrier of R:],
[.0,1.] st
for x,y being Element of bool the carrier of R holds
f.(x,y) = F(x,y) from BINOP_1:sch 4; then
consider f being
Function of [:bool the carrier of R, bool the carrier of R:],
[.0,1.] such that
A1: for x,y being Element of bool the carrier of R holds
f.(x,y) = F(x,y);
take f;
thus thesis by A1;
end;
uniqueness
proof
deffunc F(Subset of R,Subset of R) = kappa_1($1,$2);
for f1, f2 being
Function of [:bool the carrier of R, bool the carrier of R:],
[.0,1.] st
(for x,y being Subset of R holds f1.(x,y) = F(x,y)) &
(for x,y being Subset of R holds f2.(x,y) = F(x,y)) holds
f1 = f2 from BinOpEq;
hence thesis;
end;
func kappa_2 R -> preRIF of R means :DefKappa2:
for x,y being Subset of R holds it.(x,y) = kappa_2 (x,y);
existence
proof
deffunc F(Subset of R,Subset of R) = kappa_2 ($1,$2);
ex f being Function of [:bool the carrier of R, bool the carrier of R:],
[.0,1.] st
for x,y being Element of bool the carrier of R holds
f.(x,y) = F(x,y) from BINOP_1:sch 4; then
consider f being
Function of [:bool the carrier of R, bool the carrier of R:],
[.0,1.] such that
A1: for x,y being Element of bool the carrier of R holds
f.(x,y) = F(x,y);
take f;
thus thesis by A1;
end;
uniqueness
proof
deffunc F(Subset of R,Subset of R) = kappa_2($1,$2);
for f1, f2 being
Function of [:bool the carrier of R, bool the carrier of R:],
[.0,1.] st
(for x,y being Subset of R holds f1.(x,y) = F(x,y)) &
(for x,y being Subset of R holds f2.(x,y) = F(x,y)) holds
f1 = f2 from BinOpEq;
hence thesis;
end;
end;
theorem Prop11a: :: rif_1 for kappa_1
kappa_1 (X,Y) = 1 iff X c= Y
proof
per cases;
suppose
A1: X \/ Y <> {} & Y <> {}; then
B1: kappa_1 (X,Y) = card Y / card (X \/ Y) by Kappa1;
thus kappa_1 (X,Y) = 1 implies X c= Y
proof
assume kappa_1 (X,Y) = 1; then
card Y = card (X \/ Y) by XCMPLX_1:58,B1;
hence thesis by LemmaCard;
end;
assume X c= Y; then
card (X \/ Y) = card Y by XBOOLE_1:12;
hence thesis by A1,XCMPLX_1:60,B1;
end;
suppose
A1: X \/ Y <> {} & Y = {}; then
kappa_1 (X,Y) = card Y / card (X \/ Y) by Kappa1
.= 0 by A1;
hence thesis by A1;
end;
suppose
X \/ Y = {};
hence thesis by Kappa1;
end;
end;
theorem Prop11b: :: rif_1 for kappa_2
kappa_2 (X,Y) = 1 iff X c= Y
proof
thus kappa_2 (X,Y) = 1 implies X c= Y
proof
assume kappa_2 (X,Y) = 1; then
card (X` \/ Y) = card ([#]R) by XCMPLX_1:58;
hence thesis by LemmaSet,LemmaCard2;
end;
assume X c= Y; then
X` \/ Y = [#]R by LemmaSet;
hence thesis by XCMPLX_1:60;
end;
theorem LemmaProp4a:
kappa_1 (X,Y) = 0 implies Y = {}
proof
assume kappa_1 (X,Y) = 0; then
card Y / card (X \/ Y) = 0 by Kappa1;
hence thesis;
end;
theorem Prop4a: :: Proposition 4 a)
X <> {} implies (kappa_1 (X,Y) = 0 iff Y = {})
proof
assume
a3: X <> {};
thus kappa_1 (X,Y) = 0 implies Y = {} by LemmaProp4a;
assume
A2: Y = {};
kappa_1 (X,Y) = card Y / card (X \/ Y) by Kappa1,a3
.= 0 / card (X \/ Y) by A2;
hence thesis;
end;
theorem Prop4b: :: Proposition 4 b)
kappa_2(X,Y) = 0 iff X = [#]R & Y = {}
proof
thus kappa_2(X,Y) = 0 implies X = [#]R & Y = {}
proof
assume
ac: kappa_2(X,Y) = 0; then
X` = {} & Y = {}; then
X`` = ({}R)`;
hence thesis by ac;
end;
assume
A2: X = [#]R & Y = {}; then
X` = ({}R)``;
hence thesis by A2;
end;
theorem Prop2b:
Y c= Z implies kappa_1 (X,Y) <= kappa_1 (X,Z)
proof
assume
A0: Y c= Z; then
B3: card Z = card (Y \/ (Z \ Y)) by XBOOLE_1:45
.= card Y + card (Z \ Y) by XBOOLE_1:79,CARD_2:40;
ZA: card Y <= card (X \/ Y) by NAT_1:43,XBOOLE_1:7;
ZC: X \/ Z = X \/ (Y \/ (Z \ Y)) by A0,XBOOLE_1:45
.= X \/ Y \/ (Z \ Y) by XBOOLE_1:4;
per cases;
suppose
AA: X \/ Y <> {}; then
kappa_1 (X,Y) = card Y / card (X \/ Y) by Kappa1; then
ss: kappa_1 (X,Y) <= (card Y + card (Z \ Y)) /
(card (X \/ Y) + card (Z \ Y)) by AA,Lemacik,ZA;
card Z / (card (X \/ Y) + card (Z \ Y)) <=
card Z / card ((X \/ Y) \/ (Z \ Y)) by CARD_2:43,AA,XREAL_1:118; then
kappa_1 (X,Y) <= card Z / card ((X \/ Y) \/ (Z \ Y))
by ss,B3,XXREAL_0:2;
hence thesis by Kappa1,AA,ZC;
end;
suppose
X = {} & Z = {};
hence thesis by A0;
end;
suppose
T1: X \/ Y = {} & Z <> {}; then
T3: X \/ Z <> {} & X = {};
kappa_1 (X,Z) = card Z / card (X \/ Z) by Kappa1,T1
.= 1 by XCMPLX_1:60,T3;
hence thesis by T1,Kappa1;
end;
end;
theorem Prop3b:
Y c= Z implies kappa_2 (X,Y) <= kappa_2 (X,Z)
proof
assume Y c= Z; then
X` \/ Y c= X` \/ Z by XBOOLE_1:9;
hence thesis by XREAL_1:72,NAT_1:43;
end;
theorem Lemma2:
kappa_1 ({}R,X) = 1
proof
{}R c= X;
hence thesis by Prop11a;
end;
theorem Lemma3:
kappa_2 ({}R,X) = 1
proof
{}R c= X;
hence thesis by Prop11b;
end;
definition let R be non empty RelStr;
let f be preRIF of R;
attr f is satisfying_RIF1 means :RIF1Def:
for X,Y being Subset of R holds f.(X,Y) = 1 iff X c= Y;
attr f is satisfying_RIF2 means
for X,Y,Z being Subset of R st
Y c= Z holds f.(X,Y) <= f.(X,Z);
attr f is satisfying_RIF3 means
for X being Subset of R st
X <> {} holds f.(X,{}R) = 0;
attr f is satisfying_RIF4 means
for X,Y being Subset of R st
f.(X,Y) = 0 holds X misses Y;
end;
:: Towards weak quasi-RIFs, will be developed later on
definition let R be non empty RelStr;
let f be preRIF of R;
attr f is satisfying_RIF0 means
for X,Y being Subset of R st X c= Y holds f.(X,Y) = 1;
attr f is satisfying_RIF01 means
for X,Y being Subset of R st f.(X,Y) = 1 holds X c= Y;
attr f is satisfying_RIF2* means
for X,Y,Z being Subset of R st
f.(Y,Z) = 1 holds f.(X,Y) <= f.(X,Z);
end;
:: rif1 -> (rif2 iff rif2*)
:: qRifs are rif0 and rif2*
:: weak qRIFs are rif0 and rif2
registration let R be non empty RelStr;
cluster satisfying_RIF1 -> satisfying_RIF0 satisfying_RIF01
for preRIF of R;
coherence;
cluster satisfying_RIF0 satisfying_RIF01 -> satisfying_RIF1
for preRIF of R;
coherence;
end;
registration let R be finite Approximation_Space;
cluster kappa R -> satisfying_RIF1;
coherence
proof
set f = kappa R;
for X,Y being Subset of R holds f.(X,Y) = 1 iff X c= Y
proof
let X,Y be Subset of R;
thus f.(X,Y) = 1 implies X c= Y
proof
assume f.(X,Y) = 1; then
kappa(X,Y) = 1 by DefKappa;
hence thesis by Prop1a;
end;
assume X c= Y; then
kappa(X,Y) = 1 by Prop1a;
hence thesis by DefKappa;
end;
hence thesis;
end;
cluster kappa R -> satisfying_RIF2;
coherence
proof
set f = kappa R;
let X,Y,Z be Subset of R;
assume Y c= Z; then
kappa (X,Y) <= kappa (X,Z) by Prop1b; then
f.(X,Y) <= kappa (X,Z) by DefKappa;
hence thesis by DefKappa;
end;
cluster kappa_1 R -> satisfying_RIF1; :: Proposition 3
coherence
proof
set f = kappa_1 R;
for X,Y being Subset of R holds f.(X,Y) = 1 iff X c= Y
proof
let X,Y be Subset of R;
thus f.(X,Y) = 1 implies X c= Y
proof
assume f.(X,Y) = 1; then
kappa_1 (X,Y) = 1 by DefKappa1;
hence thesis by Prop11a;
end;
assume X c= Y; then
kappa_1 (X,Y) = 1 by Prop11a;
hence thesis by DefKappa1;
end;
hence thesis;
end;
cluster kappa_1 R -> satisfying_RIF2; :: Proposition 3
coherence
proof
set f = kappa_1 R;
let X,Y,Z be Subset of R;
assume Y c= Z; then
kappa_1 (X,Y) <= kappa_1 (X,Z) by Prop2b; then
f.(X,Y) <= kappa_1 (X,Z) by DefKappa1;
hence thesis by DefKappa1;
end;
cluster kappa_2 R -> satisfying_RIF1; :: Proposition 3
coherence
proof
set f = kappa_2 R;
for X,Y being Subset of R holds f.(X,Y) = 1 iff X c= Y
proof
let X,Y be Subset of R;
thus f.(X,Y) = 1 implies X c= Y
proof
assume f.(X,Y) = 1; then
kappa_2 (X,Y) = 1 by DefKappa2;
hence thesis by Prop11b;
end;
assume X c= Y; then
kappa_2 (X,Y) = 1 by Prop11b;
hence thesis by DefKappa2;
end;
hence thesis;
end;
cluster kappa_2 R -> satisfying_RIF2; :: Proposition 3
coherence
proof
set f = kappa_2 R;
let X,Y,Z be Subset of R;
assume Y c= Z; then
kappa_2 (X,Y) <= kappa_2 (X,Z) by Prop3b; then
f.(X,Y) <= kappa_2 (X,Z) by DefKappa2;
hence thesis by DefKappa2;
end;
end;
registration let R;
cluster satisfying_RIF1 satisfying_RIF2 for preRIF of R;
existence
proof
take kappa R;
thus thesis;
end;
end;
theorem RIF2Iff:
for f being satisfying_RIF1 preRIF of R holds
f is satisfying_RIF2 iff f is satisfying_RIF2*
proof
let f be satisfying_RIF1 preRIF of R;
thus f is satisfying_RIF2 implies f is satisfying_RIF2*
proof
assume
A1: f is satisfying_RIF2;
let X,Y,Z be Subset of R;
assume f.(Y,Z) = 1; then
Y c= Z by RIF1Def;
hence thesis by A1;
end;
assume
A2: f is satisfying_RIF2*;
let X,Y,Z be Subset of R;
assume Y c= Z; then
f.(Y,Z) = 1 by RIF1Def;
hence thesis by A2;
end;
registration let R;
cluster satisfying_RIF2 -> satisfying_RIF2* for
satisfying_RIF1 preRIF of R;
coherence by RIF2Iff;
cluster satisfying_RIF2* -> satisfying_RIF2 for
satisfying_RIF1 preRIF of R;
coherence by RIF2Iff;
end;
registration let R;
cluster kappa R -> satisfying_RIF0 satisfying_RIF2*;
coherence;
end;
registration let R;
cluster satisfying_RIF0 satisfying_RIF1 satisfying_RIF2 satisfying_RIF2* for
preRoughInclusionFunction of R;
existence
proof
take kappa R;
thus thesis;
end;
end;
definition let R;
mode RoughInclusionFunction of R is
satisfying_RIF1 satisfying_RIF2 preRoughInclusionFunction of R;
end;
definition let R;
mode quasi-RoughInclusionFunction of R is
satisfying_RIF0 satisfying_RIF2* preRIF of R;
mode weak_quasi-RoughInclusionFunction of R is
satisfying_RIF0 satisfying_RIF2 preRIF of R;
end;
definition let R;
mode RIF of R is RoughInclusionFunction of R;
mode qRIF of R is quasi-RoughInclusionFunction of R;
mode wqRIF of R is weak_quasi-RoughInclusionFunction of R;
end;
begin :: Proposition 2
:: The following three should be obvious (Proposition 3)
:: kappa R is RIF of R;
:: kappa_1 R is RIF of R;
:: kappa_2 R is RIF of R;
theorem :: Proposition 2 a), binary case
X <> {} & Z \/ W = [#]R & Z misses W implies
kappa (X,Z) + kappa (X,W) = 1
proof
assume
A1: X <> {} & Z \/ W = [#]R & Z misses W;
A3: kappa (X,W) = card (X /\ W) / card X by A1,KappaDef;
A6: X = X /\ (Z \/ W) by A1
.= X /\ Z \/ X /\ W by XBOOLE_1:23;
A4: card (X /\ Z) + card (X /\ W) = card X by A6,A1,CARD_2:40,XBOOLE_1:76;
kappa (X,Z) + kappa (X,W) =
card (X /\ Z) / card X + card (X /\ W) / card X by A1,A3,KappaDef
.= card X / card X by A4,XCMPLX_1:62;
hence thesis by XCMPLX_1:60,A1;
end;
theorem LemmaProp2b: :: Proposition 2 b) from left to right, without X <> {}
kappa (X,Y) = 0 implies X misses Y
proof
assume
A1: kappa (X,Y) = 0;
per cases;
suppose
A2: X <> {}; then
kappa (X,Y) = card (X /\ Y) / card X by KappaDef;
hence thesis by A1,A2;
end;
suppose X = {};
hence thesis;
end;
end;
theorem Prop2b: ::: Proposition 2 b)
X <> {} implies (kappa (X,Y) = 0 iff X misses Y)
proof
assume
AA: X <> {};
thus kappa (X,Y) = 0 implies X misses Y by LemmaProp2b;
assume X misses Y; then
card (X /\ Y) / card X = 0;
hence thesis by AA,KappaDef;
end;
theorem Prop2c: :: Proposition 2 c)
X <> {} implies kappa (X,{}R) = 0
proof
assume X <> {}; then
kappa (X,{}R) = card (X /\ {}R) / card X by KappaDef;
hence thesis;
end;
theorem :: Proposition 2 d)
X <> {} & X misses Y implies
kappa (X, Z \ Y) = kappa (X, Z \/ Y) = kappa (X,Z)
proof
assume
A1: X <> {} & X misses Y; then
D1: kappa (X,Y) = 0 by Prop2b;
D3: kappa (X,Z) = kappa (X, (Z /\ Y) \/ (Z \ Y)) by XBOOLE_1:51
.= kappa (X, Z /\ Y) + kappa (X, Z \ Y)
by Prop1e,A1,XBOOLE_1:89;
kappa (X,Z /\ Y) <= 0 by D1,Prop1b,XBOOLE_1:17; then
D5: kappa (X,Z /\ Y) = 0 by XXREAL_1:1;
e1: kappa (X, Z \/ Y) <= kappa (X,Z) + kappa (X,Y) by Prop1d;
kappa (X,Z) <= kappa (X, Z \/ Y) by Prop1b,XBOOLE_1:7;
hence thesis by D5,D3,e1,D1,XXREAL_0:1;
end;
Test1:
Z misses W implies kappa (Y \/ Z, W) <= kappa (Y, W)
proof
assume
A0: Z misses W;
per cases;
suppose
S3: Y /\ W <> {};
A1: Y <> {} by S3;
A3: (Y \/ Z) /\ W = Y /\ W by XBOOLE_1:78,A0;
card Y <= card (Y \/ Z) by NAT_1:43,XBOOLE_1:7; then
card (Y /\ W) / card (Y \/ Z) <= card (Y /\ W) / card Y
by A1,XREAL_1:118; then
card ((Y \/ Z) /\ W) / card (Y \/ Z) <= kappa (Y, W) by A1,KappaDef,A3;
hence kappa (Y \/ Z, W) <= kappa (Y, W) by A1,KappaDef;
end;
suppose
Z0: Y /\ W = {} & Y \/ Z <> {} & Y <> {}; then
Z1: Y misses W; then
Y \/ Z misses W by A0,XBOOLE_1:70; then
kappa (Y \/ Z, W) = 0 by Z0,Prop2b;
hence thesis by Z1,Z0,Prop2b;
end;
suppose
Z0: Y /\ W = {} & Y \/ Z <> {} & Y = {}; then
kappa (Y \/ Z, W) = 0 by A0,Prop2b;
hence thesis by Z0,KappaDef;
end;
suppose
Y /\ W = {} & Y \/ Z = {}; then
Y = {} & Z = {};
hence thesis;
end;
end;
Test2: :: Proposition 2 e)
Z misses W implies kappa (Y, W) <= kappa (Y \ Z,W)
proof
assume
A0: Z misses W;
per cases;
suppose
S3: Y /\ W <> {};
A1: Y <> {} by S3;
per cases;
suppose
Y c= Z; then
kappa (Y \ Z,W) = 1 by KappaDef,XBOOLE_1:37;
hence thesis by XXREAL_1:1;
end;
suppose
b1: not Y c= Z; then
B1: Y \ Z <> {} by XBOOLE_1:37;
B2: (Y \ Z) /\ W = (Y /\ W) \ (Z /\ W) by XBOOLE_1:111
.= Y /\ W by A0;
card (Y \ Z) <= card Y by NAT_1:43,XBOOLE_1:36; then
card (Y /\ W) / card Y <= card (Y /\ W) / card (Y \ Z)
by XREAL_1:118,B1; then
kappa (Y,W) <= card ((Y \ Z) /\ W) / card (Y \ Z) by A1,KappaDef,B2;
hence kappa (Y,W) <= kappa (Y \ Z,W) by KappaDef,b1,XBOOLE_1:37;
end;
end;
suppose
Z0: Y /\ W = {} & Y \/ Z <> {} & Y <> {}; then
Y misses W; then
kappa (Y, W) = 0 by Z0,Prop2b;
hence thesis by XXREAL_1:1;
end;
suppose
Y /\ W = {} & Y \/ Z <> {} & Y = {};
hence thesis;
end;
suppose
Y /\ W = {} & Y \/ Z = {}; then
Y = {} & Z = {};
hence thesis;
end;
end;
theorem :: Proposition 2 e)
Z misses W implies
kappa (Y \/ Z, W) <= kappa (Y, W) <= kappa (Y \ Z,W) by Test1,Test2;
Test1AAA:
Y misses Z & Z c= W implies kappa (Y \/ Z, W) >= kappa (Y, W)
proof
assume
A0: Y misses Z & Z c= W;
per cases;
suppose
AA: Y <> {};
Y /\ W c= Y by XBOOLE_1:17; then
T2: card (Y /\ W) / card Y <= (card (Y /\ W) + card Z) / (card Y + card Z)
by Lemacik,AA,NAT_1:43;
T4: card Y + card Z = card (Y \/ Z) by A0,CARD_2:40;
Z misses Y /\ W by A0,XBOOLE_1:63,17; then
T3: card (Y /\ W) + card Z = card ((Y /\ W) \/ Z) by CARD_2:40;
T1: (Y \/ Z) /\ W = (Y /\ W) \/ (Z /\ W) by XBOOLE_1:23
.= (Y /\ W) \/ Z by A0,XBOOLE_1:28;
kappa (Y,W) <= card ((Y /\ W) \/ Z) / card (Y \/ Z)
by T4,KappaDef,AA,T2,T3;
hence thesis by KappaDef,AA,T1;
end;
suppose
Y = {}; then
kappa (Y \/ Z, W) = 1 by Prop1a,A0;
hence thesis by XXREAL_1:1;
end;
end;
Test2AAA:
Y misses Z & Z c= W implies kappa (Y, W) >= kappa (Y \ Z, W)
proof
assume
A0: Y misses Z & Z c= W;
per cases;
suppose
Y <> {};
thus thesis by A0,XBOOLE_1:83;
end;
suppose
Y = {};
hence thesis;
end;
end;
theorem :: Proposition 2 f)
Z misses Y & Z c= W implies
kappa (Y \ Z, W) <= kappa (Y, W) <= kappa (Y \/ Z,W) by Test1AAA,Test2AAA;
begin :: Proposition 4
registration let R;
let X be non empty Subset of R;
cluster kappa (X,{}R) -> empty;
coherence by Prop2c;
end;
theorem Kappa1RIF4:
kappa_1 (X,Y) = 0 implies X misses Y
proof
assume
A1: kappa_1 (X,Y) = 0;
per cases;
suppose X <> {}; then
Y = {} by A1,Prop4a;
hence thesis;
end;
suppose X = {};
hence thesis;
end;
end;
theorem Kappa2RIF4:
kappa_2 (X,Y) = 0 implies X misses Y
proof
assume kappa_2 (X,Y) = 0; then
X = [#]R & Y = {} by Prop4b;
hence thesis;
end;
registration let R; :: Proposition 4 c)
cluster kappa R -> satisfying_RIF4;
coherence
proof
let X,Y be Subset of R;
assume (kappa R).(X,Y) = 0; then
kappa (X,Y) = 0 by DefKappa;
hence thesis by LemmaProp2b;
end;
cluster kappa_1 R -> satisfying_RIF4;
coherence
proof
let X,Y be Subset of R;
assume (kappa_1 R).(X,Y) = 0; then
kappa_1 (X,Y) = 0 by DefKappa1;
hence thesis by Kappa1RIF4;
end;
cluster kappa_2 R -> satisfying_RIF4;
coherence
proof
let X,Y be Subset of R;
assume (kappa_2 R).(X,Y) = 0; then
kappa_2 (X,Y) = 0 by DefKappa2;
hence thesis by Kappa2RIF4;
end;
end;
theorem :: Proposition 4 d)
kappa(X,Y) <= kappa_1(X,Y) <= kappa_2(X,Y)
proof
per cases;
suppose
A0: X <> {}; then
WA: kappa_1(X,Y) = card Y / card (X \/ Y) by Kappa1;
U1: card (X /\ Y) <= card X by NAT_1:43,XBOOLE_1:17;
J0: card Y <= card (X \/ Y) by NAT_1:43,XBOOLE_1:7;
X \/ Y = X \/ (Y \ X) by XBOOLE_1:39; then
D3: card (X \/ Y) = card X + card (Y \ X) by CARD_2:40,XBOOLE_1:85;
d4: Y = (X /\ Y) \/ (Y \ X) by XBOOLE_1:51;
(X /\ Y) misses (Y \ X) by XBOOLE_1:85,17; then
D4: card Y = card (X /\ Y) + card (Y \ X) by d4,CARD_2:40;
(X \/ Y)` = X` /\ Y` by XBOOLE_1:53; then
(X \/ Y)` \/ Y = (X` \/ Y) /\ (Y` \/ Y) by XBOOLE_1:24
.= (X` \/ Y) /\ [#]R by PRE_TOPC:2
.= (X` \ Y) \/ Y by XBOOLE_1:39; then
d5: X` \/ Y = (X` \ Y) \/ Y = (X \/ Y)` \/ Y by XBOOLE_1:39;
(X \/ Y)` c= Y` by SUBSET_1:12,XBOOLE_1:7; then
(X \/ Y)` misses Y by XBOOLE_1:63,79; then
D5: card (X` \/ Y) = card ((X \/ Y)`) + card Y by d5,CARD_2:40;
card (X /\ Y) / card X <= (card (X /\ Y) + card (Y \ X)) /
(card X + card (Y \ X)) by Lemacik,A0,U1; then
kappa (X,Y) <= (card (X /\ Y) + card (Y \ X)) /
card (X \/ Y) by A0,KappaDef,D3;
hence kappa(X,Y) <= kappa_1(X,Y) by A0,Kappa1,D4;
(X \/ Y)` \/ (X \/ Y) = [#]R by PRE_TOPC:2; then
card ((X \/ Y)`) + card (X \/ Y) = card [#]R by TDLAT_1:2,CARD_2:40;
hence thesis by D5,A0,J0,Lemacik,WA;
end;
suppose
X = {}; then
b3: X = {}R; then
kappa_1(X,Y) = 1 by Lemma2;
hence thesis by b3,Lemma3,KappaDef;
end;
end;
theorem :: Proposition 4 e)
kappa_1 (X,Y) = kappa (X \/ Y,Y)
proof
per cases;
suppose
A1: X \/ Y <> {}; then
kappa (X \/ Y,Y) = card ((X \/ Y) /\ Y) / card (X \/ Y) by KappaDef
.= card Y / card (X \/ Y) by XBOOLE_1:21;
hence thesis by A1,Kappa1;
end;
suppose
A1: X = {}; then
AA: X c= Y;
kappa (X \/ Y, Y) = 1 by Prop1a,A1;
hence thesis by Prop11a,AA;
end;
end;
LemmaKap1:
kappa(X,Y) = kappa(X,X /\ Y)
proof
per cases;
suppose
S0: X <> {}; then
kappa (X,X /\ Y) = card (X /\ (X /\ Y)) / card X by KappaDef
.= card (X /\ X /\ Y) / card X by XBOOLE_1:16;
hence thesis by S0,KappaDef;
end;
suppose
S1: X = {}; then
kappa (X,Y) = 1 by KappaDef;
hence thesis by S1,KappaDef;
end;
end;
LemmaKap2:
kappa_1(X,X /\ Y) = kappa_1(X \ Y,X /\ Y)
proof
per cases;
suppose
S0: X \/ (X /\ Y) <> {}; then
S2: X <> {};
S3: kappa_1 (X,X /\ Y) = card (X /\ Y) / card (X \/ (X /\ Y))
by Kappa1,S0
.= card (X /\ Y) / card X by XBOOLE_1:22;
(X \ Y) \/ (X /\ Y) = X by XBOOLE_1:51;
hence thesis by S3,S2,Kappa1;
end;
suppose
S0: X \/ (X /\ Y) = {}; then
S4: kappa_1(X,X /\ Y) = 1 by Kappa1;
(X \ Y) \/ (X /\ Y) = X by XBOOLE_1:51
.= X \/ (X /\ Y) by XBOOLE_1:22;
hence thesis by S4,S0,Kappa1;
end;
end;
LemmaKap3:
kappa(X,X /\ Y) = kappa_1(X,X /\ Y)
proof
per cases;
suppose
S0: X \/ (X /\ Y) <> {}; then
S3: kappa_1 (X,X /\ Y) = card (X /\ Y) / card (X \/ (X /\ Y))
by Kappa1
.= card (X /\ Y) / card X by XBOOLE_1:22;
X <> {} by S0; then
kappa(X,X /\ Y) = card (X /\ (X /\ Y)) / card X by KappaDef
.= card (X /\ X /\ Y) / card X by XBOOLE_1:16;
hence thesis by S3;
end;
suppose
S0: X \/ (X /\ Y) = {}; then
S3: kappa_1 (X,X /\ Y) = 1 by Kappa1;
X = {} by S0;
hence thesis by S3,KappaDef;
end;
end;
Lemma4f1:
kappa_2 (X,Y) = kappa ([#]R, X` \/ Y)
proof
kappa ([#]R, X` \/ Y) = card ([#]R /\ (X` \/ Y)) / card [#]R
by KappaDef
.= card (X` \/ Y) / card ([#]R);
hence thesis;
end;
Lemma4f2:
kappa ([#]R, X` \/ Y) = kappa ([#]R,X`) + kappa ([#]R, X /\ Y)
proof
a0: X` misses X by XBOOLE_1:85;
X` \/ Y = [#]R /\ (X` \/ Y)
.= (X` \/ X) /\ (X` \/ Y) by PRE_TOPC:2
.= X` \/ (X /\ Y) by XBOOLE_1:24; then
A1: card (X` \/ Y) = card (X`) + card (X /\ Y) by a0,CARD_2:40,XBOOLE_1:74;
kappa ([#]R, X` \/ Y) = card ([#]R /\ (X` \/ Y)) / card [#]R by KappaDef
.= (card ([#]R /\ X`) / card [#]R) + card (X /\ Y) / card [#]R
by XCMPLX_1:62,A1
.= kappa ([#]R,X`) + card (X /\ Y /\ [#]R) / card [#]R by KappaDef
.= kappa ([#]R,X`) + kappa ([#]R, X /\ Y) by KappaDef;
hence thesis;
end;
theorem :: Proposition 4 f)
kappa_2 (X,Y) = kappa ([#]R, X` \/ Y) =
kappa ([#]R,X`) + kappa ([#]R, X /\ Y) by Lemma4f1,Lemma4f2;
theorem :: Proposition 4 g)
kappa(X,Y) = kappa(X,X /\ Y) = kappa_1(X,X /\ Y) = kappa_1(X \ Y,X /\ Y)
by LemmaKap1,LemmaKap2,LemmaKap3;
theorem :: Proposition 4 h)
X \/ Y = [#]R implies kappa_1(X,Y) = kappa_2(X,Y)
proof
assume
AB: X \/ Y = [#]R;
X`` \/ Y = [#]R by AB; then
F1: card Y = card (X` \/ Y) by XBOOLE_1:12,LemmaSet;
per cases;
suppose
X \/ Y <> {};
thus thesis by F1,AB,Kappa1;
end;
suppose X \/ Y = {};
hence thesis by AB;
end;
end;
theorem :: false for X = {}!
X <> {} implies 1 - kappa (X,Y) = kappa (X,Y`)
proof
assume
A1: X <> {};
a2: Y \/ ([#]R \ Y) = [#]R by XBOOLE_1:45;
kappa (X,Y \/ Y`) = kappa (X,Y) + kappa (X,Y`)
by A1,Prop1e,SUBSET_1:23; then
kappa (X,Y) + kappa (X,Y`) = 1 by a2,Prop1a;
hence thesis;
end;
begin :: An Example of Aproximation Space where all three kappa mappings
:: are distinct -- Example 1 and 2 translated
:: calculations in Mizar seem to be too complex, my propositions are a bit
:: shorter than in the original
definition let X be set;
func DiscreteApproxSpace X -> strict RelStr equals
RelStr (# X, id X #);
coherence;
end;
registration let X be set;
cluster DiscreteApproxSpace X -> with_equivalence;
coherence;
end;
registration let X be non empty set;
cluster DiscreteApproxSpace X -> non empty;
coherence;
end;
registration let X be finite set;
cluster DiscreteApproxSpace X -> finite;
coherence;
end;
definition
func ExampleRIFSpace -> strict finite Approximation_Space equals
DiscreteApproxSpace {1,2,3,4,5};
correctness;
end;
theorem :: Example 1, kappa is not symmetric
for X,Y being Subset of ExampleRIFSpace
st X = {1,2} & Y = {2,3,4} holds
kappa (X,Y) <> kappa (Y,X)
proof
let X,Y be Subset of ExampleRIFSpace;
assume
A1: X = {1,2} & Y = {2,3,4}; then
A3: card Y = 3 by CARD_2:58;
Z1: kappa (Y,X) = card (Y /\ X) / card Y by KappaDef,A1;
set U = the carrier of ExampleRIFSpace;
2 in Y & not 1 in Y by A1,ENUMSET1:def 1; then
X /\ Y = {2} by ZFMISC_1:54,A1; then
A4: card (X /\ Y) = 1 by CARD_1:30;
kappa (X,Y) = card (X /\ Y) / card X by KappaDef,A1
.= 1 / 2 by A4,A1,CARD_2:57;
hence thesis by A3,Z1,A4;
end;
theorem :: Example 1, kappa is not monotone wrt 1st coordinate
for X,Y,U being Subset of ExampleRIFSpace
st X = {1,2} & Y = {1,2,3} & U = {2,4,5} holds
not kappa (X,U) <= kappa (Y,U)
proof
let X,Y,U be Subset of ExampleRIFSpace;
assume
A1: X = {1,2} & Y = {1,2,3} & U = {2,4,5}; then
A3: card Y = 3 by CARD_2:58;
2 in U & not 1 in U by A1,ENUMSET1:def 1; then
X /\ U = {2} by A1,ZFMISC_1:54; then
R1: card (X /\ U) = 1 by CARD_1:30;
R2: card X = 2 by CARD_2:57,A1;
R0: U = {2} \/ {4,5} by A1,ENUMSET1:2;
ro: 2 in Y by A1,ENUMSET1:def 1;
w1: not 4 in Y by A1,ENUMSET1:def 1;
not 5 in Y by A1,ENUMSET1:def 1; then
rr: Y misses {4,5} by ZFMISC_1:51,w1;
Y /\ U = Y /\ {2} \/ (Y /\ {4,5}) by R0,XBOOLE_1:23
.= Y /\ {2} by rr; then
Y /\ U = {2} by XBOOLE_1:28,ro,ZFMISC_1:31; then
R3: card (Y /\ U) = 1 by CARD_1:30;
W4: kappa (X,U) = 1 / 2 by R1,R2,A1,KappaDef;
kappa (Y,U) = 1 / 3 by A3,R3,A1,KappaDef;
hence thesis by W4;
end;
theorem :: Example 2, simplified: all three RIFs are different
for X,Y being Subset of ExampleRIFSpace
st X = {1,2} & Y = {2,3,4} holds
kappa (X,Y), kappa_1 (X,Y), kappa_2 (X,Y) are_mutually_distinct
proof
let X,Y be Subset of ExampleRIFSpace;
assume
A1: X = {1,2} & Y = {2,3,4}; then
A3: card Y = 3 by CARD_2:58;
set U = the carrier of ExampleRIFSpace;
1,2,3,4,5 are_mutually_distinct by ZFMISC_1:def 7; then
a1: card U = 5 by CARD_2:63;
2 in Y & not 1 in Y by A1,ENUMSET1:def 1; then
X /\ Y = {2} by ZFMISC_1:54,A1; then
A4: card (X /\ Y) = 1 by CARD_1:30;
a5: X \/ Y = {1,2} \/ ({2} \/ {3,4}) by A1,ENUMSET1:2
.= {1,2} \/ {2} \/ {3,4} by XBOOLE_1:4
.= {1,2} \/ {3,4} by ZFMISC_1:9
.= {1,2,3,4} by ENUMSET1:5;
not 1 in {3,4,5} & not 2 in {3,4,5} by ENUMSET1:def 1; then
W2: {1,2} misses {3,4,5} by ZFMISC_1:51;
WW: 3 in {3,4,5} & 4 in {3,4,5} by ENUMSET1:def 1;
X` = {1,2} \/ {3,4,5} \ {1,2} by A1,ENUMSET1:8
.= {3,4,5} by XBOOLE_1:88,W2; then
X` \/ Y = {3,4,5} \/ ({2} \/ {3,4}) by A1,ENUMSET1:2
.= {2} \/ ({3,4} \/ {3,4,5}) by XBOOLE_1:4
.= {2} \/ {3,4,5} by ZFMISC_1:42,WW; then
X` \/ Y = {2,3,4,5} by ENUMSET1:4; then
W3: card (X` \/ Y) / card U = 4 / 5 by a1,CARD_2:59;
W4: kappa (X,Y) = card (X /\ Y) / card X by KappaDef,A1
.= 1 / 2 by A4,A1,CARD_2:57;
kappa_1 (X,Y) = card Y / card (X \/ Y) by Kappa1,A1
.= 3 / 4 by A3,a5,CARD_2:59;
hence thesis by ZFMISC_1:def 5,W4,W3;
end;
begin :: Continuing Formalization of Theorem 4.1 from Anna Gomolinska's
:: A Comparative Study of Some Generalized Rough Approximations"
:: Fundamenta Informaticae, 51(2002), pp. 103-119
theorem ::: Theorem 4.1 c) from Gomolinska's "A Comparative Study..."
for R being finite Approximation_Space,
u being Element of R,
x,y being Subset of R st
u in (f_1 R).x & (UncertaintyMap R).u = y
holds kappa (y, x) > 0
proof
let R be finite Approximation_Space,
u be Element of R,
x,y be Subset of R;
assume
AA: u in (f_1 R).x & (UncertaintyMap R).u = y;
(f_1 R).x = { u where u is Element of R :
(UncertaintyMap R).u meets x } by ROUGHS_5:def 5; then
consider uu being Element of R such that
AB: uu = u & (UncertaintyMap R).uu meets x by AA;
kappa (y,x) <> 0 by AB,AA,LemmaProp2b;
hence thesis by XXREAL_1:1;
end;
theorem ::: Theorem 4.1 d) from Gomolinska's "A Comparative Study..."
for R being finite Approximation_Space,
u being Element of R,
x,y being Subset of R st
u in (Flip f_1 R).x & (UncertaintyMap R).u = y
holds kappa (y, x) = 1
proof
let R be finite Approximation_Space,
u be Element of R,
x,y be Subset of R;
assume
A0: u in (Flip f_1 R).x & (UncertaintyMap R).u = y;
(Flip f_1 R).x = { w where w is Element of R :
(UncertaintyMap R).w c= x } by ROUGHS_5:30; then
consider v being Element of R such that
A3: u = v & (UncertaintyMap R).v c= x by A0;
thus thesis by Prop1a,A0,A3;
end;