:: On the Lattice of Intervals and Rough Sets
:: by Adam Grabowski and Magdalena Jastrz\c{e}bska
::
:: Received October 10, 2009
:: Copyright (c) 2009-2011 Association of Mizar Users

begin

definition

let U be set ;
let X, Y be Subset of U;
func Inter (X,Y) -> Subset-Family of U equals :: INTERVA1:def 1
{ A where A is Subset of U : ( X c= A & A c= Y ) } ;
coherence
{ A where A is Subset of U : ( X c= A & A c= Y ) } is Subset-Family of U

proof end;

end;

:: deftheorem defines Inter INTERVA1:def 1 :
for U being set
for X, Y being Subset of U holds Inter (X,Y) = { A where A is Subset of U : ( X c= A & A c= Y ) } ;

theorem Th1: :: INTERVA1:1

for U being set
for X, Y being Subset of U
for x being set holds
( x in Inter (X,Y) iff ( X c= x & x c= Y ) )

proof end;

theorem Th2: :: INTERVA1:2

for U being set
for X, Y being Subset of U st Inter (X,Y) <> {} holds
( X in Inter (X,Y) & Y in Inter (X,Y) )

proof end;

theorem Th3: :: INTERVA1:3

for U being set
for A, B being Subset of U st not A c= B holds
Inter (A,B) = {}

proof end;

theorem :: INTERVA1:4

for U being set
for A, B being Subset of U st Inter (A,B) = {} holds
not A c= B by Th1;

theorem Th5: :: INTERVA1:5

for U being set
for A, B being Subset of U st Inter (A,B) <> {} holds
A c= B

proof end;

theorem Th6: :: INTERVA1:6

for U being set
for A, B, C, D being Subset of U st Inter (A,B) <> {} & Inter (A,B) = Inter (C,D) holds
( A = C & B = D )

proof end;

theorem Th7: :: INTERVA1:7

for U being non empty set
for A being non empty Subset of U holds Inter (A,({} U)) = {}

proof end;

theorem Th8: :: INTERVA1:8

for U being set
for A being Subset of U holds Inter (A,A) = {A}

proof end;

definition

let U be set ;
mode IntervalSet of U -> Subset-Family of U means :Def2: :: INTERVA1:def 2
ex A, B being Subset of U st it = Inter (A,B);
existence
ex b₁ being Subset-Family of U ex A, B being Subset of U st b₁ = Inter (A,B)

proof end;

end;

:: deftheorem Def2 defines IntervalSet INTERVA1:def 2 :
for U being set
for b₂ being Subset-Family of U holds
( b₂ is IntervalSet of U iff ex A, B being Subset of U st b₂ = Inter (A,B) );

theorem :: INTERVA1:9

for U being non empty set holds {} is IntervalSet of U

proof end;

theorem Th10: :: INTERVA1:10

for U being non empty set
for A being Subset of U holds {A} is IntervalSet of U

proof end;

definition

let U be set ;
let A, B be Subset of U;
:: original: Inter
redefine func Inter (A,B) -> IntervalSet of U;
correctness
coherence
Inter (A,B) is IntervalSet of U;
by Def2;

end;

registration

let U be non empty set ;
cluster non empty IntervalSet of U;
existence
not for b₁ being IntervalSet of U holds b₁ is empty

proof end;

end;

theorem Th11: :: INTERVA1:11

for U being non empty set
for A being set holds
( A is non empty IntervalSet of U iff ex A1, A2 being Subset of U st
( A1 c= A2 & A = Inter (A1,A2) ) )

proof end;

theorem Th12: :: INTERVA1:12

for U being non empty set
for A1, A2, B1, B2 being Subset of U st A1 c= A2 & B1 c= B2 holds
INTERSECTION ((Inter (A1,A2)),(Inter (B1,B2))) = { C where C is Subset of U : ( A1 /\ B1 c= C & C c= A2 /\ B2 ) }

proof end;

theorem Th13: :: INTERVA1:13

for U being non empty set
for A1, A2, B1, B2 being Subset of U st A1 c= A2 & B1 c= B2 holds
UNION ((Inter (A1,A2)),(Inter (B1,B2))) = { C where C is Subset of U : ( A1 \/ B1 c= C & C c= A2 \/ B2 ) }

proof end;

definition

let U be non empty set ;
let A, B be non empty IntervalSet of U;
func A _/\_ B -> IntervalSet of U equals :: INTERVA1:def 3
INTERSECTION (A,B);
coherence
INTERSECTION (A,B) is IntervalSet of U

proof end;

func A _\/_ B -> IntervalSet of U equals :: INTERVA1:def 4
UNION (A,B);
coherence
UNION (A,B) is IntervalSet of U

proof end;

end;

:: deftheorem defines _/\_ INTERVA1:def 3 :
for U being non empty set
for A, B being non empty IntervalSet of U holds A _/\_ B = INTERSECTION (A,B);

:: deftheorem defines _\/_ INTERVA1:def 4 :
for U being non empty set
for A, B being non empty IntervalSet of U holds A _\/_ B = UNION (A,B);

registration

let U be non empty set ;
let A, B be non empty IntervalSet of U;
cluster A _/\_ B -> non empty ;
coherence
not A _/\_ B is empty by TOPGEN_4:31;
cluster A _\/_ B -> non empty ;
coherence
not A _\/_ B is empty by TOPGEN_4:30;

end;

definition

let U be non empty set ;
let A be non empty IntervalSet of U;
func A ``1 -> Subset of U means :Def5: :: INTERVA1:def 5
ex B being Subset of U st A = Inter (it,B);
existence
ex b₁, B being Subset of U st A = Inter (b₁,B)

proof end;

uniqueness
for b₁, b₂ being Subset of U st ex B being Subset of U st A = Inter (b₁,B) & ex B being Subset of U st A = Inter (b₂,B) holds
b₁ = b₂ by Th6;
func A ``2 -> Subset of U means :Def6: :: INTERVA1:def 6
ex B being Subset of U st A = Inter (B,it);
existence
ex b₁, B being Subset of U st A = Inter (B,b₁)

proof end;

uniqueness
for b₁, b₂ being Subset of U st ex B being Subset of U st A = Inter (B,b₁) & ex B being Subset of U st A = Inter (B,b₂) holds
b₁ = b₂ by Th6;

end;

:: deftheorem Def5 defines ``1 INTERVA1:def 5 :
for U being non empty set
for A being non empty IntervalSet of U
for b<sub>3</sub> being Subset of U holds
( b<sub>3</sub> = A ``1 iff ex B being Subset of U st A = Inter (b₃,B) );

:: deftheorem Def6 defines ``2 INTERVA1:def 6 :
for U being non empty set
for A being non empty IntervalSet of U
for b<sub>3</sub> being Subset of U holds
( b<sub>3</sub> = A ``2 iff ex B being Subset of U st A = Inter (B,b₃) );

theorem Th14: :: INTERVA1:14

for U being non empty set
for A being non empty IntervalSet of U
for X being set holds
( X in A iff ( A ``1 c= X & X c= A ``2 ) )

proof end;

theorem Th15: :: INTERVA1:15

for U being non empty set
for A being non empty IntervalSet of U holds A = Inter ((A ``1),(A ``2))

proof end;

theorem Th16: :: INTERVA1:16

for U being non empty set
for A being non empty IntervalSet of U holds A ``1 c= A ``2

proof end;

theorem Th17: :: INTERVA1:17

for U being non empty set
for A, B being non empty IntervalSet of U holds A _\/_ B = Inter (((A ``1) \/ (B ``1)),((A ``2) \/ (B ``2)))

proof end;

theorem Th18: :: INTERVA1:18

for U being non empty set
for A, B being non empty IntervalSet of U holds A _/\_ B = Inter (((A ``1) /\ (B ``1)),((A ``2) /\ (B ``2)))

proof end;

definition

let U be non empty set ;
let A, B be non empty IntervalSet of U;
:: original: =
redefine pred A = B means :: INTERVA1:def 7
( A ``1 = B ``1 & A ``2 = B ``2 );
compatibility
( A = B iff ( A ``1 = B ``1 & A ``2 = B ``2 ) )

proof end;

end;

:: deftheorem defines = INTERVA1:def 7 :
for U being non empty set
for A, B being non empty IntervalSet of U holds
( A = B iff ( A ``1 = B ``1 & A ``2 = B ``2 ) );

theorem :: INTERVA1:19

for U being non empty set
for A being non empty IntervalSet of U holds A _\/_ A = A

proof end;

theorem :: INTERVA1:20

for U being non empty set
for A being non empty IntervalSet of U holds A _/\_ A = A

proof end;

theorem :: INTERVA1:21

for U being non empty set
for A, B being non empty IntervalSet of U holds A _\/_ B = B _\/_ A ;

theorem :: INTERVA1:22

for U being non empty set
for A, B being non empty IntervalSet of U holds A _/\_ B = B _/\_ A ;

theorem Th23: :: INTERVA1:23

for U being non empty set
for A, B, C being non empty IntervalSet of U holds (A _\/_ B) _\/_ C = A _\/_ (B _\/_ C)

proof end;

theorem Th24: :: INTERVA1:24

for U being non empty set
for A, B, C being non empty IntervalSet of U holds (A _/\_ B) _/\_ C = A _/\_ (B _/\_ C)

proof end;

Lm1: for X being set
for A, B, C being Subset-Family of X holds UNION (A,(INTERSECTION (B,C))) c= INTERSECTION ((UNION (A,B)),(UNION (A,C)))

proof end;

definition

let X be set ;
let F be Subset-Family of X;
attr F is ordered means :Def8: :: INTERVA1:def 8
ex A, B being set st
( A in F & B in F & ( for Y being set holds
( Y in F iff ( A c= Y & Y c= B ) ) ) );

end;

:: deftheorem Def8 defines ordered INTERVA1:def 8 :
for X being set
for F being Subset-Family of X holds
( F is ordered iff ex A, B being set st
( A in F & B in F & ( for Y being set holds
( Y in F iff ( A c= Y & Y c= B ) ) ) ) );

registration

let X be set ;
cluster non empty ordered Element of bool (bool X);
existence
ex b₁ being Subset-Family of X st
( not b₁ is empty & b₁ is ordered )

proof end;

end;

theorem Th25: :: INTERVA1:25

for U being non empty set
for A, B being Subset of U st A c= B holds
Inter (A,B) is non empty ordered Subset-Family of U

proof end;

theorem Th26: :: INTERVA1:26

for U being non empty set
for A being non empty IntervalSet of U holds A is non empty ordered Subset-Family of U

proof end;

notation

let X be set ;
synonym min X for meet X;
synonym max X for union X;

end;

definition

let X be set ;
let F be non empty ordered Subset-Family of X;
:: original: min
redefine func min F -> Element of F;
correctness
coherence
min F is Element of F;

proof end;

:: original: max
redefine func max F -> Element of F;
correctness
coherence
max F is Element of F;

proof end;

end;

Lm2: for X being set
for F being non empty ordered Subset-Family of X
for G being set st G in F holds
( G = min F iff for Y being set st Y in F holds
G c= Y )

proof end;

Lm3: for X being set
for F being non empty ordered Subset-Family of X
for G being set st G in F holds
( G = max F iff for Y being set st Y in F holds
Y c= G )

proof end;

theorem Th27: :: INTERVA1:27

for U being non empty set
for A, B being Subset of U
for F being non empty ordered Subset-Family of U st F = Inter (A,B) holds
( min F = A & max F = B )

proof end;

theorem Th28: :: INTERVA1:28

for X, Y being set
for A being non empty ordered Subset-Family of X holds
( Y in A iff ( min A c= Y & Y c= max A ) )

proof end;

Lm4: for U being non empty set
for A being non empty IntervalSet of U holds A is non empty ordered Subset-Family of U
by Th26;

theorem Th29: :: INTERVA1:29

for X being set
for A, B, C being non empty ordered Subset-Family of X holds UNION (A,(INTERSECTION (B,C))) = INTERSECTION ((UNION (A,B)),(UNION (A,C)))

proof end;

Lm5: for X being set
for A, B, C being Subset-Family of X holds INTERSECTION (A,(UNION (B,C))) c= UNION ((INTERSECTION (A,B)),(INTERSECTION (A,C)))

proof end;

theorem Th30: :: INTERVA1:30

for X being set
for A, B, C being non empty ordered Subset-Family of X holds INTERSECTION (A,(UNION (B,C))) = UNION ((INTERSECTION (A,B)),(INTERSECTION (A,C)))

proof end;

theorem :: INTERVA1:31

for U being non empty set
for A, B, C being non empty IntervalSet of U holds A _\/_ (B _/\_ C) = (A _\/_ B) _/\_ (A _\/_ C)

proof end;

theorem :: INTERVA1:32

for U being non empty set
for A, B, C being non empty IntervalSet of U holds A _/\_ (B _\/_ C) = (A _/\_ B) _\/_ (A _/\_ C)

proof end;

theorem Th33: :: INTERVA1:33

for X being set
for A, B being non empty ordered Subset-Family of X holds INTERSECTION (A,(UNION (A,B))) = A

proof end;

theorem Th34: :: INTERVA1:34

for X being set
for A, B being non empty ordered Subset-Family of X holds UNION ((INTERSECTION (A,B)),B) = B

proof end;

theorem Th35: :: INTERVA1:35

for U being non empty set
for A, B being non empty IntervalSet of U holds A _/\_ (A _\/_ B) = A

proof end;

theorem Th36: :: INTERVA1:36

for U being non empty set
for A, B being non empty IntervalSet of U holds (A _/\_ B) _\/_ B = B

proof end;

begin

theorem Th37: :: INTERVA1:37

for U being non empty set
for A, B being Subset-Family of U holds DIFFERENCE (A,B) is Subset-Family of U

proof end;

theorem Th38: :: INTERVA1:38

for U being non empty set
for A, B being non empty ordered Subset-Family of U holds DIFFERENCE (A,B) = { C where C is Subset of U : ( (min A) \ (max B) c= C & C c= (max A) \ (min B) ) }

proof end;

theorem Th39: :: INTERVA1:39

for U being non empty set
for A1, A2, B1, B2 being Subset of U st A1 c= A2 & B1 c= B2 holds
DIFFERENCE ((Inter (A1,A2)),(Inter (B1,B2))) = { C where C is Subset of U : ( A1 \ B2 c= C & C c= A2 \ B1 ) }

proof end;

definition

let U be non empty set ;
let A, B be non empty IntervalSet of U;
func A _\_ B -> IntervalSet of U equals :: INTERVA1:def 9
DIFFERENCE (A,B);
coherence
DIFFERENCE (A,B) is IntervalSet of U

proof end;

end;

:: deftheorem defines _\_ INTERVA1:def 9 :
for U being non empty set
for A, B being non empty IntervalSet of U holds A _\_ B = DIFFERENCE (A,B);

registration

let U be non empty set ;
let A, B be non empty IntervalSet of U;
cluster A _\_ B -> non empty ;
coherence
not A _\_ B is empty

proof end;

end;

theorem Th40: :: INTERVA1:40

for U being non empty set
for A, B being non empty IntervalSet of U holds A _\_ B = Inter (((A ``1) \ (B ``2)),((A ``2) \ (B ``1)))

proof end;

theorem Th41: :: INTERVA1:41

for U being non empty set
for A, C being non empty IntervalSet of U
for X, Y being Subset of U st A = Inter (X,Y) holds
A _\_ C = Inter ((X \ (C ``2)),(Y \ (C ``1)))

proof end;

theorem Th42: :: INTERVA1:42

for U being non empty set
for A, C being non empty IntervalSet of U
for X, Y, W, Z being Subset of U st A = Inter (X,Y) & C = Inter (W,Z) holds
A _\_ C = Inter ((X \ Z),(Y \ W))

proof end;

theorem Th43: :: INTERVA1:43

for U being non empty set holds Inter (([#] U),([#] U)) is non empty IntervalSet of U

proof end;

theorem Th44: :: INTERVA1:44

for U being non empty set holds Inter (({} U),({} U)) is non empty IntervalSet of U

proof end;

registration

let U be non empty set ;
cluster Inter (([#] U),([#] U)) -> non empty ;
coherence
not Inter (([#] U),([#] U)) is empty by Th43;
cluster Inter (({} U),({} U)) -> non empty ;
coherence
not Inter (({} U),({} U)) is empty by Th44;

end;

definition

let U be non empty set ;
let A be non empty IntervalSet of U;
func A ^ -> non empty IntervalSet of U equals :: INTERVA1:def 10
(Inter (([#] U),([#] U))) _\_ A;
coherence
(Inter (([#] U),([#] U))) _\_ A is non empty IntervalSet of U ;

end;

:: deftheorem defines ^ INTERVA1:def 10 :
for U being non empty set
for A being non empty IntervalSet of U holds A ^ = (Inter (([#] U),([#] U))) _\_ A;

theorem Th45: :: INTERVA1:45

for U being non empty set
for A being non empty IntervalSet of U holds A ^ = Inter (((A ``2) `),((A ``1) `)) by Th41;

theorem Th46: :: INTERVA1:46

for U being non empty set
for A being non empty IntervalSet of U
for X, Y being Subset of U st A = Inter (X,Y) & X c= Y holds
A ^ = Inter ((Y `),(X `))

proof end;

theorem :: INTERVA1:47

for U being non empty set holds (Inter (({} U),({} U))) ^ = Inter (([#] U),([#] U))

proof end;

theorem :: INTERVA1:48

for U being non empty set holds (Inter (([#] U),([#] U))) ^ = Inter (({} U),({} U))

proof end;

begin

theorem :: INTERVA1:49

for U being non empty set ex A being non empty IntervalSet of U st (A _/\_ A) ^ <> Inter (({} U),({} U))

proof end;

theorem :: INTERVA1:50

for U being non empty set ex A being non empty IntervalSet of U st (A _\/_ A) ^ <> Inter (([#] U),([#] U))

proof end;

theorem :: INTERVA1:51

for U being non empty set ex A being non empty IntervalSet of U st A _\_ A <> Inter (({} U),({} U))

proof end;

theorem :: INTERVA1:52

for U being non empty set
for A being non empty IntervalSet of U holds U in A _\/_ (A ^)

proof end;

theorem :: INTERVA1:53

for U being non empty set
for A being non empty IntervalSet of U holds {} in A _/\_ (A ^)

proof end;

theorem :: INTERVA1:54

for U being non empty set
for A being non empty IntervalSet of U holds {} in A _\_ A

proof end;

begin

definition

let U be non empty set ;
func IntervalSets U -> non empty set means :Def11: :: INTERVA1:def 11
for x being set holds
( x in it iff x is non empty IntervalSet of U );
existence
ex b₁ being non empty set st
for x being set holds
( x in b₁ iff x is non empty IntervalSet of U )

proof end;

uniqueness
for b₁, b₂ being non empty set st ( for x being set holds
( x in b₁ iff x is non empty IntervalSet of U ) ) & ( for x being set holds
( x in b₂ iff x is non empty IntervalSet of U ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def11 defines IntervalSets INTERVA1:def 11 :
for U, b₂ being non empty set holds
( b₂ = IntervalSets U iff for x being set holds
( x in b₂ iff x is non empty IntervalSet of U ) );

definition

let U be non empty set ;
func InterLatt U -> non empty strict LattStr means :Def12: :: INTERVA1:def 12
( the carrier of it = IntervalSets U & ( for a, b being Element of the carrier of it
for a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds
( the L_join of it . (a,b) = a9 _\/_ b9 & the L_meet of it . (a,b) = a9 _/\_ b9 ) ) );
existence
ex b₁ being non empty strict LattStr st
( the carrier of b₁ = IntervalSets U & ( for a, b being Element of the carrier of b₁
for a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds
( the L_join of b₁ . (a,b) = a9 _\/_ b9 & the L_meet of b₁ . (a,b) = a9 _/\_ b9 ) ) )

proof end;

uniqueness
for b₁, b₂ being non empty strict LattStr st the carrier of b₁ = IntervalSets U & ( for a, b being Element of the carrier of b₁
for a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds
( the L_join of b₁ . (a,b) = a9 _\/_ b9 & the L_meet of b₁ . (a,b) = a9 _/\_ b9 ) ) & the carrier of b₂ = IntervalSets U & ( for a, b being Element of the carrier of b₂
for a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds
( the L_join of b₂ . (a,b) = a9 _\/_ b9 & the L_meet of b₂ . (a,b) = a9 _/\_ b9 ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def12 defines InterLatt INTERVA1:def 12 :
for U being non empty set
for b₂ being non empty strict LattStr holds
( b₂ = InterLatt U iff ( the carrier of b₂ = IntervalSets U & ( for a, b being Element of the carrier of b₂
for a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds
( the L_join of b₂ . (a,b) = a9 _\/_ b9 & the L_meet of b₂ . (a,b) = a9 _/\_ b9 ) ) ) );

registration

let U be non empty set ;
cluster InterLatt U -> non empty strict Lattice-like ;
correctness
coherence
InterLatt U is Lattice-like ;

proof end;

end;

definition

let X be Tolerance_Space;
mode RoughSet of X -> Element of [:(bool the carrier of X),(bool the carrier of X):] means :Def13: :: INTERVA1:def 13
verum;
existence
ex b₁ being Element of [:(bool the carrier of X),(bool the carrier of X):] st verum ;

end;

:: deftheorem Def13 defines RoughSet INTERVA1:def 13 :
for X being Tolerance_Space
for b₂ being Element of [:(bool the carrier of X),(bool the carrier of X):] holds
( b₂ is RoughSet of X iff verum );

theorem Th55: :: INTERVA1:55

for X being Tolerance_Space
for A being RoughSet of X ex B, C being Subset of X st A = [B,C]

proof end;

definition

let X be Tolerance_Space;
let A be Subset of X;
func RS A -> RoughSet of X equals :: INTERVA1:def 14
[(LAp A),(UAp A)];
coherence
[(LAp A),(UAp A)] is RoughSet of X

proof end;

end;

:: deftheorem defines RS INTERVA1:def 14 :
for X being Tolerance_Space
for A being Subset of X holds RS A = [(LAp A),(UAp A)];

definition

let X be Tolerance_Space;
let A be RoughSet of X;
func LAp A -> Subset of X equals :: INTERVA1:def 15
A `1 ;
coherence
A `1 is Subset of X

proof end;

func UAp A -> Subset of X equals :: INTERVA1:def 16
A `2 ;
coherence
A `2 is Subset of X

proof end;

end;

:: deftheorem defines LAp INTERVA1:def 15 :
for X being Tolerance_Space
for A being RoughSet of X holds LAp A = A `1 ;

:: deftheorem defines UAp INTERVA1:def 16 :
for X being Tolerance_Space
for A being RoughSet of X holds UAp A = A `2 ;

definition

let X be Tolerance_Space;
let A, B be RoughSet of X;
:: original: =
redefine pred A = B means :Def17: :: INTERVA1:def 17
( LAp A = LAp B & UAp A = UAp B );
compatibility
( A = B iff ( LAp A = LAp B & UAp A = UAp B ) )

proof end;

end;

:: deftheorem Def17 defines = INTERVA1:def 17 :
for X being Tolerance_Space
for A, B being RoughSet of X holds
( A = B iff ( LAp A = LAp B & UAp A = UAp B ) );

definition

let X be Tolerance_Space;
let A, B be RoughSet of X;
func A _\/_ B -> RoughSet of X equals :: INTERVA1:def 18
[((LAp A) \/ (LAp B)),((UAp A) \/ (UAp B))];
coherence
[((LAp A) \/ (LAp B)),((UAp A) \/ (UAp B))] is RoughSet of X

proof end;

func A _/\_ B -> RoughSet of X equals :: INTERVA1:def 19
[((LAp A) /\ (LAp B)),((UAp A) /\ (UAp B))];
coherence
[((LAp A) /\ (LAp B)),((UAp A) /\ (UAp B))] is RoughSet of X

proof end;

end;

:: deftheorem defines _\/_ INTERVA1:def 18 :
for X being Tolerance_Space
for A, B being RoughSet of X holds A _\/_ B = [((LAp A) \/ (LAp B)),((UAp A) \/ (UAp B))];

:: deftheorem defines _/\_ INTERVA1:def 19 :
for X being Tolerance_Space
for A, B being RoughSet of X holds A _/\_ B = [((LAp A) /\ (LAp B)),((UAp A) /\ (UAp B))];

theorem Th56: :: INTERVA1:56

for X being Tolerance_Space
for A, B being RoughSet of X holds LAp (A _\/_ B) = (LAp A) \/ (LAp B) by MCART_1:7;

theorem Th57: :: INTERVA1:57

for X being Tolerance_Space
for A, B being RoughSet of X holds UAp (A _\/_ B) = (UAp A) \/ (UAp B) by MCART_1:7;

theorem Th58: :: INTERVA1:58

for X being Tolerance_Space
for A, B being RoughSet of X holds LAp (A _/\_ B) = (LAp A) /\ (LAp B) by MCART_1:7;

theorem Th59: :: INTERVA1:59

for X being Tolerance_Space
for A, B being RoughSet of X holds UAp (A _/\_ B) = (UAp A) /\ (UAp B) by MCART_1:7;

theorem :: INTERVA1:60

for X being Tolerance_Space
for A being RoughSet of X holds A _\/_ A = A

proof end;

theorem Th61: :: INTERVA1:61

for X being Tolerance_Space
for A being RoughSet of X holds A _/\_ A = A

proof end;

theorem :: INTERVA1:62

for X being Tolerance_Space
for A, B being RoughSet of X holds A _\/_ B = B _\/_ A ;

theorem :: INTERVA1:63

for X being Tolerance_Space
for A, B being RoughSet of X holds A _/\_ B = B _/\_ A ;

theorem Th64: :: INTERVA1:64

for X being Tolerance_Space
for A, B, C being RoughSet of X holds (A _\/_ B) _\/_ C = A _\/_ (B _\/_ C)

proof end;

theorem Th65: :: INTERVA1:65

for X being Tolerance_Space
for A, B, C being RoughSet of X holds (A _/\_ B) _/\_ C = A _/\_ (B _/\_ C)

proof end;

theorem Th66: :: INTERVA1:66

for X being Tolerance_Space
for A, B, C being RoughSet of X holds A _/\_ (B _\/_ C) = (A _/\_ B) _\/_ (A _/\_ C)

proof end;

theorem Th67: :: INTERVA1:67

for X being Tolerance_Space
for A, B being RoughSet of X holds A _\/_ (A _/\_ B) = A

proof end;

theorem :: INTERVA1:68

for X being Tolerance_Space
for A, B being RoughSet of X holds A _/\_ (A _\/_ B) = A

proof end;

begin

definition

let X be Tolerance_Space;
func RoughSets X -> set means :Def20: :: INTERVA1:def 20
for x being set holds
( x in it iff x is RoughSet of X );
existence
ex b₁ being set st
for x being set holds
( x in b₁ iff x is RoughSet of X )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being set holds
( x in b₁ iff x is RoughSet of X ) ) & ( for x being set holds
( x in b₂ iff x is RoughSet of X ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def20 defines RoughSets INTERVA1:def 20 :
for X being Tolerance_Space
for b₂ being set holds
( b₂ = RoughSets X iff for x being set holds
( x in b₂ iff x is RoughSet of X ) );

registration

let X be Tolerance_Space;
cluster RoughSets X -> non empty ;
coherence
not RoughSets X is empty

proof end;

end;

definition

let X be Tolerance_Space;
let R be Element of RoughSets X;
func @ R -> RoughSet of X equals :: INTERVA1:def 21
R;
coherence
R is RoughSet of X by Def20;

end;

:: deftheorem defines @ INTERVA1:def 21 :
for X being Tolerance_Space
for R being Element of RoughSets X holds @ R = R;

definition

let X be Tolerance_Space;
let R be RoughSet of X;
func R @ -> Element of RoughSets X equals :: INTERVA1:def 22
R;
coherence
R is Element of RoughSets X by Def20;

end;

:: deftheorem defines @ INTERVA1:def 22 :
for X being Tolerance_Space
for R being RoughSet of X holds R @ = R;

definition

let X be Tolerance_Space;
func RSLattice X -> strict LattStr means :Def23: :: INTERVA1:def 23
( the carrier of it = RoughSets X & ( for A, B being Element of RoughSets X
for A9, B9 being RoughSet of X st A = A9 & B = B9 holds
( the L_join of it . (A,B) = A9 _\/_ B9 & the L_meet of it . (A,B) = A9 _/\_ B9 ) ) );
existence
ex b₁ being strict LattStr st
( the carrier of b₁ = RoughSets X & ( for A, B being Element of RoughSets X
for A9, B9 being RoughSet of X st A = A9 & B = B9 holds
( the L_join of b₁ . (A,B) = A9 _\/_ B9 & the L_meet of b₁ . (A,B) = A9 _/\_ B9 ) ) )

proof end;

uniqueness
for b₁, b₂ being strict LattStr st the carrier of b₁ = RoughSets X & ( for A, B being Element of RoughSets X
for A9, B9 being RoughSet of X st A = A9 & B = B9 holds
( the L_join of b₁ . (A,B) = A9 _\/_ B9 & the L_meet of b₁ . (A,B) = A9 _/\_ B9 ) ) & the carrier of b₂ = RoughSets X & ( for A, B being Element of RoughSets X
for A9, B9 being RoughSet of X st A = A9 & B = B9 holds
( the L_join of b₂ . (A,B) = A9 _\/_ B9 & the L_meet of b₂ . (A,B) = A9 _/\_ B9 ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def23 defines RSLattice INTERVA1:def 23 :
for X being Tolerance_Space
for b₂ being strict LattStr holds
( b₂ = RSLattice X iff ( the carrier of b₂ = RoughSets X & ( for A, B being Element of RoughSets X
for A9, B9 being RoughSet of X st A = A9 & B = B9 holds
( the L_join of b₂ . (A,B) = A9 _\/_ B9 & the L_meet of b₂ . (A,B) = A9 _/\_ B9 ) ) ) );

registration

let X be Tolerance_Space;
cluster RSLattice X -> non empty strict ;
coherence
not RSLattice X is empty

proof end;

end;

Lm6: for X being Tolerance_Space
for a, b being Element of (RSLattice X) holds a "\/" b = b "\/" a

proof end;

Lm7: for X being Tolerance_Space
for a, b, c being Element of (RSLattice X) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c

proof end;

Lm8: for X being Tolerance_Space
for K, L being Element of RoughSets X holds the L_join of (RSLattice X) . (( the L_meet of (RSLattice X) . (K,L)),L) = L

proof end;

Lm9: for X being Tolerance_Space
for a, b being Element of (RSLattice X) holds (a "/\" b) "\/" b = b

proof end;

Lm10: for X being Tolerance_Space
for a, b being Element of (RSLattice X) holds a "/\" b = b "/\" a

proof end;

Lm11: for X being Tolerance_Space
for a, b, c being Element of (RSLattice X) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c

proof end;

Lm12: for X being Tolerance_Space
for K, L, M being Element of RoughSets X holds the L_meet of (RSLattice X) . (K,( the L_join of (RSLattice X) . (L,M))) = the L_join of (RSLattice X) . (( the L_meet of (RSLattice X) . (K,L)),( the L_meet of (RSLattice X) . (K,M)))

proof end;

Lm13: for X being Tolerance_Space
for a, b being Element of (RSLattice X) holds a "/\" (a "\/" b) = a

proof end;

registration

let X be Tolerance_Space;
cluster RSLattice X -> strict Lattice-like ;
coherence
RSLattice X is Lattice-like

proof end;

end;

registration

let X be Tolerance_Space;
cluster RSLattice X -> strict distributive ;
coherence
RSLattice X is distributive

proof end;

end;

definition

let X be Tolerance_Space;
func ERS X -> RoughSet of X equals :: INTERVA1:def 24
[{},{}];
coherence
[{},{}] is RoughSet of X

proof end;

end;

:: deftheorem defines ERS INTERVA1:def 24 :
for X being Tolerance_Space holds ERS X = [{},{}];

Lm14: for X being Tolerance_Space holds ERS X in RoughSets X
by Def20;

theorem Th69: :: INTERVA1:69

for X being Tolerance_Space
for A being RoughSet of X holds (ERS X) _\/_ A = A

proof end;

definition

let X be Tolerance_Space;
func TRS X -> RoughSet of X equals :: INTERVA1:def 25
[([#] X),([#] X)];
coherence
[([#] X),([#] X)] is RoughSet of X

proof end;

end;

:: deftheorem defines TRS INTERVA1:def 25 :
for X being Tolerance_Space holds TRS X = [([#] X),([#] X)];

Lm15: for X being Tolerance_Space holds TRS X in RoughSets X
by Def20;

theorem Th70: :: INTERVA1:70

for X being Tolerance_Space
for A being RoughSet of X holds (TRS X) _/\_ A = A

proof end;

registration

let X be Tolerance_Space;
cluster RSLattice X -> strict bounded ;
coherence
RSLattice X is bounded

proof end;

end;

theorem Th71: :: INTERVA1:71

for X being Tolerance_Space
for A, B being Element of (RSLattice X)
for A9, B9 being RoughSet of X st A = A9 & B = B9 holds
( A [= B iff ( LAp A9 c= LAp B9 & UAp A9 c= UAp B9 ) )

proof end;

Lm16: for X being Tolerance_Space holds RSLattice X is complete

proof end;

registration

let X be Tolerance_Space;
cluster RSLattice X -> strict complete ;
coherence
RSLattice X is complete by Lm16;

end;