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