:: On the Lattice of Intervals and Rough Sets
:: by Adam Grabowski and Magdalena Jastrz\c{e}bska
::
:: Received October 10, 2009
:: Copyright (c) 2009-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies SUBSET_1, SETFAM_1, TARSKI, ZFMISC_1, XBOOLE_0, LEXBFS, XXREAL_0,
ORDINAL4, STRUCT_0, LATTICES, FUNCT_1, BINOP_1, EQREL_1, ROUGHS_1,
MCART_1, QC_LANG1, MSUALG_6, XXREAL_2, PBOOLE, REWRITE1, LATTICE3,
INTERVA1;
notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, SETFAM_1, MCART_1, BINOP_1,
STRUCT_0, LATTICES, LATTICE3, ROUGHS_1;
constructors LATTICE3, ROUGHS_1, BINOP_1, XTUPLE_0;
registrations RELSET_1, STRUCT_0, SUBSET_1, XBOOLE_0, LATTICES, XTUPLE_0;
requirements BOOLE, SUBSET;
begin :: Interval Sets
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 };
end;
reserve U for set,
X, Y for Subset of U;
theorem :: INTERVA1:1
for x being set holds x in Inter (X,Y) iff X c= x & x c= Y;
theorem :: INTERVA1:2
Inter (X,Y) <> {} implies X in Inter (X,Y) & Y in Inter (X,Y);
theorem :: INTERVA1:3
for U being set, A, B being Subset of U st not A c= B holds Inter (A, B) = {}
;
theorem :: INTERVA1:4
for U being set, A, B being Subset of U st Inter (A,B) = {} holds
not A c= B;
theorem :: INTERVA1:5
for A, B being Subset of U st Inter (A, B) <> {} holds A c= B;
theorem :: INTERVA1:6
for A, B, C, D being Subset of U st
Inter (A, B) <> {} & Inter (A, B) = Inter (C, D) holds
A = C & B = D;
theorem :: INTERVA1:7
for U being non empty set, A being non empty Subset of U holds
Inter (A, {}U) = {};
theorem :: INTERVA1:8
for A being Subset of U holds Inter (A, A) = { A };
definition let U;
mode IntervalSet of U -> Subset-Family of U means
:: INTERVA1:def 2
ex A, B be Subset of U st it = Inter (A, B);
end;
theorem :: INTERVA1:9
for U being non empty set holds {} is IntervalSet of U;
theorem :: INTERVA1:10
for U being non empty set, A being Subset of U holds
{ A } is IntervalSet of U;
definition let U; let A, B be Subset of U;
redefine func Inter (A, B) -> IntervalSet of U;
end;
registration let U be non empty set;
cluster non empty for IntervalSet of U;
end;
theorem :: INTERVA1:11
for U being non empty set, 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);
theorem :: INTERVA1:12
for U being non empty set, 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 };
theorem :: INTERVA1:13
for U being non empty set, 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 };
definition let U be non empty set,
A, B be non empty IntervalSet of U;
func A _/\_ B -> IntervalSet of U equals
:: INTERVA1:def 3
INTERSECTION (A, B);
func A _\/_ B -> IntervalSet of U equals
:: INTERVA1:def 4
UNION (A, B);
end;
registration let U be non empty set,
A, B be non empty IntervalSet of U;
cluster A _/\_ B -> non empty;
cluster A _\/_ B -> non empty;
end;
reserve U for non empty set,
A, B, C for non empty IntervalSet of U;
definition let U, A;
func A``1 -> Subset of U means
:: INTERVA1:def 5
ex B being Subset of U st A = Inter (it, B);
func A``2 -> Subset of U means
:: INTERVA1:def 6
ex B being Subset of U st A = Inter (B, it);
end;
theorem :: INTERVA1:14
for X being set holds X in A iff A``1 c= X & X c= A``2;
theorem :: INTERVA1:15
A = Inter (A``1,A``2);
theorem :: INTERVA1:16
A``1 c= A``2;
theorem :: INTERVA1:17
A _\/_ B = Inter (A``1 \/ B``1, A``2 \/ B``2);
theorem :: INTERVA1:18
A _/\_ B = Inter (A``1 /\ (B``1), A``2 /\ B``2);
definition let U; let A, B;
redefine pred A = B means
:: INTERVA1:def 7
A``1 = B``1 & A``2 = B``2;
end;
theorem :: INTERVA1:19
A _\/_ A = A;
theorem :: INTERVA1:20
A _/\_ A = A;
theorem :: INTERVA1:21
A _\/_ B = B _\/_ A;
theorem :: INTERVA1:22
A _/\_ B = B _/\_ A;
theorem :: INTERVA1:23
A _\/_ B _\/_ C = A _\/_ (B _\/_ C);
theorem :: INTERVA1:24
A _/\_ B _/\_ C = A _/\_ (B _/\_ C);
definition let X be set; let F be Subset-Family of X;
attr F is ordered means
:: 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;
registration let X be set;
cluster non empty ordered for Subset-Family of X;
end;
theorem :: INTERVA1:25
for A,B being Subset of U st A c= B holds
Inter (A,B) is non empty ordered Subset-Family of U;
theorem :: INTERVA1:26
for A being non empty IntervalSet of U holds
A is non empty ordered Subset-Family of U;
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;
redefine func min F -> Element of F;
redefine func max F -> Element of F;
end;
theorem :: INTERVA1:27
for A,B being Subset of U, F being ordered non empty Subset-Family of U st
F = Inter (A,B) holds
min F = A & max F = B;
theorem :: INTERVA1:28
for X,Y being set, A being non empty ordered Subset-Family of X holds
Y in A iff min A c= Y & Y c= max A;
theorem :: INTERVA1:29
for X being set, A, B, C being non empty ordered Subset-Family of X holds
UNION (A, INTERSECTION (B,C)) =
INTERSECTION (UNION (A,B), UNION (A,C));
theorem :: INTERVA1:30
for X being set, A, B, C being non empty ordered Subset-Family of X holds
INTERSECTION (A, UNION (B,C)) =
UNION (INTERSECTION (A,B), INTERSECTION (A,C));
theorem :: INTERVA1:31
A _\/_ (B _/\_ C) = (A _\/_ B) _/\_ (A _\/_ C);
theorem :: INTERVA1:32
A _/\_ (B _\/_ C) = (A _/\_ B) _\/_ (A _/\_ C);
theorem :: INTERVA1:33
for X being set, A, B being non empty ordered Subset-Family of X holds
INTERSECTION (A, (UNION (A,B))) = A;
theorem :: INTERVA1:34
for X being set, A, B being non empty ordered Subset-Family of X holds
UNION (INTERSECTION(A,B),B) = B;
theorem :: INTERVA1:35
A _/\_ (A _\/_ B) = A;
theorem :: INTERVA1:36
(A _/\_ B) _\/_ B = B;
begin :: Families of Subsets
theorem :: INTERVA1:37
for U being non empty set, A, B being Subset-Family of U holds
DIFFERENCE (A,B) is Subset-Family of U;
theorem :: INTERVA1:38
for U being non empty set,
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};
theorem :: INTERVA1:39
for U being non empty set, 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 };
definition let U be non empty set,
A, B be non empty IntervalSet of U;
func A _\_ B -> IntervalSet of U equals
:: INTERVA1:def 9
DIFFERENCE (A, B);
end;
registration let U be non empty set,
A, B be non empty IntervalSet of U;
cluster A _\_ B -> non empty;
end;
theorem :: INTERVA1:40
A _\_ B = Inter (A``1 \ B``2, A``2 \ B``1);
theorem :: INTERVA1:41
for X,Y being Subset of U st A = Inter (X,Y) holds
A _\_ C = Inter (X \ C``2, Y \ C``1);
theorem :: INTERVA1:42
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);
theorem :: INTERVA1:43
for U being non empty set holds
Inter ([#]U,[#]U) is non empty IntervalSet of U;
theorem :: INTERVA1:44
for U being non empty set holds Inter ({}U,{}U) is non empty IntervalSet of U
;
registration let U be non empty set;
cluster Inter ([#]U,[#]U) -> non empty;
cluster Inter ({}U,{}U) -> non empty;
end;
definition let U be non empty set, A be non empty IntervalSet of U;
func A ^ -> non empty IntervalSet of U equals
:: INTERVA1:def 10
Inter ([#]U,[#]U) _\_ A;
end;
theorem :: INTERVA1:45
for U being non empty set, A being non empty IntervalSet of U holds
A^ = Inter ((A``2)`,(A``1)`);
theorem :: INTERVA1:46
for X,Y being Subset of U st A = Inter (X,Y) & X c= Y holds
A^ = Inter (Y`,X`);
theorem :: INTERVA1:47
(Inter ({}U,{}U))^ = Inter ([#]U,[#]U);
theorem :: INTERVA1:48
(Inter ([#]U,[#]U))^ = Inter ({}U,{}U);
begin :: Counterexamples
theorem :: INTERVA1:49
ex A being non empty IntervalSet of U st A _/\_ A^ <> Inter ({}U,{}U);
theorem :: INTERVA1:50
ex A being non empty IntervalSet of U st A _\/_ A^ <> Inter ([#]U,[#]U);
theorem :: INTERVA1:51
ex A being non empty IntervalSet of U st A _\_ A <> Inter ({}U,{}U);
theorem :: INTERVA1:52
for A being non empty IntervalSet of U holds U in A _\/_ (A^);
theorem :: INTERVA1:53
for A being non empty IntervalSet of U holds {} in A _/\_ (A^);
theorem :: INTERVA1:54
for A being non empty IntervalSet of U holds {} in A _\_ A;
begin :: Lattice of Interval Sets
definition let U be non empty set;
func IntervalSets U -> non empty set means
:: INTERVA1:def 11
for x being set holds x in it iff x is non empty IntervalSet of U;
end;
definition let U be non empty set;
func InterLatt U -> strict non empty LattStr means
:: INTERVA1:def 12
the carrier of it = IntervalSets U &
for a, b being Element of the carrier of it,
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;
end;
registration let U be non empty set;
cluster InterLatt U -> Lattice-like;
end;
definition let X be Tolerance_Space;
mode RoughSet of X ->
Element of [:bool the carrier of X, bool the carrier of X:] means
:: INTERVA1:def 13
not contradiction;
end;
theorem :: INTERVA1:55
for X being Tolerance_Space, A being RoughSet of X holds
ex B, C being Subset of X st A = [B,C];
definition let X be Tolerance_Space, A be Subset of X;
func RS A -> RoughSet of X equals
:: INTERVA1:def 14
[LAp A, UAp A];
end;
definition let X be Tolerance_Space, A be RoughSet of X;
func LAp A -> Subset of X equals
:: INTERVA1:def 15
A`1;
func UAp A -> Subset of X equals
:: INTERVA1:def 16
A`2;
end;
definition let X be Tolerance_Space; let A, B be RoughSet of X;
redefine pred A = B means
:: INTERVA1:def 17
LAp A = LAp B & UAp A = UAp B;
end;
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];
func A _/\_ B -> RoughSet of X equals
:: INTERVA1:def 19
[LAp A /\ LAp B, UAp A /\ UAp B];
end;
reserve X for Tolerance_Space,
A, B, C for RoughSet of X;
theorem :: INTERVA1:56
LAp (A _\/_ B) = LAp A \/ LAp B;
theorem :: INTERVA1:57
UAp (A _\/_ B) = UAp A \/ UAp B;
theorem :: INTERVA1:58
LAp (A _/\_ B) = LAp A /\ LAp B;
theorem :: INTERVA1:59
UAp (A _/\_ B) = UAp A /\ UAp B;
:: Properties
theorem :: INTERVA1:60
A _\/_ A = A;
theorem :: INTERVA1:61
A _/\_ A = A;
theorem :: INTERVA1:62
A _\/_ B = B _\/_ A;
theorem :: INTERVA1:63
A _/\_ B = B _/\_ A;
theorem :: INTERVA1:64
A _\/_ B _\/_ C = A _\/_ (B _\/_ C);
theorem :: INTERVA1:65
A _/\_ B _/\_ C = A _/\_ (B _/\_ C);
theorem :: INTERVA1:66
A _/\_ (B _\/_ C) = (A _/\_ B) _\/_ (A _/\_ C);
theorem :: INTERVA1:67
A _\/_ (A _/\_ B) = A;
theorem :: INTERVA1:68
A _/\_ (A _\/_ B) = A;
begin :: Lattice of Rough Sets
definition let X;
func RoughSets X -> set means
:: INTERVA1:def 20
for x being set holds x in it iff x is RoughSet of X;
end;
registration let X;
cluster RoughSets X -> non empty;
end;
definition let X; let R be Element of RoughSets X;
func @R -> RoughSet of X equals
:: INTERVA1:def 21
R;
end;
definition let X; let R be RoughSet of X;
func R@ -> Element of RoughSets X equals
:: INTERVA1:def 22
R;
end;
definition let X;
func RSLattice X -> strict LattStr means
:: INTERVA1:def 23
the carrier of it = RoughSets X & for A, B being Element of RoughSets X,
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;
end;
registration let X;
cluster RSLattice X -> non empty;
end;
reserve K,L,M for Element of RoughSets X;
registration let X;
cluster RSLattice X -> Lattice-like;
end;
registration let X;
cluster RSLattice X -> distributive;
end;
definition let X;
func ERS X -> RoughSet of X equals
:: INTERVA1:def 24
[{},{}];
end;
theorem :: INTERVA1:69
for A being RoughSet of X holds ERS X _\/_ A = A;
definition let X;
func TRS X -> RoughSet of X equals
:: INTERVA1:def 25
[[#]X,[#]X];
end;
theorem :: INTERVA1:70
for A being RoughSet of X holds TRS X _/\_ A = A;
registration let X;
cluster RSLattice X -> bounded;
end;
theorem :: INTERVA1:71
for X being Tolerance_Space, A, B being Element of RSLattice X,
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;
registration let X;
cluster RSLattice X -> complete;
end;