:: Relational Formal Characterization of Rough Sets
:: by Adam Grabowski
::
:: Received January 17, 2013
:: Copyright (c) 2013-2016 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, PRE_TOPC, RELAT_2,
XBOOLE_0, PARTFUN1, SUBSET_1, TOPS_1, FUNCT_1, FINSET_1, EQREL_1,
XXREAL_0, ROUGHS_1, RCOMP_1, ROUGHS_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, RELAT_1, RELAT_2,
FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1, STRUCT_0, ORDERS_2,
EQREL_1, PRE_TOPC, TOPS_1, ROUGHS_1, YELLOW_3;
constructors EQREL_1, REALSET2, RELSET_1, ROUGHS_1, YELLOW_3, TOPS_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FINSET_1, NAT_1, STRUCT_0,
ORDERS_2, RELSET_1, FUNCT_1, FUNCT_2, YELLOW_3, TOPS_1, PRE_TOPC;
requirements BOOLE, SUBSET, NUMERALS;
begin :: Preliminaries
registration
cluster non empty void for RelStr;
end;
theorem :: ROUGHS_2:1
for R being total non empty RelStr,
x being Element of R holds
x in field the InternalRel of R;
theorem :: ROUGHS_2:2
for R being non empty 1-sorted,
X being Subset of R holds
{ x where x is Element of R : {} c= X } = [#]R;
theorem :: ROUGHS_2:3
for R being 1-sorted,
X being Subset of R holds
{ x where x is Element of R : {} meets X } = {}R;
begin :: Missing Ordinary Properties of Binary Relations
definition let R be Relation, X be set;
pred R is_serial_in X means
:: ROUGHS_2:def 1
for x being object st x in X holds
ex y being object st y in X & [x,y] in R;
end;
definition let R be Relation;
attr R is serial means
:: ROUGHS_2:def 2
R is_serial_in field R;
end;
definition let R be RelStr;
attr R is serial means
:: ROUGHS_2:def 3
the InternalRel of R is_serial_in the carrier of R;
end;
registration
cluster reflexive -> serial for RelStr;
end;
definition let R be non empty RelStr;
redefine attr R is serial means
:: ROUGHS_2:def 4
for x being Element of R ex y being Element of R st x <= y;
end;
registration
cluster total -> serial for RelStr;
cluster serial -> total for RelStr;
end;
registration let R be non empty serial RelStr,
x be Element of R;
cluster Class (the InternalRel of R,x) -> non empty;
end;
:: Reflexive relations
theorem :: ROUGHS_2:4
for R being non empty reflexive RelStr,
x being Element of R holds
x in Class (the InternalRel of R,x);
registration let R be non empty reflexive RelStr,
x be Element of R;
cluster Class (the InternalRel of R,x) -> non empty;
end;
:: Mediate relations
definition let R be Relation, X be set;
pred R is_mediate_in X means
:: ROUGHS_2:def 5
for x,y being object st x in X & y in X holds
[x,y] in R implies
ex z being object st z in X & [x,z] in R & [z,y] in R;
end;
definition let R be Relation;
attr R is mediate means
:: ROUGHS_2:def 6
R is_mediate_in field R;
end;
definition let R be RelStr;
attr R is mediate means
:: ROUGHS_2:def 7
the InternalRel of R is_mediate_in the carrier of R;
end;
registration
cluster reflexive -> mediate for RelStr;
end;
begin :: Approximations Revisited
theorem :: ROUGHS_2:5
for R being non empty RelStr,
a, b being Element of R st
a in UAp ({b}) holds [a,b] in the InternalRel of R;
definition let R be non empty RelStr;
let X be Subset of R;
func Uap X -> Subset of R equals
:: ROUGHS_2:def 8
(LAp X`)`;
end;
definition let R be non empty RelStr;
let X be Subset of R;
func Lap X -> Subset of R equals
:: ROUGHS_2:def 9
(UAp X`)`;
end;
theorem :: ROUGHS_2:6
for R being non empty RelStr,
X being Subset of R
for x being object st x in LAp X holds
Class (the InternalRel of R, x) c= X;
theorem :: ROUGHS_2:7
for R being non empty RelStr,
X being Subset of R
for x being set st x in UAp X holds
Class (the InternalRel of R, x) meets X;
theorem :: ROUGHS_2:8
for R being non empty RelStr,
X being Subset of R holds
Uap X = UAp X;
theorem :: ROUGHS_2:9
for R being non empty RelStr,
X being Subset of R holds
Lap X = LAp X;
theorem :: ROUGHS_2:10 :: Example 2
for R being non empty void RelStr,
X being Subset of R holds
LAp X = [#]R;
theorem :: ROUGHS_2:11 :: Example 2
for R being non empty void RelStr,
X being Subset of R holds
UAp X = {}R;
begin :: General Properties of Approximations
registration
let R be non empty RelStr;
reduce LAp ([#]R) to [#]R;
end;
registration
let R be non empty serial RelStr;
reduce UAp ([#]R) to [#]R;
end;
registration
let R be non empty serial RelStr;
reduce LAp {}R to {}R;
end;
registration
let R be non empty RelStr;
reduce UAp ({}R) to {}R;
end;
theorem :: ROUGHS_2:12 :: Proposition 2 4L
for R being non empty RelStr,
X, Y being Subset of R holds
LAp (X /\ Y) = LAp (X) /\ LAp (Y);
theorem :: ROUGHS_2:13 :: Proposition 2 4H
for R being non empty RelStr,
X, Y being Subset of R holds
UAp (X \/ Y) = UAp X \/ UAp Y;
theorem :: ROUGHS_2:14 :: Proposition 2 6L
for R being non empty RelStr,
X, Y being Subset of R st
X c= Y holds LAp X c= LAp Y;
theorem :: ROUGHS_2:15 :: Proposition 2 6H
for R being non empty RelStr,
X, Y being Subset of R st
X c= Y holds UAp X c= UAp Y;
theorem :: ROUGHS_2:16 :: Proposition 2 8LH
for R being non empty RelStr,
X being Subset of R holds
LAp (X`) = (UAp X)`;
theorem :: ROUGHS_2:17 :: Proposition 2 9LH
for R being non empty serial RelStr,
X being Subset of R holds
LAp X c= UAp X;
begin :: Auxiliary Operation on Approximation Operators
definition let R be non empty RelStr;
func LAp R -> Function of bool the carrier of R, bool the carrier of R
means
:: ROUGHS_2:def 10
for X being Subset of R holds it.X = LAp X;
func UAp R -> Function of bool the carrier of R, bool the carrier of R
means
:: ROUGHS_2:def 11
for X being Subset of R holds it.X = UAp X;
end;
definition
let f be Function;
attr f is empty-preserving means
:: ROUGHS_2:def 12
f.{} = {};
end;
definition
let A be set;
let f be Function of bool A, bool A;
attr f is universe-preserving means
:: ROUGHS_2:def 13
f.A = A;
end;
registration let A be non empty set;
cluster id bool A -> empty-preserving universe-preserving
for Function of bool A, bool A;
end;
registration let A be non empty set;
cluster empty-preserving universe-preserving for
Function of bool A, bool A;
end;
definition let X be set;
let f be Function of bool X, bool X;
func Flip f -> Function of bool X, bool X means
:: ROUGHS_2:def 14
for x being Subset of X holds
it.x = (f.x`)`;
end;
theorem :: ROUGHS_2:18
for X being set,
f being Function of bool X, bool X st
f.{} = {} holds
(Flip f).X = X;
theorem :: ROUGHS_2:19
for X being set,
f being Function of bool X, bool X st
f.X = X holds
(Flip f).{} = {};
theorem :: ROUGHS_2:20
for X being set,
f being Function of bool X, bool X st
f = id bool X holds
Flip f = f;
theorem :: ROUGHS_2:21
for X being set,
f being Function of bool X, bool X st
for A, B being Subset of X holds f.(A \/ B) = f.A \/ f.B holds
for A, B being Subset of X holds
(Flip f).(A /\ B) = (Flip f).A /\ (Flip f).B;
theorem :: ROUGHS_2:22
for X being set,
f being Function of bool X, bool X st
for A, B being Subset of X holds f.(A /\ B) = f.A /\ f.B holds
for A, B being Subset of X holds
(Flip f).(A \/ B) = (Flip f).A \/ (Flip f).B;
theorem :: ROUGHS_2:23
for X being set,
f being Function of bool X, bool X holds
Flip Flip f = f;
registration let A be non empty set;
let f be universe-preserving Function of bool A, bool A;
cluster Flip f -> empty-preserving;
end;
registration let A be non empty set;
let f be empty-preserving Function of bool A, bool A;
cluster Flip f -> universe-preserving;
end;
theorem :: ROUGHS_2:24
for A being non empty set,
L, U being Function of bool A, bool A st
U = Flip L &
for X being Subset of A holds L.(L.X) c= L.X holds
for X being Subset of A holds U.X c= U.(U.X);
begin :: Towards Topological Models of Rough Sets
definition let T be TopSpace;
func ClMap T -> Function of bool the carrier of T, bool the carrier of T
means
:: ROUGHS_2:def 15
for X being Subset of T holds it.X = Cl X;
func IntMap T -> Function of bool the carrier of T, bool the carrier of T
means
:: ROUGHS_2:def 16
for X being Subset of T holds
it.X = Int X;
end;
definition let T be TopSpace;
let f be Function of bool the carrier of T, bool the carrier of T;
attr f is closed-valued means
:: ROUGHS_2:def 17
for X being Subset of T holds f.X is closed;
attr f is open-valued means
:: ROUGHS_2:def 18
for X being Subset of T holds f.X is open;
end;
registration let T be TopSpace;
cluster ClMap T -> closed-valued;
cluster IntMap T -> open-valued;
end;
registration let T be TopSpace;
cluster closed-valued
for Function of bool the carrier of T, bool the carrier of T;
cluster open-valued
for Function of bool the carrier of T, bool the carrier of T;
end;
theorem :: ROUGHS_2:25
for T being TopSpace holds
Flip ClMap T = IntMap T;
theorem :: ROUGHS_2:26
for T being TopSpace holds
Flip IntMap T = ClMap T;
registration let T be non empty TopSpace;
cluster ClMap T -> empty-preserving universe-preserving;
cluster IntMap T -> empty-preserving universe-preserving;
end;
begin :: Formalization of Zhu's Paper
:: General Finite Relations
theorem :: ROUGHS_2:27
for R being non empty RelStr holds
Flip UAp R = LAp R;
theorem :: ROUGHS_2:28
for R being non empty RelStr holds
Flip LAp R = UAp R;
theorem :: ROUGHS_2:29 :: Proposition 1 2H 4H
for A being non empty finite set,
U being Function of bool A, bool A st
U.{} = {} &
(for X, Y being Subset of A holds U.(X \/ Y) = U.X \/ U.Y) holds
ex R being non empty finite RelStr st
the carrier of R = A & U = UAp R;
theorem :: ROUGHS_2:30 :: Proposition 1 1L 4L
for A being non empty finite set,
L being Function of bool A, bool A st
L.A = A &
(for X, Y being Subset of A holds L.(X /\ Y) = L.X /\ L.Y) holds
ex R being non empty finite RelStr st
the carrier of R = A & L = LAp R;
:: Serial Relations
theorem :: ROUGHS_2:31 :: Proposition 2 1L 4L 2L
for A being non empty finite set,
L being Function of bool A, bool A st
L.A = A &
L.{} = {} &
(for X, Y being Subset of A holds L.(X /\ Y) = L.X /\ L.Y) holds
ex R being non empty serial RelStr st
the carrier of R = A & L = LAp R;
theorem :: ROUGHS_2:32 :: Proposition 2 1H 4H 2H
for A being non empty finite set,
U being Function of bool A, bool A st
U.A = A &
U.{} = {} &
(for X, Y being Subset of A holds U.(X \/ Y) = U.X \/ U.Y) holds
ex R being non empty finite serial RelStr st
the carrier of R = A & U = UAp R;
theorem :: ROUGHS_2:33 :: Proposition 3 1L 4L 8LH
for A being non empty finite set,
L being Function of bool A, bool A st
L.A = A &
(for X being Subset of A holds L.X c= (L.(X`))`) &
(for X, Y being Subset of A holds L.(X /\ Y) = L.X /\ L.Y) holds
ex R being non empty finite serial RelStr st
the carrier of R = A & L = LAp R;
theorem :: ROUGHS_2:34 :: Proposition 4 2H 4H 8LH
for A being non empty finite set,
U being Function of bool A, bool A st
U.{} = {} &
(for X being Subset of A holds (U.(X`))` c= U.X) &
(for X, Y being Subset of A holds U.(X \/ Y) = U.X \/ U.Y) holds
ex R being non empty serial RelStr st
the carrier of R = A & U = UAp R;
:: Reflexive binary relations
theorem :: ROUGHS_2:35 :: Proposition 5 3L
for R being non empty reflexive RelStr,
X being Subset of R holds
LAp X c= X;
theorem :: ROUGHS_2:36 :: Proposition 5 3H
for R being non empty reflexive RelStr,
X being Subset of R holds
X c= UAp X;
theorem :: ROUGHS_2:37 :: Proposition 5 1H 4H 3H
for A being non empty finite set,
U being Function of bool A, bool A st
U.{} = {} &
(for X being Subset of A holds X c= U.X) &
(for X,Y being Subset of A holds U.(X \/ Y) = U.X \/ U.Y) holds
ex R being non empty finite reflexive RelStr st
the carrier of R = A & U = UAp R;
theorem :: ROUGHS_2:38 :: Proposition 5 1L 4L 3L
for A being non empty finite set,
L being Function of bool A, bool A st
L.A = A &
(for X being Subset of A holds L.X c= X) &
(for X,Y being Subset of A holds L.(X /\ Y) = L.X /\ L.Y) holds
ex R being non empty finite reflexive RelStr st
the carrier of R = A & L = LAp R;
:: Mediate Relations
theorem :: ROUGHS_2:39 :: Proposition 6 5H'
for R being non empty mediate RelStr,
X being Subset of R holds
UAp X c= UAp (UAp X);
theorem :: ROUGHS_2:40 :: Proposition 6 5L'
for R being non empty mediate RelStr,
X being Subset of R holds
LAp (LAp X) c= LAp X;
theorem :: ROUGHS_2:41 :: Proposition 7 2H 4H 5H'
for A being non empty finite set,
U being Function of bool A, bool A st
U.{} = {} &
(for X being Subset of A holds U.X c= U.(U.X)) &
(for X,Y being Subset of A holds U.(X \/ Y) = U.X \/ U.Y) holds
ex R being non empty mediate finite RelStr st
the carrier of R = A & U = UAp R;
theorem :: ROUGHS_2:42 :: Proposition 8 1L 4L 5L'
for A being non empty finite set,
L being Function of bool A, bool A st
L.A = A &
(for X being Subset of A holds L.(L.X) c= L.X) &
(for X,Y being Subset of A holds L.(X /\ Y) = L.X /\ L.Y) holds
ex R being non empty mediate finite RelStr st
the carrier of R = A & L = LAp R;
:: Corollaries
theorem :: ROUGHS_2:43 :: Corollary 1
for A being non empty finite set,
L being Function of bool A, bool A st
L.A = A &
(for X, Y being Subset of A holds L.(X /\ Y) = L.X /\ L.Y) holds
(for X being Subset of A holds L.X c= (L.(X`))`)
iff
L.{} = {};
theorem :: ROUGHS_2:44 :: Corollary 2
for A being non empty finite set,
U being Function of bool A, bool A st
U.{} = {} &
(for X,Y being Subset of A holds U.(X \/ Y) = U.X \/ U.Y) holds
(for X being Subset of A holds (U.(X`))` c= U.X)
iff
U.A = A;