:: by Adam Grabowski

::

:: Received March 31, 2014

:: Copyright (c) 2014-2017 Association of Mizar Users

definition
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 );

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;

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

( F is cap-closed iff for a, b being Subset of X st a in F & b in F holds

a /\ b in F ) ;

:: 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 );

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;

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

for a being Subset-Family of X st a c= F holds

union a in F;

:: 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 );

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;

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

( {} in F & X in F & F is union-closed & F is V97() );

:: 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() ) );

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

definition

let X be set ;

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

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

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;

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

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

for A, B being Subset of X holds f . (A /\ B) = (f . A) /\ (f . B);

:: 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 );

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

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

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

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

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

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

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

( 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 );

( 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 );

( 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 );

( O is intensive & O is idempotent & O is /\-preserving & O is universe-preserving );

:: 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 ) );

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

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

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

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 ;

for b_{1} being Function of (bool X),(bool X) st b_{1} is \/-preserving holds

b_{1} is c=-monotone

for b_{1} being Function of (bool X),(bool X) st b_{1} is /\-preserving holds

b_{1} is c=-monotone

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

coherence for b

b

proof end;

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

coherence for b

b

proof end;

registration

let X be set ;

coherence

for b_{1} being Function of (bool X),(bool X) st b_{1} = id (bool X) holds

b_{1} is closure

for b_{1} being Function of (bool X),(bool X) st b_{1} = id (bool X) holds

b_{1} is interior

end;
coherence

for b

b

proof end;

coherence for b

b

proof end;

registration

let X be set ;

ex b_{1} being Function of (bool X),(bool X) st

( b_{1} is closure & b_{1} is interior )

end;
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):];

existence ex b

( b

proof end;

registration

let X be set ;

for b_{1} being Function of (bool X),(bool X) st b_{1} is closure holds

b_{1} is preclosure
;

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

coherence for b

b

definition
end;

definition

attr c_{1} is strict ;

struct 1stOpStr -> 1-sorted ;

aggr 1stOpStr(# carrier, FirstOp #) -> 1stOpStr ;

sel FirstOp c_{1} -> Function of (bool the carrier of c_{1}),(bool the carrier of c_{1});

end;
struct 1stOpStr -> 1-sorted ;

aggr 1stOpStr(# carrier, FirstOp #) -> 1stOpStr ;

sel FirstOp c

definition

attr c_{1} is strict ;

struct 2ndOpStr -> 1-sorted ;

aggr 2ndOpStr(# carrier, SecondOp #) -> 2ndOpStr ;

sel SecondOp c_{1} -> Function of (bool the carrier of c_{1}),(bool the carrier of c_{1});

end;
struct 2ndOpStr -> 1-sorted ;

aggr 2ndOpStr(# carrier, SecondOp #) -> 2ndOpStr ;

sel SecondOp c

definition

attr c_{1} is strict ;

struct TwoOpStruct -> 1stOpStr , 2ndOpStr ;

aggr TwoOpStruct(# carrier, FirstOp, SecondOp #) -> TwoOpStruct ;

end;
struct TwoOpStruct -> 1stOpStr , 2ndOpStr ;

aggr TwoOpStruct(# carrier, FirstOp, SecondOp #) -> TwoOpStruct ;

:: 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 );

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

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

IntMap T is interior

end;
coherence

ClMap T is closure

proof end;

coherence IntMap T is interior

proof end;

registration
end;

registration
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 );

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 ;

end;
attr X is with_op-closed_subsets means :OCS: :: ROUGHS_4:def 18

ex A being Subset of X st A is op-closed ;

ex A being Subset of X st A is op-closed ;

:: 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 );

for X being 1stOpStr holds

( X is with_op-closed_subsets iff ex A being Subset of X st A is op-closed );

registration

let X be with_op-closed_subsets 1stOpStr ;

existence

ex b_{1} being Subset of X st b_{1} is op-closed
by OCS;

end;
existence

ex b

:: 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 );

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 ;

end;
attr X is with_op-open_subsets means :OOS: :: ROUGHS_4:def 20

ex A being Subset of X st A is op-open ;

ex A being Subset of X st A is op-open ;

:: 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 );

for X being 2ndOpStr holds

( X is with_op-open_subsets iff ex A being Subset of X st A is op-open );

registration

let X be with_op-open_subsets 2ndOpStr ;

existence

ex b_{1} being Subset of X st b_{1} is op-open
by OOS;

end;
existence

ex b

:: deftheorem defines with_interior ROUGHS_4:def 21 :

for X being 2ndOpStr holds

( X is with_interior iff the SecondOp of X is interior );

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

for X being 2ndOpStr holds

( X is with_preinterior iff the SecondOp of X is preinterior );

registration

existence

ex b_{1} being TwoOpStruct st

( b_{1} is with_closure & b_{1} is with_interior )

end;
ex b

( b

proof end;

definition

attr c_{1} is strict ;

struct 1TopStruct -> 1stOpStr , TopStruct ;

aggr 1TopStruct(# carrier, FirstOp, topology #) -> 1TopStruct ;

end;
struct 1TopStruct -> 1stOpStr , TopStruct ;

aggr 1TopStruct(# carrier, FirstOp, topology #) -> 1TopStruct ;

definition

attr c_{1} is strict ;

struct 2TopStruct -> 2ndOpStr , TopStruct ;

aggr 2TopStruct(# carrier, SecondOp, topology #) -> 2TopStruct ;

end;
struct 2TopStruct -> 2ndOpStr , TopStruct ;

aggr 2TopStruct(# carrier, SecondOp, topology #) -> 2TopStruct ;

registration
end;

registration
end;

definition

let T be 1TopStruct ;

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

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

:: 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 ) ) );

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 ;

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

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

:: 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 ) ) );

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 b_{1} being 1TopStruct st

( b_{1} is with_closure & b_{1} is with_properly_defined_topology )

ex b_{1} being 2TopStruct st

( b_{1} is with_interior & b_{1} is with_properly_defined_Topology )

end;
ex b

( b

proof end;

existence ex b

( b

proof 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 )

for A being Subset of T holds

( A is op-closed iff A is closed )

proof end;

registration

for b_{1} being with_properly_defined_topology 1TopStruct st b_{1} is with_preclosure holds

b_{1} is TopSpace-like
end;

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

coherence for b

b

proof 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 )

for A being Subset of T holds

( A is op-open iff A is open )

proof end;

registration

for b_{1} being with_properly_defined_Topology 2TopStruct st b_{1} is with_preinterior holds

b_{1} is TopSpace-like
end;

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

coherence for b

b

proof 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

for A being Subset of T holds the FirstOp of T . A = Cl A

proof end;

registration

let R be Tolerance_Space;

coherence

LAp R is preinterior

UAp R is preclosure

end;
coherence

LAp R is preinterior

proof end;

coherence UAp R is preclosure

proof end;

registration

let R be Approximation_Space;

coherence

LAp R is interior

UAp R is closure

end;
coherence

LAp R is interior

proof end;

coherence UAp R is closure

proof end;

definition

let X be set ;

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

ex b_{1} being Subset-Family of X st

for x being object holds

( x in b_{1} iff ex S being Subset of X st

( S = x & S is f -closed ) )

for b_{1}, b_{2} being Subset-Family of X st ( for x being object holds

( x in b_{1} iff ex S being Subset of X st

( S = x & S is f -closed ) ) ) & ( for x being object holds

( x in b_{2} iff ex S being Subset of X st

( S = x & S is f -closed ) ) ) holds

b_{1} = b_{2}

end;
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 for x being object holds

( x in it iff ex S being Subset of X st

( S = x & S is f -closed ) );

ex b

for x being object holds

( x in b

( S = x & S is f -closed ) )

proof end;

uniqueness for b

( x in b

( S = x & S is f -closed ) ) ) & ( for x being object holds

( x in b

( S = x & S is f -closed ) ) ) holds

b

proof end;

:: deftheorem GTDef defines GenTop ROUGHS_4:def 25 :

for X being set

for f being Function of (bool X),(bool X)

for b_{3} being Subset-Family of X holds

( b_{3} = GenTop f iff for x being object holds

( x in b_{3} iff ex S being Subset of X st

( S = x & S is f -closed ) ) );

for X being set

for f being Function of (bool X),(bool X)

for b

( b

( x in b

( 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

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;

coherence

TopRelStr(# C,I,f #) is TopSpace-like

end;
let I be Relation of C;

let f be topology-like Subset-Family of C;

coherence

TopRelStr(# C,I,f #) is TopSpace-like

proof end;

registration

existence

ex b_{1} being TopRelStr st

( b_{1} is TopSpace-like & b_{1} is with_equivalence & not b_{1} is empty )

end;
ex b

( b

proof end;

definition

let T be non empty TopSpace;

ex b_{1} being map of T st

for A being Subset of T holds b_{1} . A = Cl_Seq A

for b_{1}, b_{2} being map of T st ( for A being Subset of T holds b_{1} . A = Cl_Seq A ) & ( for A being Subset of T holds b_{2} . A = Cl_Seq A ) holds

b_{1} = b_{2}

;

end;
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 for A being Subset of T holds it . A = Cl_Seq A;

ex b

for A being Subset of T holds b

proof end;

uniqueness for b

b

proof end;

correctness ;

:: deftheorem SeqDef defines Cl_Seq ROUGHS_4:def 26 :

for T being non empty TopSpace

for b_{2} being map of T holds

( b_{2} = Cl_Seq T iff for A being Subset of T holds b_{2} . A = Cl_Seq A );

for T being non empty TopSpace

for b

( b

:: 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 ) );

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

:: 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) );

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 )

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

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

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 b_{1} being non empty TopRelStr st

( b_{1} is Natural & b_{1} is TopSpace-like & b_{1} is with_equivalence )

end;
ex b

( b

proof end;

registration

for b_{1} being non empty with_equivalence TopRelStr st b_{1} is naturally_generated holds

b_{1} is TopSpace-like
end;

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

coherence for b

b

proof end;

registration

existence

ex b_{1} being non empty TopRelStr st

( b_{1} is naturally_generated & b_{1} is TopSpace-like & b_{1} is with_equivalence )

end;
ex b

( b

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

coherence

LAp A is open

end;
let A be Subset of T;

coherence

LAp A is open

proof 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

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 )

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;

coherence

UAp A is closed

end;
let A be Subset of T;

coherence

UAp A is closed

proof 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

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

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;

correctness

compatibility

Int A = LAp A;

by LApInt;

correctness

compatibility

Cl A = UAp A;

by UApCl;

correctness

compatibility

LAp A = Int A;

;

correctness

compatibility

UAp A = Cl A;

;

correctness

compatibility

BndAp A = Fr A;

;

correctness

compatibility

Fr A = BndAp A;

;

end;
let A be Subset of T;

correctness

compatibility

Int A = LAp A;

by LApInt;

correctness

compatibility

Cl A = UAp A;

by UApCl;

correctness

compatibility

LAp A = Int A;

;

correctness

compatibility

UAp A = Cl A;

;

correctness

compatibility

BndAp A = Fr A;

;

correctness

compatibility

Fr A = BndAp A;

;

theorem :: ROUGHS_4:13

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 )

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 )

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 ;

coherence

for b_{1} being Subset of T st b_{1} is 1st_class holds

b_{1} is exact
by FirstIsExact;

coherence

for b_{1} being Subset of T st b_{1} is exact holds

b_{1} is 1st_class
by FirstIsExact;

end;
coherence

for b

b

coherence

for b

b

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 )

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 )

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 ;

coherence

for b_{1} being Subset of T st b_{1} is 2nd_class holds

b_{1} is rough
;

coherence

for b_{1} being Subset of T st b_{1} is rough holds

b_{1} is 2nd_class
by SecondRough;

end;
coherence

for b

b

coherence

for b

b

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;

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

for A being Subset of T holds not A is 3rd_class

proof end;

registration

for b_{1} being non empty with_equivalence naturally_generated TopRelStr holds b_{1} is without_3rd_class_subsets
by ApproxWithout;

existence

ex b_{1} being TopSpace st b_{1} is without_3rd_class_subsets
end;

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

coherence for b

existence

ex b

proof end;

registration
end;

registration

let T be non empty with_equivalence naturally_generated TopRelStr ;

let A be Subset of T;

coherence

Cl A is open

Int A is closed

end;
let A be Subset of T;

coherence

Cl A is open

proof end;

coherence Int A is closed

proof end;

registration

for b_{1} being non empty with_equivalence naturally_generated TopRelStr holds b_{1} is extremally_disconnected
;

end;

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

coherence for b

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)}

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

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)}

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

for A being Subset of T holds card (Kurat14Set A) <= 6

proof end;

:: Cl_Seq from FRECHET2 is important example of preclosure