ROUGHS_4: Topological Interpretation of Rough Sets

:: Topological Interpretation of Rough Sets
:: by Adam Grabowski
::
:: Received March 31, 2014
:: Copyright (c) 2014-2021 Association of Mizar Users

theorem Lemma: :: ROUGHS_4:1

for T being set
for F being Subset-Family of T holds F = { B where B is Subset of T : B in F }

proof end;

definition

let f be Function;
let A be set ;

attr A is f -closed means :: ROUGHS_4:def 1
A = f . A;

end;

:: deftheorem defines -closed ROUGHS_4:def 1 :

definition

let X be set ;
let F be Subset-Family of X;

:: original: cap-closed
redefine attr F is cap-closed means :: ROUGHS_4:def 2
for a, b being Subset of X st a in F & b in F holds
a /\ b in F;

compatibility ;

end;

:: deftheorem defines cap-closed ROUGHS_4:def 2 :

definition

let X be set ;
let F be Subset-Family of X;

attr F is union-closed means :: ROUGHS_4:def 3
for a being Subset-Family of X st a c= F holds
union a in F;

end;

:: deftheorem defines union-closed ROUGHS_4:def 3 :

definition

let X be set ;
let F be Subset-Family of X;

attr F is topology-like means :TLDef: :: ROUGHS_4:def 4
( {} in F & X in F & F is union-closed & F is V97() );

end;

:: deftheorem TLDef defines topology-like ROUGHS_4:def 4 :

registration

let X be set ;

cluster topology-like for Element of bool (bool X);

proof end;

end;

definition

let X be set ;
let f be Function of (bool X),(bool X);

attr f is extensive means :: ROUGHS_4:def 5
for A being Subset of X holds A c= f . A;

attr f is intensive means :: ROUGHS_4:def 6
for A being Subset of X holds f . A c= A;

attr f is idempotent means :: ROUGHS_4:def 7
for A being Subset of X holds f . (f . A) = f . A;

attr f is c=-monotone means :: ROUGHS_4:def 8
for A, B being Subset of X st A c= B holds
f . A c= f . B;

attr f is \/-preserving means :: ROUGHS_4:def 9
for A, B being Subset of X holds f . (A \/ B) = (f . A) \/ (f . B);

attr f is /\-preserving means :: ROUGHS_4:def 10
for A, B being Subset of X holds f . (A /\ B) = (f . A) /\ (f . B);

end;

:: deftheorem defines extensive ROUGHS_4:def 5 :

:: deftheorem defines intensive ROUGHS_4:def 6 :

:: deftheorem defines idempotent ROUGHS_4:def 7 :

:: deftheorem defines c=-monotone ROUGHS_4:def 8 :

:: deftheorem defines \/-preserving ROUGHS_4:def 9 :

:: deftheorem defines /\-preserving ROUGHS_4:def 10 :

definition

let X be set ;
let O be Function of (bool X),(bool X);

attr O is preclosure means :: ROUGHS_4:def 11
( O is extensive & O is \/-preserving & O is empty-preserving );

attr O is closure means :: ROUGHS_4:def 12
( O is extensive & O is idempotent & O is \/-preserving & O is empty-preserving );

attr O is preinterior means :: ROUGHS_4:def 13
( O is intensive & O is /\-preserving & O is universe-preserving );

attr O is interior means :: ROUGHS_4:def 14
( O is intensive & O is idempotent & O is /\-preserving & O is universe-preserving );

end;

:: deftheorem defines preclosure ROUGHS_4:def 11 :

:: deftheorem defines closure ROUGHS_4:def 12 :

:: deftheorem defines preinterior ROUGHS_4:def 13 :

:: deftheorem defines interior ROUGHS_4:def 14 :

registration

let X be set ;

cluster Function-like V21( bool X, bool X) \/-preserving -> c=-monotone for Element of bool [:(bool X),(bool X):];

proof end;

cluster Function-like V21( bool X, bool X) /\-preserving -> c=-monotone for Element of bool [:(bool X),(bool X):];

proof end;

end;

:: preclosure implies monotonicity
:: Cl_Seq from FRECHET2 is important example of preclosure

registration

let X be set ;

cluster id (bool X) -> closure for Function of (bool X),(bool X);

proof end;

cluster id (bool X) -> interior for Function of (bool X),(bool X);

proof end;

end;

registration

let X be set ;

cluster non empty Relation-like bool X -defined bool X -valued Function-like V17( bool X) V21( bool X, bool X) closure interior for Element of bool [:(bool X),(bool X):];

proof end;

end;

registration

let X be set ;

cluster Function-like V21( bool X, bool X) closure -> preclosure for Element of bool [:(bool X),(bool X):];

end;

definition

let T be 1-sorted ;
mode map of T is Function of (bool the carrier of T),(bool the carrier of T);

end;

definition

attr c₁ is strict ;
struct 1stOpStr -> 1-sorted ;
aggr 1stOpStr(# carrier, FirstOp #) -> 1stOpStr ;
sel FirstOp c₁ -> Function of (bool the carrier of c₁),(bool the carrier of c₁);

end;

definition

attr c₁ is strict ;
struct 2ndOpStr -> 1-sorted ;
aggr 2ndOpStr(# carrier, SecondOp #) -> 2ndOpStr ;
sel SecondOp c₁ -> Function of (bool the carrier of c₁),(bool the carrier of c₁);

end;

definition

attr c₁ is strict ;
struct TwoOpStruct -> 1stOpStr , 2ndOpStr ;
aggr TwoOpStruct(# carrier, FirstOp, SecondOp #) -> TwoOpStruct ;

end;

definition

let X be 1stOpStr ;

attr X is with_closure means :CDef: :: ROUGHS_4:def 15
the FirstOp of X is closure ;

attr X is with_preclosure means :: ROUGHS_4:def 16
the FirstOp of X is preclosure ;

end;

:: deftheorem CDef defines with_closure ROUGHS_4:def 15 :

:: deftheorem defines with_preclosure ROUGHS_4:def 16 :

registration

let T be TopSpace;

cluster ClMap T -> closure ;

proof end;

cluster IntMap T -> interior ;

proof end;

end;

registration

cluster non empty with_closure for 1stOpStr ;

proof end;

end;

registration

cluster with_closure -> with_preclosure for 1stOpStr ;

end;

definition

let X be 1stOpStr ;
let A be Subset of X;

attr A is op-closed means :: ROUGHS_4:def 17
A = the FirstOp of X . A;

end;

:: deftheorem defines op-closed ROUGHS_4:def 17 :

definition

let X be 1stOpStr ;

attr X is with_op-closed_subsets means :OCS: :: ROUGHS_4:def 18
ex A being Subset of X st A is op-closed ;

end;

:: deftheorem OCS defines with_op-closed_subsets ROUGHS_4:def 18 :

registration

cluster with_op-closed_subsets for 1stOpStr ;

proof end;

end;

registration

let X be with_op-closed_subsets 1stOpStr ;

cluster op-closed for Element of bool the carrier of X;

existence by OCS;

end;

definition

let X be 2ndOpStr ;
let A be Subset of X;

attr A is op-open means :: ROUGHS_4:def 19
A = the SecondOp of X . A;

end;

:: deftheorem defines op-open ROUGHS_4:def 19 :

definition

let X be 2ndOpStr ;

attr X is with_op-open_subsets means :OOS: :: ROUGHS_4:def 20
ex A being Subset of X st A is op-open ;

end;

:: deftheorem OOS defines with_op-open_subsets ROUGHS_4:def 20 :

registration

cluster with_op-open_subsets for 2ndOpStr ;

proof end;

end;

registration

let X be with_op-open_subsets 2ndOpStr ;

cluster op-open for Element of bool the carrier of X;

existence by OOS;

end;

definition

let X be 2ndOpStr ;

attr X is with_interior means :: ROUGHS_4:def 21
the SecondOp of X is interior ;

attr X is with_preinterior means :: ROUGHS_4:def 22
the SecondOp of X is preinterior ;

end;

:: deftheorem defines with_interior ROUGHS_4:def 21 :

:: deftheorem defines with_preinterior ROUGHS_4:def 22 :

registration

cluster with_closure with_interior for TwoOpStruct ;

proof end;

end;

definition

attr c₁ is strict ;
struct 1TopStruct -> 1stOpStr , TopStruct ;
aggr 1TopStruct(# carrier, FirstOp, topology #) -> 1TopStruct ;

end;

definition

attr c₁ is strict ;
struct 2TopStruct -> 2ndOpStr , TopStruct ;
aggr 2TopStruct(# carrier, SecondOp, topology #) -> 2TopStruct ;

end;

registration

cluster non empty strict for 1TopStruct ;

proof end;

end;

registration

cluster non empty strict for 2TopStruct ;

proof end;

end;

definition

let T be 1TopStruct ;

attr T is with_properly_defined_topology means :PDT: :: ROUGHS_4:def 23
for x being object holds
( x in the topology of T iff ex S being Subset of T st
( S ` = x & S is op-closed ) );

end;

:: deftheorem PDT defines with_properly_defined_topology ROUGHS_4:def 23 :

definition

let T be 2TopStruct ;

attr T is with_properly_defined_Topology means :PDTo: :: ROUGHS_4:def 24
for x being object holds
( x in the topology of T iff ex S being Subset of T st
( S = x & S is op-open ) );

end;

:: deftheorem PDTo defines with_properly_defined_Topology ROUGHS_4:def 24 :

registration

cluster with_closure with_properly_defined_topology for 1TopStruct ;

proof end;

cluster with_interior with_properly_defined_Topology for 2TopStruct ;

proof end;

end;

theorem Lem1: :: ROUGHS_4:2

for T being with_properly_defined_topology 1TopStruct
for A being Subset of T holds
( A is op-closed iff A is closed )

proof end;

registration

cluster with_preclosure with_properly_defined_topology -> TopSpace-like with_properly_defined_topology for 1TopStruct ;

proof end;

end;

theorem :: ROUGHS_4:3

for T being with_properly_defined_Topology 2TopStruct
for A being Subset of T holds
( A is op-open iff A is open )

proof end;

registration

cluster with_preinterior with_properly_defined_Topology -> TopSpace-like with_properly_defined_Topology for 2TopStruct ;

proof end;

end;

theorem :: ROUGHS_4:4

for T being with_closure with_properly_defined_topology 1TopStruct
for A being Subset of T holds the FirstOp of T . A = Cl A

proof end;

registration

let R be Tolerance_Space;

cluster LAp R -> preinterior ;

proof end;

cluster UAp R -> preclosure ;

proof end;

end;

registration

let R be Approximation_Space;

cluster LAp R -> interior ;

proof end;

cluster UAp R -> closure ;

proof end;

end;

definition

let X be set ;
let f be Function of (bool X),(bool X);

func GenTop f -> Subset-Family of X means :GTDef: :: ROUGHS_4:def 25
for x being object holds
( x in it iff ex S being Subset of X st
( S = x & S is f -closed ) );

proof end;

proof end;

end;

:: deftheorem GTDef defines GenTop ROUGHS_4:def 25 :

theorem ImportTop: :: ROUGHS_4:5

for X being set
for f being Function of (bool X),(bool X) st f is preinterior holds
GenTop f is topology-like

proof end;

registration

let C be set ;
let I be Relation of C;
let f be topology-like Subset-Family of C;

cluster TopRelStr(# C,I,f #) -> TopSpace-like ;

proof end;

end;

registration

cluster non empty TopSpace-like with_equivalence for TopRelStr ;

proof end;

end;

definition

let T be non empty TopSpace;

func Cl_Seq T -> map of T means :SeqDef: :: ROUGHS_4:def 26
for A being Subset of T holds it . A = Cl_Seq A;

proof end;

proof end;

end;

:: deftheorem SeqDef defines Cl_Seq ROUGHS_4:def 26 :

registration

let T be non empty TopSpace;

cluster Cl_Seq T -> preclosure ;

proof end;

end;

registration

cluster non empty TopSpace-like Frechet for TopStruct ;

existence by FRECHET:33;

end;

registration

let T be non empty Frechet TopSpace;

cluster Cl_Seq T -> closure ;

proof end;

end;

definition

let T be non empty TopRelStr ;

attr T is Natural means :: ROUGHS_4:def 27
for x being Subset of T holds
( x in the topology of T iff x is LAp T -closed );

end;

:: deftheorem defines Natural ROUGHS_4:def 27 :

definition

let T be non empty TopRelStr ;

attr T is naturally_generated means :: ROUGHS_4:def 28
the topology of T = GenTop (LAp T);

end;

:: deftheorem defines naturally_generated ROUGHS_4:def 28 :

theorem OpIsLap: :: ROUGHS_4:6

for T being non empty TopRelStr st T is naturally_generated holds
for A being Subset of T holds
( A is open iff LAp A = A )

proof end;

theorem Fiu: :: ROUGHS_4:7

for T being non empty TopRelStr
for R being non empty RelStr st RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) holds
LAp T = LAp R

proof end;

theorem :: ROUGHS_4:8

for T being non empty TopRelStr
for R being non empty RelStr st RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) holds
UAp T = UAp R

proof end;

registration

cluster non empty TopSpace-like with_equivalence Natural for TopRelStr ;

proof end;

end;

registration

cluster non empty with_equivalence naturally_generated -> non empty TopSpace-like with_equivalence for TopRelStr ;

proof end;

end;

registration

cluster non empty TopSpace-like with_equivalence naturally_generated for TopRelStr ;

proof end;

end;

OpenLap: for T being non empty with_equivalence naturally_generated TopRelStr
for A being open Subset of T holds LAp A = Int A

proof end;

registration

let T be non empty with_equivalence naturally_generated TopRelStr ;
let A be Subset of T;

cluster LAp A -> open ;

proof end;

end;

theorem LApInt: :: ROUGHS_4:9

for T being non empty with_equivalence naturally_generated TopRelStr
for A being Subset of T holds LAp A = Int A

proof end;

theorem UApCl1: :: ROUGHS_4:10

for T being non empty with_equivalence naturally_generated TopRelStr
for A being Subset of T holds
( A is closed iff UAp A = A )

proof end;

registration

let T be non empty with_equivalence naturally_generated TopRelStr ;
let A be Subset of T;

cluster UAp A -> closed ;

proof end;

end;

theorem UApCl: :: ROUGHS_4:11

for T being non empty with_equivalence naturally_generated TopRelStr
for A being Subset of T holds UAp A = Cl A

proof end;

theorem :: ROUGHS_4:12

for T being non empty with_equivalence naturally_generated TopRelStr
for A being Subset of T holds BndAp A = Fr A

proof end;

registration

let T be non empty with_equivalence naturally_generated TopRelStr ;
let A be Subset of T;

identify Int A with LAp A;

correctness by LApInt;

identify Cl A with UAp A;

correctness by UApCl;

identify LAp A with Int A;

identify UAp A with Cl A;

identify BndAp A with Fr A;

identify Fr A with BndAp A;

end;

theorem :: ROUGHS_4:13

for T being non empty with_equivalence naturally_generated TopRelStr
for A being Subset of T holds
( A is 1st_class iff LAp (UAp A) c= UAp (LAp A) ) ;

theorem FirstApprox: :: ROUGHS_4:14

for T being non empty with_equivalence naturally_generated TopRelStr
for A being Subset of T holds
( A is 1st_class iff UAp A c= LAp A )

proof end;

theorem FirstIsExact: :: ROUGHS_4:15

for T being non empty with_equivalence naturally_generated TopRelStr
for A being Subset of T holds
( A is 1st_class iff A is exact )

proof end;

registration

let T be non empty with_equivalence naturally_generated TopRelStr ;

cluster 1st_class -> exact for Element of bool the carrier of T;

coherence by FirstIsExact;

cluster exact -> 1st_class for Element of bool the carrier of T;

coherence by FirstIsExact;

end;

theorem SecondClass: :: ROUGHS_4:16

for T being non empty with_equivalence naturally_generated TopRelStr
for A being Subset of T holds
( A is 2nd_class iff LAp A c< UAp A )

proof end;

theorem SecondRough: :: ROUGHS_4:17

for T being non empty with_equivalence naturally_generated TopRelStr
for A being Subset of T holds
( A is 2nd_class iff A is rough )

proof end;

registration

let T be non empty with_equivalence naturally_generated TopRelStr ;

cluster 2nd_class -> rough for Element of bool the carrier of T;

cluster rough -> 2nd_class for Element of bool the carrier of T;

coherence by SecondRough;

end;

theorem :: ROUGHS_4:18

for T being non empty with_equivalence naturally_generated TopRelStr
for A being Subset of T holds Cl (Int A), Cl A are_c=-comparable by ROUGHS_1:25, ROUGHS_1:12;

theorem ApproxWithout: :: ROUGHS_4:19

for T being non empty with_equivalence naturally_generated TopRelStr
for A being Subset of T holds not A is 3rd_class

proof end;

notation

let T be TopSpace;
antonym without_3rd_class_subsets T for with_3rd_class_subsets ;

end;

registration

cluster non empty with_equivalence naturally_generated -> non empty with_equivalence without_3rd_class_subsets naturally_generated for TopRelStr ;

coherence by ApproxWithout;

cluster TopSpace-like without_3rd_class_subsets for TopStruct ;

proof end;

end;

registration

let T be TopSpace;
let A be 1st_class Subset of T;

cluster Border A -> empty ;

coherence by ISOMICHI:37;

end;

registration

let T be non empty with_equivalence naturally_generated TopRelStr ;
let A be Subset of T;

cluster Cl A -> open ;

proof end;

cluster Int A -> closed ;

proof end;

end;

registration

cluster non empty with_equivalence naturally_generated -> non empty with_equivalence extremally_disconnected naturally_generated for TopRelStr ;

end;

::

WP:

Kuratowski's closure-complement problem

theorem Seven1: :: ROUGHS_4:20

for T being non empty with_equivalence naturally_generated TopRelStr
for A being Subset of T holds Kurat7Set A = {A,(Cl A),(Int A)}

proof end;

theorem :: ROUGHS_4:21

for T being non empty with_equivalence naturally_generated TopRelStr
for A being Subset of T holds card (Kurat7Set A) <= 3

proof end;

theorem Fourteen: :: ROUGHS_4:22

for T being non empty with_equivalence naturally_generated TopRelStr
for A being Subset of T holds Kurat14Set A = {A,(UAp A),((UAp A) `),(A `),((LAp A) `),(LAp A)}

proof end;

theorem :: ROUGHS_4:23

for T being non empty with_equivalence naturally_generated TopRelStr
for A being Subset of T holds card (Kurat14Set A) <= 6

proof end;