:: by Adam Grabowski and Magdalena Jastrz\c{e}bska

::

:: Received October 10, 2009

:: Copyright (c) 2009-2016 Association of Mizar Users

definition

let U be set ;

let X, Y be Subset of U;

{ A where A is Subset of U : ( X c= A & A c= Y ) } is Subset-Family of U

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

{ A where A is Subset of U : ( X c= A & A c= Y ) } is Subset-Family of U

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

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

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

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 :: INTERVA1:4

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 )

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;

definition

let U be set ;

ex b_{1} being Subset-Family of U ex A, B being Subset of U st b_{1} = Inter (A,B)

end;
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 A, B being Subset of U st it = Inter (A,B);

ex b

proof end;

:: deftheorem Def2 defines IntervalSet INTERVA1:def 2 :

for U being set

for b_{2} being Subset-Family of U holds

( b_{2} is IntervalSet of U iff ex A, B being Subset of U st b_{2} = Inter (A,B) );

for U being set

for b

( b

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

registration

let U be non empty set ;

existence

not for b_{1} being IntervalSet of U holds b_{1} is empty

end;
existence

not for b

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

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

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

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;

coherence

INTERSECTION (A,B) is IntervalSet of U

UNION (A,B) is IntervalSet of U

end;
let A, B be non empty IntervalSet of U;

coherence

INTERSECTION (A,B) is IntervalSet of U

proof end;

coherence UNION (A,B) is IntervalSet of U

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

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

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;

coherence

not A _/\_ B is empty by TOPGEN_4:31;

coherence

not A _\/_ B is empty by TOPGEN_4:30;

end;
let A, B be non empty IntervalSet of U;

coherence

not A _/\_ B is empty by TOPGEN_4:31;

coherence

not A _\/_ B is empty by TOPGEN_4:30;

definition

let U be non empty set ;

let A be non empty IntervalSet of U;

ex b_{1}, B being Subset of U st A = Inter (b_{1},B)

for b_{1}, b_{2} being Subset of U st ex B being Subset of U st A = Inter (b_{1},B) & ex B being Subset of U st A = Inter (b_{2},B) holds

b_{1} = b_{2}
by Th6;

ex b_{1}, B being Subset of U st A = Inter (B,b_{1})

for b_{1}, b_{2} being Subset of U st ex B being Subset of U st A = Inter (B,b_{1}) & ex B being Subset of U st A = Inter (B,b_{2}) holds

b_{1} = b_{2}
by Th6;

end;
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 being Subset of U st A = Inter (it,B);

ex b

proof end;

uniqueness for b

b

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 being Subset of U st A = Inter (B,it);

ex b

proof end;

uniqueness for b

b

:: deftheorem Def5 defines ``1 INTERVA1:def 5 :

for U being non empty set

for A being non empty IntervalSet of U

for b_{3} being Subset of U holds

( b_{3} = A ``1 iff ex B being Subset of U st A = Inter (b_{3},B) );

for U being non empty set

for A being non empty IntervalSet of U

for 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_{3} being Subset of U holds

( b_{3} = A ``2 iff ex B being Subset of U st A = Inter (B,b_{3}) );

for U being non empty set

for A being non empty IntervalSet of U

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

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

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

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;

compatibility

( A = B iff ( A ``1 = B ``1 & A ``2 = B ``2 ) )

end;
let A, B be non empty IntervalSet of U;

compatibility

( A = B iff ( A ``1 = B ``1 & A ``2 = B ``2 ) )

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

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:21

theorem :: INTERVA1:22

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)

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)

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;

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

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 ;

existence

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

( not b_{1} is empty & b_{1} is ordered )

end;
existence

ex b

( not b

proof 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

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

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

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

redefine func max F -> Element of F;

correctness

coherence

max F is Element of F;

end;
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: maxredefine func max F -> Element of F;

correctness

coherence

max F is Element of F;

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

by SETFAM_1:3;

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 )

by ZFMISC_1:74;

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 )

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

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

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

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)

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)

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

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

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

proof end;

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

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

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

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;

coherence

DIFFERENCE (A,B) is IntervalSet of U

end;
let A, B be non empty IntervalSet of U;

coherence

DIFFERENCE (A,B) is IntervalSet of U

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

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;

coherence

not A _\_ B is empty

end;
let A, B be non empty IntervalSet of U;

coherence

not A _\_ B is empty

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

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

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

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;

registration

let U be non empty set ;

coherence

not Inter (([#] U),([#] U)) is empty by Th43;

coherence

not Inter (({} U),({} U)) is empty by Th44;

end;
coherence

not Inter (([#] U),([#] U)) is empty by Th43;

coherence

not Inter (({} U),({} U)) is empty by Th44;

definition

let U be non empty set ;

let A be non empty IntervalSet of U;

coherence

(Inter (([#] U),([#] U))) _\_ A is non empty IntervalSet of U ;

end;
let A be non empty IntervalSet of U;

coherence

(Inter (([#] U),([#] U))) _\_ A is non empty IntervalSet of U ;

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

for U being non empty set

for A being non empty IntervalSet of U holds A ^ = (Inter (([#] U),([#] U))) _\_ A;

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

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

definition

let U be non empty set ;

ex b_{1} being non empty set st

for x being set holds

( x in b_{1} iff x is non empty IntervalSet of U )

for b_{1}, b_{2} being non empty set st ( for x being set holds

( x in b_{1} iff x is non empty IntervalSet of U ) ) & ( for x being set holds

( x in b_{2} iff x is non empty IntervalSet of U ) ) holds

b_{1} = b_{2}

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

( x in it iff x is non empty IntervalSet of U );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def11 defines IntervalSets INTERVA1:def 11 :

for U, b_{2} being non empty set holds

( b_{2} = IntervalSets U iff for x being set holds

( x in b_{2} iff x is non empty IntervalSet of U ) );

for U, b

( b

( x in b

definition

let U be non empty set ;

ex b_{1} being non empty strict LattStr st

( the carrier of b_{1} = IntervalSets U & ( for a, b being Element of the carrier of b_{1}

for a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds

( the L_join of b_{1} . (a,b) = a9 _\/_ b9 & the L_meet of b_{1} . (a,b) = a9 _/\_ b9 ) ) )

for b_{1}, b_{2} being non empty strict LattStr st the carrier of b_{1} = IntervalSets U & ( for a, b being Element of the carrier of b_{1}

for a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds

( the L_join of b_{1} . (a,b) = a9 _\/_ b9 & the L_meet of b_{1} . (a,b) = a9 _/\_ b9 ) ) & the carrier of b_{2} = IntervalSets U & ( for a, b being Element of the carrier of b_{2}

for a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds

( the L_join of b_{2} . (a,b) = a9 _\/_ b9 & the L_meet of b_{2} . (a,b) = a9 _/\_ b9 ) ) holds

b_{1} = b_{2}

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

ex b

( the carrier of b

for a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds

( the L_join of b

proof end;

uniqueness for b

for a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds

( the L_join of b

for a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds

( the L_join of b

b

proof end;

:: deftheorem Def12 defines InterLatt INTERVA1:def 12 :

for U being non empty set

for b_{2} being non empty strict LattStr holds

( b_{2} = InterLatt U iff ( the carrier of b_{2} = IntervalSets U & ( for a, b being Element of the carrier of b_{2}

for a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds

( the L_join of b_{2} . (a,b) = a9 _\/_ b9 & the L_meet of b_{2} . (a,b) = a9 _/\_ b9 ) ) ) );

for U being non empty set

for b

( b

for a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds

( the L_join of b

registration
end;

definition

let X be Tolerance_Space;

ex b_{1} being Element of [:(bool the carrier of X),(bool the carrier of X):] st verum
;

end;
mode RoughSet of X -> Element of [:(bool the carrier of X),(bool the carrier of X):] means :Def13: :: INTERVA1:def 13

verum;

existence verum;

ex b

:: deftheorem Def13 defines RoughSet INTERVA1:def 13 :

for X being Tolerance_Space

for b_{2} being Element of [:(bool the carrier of X),(bool the carrier of X):] holds

( b_{2} is RoughSet of X iff verum );

for X being Tolerance_Space

for b

( b

definition

let X be Tolerance_Space;

let A be Subset of X;

coherence

[(LAp A),(UAp A)] is RoughSet of X

end;
let A be Subset of X;

coherence

[(LAp A),(UAp A)] is RoughSet of X

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

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;

coherence

A `1 is Subset of X

A `2 is Subset of X

end;
let A be RoughSet of X;

coherence

A `1 is Subset of X

proof end;

coherence A `2 is Subset of X

proof end;

:: deftheorem defines LAp INTERVA1:def 15 :

for X being Tolerance_Space

for A being RoughSet of X holds LAp A = A `1 ;

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 ;

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;

compatibility

( A = B iff ( LAp A = LAp B & UAp A = UAp B ) )

end;
let A, B be RoughSet of X;

compatibility

( A = B iff ( LAp A = LAp B & UAp A = UAp B ) )

proof end;

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

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;

[((LAp A) \/ (LAp B)),((UAp A) \/ (UAp B))] is RoughSet of X

[((LAp A) /\ (LAp B)),((UAp A) /\ (UAp B))] is RoughSet of X

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

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

[((LAp A) /\ (LAp B)),((UAp A) /\ (UAp B))] is RoughSet of X

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

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

for X being Tolerance_Space

for A, B being RoughSet of X holds A _/\_ B = [((LAp A) /\ (LAp B)),((UAp A) /\ (UAp B))];

theorem :: INTERVA1:56

theorem :: INTERVA1:57

theorem :: INTERVA1:58

theorem :: INTERVA1:59

:: Properties

theorem :: INTERVA1:62

theorem :: INTERVA1:63

theorem Th64: :: INTERVA1:64

for X being Tolerance_Space

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

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)

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)

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

proof end;

definition

let X be Tolerance_Space;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff x is RoughSet of X )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff x is RoughSet of X ) ) & ( for x being set holds

( x in b_{2} iff x is RoughSet of X ) ) holds

b_{1} = b_{2}

end;
func RoughSets X -> set means :Def20: :: INTERVA1:def 20

for x being set holds

( x in it iff x is RoughSet of X );

existence for x being set holds

( x in it iff x is RoughSet of X );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def20 defines RoughSets INTERVA1:def 20 :

for X being Tolerance_Space

for b_{2} being set holds

( b_{2} = RoughSets X iff for x being set holds

( x in b_{2} iff x is RoughSet of X ) );

for X being Tolerance_Space

for b

( b

( x in b

definition
end;

:: deftheorem defines @ INTERVA1:def 21 :

for X being Tolerance_Space

for R being Element of RoughSets X holds @ R = R;

for X being Tolerance_Space

for R being Element of RoughSets X holds @ R = R;

definition
end;

:: deftheorem defines @ INTERVA1:def 22 :

for X being Tolerance_Space

for R being RoughSet of X holds R @ = R;

for X being Tolerance_Space

for R being RoughSet of X holds R @ = R;

definition

let X be Tolerance_Space;

ex b_{1} being strict LattStr st

( the carrier of b_{1} = 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_{1} . (A,B) = A9 _\/_ B9 & the L_meet of b_{1} . (A,B) = A9 _/\_ B9 ) ) )

for b_{1}, b_{2} being strict LattStr st the carrier of b_{1} = 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_{1} . (A,B) = A9 _\/_ B9 & the L_meet of b_{1} . (A,B) = A9 _/\_ B9 ) ) & the carrier of b_{2} = 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_{2} . (A,B) = A9 _\/_ B9 & the L_meet of b_{2} . (A,B) = A9 _/\_ B9 ) ) holds

b_{1} = b_{2}

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

ex b

( the carrier of b

for A9, B9 being RoughSet of X st A = A9 & B = B9 holds

( the L_join of b

proof end;

uniqueness for b

for A9, B9 being RoughSet of X st A = A9 & B = B9 holds

( the L_join of b

for A9, B9 being RoughSet of X st A = A9 & B = B9 holds

( the L_join of b

b

proof end;

:: deftheorem Def23 defines RSLattice INTERVA1:def 23 :

for X being Tolerance_Space

for b_{2} being strict LattStr holds

( b_{2} = RSLattice X iff ( the carrier of b_{2} = 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_{2} . (A,B) = A9 _\/_ B9 & the L_meet of b_{2} . (A,B) = A9 _/\_ B9 ) ) ) );

for X being Tolerance_Space

for b

( b

for A9, B9 being RoughSet of X st A = A9 & B = B9 holds

( the L_join of b

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;

Lm14: for X being Tolerance_Space holds ERS X in RoughSets X

by Def20;

:: deftheorem defines TRS INTERVA1:def 25 :

for X being Tolerance_Space holds TRS X = [([#] X),([#] X)];

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

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;