:: Topological Interpretation of Rough Sets
::
:: Copyright (c) 2014-2019 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 :
for f being Function
for A being set holds
( A is f -closed iff A = f . A );

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
( F is cap-closed iff for a, b being Subset of X st a in F & b in F holds
a /\ b in F )
;
end;

:: deftheorem defines cap-closed ROUGHS_4:def 2 :
for X being set
for F being Subset-Family of X holds
( F is cap-closed iff for a, b being Subset of X st a in F & b in F holds
a /\ b in F );

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 :
for X being set
for F being Subset-Family of X holds
( F is union-closed iff for a being Subset-Family of X st a c= F holds
union a in F );

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 :
for X being set
for F being Subset-Family of X holds
( F is topology-like iff ( {} in F & X in F & F is union-closed & F is V97() ) );

registration
let X be set ;
cluster topology-like for Element of bool (bool X);
existence
ex b1 being Subset-Family of X st b1 is topology-like
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 :
for X being set
for f being Function of (bool X),(bool X) holds
( f is extensive iff for A being Subset of X holds A c= f . A );

:: deftheorem defines intensive ROUGHS_4:def 6 :
for X being set
for f being Function of (bool X),(bool X) holds
( f is intensive iff for A being Subset of X holds f . A c= A );

:: deftheorem defines idempotent ROUGHS_4:def 7 :
for X being set
for f being Function of (bool X),(bool X) holds
( f is idempotent iff for A being Subset of X holds f . (f . A) = f . A );

:: deftheorem defines c=-monotone ROUGHS_4:def 8 :
for X being set
for f being Function of (bool X),(bool X) holds
( f is c=-monotone iff for A, B being Subset of X st A c= B holds
f . A c= f . B );

:: deftheorem defines \/-preserving ROUGHS_4:def 9 :
for X being set
for f being Function of (bool X),(bool X) holds
( f is \/-preserving iff for A, B being Subset of X holds f . (A \/ B) = (f . A) \/ (f . B) );

:: deftheorem defines /\-preserving ROUGHS_4:def 10 :
for X being set
for f being Function of (bool X),(bool X) holds
( f is /\-preserving iff for A, B being Subset of X holds f . (A /\ B) = (f . A) /\ (f . B) );

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 :
for X being set
for O being Function of (bool X),(bool X) holds
( O is preclosure iff ( O is extensive & O is \/-preserving & O is empty-preserving ) );

:: deftheorem defines closure ROUGHS_4:def 12 :
for X being set
for O being Function of (bool X),(bool X) holds
( O is closure iff ( O is extensive & O is idempotent & O is \/-preserving & O is empty-preserving ) );

:: deftheorem defines preinterior ROUGHS_4:def 13 :
for X being set
for O being Function of (bool X),(bool X) holds
( O is preinterior iff ( O is intensive & O is /\-preserving & O is universe-preserving ) );

:: deftheorem defines interior ROUGHS_4:def 14 :
for X being set
for O being Function of (bool X),(bool X) holds
( O is interior iff ( O is intensive & O is idempotent & O is /\-preserving & O is universe-preserving ) );

registration
let X be set ;
cluster Function-like V21( bool X, bool X) \/-preserving -> c=-monotone for Element of bool [:(bool X),(bool X):];
coherence
for b1 being Function of (bool X),(bool X) st b1 is \/-preserving holds
b1 is c=-monotone
proof end;
cluster Function-like V21( bool X, bool X) /\-preserving -> c=-monotone for Element of bool [:(bool X),(bool X):];
coherence
for b1 being Function of (bool X),(bool X) st b1 is /\-preserving holds
b1 is c=-monotone
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);
coherence
for b1 being Function of (bool X),(bool X) st b1 = id (bool X) holds
b1 is closure
proof end;
cluster id (bool X) -> interior for Function of (bool X),(bool X);
coherence
for b1 being Function of (bool X),(bool X) st b1 = id (bool X) holds
b1 is interior
proof end;
end;

registration
let X be set ;
existence
ex b1 being Function of (bool X),(bool X) st
( b1 is closure & b1 is interior )
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):];
coherence
for b1 being Function of (bool X),(bool X) st b1 is closure holds
b1 is preclosure
;
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 c1 is strict ;
struct 1stOpStr -> 1-sorted ;
aggr 1stOpStr(# carrier, FirstOp #) -> 1stOpStr ;
sel FirstOp c1 -> Function of (bool the carrier of c1),(bool the carrier of c1);
end;

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

definition 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 :
for X being 1stOpStr holds
( X is with_closure iff the FirstOp of X is closure );

:: deftheorem defines with_preclosure ROUGHS_4:def 16 :
for X being 1stOpStr holds
( X is with_preclosure iff the FirstOp of X is preclosure );

registration
let T be TopSpace;
coherence
ClMap T is closure
proof end;
coherence
proof end;
end;

registration
existence
ex b1 being 1stOpStr st
( b1 is with_closure & not b1 is empty )
proof end;
end;

registration
coherence
for b1 being 1stOpStr st b1 is with_closure holds
b1 is with_preclosure
;
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 :
for X being 1stOpStr
for A being Subset of X holds
( A is op-closed iff A = the FirstOp of X . A );

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 :
for X being 1stOpStr holds
( X is with_op-closed_subsets iff ex A being Subset of X st A is op-closed );

registration
existence
ex b1 being 1stOpStr st b1 is with_op-closed_subsets
proof end;
end;

registration
let X be with_op-closed_subsets 1stOpStr ;
cluster op-closed for Element of bool the carrier of X;
existence
ex b1 being Subset of X st b1 is op-closed
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 :
for X being 2ndOpStr
for A being Subset of X holds
( A is op-open iff A = the SecondOp of X . A );

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 :
for X being 2ndOpStr holds
( X is with_op-open_subsets iff ex A being Subset of X st A is op-open );

registration
existence
ex b1 being 2ndOpStr st b1 is with_op-open_subsets
proof end;
end;

registration
let X be with_op-open_subsets 2ndOpStr ;
cluster op-open for Element of bool the carrier of X;
existence
ex b1 being Subset of X st b1 is op-open
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 :
for X being 2ndOpStr holds
( X is with_interior iff the SecondOp of X is interior );

:: deftheorem defines with_preinterior ROUGHS_4:def 22 :
for X being 2ndOpStr holds
( X is with_preinterior iff the SecondOp of X is preinterior );

registration
existence
ex b1 being TwoOpStruct st
( b1 is with_closure & b1 is with_interior )
proof end;
end;

definition end;

definition end;

registration
cluster non empty strict for 1TopStruct ;
existence
ex b1 being 1TopStruct st
( not b1 is empty & b1 is strict )
proof end;
end;

registration
cluster non empty strict for 2TopStruct ;
existence
ex b1 being 2TopStruct st
( not b1 is empty & b1 is strict )
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 :
for T being 1TopStruct holds
( T is with_properly_defined_topology iff 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 ) ) );

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 :
for T being 2TopStruct holds
( T is with_properly_defined_Topology iff 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 ) ) );

registration
existence
ex b1 being 1TopStruct st
( b1 is with_closure & b1 is with_properly_defined_topology )
proof end;
existence
ex b1 being 2TopStruct st
( b1 is with_interior & b1 is with_properly_defined_Topology )
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
coherence
for b1 being with_properly_defined_topology 1TopStruct st b1 is with_preclosure holds
b1 is TopSpace-like
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
coherence
for b1 being with_properly_defined_Topology 2TopStruct st b1 is with_preinterior holds
b1 is TopSpace-like
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;
coherence
proof end;
coherence
proof end;
end;

registration
let R be Approximation_Space;
coherence
LAp R is interior
proof end;
coherence
UAp R is 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 ) );
existence
ex b1 being Subset-Family of X st
for x being object holds
( x in b1 iff ex S being Subset of X st
( S = x & S is f -closed ) )
proof end;
uniqueness
for b1, b2 being Subset-Family of X st ( for x being object holds
( x in b1 iff ex S being Subset of X st
( S = x & S is f -closed ) ) ) & ( for x being object holds
( x in b2 iff ex S being Subset of X st
( S = x & S is f -closed ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem GTDef defines GenTop ROUGHS_4:def 25 :
for X being set
for f being Function of (bool X),(bool X)
for b3 being Subset-Family of X holds
( b3 = GenTop f iff for x being object holds
( x in b3 iff ex S being Subset of X st
( S = x & S is f -closed ) ) );

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 ;
coherence
TopRelStr(# C,I,f #) is TopSpace-like
proof end;
end;

registration
existence
ex b1 being TopRelStr st
( b1 is TopSpace-like & b1 is with_equivalence & not b1 is empty )
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;
existence
ex b1 being map of T st
for A being Subset of T holds b1 . A = Cl_Seq A
proof end;
uniqueness
for b1, b2 being map of T st ( for A being Subset of T holds b1 . A = Cl_Seq A ) & ( for A being Subset of T holds b2 . A = Cl_Seq A ) holds
b1 = b2
proof end;
correctness
;
end;

:: deftheorem SeqDef defines Cl_Seq ROUGHS_4:def 26 :
for T being non empty TopSpace
for b2 being map of T holds
( b2 = Cl_Seq T iff for A being Subset of T holds b2 . A = Cl_Seq A );

registration
let T be non empty TopSpace;
coherence
proof end;
end;

registration
existence
ex b1 being non empty TopSpace st b1 is Frechet
by FRECHET:33;
end;

registration
let T be non empty Frechet TopSpace;
coherence
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 :
for T being non empty TopRelStr holds
( T is Natural iff for x being Subset of T holds
( x in the topology of T iff x is LAp T -closed ) );

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 :
for T being non empty TopRelStr holds
( T is naturally_generated iff the topology of T = GenTop (LAp T) );

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
existence
ex b1 being non empty TopRelStr st
( b1 is Natural & b1 is TopSpace-like & b1 is with_equivalence )
proof end;
end;

registration
coherence
for b1 being non empty with_equivalence TopRelStr st b1 is naturally_generated holds
b1 is TopSpace-like
proof end;
end;

registration
existence
ex b1 being non empty TopRelStr st
( b1 is naturally_generated & b1 is TopSpace-like & b1 is with_equivalence )
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 ;
coherence
LAp A is 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 ;
coherence
UAp A is 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
compatibility
Int A = LAp A
;
by LApInt;
identify Cl A with UAp A;
correctness
compatibility
Cl A = UAp A
;
by UApCl;
identify LAp A with Int A;
correctness
compatibility
LAp A = Int A
;
;
identify UAp A with Cl A;
correctness
compatibility
UAp A = Cl A
;
;
identify BndAp A with Fr A;
correctness
compatibility
BndAp A = Fr A
;
;
identify Fr A with BndAp A;
correctness
compatibility
Fr A = 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
for b1 being Subset of T st b1 is 1st_class holds
b1 is exact
by FirstIsExact;
cluster exact -> 1st_class for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is exact holds
b1 is 1st_class
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;
coherence
for b1 being Subset of T st b1 is 2nd_class holds
b1 is rough
;
cluster rough -> 2nd_class for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is rough holds
b1 is 2nd_class
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 ;

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 end;

registration
coherence
for b1 being non empty with_equivalence naturally_generated TopRelStr holds b1 is without_3rd_class_subsets
by ApproxWithout;
existence
ex b1 being TopSpace st b1 is without_3rd_class_subsets
proof end;
end;

registration
let T be TopSpace;
let A be 1st_class Subset of T;
coherence
Border A is empty
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 ;
coherence
Cl A is open
proof end;
cluster Int A -> closed ;
coherence
Int A is closed
proof end;
end;

registration
coherence
for b1 being non empty with_equivalence naturally_generated TopRelStr holds b1 is extremally_disconnected
;
end;

:: 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 () <= 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 () <= 6
proof end;