:: Formalizing Two Generalized Approximation Operators
:: by Adam Grabowski and Micha{\l} Sielwiesiuk
::
:: Received June 29, 2018
:: Copyright (c) 2018-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, RELAT_2, XBOOLE_0,
PARTFUN1, SUBSET_1, FUNCT_1, EQREL_1, ROUGHS_1, ROUGHS_2, ROUGHS_5,
ALTCAT_2, FIB_NUM, FUNCT_7, COHSP_1, ROUGHS_4, SETWISEO;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1,
RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1, STRUCT_0, ORDERS_2, SETWISEO,
EQREL_1, PRE_TOPC, ROUGHS_1, YELLOW_3, ROUGHS_2, ALTCAT_2, ROUGHS_4;
constructors EQREL_1, REALSET2, RELSET_1, ROUGHS_1, YELLOW_3, TOPS_1,
ROUGHS_2, ALTCAT_2, COHSP_1, ROUGHS_3, ROUGHS_4, RELAT_2, SETWISEO,
PARTIT1, BVFUNC_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, STRUCT_0, ORDERS_2, RELSET_1,
FUNCT_1, FUNCT_2, ROUGHS_1;
requirements BOOLE, SUBSET;
begin :: Definitions of the mappings defined in the paper by Gomolinska
definition :: property (1) p. 105
let R be non empty set;
let I be Function of R, bool R;
attr I is map-reflexive means
:: ROUGHS_5:def 1
for u being Element of R holds u in I.u;
end;
definition :: stolen from SETWISEO
let R be non empty set;
func singleton R -> Function of R, bool R means
:: ROUGHS_5:def 2
for x being Element of R holds it.x = {x};
end;
registration let R be non empty set;
cluster singleton R -> map-reflexive;
end;
theorem :: ROUGHS_5:1 :: property (2)
for R being non empty RelStr,
I being Function of the carrier of R, bool the carrier of R
st I is map-reflexive holds
the carrier of R = union (I.:[#]R);
reserve f,g for Function;
reserve R for non empty reflexive RelStr;
theorem :: ROUGHS_5:2 :: Theorem 4.1 b)
LAp R cc= id bool the carrier of R;
theorem :: ROUGHS_5:3 :: 4.1 b)
id bool the carrier of R cc= UAp R;
reserve R for non empty RelStr;
theorem :: ROUGHS_5:4 :: Proposition 1.1 a)
for f being map of R,
x,y being Subset of R holds
Flip (Flip f) = f;
::: $f^d$
theorem :: ROUGHS_5:5
for f,g being map of R holds
Flip (f * g) = Flip f * Flip g;
theorem :: ROUGHS_5:6 :: c)
for f being map of R holds
f.{} = {} iff (Flip f).(the carrier of R) = the carrier of R;
begin :: Formalization of I and tau mappings
definition
let R be non empty RelStr;
func UncertaintyMap R -> Function of the carrier of R,
bool the carrier of R means
:: ROUGHS_5:def 3
for x being Element of R holds
it.x = Coim(the InternalRel of R,x);
end;
theorem :: ROUGHS_5:7 :: property (3)
for w,u being Element of R holds
[w,u] in the InternalRel of R iff w in (UncertaintyMap R).u;
definition let R be non empty RelStr;
func tau R -> Function of the carrier of R, bool the carrier of R means
:: ROUGHS_5:def 4
for u being Element of R holds
it.u = Im(the InternalRel of R,u);
end;
theorem :: ROUGHS_5:8
for u,w being Element of R holds
u in Im (the InternalRel of R,w) iff
w in Coim (the InternalRel of R,u);
theorem :: ROUGHS_5:9 :: formula (3)
for w,u being Element of R holds
[w,u] in the InternalRel of R iff u in (tau R).w;
:: General version of the induced mapping
definition let R be non empty RelStr;
let f be Function of the carrier of R, bool the carrier of R;
func ff_0 f -> map of R means
:: ROUGHS_5:def 5
for x being Subset of R holds
it.x = { u where u is Element of R : f.u meets x };
end;
definition
let R be non empty RelStr;
func f_0 R -> map of R equals
:: ROUGHS_5:def 6
ff_0 tau R;
func f_1 R -> map of R equals
:: ROUGHS_5:def 7
ff_0 UncertaintyMap R;
end;
theorem :: ROUGHS_5:10
the InternalRel of R is symmetric implies
UncertaintyMap R = tau R;
theorem :: ROUGHS_5:11 :: Proposition 4.2
the InternalRel of R is symmetric implies
f_0 R = f_1 R;
theorem :: ROUGHS_5:12 :: (6)
the InternalRel of R is symmetric iff
for u,v being Element of R holds
u in (tau R).v implies v in (tau R).u;
theorem :: ROUGHS_5:13
f_0 R = UAp R;
theorem :: ROUGHS_5:14
Flip f_0 R = LAp R;
theorem :: ROUGHS_5:15 :: Theorem 4.1 c)
for R being Approximation_Space
for x being Subset of R holds
(f_0 R).x is exact;
theorem :: ROUGHS_5:16 :: 4.1 a)
the InternalRel of R is total reflexive implies
id bool the carrier of R cc= f_0 R;
theorem :: ROUGHS_5:17 :: 4.1 a)
R is reflexive implies
Flip (f_0 R) cc= id bool the carrier of R;
theorem :: ROUGHS_5:18 :: 4.1 b)
the InternalRel of R is total reflexive implies
id bool the carrier of R cc= f_1 R;
reserve f for Function of the carrier of R, bool the carrier of R;
theorem :: ROUGHS_5:19 :: 4.1 h)
(ff_0 f).{} = {};
registration let R;
let f;
cluster ff_0 f -> empty-preserving;
end;
theorem :: ROUGHS_5:20 :: 4.1 h)
(f_0 R).{} = {};
theorem :: ROUGHS_5:21 :: 4.1 h)
(f_1 R).{} = {};
registration let R be non empty reflexive RelStr;
cluster the InternalRel of R -> total reflexive;
end;
theorem :: ROUGHS_5:22 :: 4.1 h)
f is map-reflexive implies
(ff_0 f).the carrier of R = the carrier of R;
theorem :: ROUGHS_5:23 :: 4.1 h)
the InternalRel of R is reflexive total implies
(f_0 R).the carrier of R = the carrier of R;
theorem :: ROUGHS_5:24 :: 4.1 h)
the InternalRel of R is reflexive total implies
(f_1 R).the carrier of R = the carrier of R;
theorem :: ROUGHS_5:25 :: 4.1 f) g) general version
for u,w being Element of R,
x being Subset of R st
f.u = f.w holds u in (ff_0 f).x iff w in (ff_0 f).x;
theorem :: ROUGHS_5:26 :: 4.1 g)
for u,w being Element of R,
x being Subset of R st
(UncertaintyMap R).u = (UncertaintyMap R).w holds
u in (f_1 R).x iff w in (f_1 R).x;
theorem :: ROUGHS_5:27 :: 4.1 f)
for u,w being Element of R,
x being Subset of R st
(tau R).u = (tau R).w holds
u in (f_0 R).x iff w in (f_0 R).x;
theorem :: ROUGHS_5:28
for f being Function of the carrier of R, bool the carrier of R
for x being Subset of R holds
(Flip ff_0 f).x = { w where w is Element of R : f.w c= x };
theorem :: ROUGHS_5:29
for x being Subset of R holds
(Flip f_0 R).x = { w where w is Element of R : (tau R).w c= x };
theorem :: ROUGHS_5:30
for x being Subset of R holds
(Flip f_1 R).x = { w where w is Element of R :
(UncertaintyMap R).w c= x };
theorem :: ROUGHS_5:31 :: 4.1 f) Flip
for u,w being Element of R,
x being Subset of R st
f.u = f.w holds
u in (Flip ff_0 f).x iff w in (Flip ff_0 f).x;
theorem :: ROUGHS_5:32 :: 4.1 f) Flip
for u,w being Element of R,
x being Subset of R st
(tau R).u = (tau R).w holds
u in (Flip f_0 R).x iff w in (Flip f_0 R).x;
theorem :: ROUGHS_5:33 :: 4.1 g) Flip
for u,w being Element of R,
x being Subset of R st
(UncertaintyMap R).u = (UncertaintyMap R).w holds
u in (Flip f_1 R).x iff w in (Flip f_1 R).x;
theorem :: ROUGHS_5:34
R is reflexive implies
for w being Element of R holds w in (UncertaintyMap R).w;
theorem :: ROUGHS_5:35
R is reflexive implies
for w being Element of R holds w in (tau R).w;
registration let R be reflexive non empty RelStr;
cluster UncertaintyMap R -> map-reflexive;
cluster tau R -> map-reflexive;
end;
theorem :: ROUGHS_5:36 :: 4.1 b)
R is reflexive implies
Flip f_1 R cc= id bool the carrier of R;
theorem :: ROUGHS_5:37 :: Theorem 4.2 (a) <=> (b)
(f_0 R) * (f_0 R) = f_0 R
iff
Flip (f_0 R) * Flip (f_0 R) = Flip (f_0 R);
theorem :: ROUGHS_5:38
R is reflexive implies
union ((UncertaintyMap R).:[#]R) = the carrier of R;
registration let R be non empty RelStr; :: i)
cluster f_0 R -> c=-monotone;
cluster f_1 R -> c=-monotone;
end;
theorem :: ROUGHS_5:39
for f being map of R st f is c=-monotone holds
Flip f is c=-monotone;
theorem :: ROUGHS_5:40 :: i)
Flip f_0 R is c=-monotone;
theorem :: ROUGHS_5:41 :: i)
Flip f_1 R is c=-monotone;
theorem :: ROUGHS_5:42 :: j)
for f being Function of the carrier of R, bool the carrier of R
for x,y being Subset of R holds
(ff_0 f).(x \/ y) = (ff_0 f).x \/ (ff_0 f).y;
theorem :: ROUGHS_5:43 :: j) version
for x,y being Subset of R holds
(f_0 R).(x \/ y) = (f_0 R).x \/ (f_0 R).y;
theorem :: ROUGHS_5:44 :: j) version
for x,y being Subset of R holds
(f_1 R).(x \/ y) = (f_1 R).x \/ (f_1 R).y;
theorem :: ROUGHS_5:45 :: k)
for f being Function of the carrier of R, bool the carrier of R
for x,y being Subset of R holds
(Flip ff_0 f).x \/ (Flip ff_0 f).y c= (Flip ff_0 f).(x \/ y);
theorem :: ROUGHS_5:46 :: k)
for x,y being Subset of R holds
((Flip f_0 R).x \/ (Flip f_0 R).y) c= (Flip f_0 R).(x \/ y);
theorem :: ROUGHS_5:47 :: k)
for x,y being Subset of R holds
((Flip f_1 R).x \/ (Flip f_1 R).y) c= (Flip f_1 R).(x \/ y);
theorem :: ROUGHS_5:48 :: l)
for f being Function of the carrier of R, bool the carrier of R
for x,y being Subset of R holds
(ff_0 f).(x /\ y) c= (ff_0 f).x /\ (ff_0 f).y;
theorem :: ROUGHS_5:49 :: l)
for x,y being Subset of R holds
(f_0 R).(x /\ y) c= (f_0 R).x /\ (f_0 R).y;
theorem :: ROUGHS_5:50 :: l)
for x,y being Subset of R holds
(f_1 R).(x /\ y) c= (f_1 R).x /\ (f_1 R).y;
theorem :: ROUGHS_5:51 :: m)
for f being Function of the carrier of R, bool the carrier of R
for x,y being Subset of R holds
(Flip ff_0 f).x /\ (Flip ff_0 f).y = (Flip ff_0 f).(x /\ y);
theorem :: ROUGHS_5:52 :: m)
for x,y being Subset of R holds
(Flip f_0 R).x /\ (Flip f_0 R).y = (Flip f_0 R).(x /\ y);
theorem :: ROUGHS_5:53 :: m)
for x,y being Subset of R holds
(Flip f_1 R).x /\ (Flip f_1 R).y = (Flip f_1 R).(x /\ y);