:: On the Lattice of Intervals and Rough Sets
:: by Adam Grabowski and Magdalena Jastrz\c{e}bska
::
:: Received October 10, 2009
:: Copyright (c) 2009-2026 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;
definitions XBOOLE_0, TARSKI, LATTICES, LATTICE3, VECTSP_8;
equalities LATTICES, SUBSET_1, STRUCT_0;
expansions XBOOLE_0, TARSKI, LATTICES, LATTICE3;
theorems ROUGHS_1, ZFMISC_1, XBOOLE_1, BINOP_1, LATTICES, TARSKI, SETFAM_1,
XBOOLE_0, TOPGEN_4, SUBSET_1;
schemes BINOP_1, XBOOLE_0, XFAMILY;
begin :: Interval Sets
definition let U be set;
let X, Y be Subset of U;
func Inter (X,Y) -> Subset-Family of U equals
{ A where A is Subset of U : X c= A & A c= Y };
coherence
proof
set IT = { A where A is Subset of U : X c= A & A c= Y };
IT c= bool U
proof
let x be object;
assume x in IT; then
x in { A where A is Subset of U : X c= A & A c= Y }; then
consider B being Subset of U such that
A1: x = B & X c= B & B c= Y;
thus thesis by A1;
end; then
IT is Subset-Family of U;
hence thesis;
end;
end;
reserve U for set,
X, Y for Subset of U;
theorem Th1:
for x being set holds x in Inter (X,Y) iff X c= x & x c= Y
proof
let x be set;
hereby assume x in Inter (X,Y); then
consider A9 being Element of bool U such that
A1: x = A9 & X c= A9 & A9 c= Y;
thus X c= x & x c= Y by A1;
end;
assume
A2: X c= x & x c= Y; then
x is Subset of U by XBOOLE_1:1;
hence thesis by A2;
end;
theorem Th2:
Inter (X,Y) <> {} implies X in Inter (X,Y) & Y in Inter (X,Y)
proof
assume Inter (X,Y) <> {}; then
consider x being object such that
A1: x in Inter (X,Y) by XBOOLE_0:def 1;
reconsider x as set by TARSKI:1;
X c= x & x c= Y by A1,Th1; then
X c= Y;
hence thesis;
end;
theorem Th3:
for U being set, A, B being Subset of U st not A c= B holds Inter (A, B) = {}
proof
let U be set, A, B be Subset of U;
assume
A1: not A c= B;
assume Inter (A, B) <> {}; then
consider x being object such that
A2: x in Inter (A, B) by XBOOLE_0:def 1;
reconsider x as set by TARSKI:1;
A c= x & x c= B by A2,Th1;
hence thesis by A1;
end;
theorem
for U being set, A, B being Subset of U st Inter (A,B) = {} holds
not A c= B by Th1;
theorem Th5:
for A, B being Subset of U st Inter (A, B) <> {} holds A c= B
proof
let A, B be Subset of U;
assume Inter (A, B) <> {}; then
consider x being object such that
A1: x in Inter (A, B) by XBOOLE_0:def 1;
reconsider x as set by TARSKI:1;
A c= x & x c= B by A1,Th1;
hence thesis;
end;
theorem Th6:
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
let A,B,C,D be Subset of U;
assume A1: Inter (A,B) <> {} & Inter (A,B) = Inter (C,D);
then A in Inter (A,B) by Th2; then
A2: C c= A & A c= D by Th1,A1;
C in Inter (C,D) by A1,Th2; then
A3: A c= C & C c= B by A1,Th1;
B in Inter (A,B) by A1,Th2; then
A4: B c= D by Th1,A1;
D in Inter (C,D) by A1,Th2; then
D c= B by A1,Th1;
hence thesis by A3,A4,A2;
end;
theorem Th7:
for U being non empty set, A being non empty Subset of U holds
Inter (A, {}U) = {}
proof
let U be non empty set,
A be non empty Subset of U;
thus Inter (A,{}U) c= {}
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in Inter (A,{}U); then
A c= xx & xx c= {}U by Th1;
hence thesis;
end;
thus thesis;
end;
theorem Th8:
for A being Subset of U holds Inter (A, A) = { A }
proof
let A be Subset of U;
thus Inter (A, A) c= { A }
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in Inter (A,A); then
A c= xx & xx c= A by Th1; then
A = x by XBOOLE_0:def 10;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in { A }; then
x = A by TARSKI:def 1;
hence thesis;
end;
definition let U;
mode IntervalSet of U -> Subset-Family of U means :Def2:
ex A, B be Subset of U st it = Inter (A, B);
existence
proof
set A = the Subset of U;
set IT = { A };
IT = Inter (A,A) by Th8;
hence thesis;
end;
end;
theorem
for U being non empty set holds {} is IntervalSet of U
proof
let U be non empty set;
set A = the non empty Subset of U;
Inter (A, {}U) = {} by Th7;
hence thesis by Def2;
end;
theorem Th10:
for U being non empty set, A being Subset of U holds
{ A } is IntervalSet of U
proof
let U be non empty set,
A be Subset of U;
Inter (A, A) = { A } by Th8;
hence thesis by Def2;
end;
definition let U; let A, B be Subset of U;
redefine func Inter (A, B) -> IntervalSet of U; :: redefines Inter (INTERVA1, definition)
correctness by Def2;
end;
registration let U be non empty set;
cluster non empty for IntervalSet of U;
existence
proof
set A = the Subset of U;
{ A } is IntervalSet of U by Th10;
hence thesis;
end;
end;
theorem Th11:
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)
proof
let U be non empty set,
A be set;
hereby assume
A1: A is non empty IntervalSet of U; then
consider A1, A2 be Subset of U such that
A2: A = Inter (A1, A2) by Def2;
take A1, A2;
thus A1 c= A2 by A1,A2,Th3;
thus A = Inter (A1, A2) by A2;
end;
given A1, A2 being Subset of U such that
A3: A1 c= A2 & A = Inter (A1, A2);
A1 in Inter (A1,A2) by A3;
hence thesis by A3;
end;
theorem Th12:
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 }
proof
let U be non empty set,
A1, A2, B1, B2 be Subset of U;
assume that
A1: A1 c= A2 and
A2: B1 c= B2;
set A = Inter (A1,A2), B = Inter (B1,B2);
set LAB = A1 /\ B1;
set UAB = A2 /\ B2;
set IT = INTERSECTION (Inter (A1,A2), Inter (B1,B2));
thus IT c= { C where C is Subset of U : LAB c= C & C c= UAB }
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in IT; then
consider X, Y be set such that
A3: X in A & Y in B & x = X /\ Y by SETFAM_1:def 5;
xx c= X by A3,XBOOLE_1:17; then
A4: x is Subset of U by A3,XBOOLE_1:1;
A5: A1 c= X by Th1,A3;
B1 c= Y by Th1,A3; then
A6: LAB c= xx by A5,A3,XBOOLE_1:27;
A7: X c= A2 by Th1,A3;
Y c= B2 by Th1,A3; then
xx c= UAB by A7,A3,XBOOLE_1:27;
hence thesis by A6,A4;
end;
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in { C where C is Subset of U : LAB c= C & C c= UAB };
then consider C9 being Subset of U such that
A8: C9 = x & LAB c= C9 & C9 c= UAB;
set x1 = (xx \/ A1) /\ A2;
set x2 = (xx \/ B1) /\ B2;
A9: LAB \/ xx = x by A8,XBOOLE_1:12;
A10: UAB /\ xx = x by A8,XBOOLE_1:28;
A11: x1 /\ x2 = (xx \/ A1) /\ (A2 /\ ((xx \/ B1) /\ B2)) by XBOOLE_1:16
.= (xx \/ A1) /\ ((xx \/ B1) /\ (B2 /\ A2)) by XBOOLE_1:16
.= (xx \/ A1) /\ (xx \/ B1) /\ UAB by XBOOLE_1:16
.= x by A9,A10,XBOOLE_1:24;
A1 /\ A2 = A1 by A1,XBOOLE_1:28;
then x1 = (xx /\ A2) \/ A1 by XBOOLE_1:23; then
A12: A1 c= x1 by XBOOLE_1:7;
x1 c= A2 by XBOOLE_1:17; then
A13: x1 in A by A12;
B1 /\ B2 = B1 by A2,XBOOLE_1:28;
then x2 = (xx /\ B2) \/ B1 by XBOOLE_1:23; then
A14: B1 c= x2 by XBOOLE_1:7;
x2 c= B2 by XBOOLE_1:17; then
x2 in B by A14;
hence thesis by A11,A13,SETFAM_1:def 5;
end;
theorem Th13:
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 }
proof
let U be non empty set,
A1, A2, B1, B2 be Subset of U;
assume that
A1: A1 c= A2 and
A2: B1 c= B2;
set A = Inter (A1,A2), B = Inter (B1,B2);
set LAB = A1 \/ B1;
set UAB = A2 \/ B2;
set IT = UNION (A, B);
thus IT c= { C where C is Subset of U : LAB c= C & C c= UAB }
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in IT; then
consider X, Y be set such that
A3: X in A & Y in B & x = X \/ Y by SETFAM_1:def 4;
A4: x is Subset of U by A3,XBOOLE_1:8;
A5: A1 c= X by Th1,A3;
B1 c= Y by Th1,A3; then
A6: LAB c= xx by A5,A3,XBOOLE_1:13;
A7: X c= A2 by Th1,A3;
Y c= B2 by Th1,A3; then
xx c= UAB by A7,A3,XBOOLE_1:13;
hence thesis by A4,A6;
end;
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in { C where C is Subset of U : LAB c= C & C c= UAB };
then consider C9 being Subset of U such that
A8: C9 = x & LAB c= C9 & C9 c= UAB;
set x1 = (xx \/ A1) /\ A2;
set x2 = (xx \/ B1) /\ B2;
A9: LAB \/ xx = x by A8,XBOOLE_1:12;
A10: UAB /\ xx = x by A8,XBOOLE_1:28;
A11: A1 /\ A2 = A1 by A1,XBOOLE_1:28;
A12: B1 /\ B2 = B1 by A2,XBOOLE_1:28;
A13: x1 \/ x2 = ((xx /\ A2) \/ (A1 /\ A2)) \/ ((xx \/ B1) /\ B2) by XBOOLE_1:23
.= ((xx /\ A2) \/ A1) \/ ((xx /\ B2) \/ (B1 /\ B2))
by A11,XBOOLE_1:23
.= (xx /\ A2) \/ (A1 \/ ((xx /\ B2) \/ B1)) by A12,XBOOLE_1:4
.= (xx /\ A2) \/ ((xx /\ B2) \/ LAB) by XBOOLE_1:4
.= (xx /\ A2) \/ (xx /\ B2) \/ LAB by XBOOLE_1:4
.= x by A9,A10,XBOOLE_1:23;
A1 /\ A2 = A1 by A1,XBOOLE_1:28;
then x1 = (xx /\ A2) \/ A1 by XBOOLE_1:23; then
A14: A1 c= x1 by XBOOLE_1:7;
x1 c= A2 by XBOOLE_1:17; then
A15: x1 in A by A14;
B1 /\ B2 = B1 by A2,XBOOLE_1:28;
then x2 = (xx /\ B2) \/ B1 by XBOOLE_1:23; then
A16: B1 c= x2 by XBOOLE_1:7;
x2 c= B2 by XBOOLE_1:17; then
x2 in B by A16;
hence thesis by A13,A15,SETFAM_1:def 4;
end;
definition let U be non empty set,
A, B be non empty IntervalSet of U;
func A _/\_ B -> IntervalSet of U equals
INTERSECTION (A, B);
coherence
proof
set IT = INTERSECTION (A, B);
consider A1, A2 being Subset of U such that
A1: A1 c= A2 & A = Inter (A1, A2) by Th11;
consider B1, B2 being Subset of U such that
A2: B1 c= B2 & B = Inter (B1, B2) by Th11;
set LAB = A1 /\ B1;
set UAB = A2 /\ B2;
IT = Inter (LAB, UAB) by Th12,A1,A2;
hence thesis;
end;
func A _\/_ B -> IntervalSet of U equals
UNION (A, B);
coherence
proof
set IT = UNION (A, B);
consider A1, A2 being Subset of U such that
A3: A1 c= A2 & A = Inter (A1, A2) by Th11;
consider B1, B2 being Subset of U such that
A4: B1 c= B2 & B = Inter (B1, B2) by Th11;
set LAB = A1 \/ B1;
set UAB = A2 \/ B2;
IT = Inter (LAB, UAB) by Th13,A3,A4;
hence thesis;
end;
end;
registration let U be non empty set,
A, B be non empty IntervalSet of U;
cluster A _/\_ B -> non empty;
coherence by TOPGEN_4:31;
cluster A _\/_ B -> non empty;
coherence by TOPGEN_4:30;
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 :Def5:
ex B being Subset of U st A = Inter (it, B);
existence
proof
consider A1, A2 being Subset of U such that
A1: A1 c= A2 & A = Inter (A1, A2) by Th11;
thus thesis by A1;
end;
uniqueness by Th6;
func A``2 -> Subset of U means :Def6:
ex B being Subset of U st A = Inter (B, it);
existence
proof
consider A1, A2 being Subset of U such that
A2: A1 c= A2 & A = Inter (A1, A2) by Th11;
thus thesis by A2;
end;
uniqueness by Th6;
end;
theorem Th14:
for X being set holds X in A iff A``1 c= X & X c= A``2
proof
let X be set;
A1: X in A implies A``1 c= X & X c= A``2
proof
assume A2: X in A;
A3: A``1 c= X
proof
consider B being Subset of U such that
A4: A = Inter (A``1, B) by Def5;
thus thesis by Th1,A2,A4;
end;
X c= A``2
proof
consider B being Subset of U such that
A5: A = Inter (B, A``2) by Def6;
thus thesis by Th1,A2,A5;
end;
hence thesis by A3;
end;
A``1 c= X & X c= A``2 implies X in A
proof
assume A``1 c= X & X c= A``2; then
A6: X in Inter (A``1,A``2) by Th1;
consider B being Subset of U such that A7: A = Inter (A``1, B) by Def5;
consider C being Subset of U such that A8: A = Inter (C, A``2) by Def6;
thus thesis by A7,A6,Th6,A8;
end;
hence thesis by A1;
end;
theorem Th15:
A = Inter (A``1,A``2)
proof
A1: Inter (A``1,A``2) c= A
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in Inter (A``1,A``2); then
A``1 c= xx & xx c= A``2 by Th1;
hence thesis by Th14;
end;
A c= Inter (A``1,A``2)
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in A; then
A``1 c= xx & xx c= A``2 by Th14;
hence thesis by Th1;
end;
hence thesis by A1;
end;
theorem Th16:
A``1 c= A``2
proof
consider B being Subset of U such that A1: A = Inter (A``1,B) by Def5;
consider C being Subset of U such that A2: A = Inter (C,A``2) by Def6;
A``1 = C by Th6,A2,A1;
hence thesis by Th5,A2;
end;
theorem Th17:
A _\/_ B = Inter (A``1 \/ B``1, A``2 \/ B``2)
proof
thus A _\/_ B c= Inter (A``1 \/ B``1, A``2 \/ B``2)
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume
A1: x in A _\/_ B; then
consider X, Y being set such that
A2: X in A & Y in B & x = X \/ Y by SETFAM_1:def 4;
A3: A``1 c= X & X c= A``2 by A2,Th14;
A4: B``1 c= Y & Y c= B``2 by A2,Th14; then
A5: xx c= A``2 \/ B``2 by A3,A2,XBOOLE_1:13;
A``1 \/ B``1 c= xx by A3,A2,A4,XBOOLE_1:13;
hence thesis by A1,A5;
end;
thus Inter (A``1 \/ B``1, A``2 \/ B``2) c= A _\/_ B
proof
let x be object;
assume x in Inter (A``1 \/ B``1, A``2 \/ B``2); then
consider Z being Element of bool U such that
A6: x = Z & A``1 \/ B``1 c= Z & Z c= A``2 \/ B``2;
A``1 c= (Z \/ A``1) /\ A``2
proof
let x be object;
assume A7: x in A``1;
assume A8: not x in (Z \/ A``1) /\ A``2;
per cases by A8,XBOOLE_0:def 4;
suppose not x in Z \/ A``1;
hence thesis by A7,XBOOLE_0:def 3;
end;
suppose A9: not x in A``2;
A``1 c= A``2 & x in A``1 by A7,Th16;
hence thesis by A9;
end;
end; then
A``1 c= (Z \/ A``1) /\ A``2 & (Z \/ A``1) /\ A``2 c= A``2
by XBOOLE_1:17; then
A10: (Z \/ A``1) /\ A``2 in A by Th14;
B``1 c= (Z \/ B``1) /\ B``2
proof
let x be object;
assume A11: x in B``1; then
A12: x in Z \/ B``1 by XBOOLE_0:def 3;
B``1 c= B``2 by Th16;
hence thesis by A11,A12,XBOOLE_0:def 4;
end; then
B``1 c= (Z \/ B``1) /\ B``2 & (Z \/ B``1) /\ B``2 c= B``2
by XBOOLE_1:17; then
A13: (Z \/ B``1) /\ B``2 in B by Th14;
((Z \/ A``1) /\ A``2) \/ ((Z \/ B``1) /\ B``2) = (((Z \/ A``1) /\ A``2)
\/ (Z \/ B``1)) /\ (((Z \/ A``1) /\ A``2) \/ B``2) by XBOOLE_1:24
.= (((Z \/ A``1) \/ (Z \/ B``1)) /\ (A``2 \/ (Z \/ B``1)))
/\ (((Z \/ A``1) /\ A``2) \/ B``2) by XBOOLE_1:24
.= ((Z \/ (A``1 \/ B``1)) /\ (A``2 \/ (Z \/ B``1)))
/\ (((Z \/ A``1) /\ A``2) \/ B``2) by XBOOLE_1:5
.= (Z /\ (A``2 \/ (Z \/ B``1)))
/\ (((Z \/ A``1) /\ A``2) \/ B``2) by A6,XBOOLE_1:12
.= ((Z /\ A``2) \/ (Z /\ (Z \/ B``1)))
/\ (((Z \/ A``1) /\ A``2) \/ B``2) by XBOOLE_1:23
.= ((Z /\ A``2) \/ Z)
/\ (((Z \/ A``1) /\ A``2) \/ B``2) by XBOOLE_1:7,28
.= Z /\ (B``2 \/ ((Z \/ A``1) /\ A``2)) by XBOOLE_1:12,17
.= Z /\ (((Z \/ A``1) \/ B``2) /\ (A``2 \/ B``2)) by XBOOLE_1:24
.= Z /\ ((Z \/ (A``1 \/ B``2)) /\ (A``2 \/ B``2)) by XBOOLE_1:4
.= Z /\ ((Z /\ (A``2 \/ B``2)) \/ ((A``1 \/ B``2) /\ (A``2 \/ B``2)))
by XBOOLE_1:23
.= Z /\ (Z \/ ((A``1 \/ B``2) /\ (A``2 \/ B``2))) by A6,XBOOLE_1:28
.= Z /\ ((Z \/ (A``1 \/ B``2)) /\ (Z \/ (A``2 \/ B``2))) by XBOOLE_1:24
.= (Z /\ (Z \/ (A``1 \/ B``2))) /\ (Z \/ (A``2 \/ B``2)) by XBOOLE_1:16
.= Z /\ (Z \/ (A``2 \/ B``2)) by XBOOLE_1:7,28
.= Z by XBOOLE_1:7,28; then
consider X,Y being Subset of U such that
A14: X in A & Y in B & Z = X \/ Y by A10,A13;
thus thesis by A14,A6,SETFAM_1:def 4;
end;
end;
theorem Th18:
A _/\_ B = Inter (A``1 /\ (B``1), A``2 /\ B``2)
proof
A1: A _/\_ B c= Inter (A``1 /\ (B``1), A``2 /\ B``2)
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in A _/\_ B; then
consider X,Y being set such that
A2: X in A & Y in B & x = X /\ Y by SETFAM_1:def 5;
A``1 c= X & B``1 c= Y & X c= A``2 & Y c= B``2 by A2,Th14; then
A``1 /\ (B``1) c= xx & xx c= A``2 /\ B``2 by A2,XBOOLE_1:27;
hence thesis by Th1;
end;
Inter (A``1 /\ (B``1), A``2 /\ B``2) c= A _/\_ B
proof
let x be object;
assume x in Inter (A``1 /\ (B``1), A``2 /\ B``2); then
consider Z being Element of bool U such that
A3: x = Z & A``1 /\ (B``1) c= Z & Z c= A``2 /\ B``2;
A``1 c= (Z \/ A``1) /\ A``2
proof
let x be object;
assume A4: x in A``1;
assume A5: not x in (Z \/ A``1) /\ A``2;
per cases by A5,XBOOLE_0:def 4;
suppose not x in Z \/ A``1;
hence thesis by A4,XBOOLE_0:def 3;
end;
suppose A6: not x in A``2;
A``1 c= A``2 & x in A``1 by A4,Th16;
hence thesis by A6;
end;
end; then
A``1 c= (Z \/ A``1) /\ A``2 & (Z \/ A``1) /\ A``2 c= A``2
by XBOOLE_1:17; then
A7: (Z \/ A``1) /\ A``2 in A by Th14;
B``1 c= (Z \/ B``1) /\ B``2
proof
let x be object;
assume A8: x in B``1; then
A9: x in Z \/ B``1 by XBOOLE_0:def 3;
B``1 c= B``2 by Th16;
hence thesis by A8,A9,XBOOLE_0:def 4;
end; then
B``1 c= (Z \/ B``1) /\ B``2 & (Z \/ B``1) /\ B``2 c= B``2
by XBOOLE_1:17; then
A10: (Z \/ B``1) /\ B``2 in B by Th14;
((Z \/ A``1) /\ A``2) /\ ((Z \/ B``1) /\ B``2)
= (A``2 /\ (Z \/ A``1)) /\ (Z \/ B``1) /\ B``2 by XBOOLE_1:16
.=A``2 /\ ((Z \/ A``1) /\ (Z \/ B``1)) /\ B``2 by XBOOLE_1:16
.= A``2 /\ (Z \/ (A``1 /\ (B``1))) /\ B``2 by XBOOLE_1:24
.= A``2 /\ Z /\ B``2 by A3,XBOOLE_1:12
.= Z /\ (A``2 /\ B``2) by XBOOLE_1:16
.= Z by A3,XBOOLE_1:28;
hence thesis by A3,A7,A10,SETFAM_1:def 5;
end;
hence thesis by A1;
end;
definition let U; let A, B;
redefine pred A = B means :: redefines = (XBOOLE_0, redefinition) → = (HIDDEN, definition)
A``1 = B``1 & A``2 = B``2;
compatibility
proof
thus A = B implies A``1 = B``1 & A``2 = B``2;
assume that
A1: A``1 = B``1 and
A2: A``2 = B``2;
A3: A c= B
proof
let x be object;
assume
A4: x in A;
consider A1, B1 be Subset of U such that
A5: A = Inter (A1, B1) by Def2;
consider C1 being Subset of U such that
A6: A = Inter (A``1, C1) by Def5;
A7: A1 = B``1 by A1,A5,Th6,A6;
consider C2 being Subset of U such that
A8: B = Inter (B``1,C2) by Def5;
consider D1 being Subset of U such that
A9: A = Inter (D1,A``2) by Def6;
A10: B``2 = B1 by A2,A9,A5,Th6;
consider D2 being Subset of U such that
A11: B = Inter (D2,B``2) by Def6;
thus thesis by A4,A5,A7,A8,A10,A11,Th6;
end;
B c= A
proof
let x be object;
assume A12: x in B;
consider A1, B1 be Subset of U such that
A13: B = Inter (A1, B1) by Def2;
consider C1 being Subset of U such that
A14: B = Inter (B``1, C1) by Def5;
A15: A``1 = A1 by A1,A14,Th6,A13;
consider C2 being Subset of U such that
A16: A = Inter (A``1,C2) by Def5;
consider D1 being Subset of U such that
A17: B = Inter (D1,B``2) by Def6;
A18: A``2 = B1 by A2,A17,A13,Th6;
consider D2 being Subset of U such that
A19: A = Inter (D2,A``2) by Def6;
thus thesis by A12,A13,A15,A16,A18,A19,Th6;
end;
hence thesis by A3;
end;
end;
theorem
A _\/_ A = A
proof
A1: A _\/_ A c= A
proof
let x be object;
assume x in A _\/_ A; then
consider X, Y being set such that
A2: X in A & Y in A & x = X \/ Y by SETFAM_1:def 4;
A3: A``1 c= X & X c= A``2 by A2,Th14;
A``1 c= Y & Y c= A``2 by A2,Th14; then
A4: X \/ Y c= A``2 by A3,XBOOLE_1:8;
X c= X \/ Y by XBOOLE_1:7; then
A``1 c= X \/ Y by A3;
hence thesis by Th14,A4,A2;
end;
A c= A _\/_ A
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume
A5: x in A;
x = xx \/ xx;
hence thesis by A5,SETFAM_1:def 4;
end;
hence thesis by A1;
end;
theorem
A _/\_ A = A
proof
A1: A _/\_ A c= A
proof
let x be object;
assume x in A _/\_ A; then
consider X, Y being set such that
A2: X in A & Y in A & x = X /\ Y by SETFAM_1:def 5;
A3: A``1 c= X & X c= A``2 by A2,Th14;
A``1 c= Y & Y c= A``2 by A2,Th14; then
A4: A``1 c= X /\ Y by A3,XBOOLE_1:19;
X /\ Y c= X by XBOOLE_1:17; then
X /\ Y c= A``2 by A3;
hence thesis by A4,A2,Th14;
end;
A c= A _/\_ A
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume
A5: x in A;
x = xx /\ xx;
hence thesis by A5,SETFAM_1:def 5;
end;
hence thesis by A1;
end;
theorem
A _\/_ B = B _\/_ A;
theorem
A _/\_ B = B _/\_ A;
theorem Th23:
A _\/_ B _\/_ C = A _\/_ (B _\/_ C)
proof
A1: A _\/_ B _\/_ C c= A _\/_ (B _\/_ C)
proof
let x be object;
assume x in A _\/_ B _\/_ C; then
consider X, Y being set such that
A2: X in UNION (A, B) & Y in C & x = X \/ Y by SETFAM_1:def 4;
consider Z, W being set such that
A3: Z in A & W in B & X = Z \/ W by A2,SETFAM_1:def 4;
W \/ Y in UNION (B,C) by A2,A3,SETFAM_1:def 4; then
Z \/ (W \/ Y) in UNION (A,UNION (B,C)) by A3,SETFAM_1:def 4;
hence thesis by A2,A3,XBOOLE_1:4;
end;
A _\/_ (B _\/_ C) c= A _\/_ B _\/_ C
proof
let x be object;
assume x in A _\/_ (B _\/_ C); then
consider X, Y being set such that
A4: X in A & Y in UNION (B, C) & x = X \/ Y by SETFAM_1:def 4;
consider Z, W being set such that
A5: Z in B & W in C & Y = Z \/ W by A4,SETFAM_1:def 4;
X \/ Z in UNION (A,B) by A4,A5,SETFAM_1:def 4; then
(X \/ Z) \/ W in UNION (UNION (A,B), C) by A5,SETFAM_1:def 4;
hence thesis by A4,A5,XBOOLE_1:4;
end;
hence thesis by A1;
end;
theorem Th24:
A _/\_ B _/\_ C = A _/\_ (B _/\_ C)
proof
A1: A _/\_ B _/\_ C c= A _/\_ (B _/\_ C)
proof
let x be object;
assume x in A _/\_ B _/\_ C; then
consider X, Y being set such that
A2: X in INTERSECTION (A, B) & Y in C & x = X /\ Y by SETFAM_1:def 5;
consider Z, W being set such that
A3: Z in A & W in B & X = Z /\ W by A2,SETFAM_1:def 5;
W /\ Y in INTERSECTION (B,C) by A2,A3,SETFAM_1:def 5; then
Z /\ (W /\ Y) in INTERSECTION (A,INTERSECTION (B,C))
by A3,SETFAM_1:def 5;
hence thesis by A2,A3,XBOOLE_1:16;
end;
A _/\_ (B _/\_ C) c= A _/\_ B _/\_ C
proof
let x be object;
assume x in A _/\_ (B _/\_ C); then
consider X, Y being set such that
A4: X in A & Y in INTERSECTION (B, C) & x = X /\ Y by SETFAM_1:def 5;
consider Z, W being set such that
A5: Z in B & W in C & Y = Z /\ W by A4,SETFAM_1:def 5;
X /\ Z in INTERSECTION (A,B) by A4,A5,SETFAM_1:def 5; then
(X /\ Z) /\ W in INTERSECTION (INTERSECTION (A,B), C)
by A5,SETFAM_1:def 5;
hence thesis by A4,A5,XBOOLE_1:16;
end;
hence thesis by A1;
end;
Lm1:
for X being set, A, B, C being Subset-Family of X holds
UNION (A, INTERSECTION (B,C)) c=
INTERSECTION (UNION (A,B), UNION (A,C))
proof
let X be set, A, B, C be Subset-Family of X;
let x be object;
assume x in UNION (A, INTERSECTION (B,C)); then
consider X, Y being set such that
A1: X in A & Y in INTERSECTION (B,C) & x = X \/ Y by SETFAM_1:def 4;
consider W, Z being set such that
A2: W in B & Z in C & Y = W /\ Z by A1,SETFAM_1:def 5;
A3: x = (X \/ W) /\ (X \/ Z) by A1,A2,XBOOLE_1:24;
A4: X \/ W in UNION (A,B) by A1,A2,SETFAM_1:def 4;
X \/ Z in UNION (A,C) by A1,A2,SETFAM_1:def 4;
hence thesis by A3,A4,SETFAM_1:def 5;
end;
definition let X be set; let F be Subset-Family of X;
attr F is ordered means :Def8:
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;
existence
proof
reconsider F = {X} as Subset-Family of X by ZFMISC_1:68;
take F;
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
proof
take X, X;
thus X in F & X in F by TARSKI:def 1;
let Y be set;
thus Y in F implies X c= Y & Y c= X by TARSKI:def 1;
assume X c= Y & Y c= X; then
X = Y;
hence thesis by TARSKI:def 1;
end;
hence thesis;
end;
end;
theorem Th25:
for A,B being Subset of U st A c= B holds
Inter (A,B) is non empty ordered Subset-Family of U
proof
let A,B be Subset of U;
assume A1: A c= B;
consider C,D being set such that
A2: C=A & D=B;
C in Inter(A,B) & D in Inter(A,B) & for Y being set holds
Y in Inter(A,B) iff C c= Y & Y c= D by A2,Th1,A1;
hence thesis by Def8;
end;
theorem Th26:
for A being non empty IntervalSet of U holds
A is non empty ordered Subset-Family of U
proof
let A be non empty IntervalSet of U;
A = Inter (A``1,A``2) & A``1 c= A``2 by Th15,Th16;
hence thesis by Th25;
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;
redefine func min F -> Element of F; :: redefines min (INTERVA1, synonym) → meet (SETFAM_1, definition)
correctness
proof
consider A, B being set such that
A1: A in F & B in F &
for Y being set holds Y in F iff A c= Y & Y c= B by Def8;
for Z1 being set st Z1 in F holds A c= Z1 by A1; then
A2: A c= meet F by SETFAM_1:5;
meet F c= B by A1,SETFAM_1:3;
hence thesis by A1,A2;
end;
redefine func max F -> Element of F; :: redefines max (INTERVA1, synonym) → union (TARSKI, definition)
correctness
proof
consider A, B being set such that
A3: A in F & B in F &
for Y being set holds Y in F iff A c= Y & Y c= B by Def8;
A4: for Z1 being set st Z1 in F holds Z1 c= B by A3;
A5: A c= union F by A3,ZFMISC_1:74;
union F c= B by A4,ZFMISC_1:76;
hence thesis by A3,A5;
end;
end;
Lm2:
for X being set, F being non empty ordered Subset-Family of X,
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, F being non empty ordered Subset-Family of X,
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:
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
proof
let A,B be Subset of U;
let F be ordered non empty Subset-Family of U;
assume A1: F = Inter (A,B);
then A is Element of F & for Y being set st Y in F holds A c= Y
by Th2,Th1; then
A2: A = min F by Lm2;
B is Element of F & for Y being set st Y in F holds Y c= B
by Th2,A1,Th1;
hence thesis by A2,Lm3;
end;
theorem Th28:
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
proof
let X,Y be set;
let A be non empty ordered Subset-Family of X;
min A c= Y & Y c= max A implies Y in A
proof
assume A1: min A c= Y & Y c= max A;
consider C,D being set such that
A2: C in A & D in A & for X being set holds X in A iff C c= X & X c= D
by Def8;
A3: min A c= C & D c= max A by Lm2,Lm3,A2;
C c= min A & max A c= D by A2; then
min A = C & max A = D by A3;
hence thesis by A2,A1;
end;
hence thesis by Lm2,Lm3;
end;
Lm4:
for A being non empty IntervalSet of U holds
A is non empty ordered Subset-Family of U by Th26;
theorem Th29:
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))
proof
let X be set,
A, B, C be non empty ordered Subset-Family of X;
A1: UNION (A, INTERSECTION (B,C)) c=
INTERSECTION (UNION (A,B), UNION (A,C)) by Lm1;
INTERSECTION (UNION (A,B), UNION (A,C)) c= UNION (A, INTERSECTION (B,C))
proof
let x be object;
assume x in INTERSECTION (UNION (A,B), UNION (A,C)); then
consider X,Y being set such that
A2: X in UNION (A,B) & Y in UNION (A,C) & x = X /\ Y by SETFAM_1:def 5;
consider X1,X2 being set such that
A3: X1 in A & X2 in B & X = X1 \/ X2 by A2,SETFAM_1:def 4;
consider Y1,Y2 being set such that
A4: Y1 in A & Y2 in C & Y = Y1 \/ Y2 by A2,SETFAM_1:def 4;
A5: x = (X1 /\ (Y1 \/ Y2)) \/ (X2 /\ (Y1 \/ Y2)) by A2,A3,A4,XBOOLE_1:23
.= ((X1 /\ Y1) \/ (X1 /\ Y2)) \/ (X2 /\ (Y1 \/ Y2)) by XBOOLE_1:23
.= (X1 /\ Y1) \/ (X1 /\ Y2) \/
((X2 /\ Y1) \/ (X2 /\ Y2)) by XBOOLE_1:23
.= ((X1 /\ Y1) \/ (X1 /\ Y2) \/ (X2 /\ Y1)) \/ (X2 /\ Y2)
by XBOOLE_1:4;
set A1 = min A, A2 = max A;
A1 c= X1 & X1 c= A2 & A1 c= Y1 & Y1 c= A2 by A3,A4,Th28; then
A6: A1 /\ A1 c= X1 /\ Y1 & X1 /\ Y1 c= A2 /\ A2 by XBOOLE_1:27;
Y1 c= A2 & X2 /\ Y1 c= Y1 by A4,Th28,XBOOLE_1:17; then
X2 /\ Y1 c= A2; then
A7: A1 c= (X1 /\ Y1) \/ (X2 /\ Y1) &
(X1 /\ Y1) \/ (X2 /\ Y1) c= A2 by A6,XBOOLE_1:8,10;
X1 c= A2 & X1 /\ Y2 c= X1 by A3,Th28,XBOOLE_1:17; then
(X1 /\ Y2) c= A2; then
(X1 /\ Y1) \/ (X2 /\ Y1) \/ (X1 /\ Y2) c= A2 by A7,XBOOLE_1:8; then
A1 c= (X1 /\ Y1) \/ (X2 /\ Y1) \/ (X1 /\ Y2) &
(X1 /\ Y1) \/ (X1 /\ Y2) \/ (X2 /\ Y1) c= A2
by A7,XBOOLE_1:4,10; then
A1 c= (X1 /\ Y1) \/ (X1 /\ Y2) \/ (X2 /\ Y1) &
(X1 /\ Y1) \/ (X1 /\ Y2) \/ (X2 /\ Y1) c= A2
by XBOOLE_1:4; then
A8: (X1 /\ Y1) \/ (X1 /\ Y2) \/ (X2 /\ Y1) in A by Th28;
(X2 /\ Y2) in INTERSECTION (B,C) by A3,A4,SETFAM_1:def 5;
hence thesis by A8,A5,SETFAM_1:def 4;
end;
hence thesis by A1;
end;
Lm5:
for X being set, A, B, C being Subset-Family of X holds
INTERSECTION (A, UNION (B,C)) c=
UNION (INTERSECTION (A,B), INTERSECTION (A,C))
proof
let X be set, A, B, C be Subset-Family of X;
let x be object;
assume x in INTERSECTION (A, UNION (B,C)); then
consider X, Y being set such that
A1: X in A & Y in UNION (B,C) & x = X /\ Y by SETFAM_1:def 5;
consider Z, W being set such that
A2: Z in B & W in C & Y = Z \/ W by A1,SETFAM_1:def 4;
A3: x = (X /\ Z) \/ (X /\ W) by A1,A2,XBOOLE_1:23;
A4: X /\ Z in INTERSECTION (A,B) by A1,A2,SETFAM_1:def 5;
X /\ W in INTERSECTION (A,C) by A1,A2,SETFAM_1:def 5;
hence thesis by A3,A4,SETFAM_1:def 4;
end;
theorem Th30:
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))
proof
let X be set, A, B, C be non empty ordered Subset-Family of X;
A1: INTERSECTION (A, UNION (B,C)) c=
UNION (INTERSECTION (A,B), INTERSECTION (A,C)) by Lm5;
UNION (INTERSECTION (A,B), INTERSECTION (A,C)) c=
INTERSECTION (A, UNION (B,C))
proof
let x be object;
assume x in UNION (INTERSECTION (A,B), INTERSECTION (A,C)); then
consider X, Y being set such that
A2: X in INTERSECTION (A,B) & Y in INTERSECTION (A,C) & x = X \/ Y
by SETFAM_1:def 4;
consider X1,X2 being set such that
A3: X1 in A & X2 in B & X = X1 /\ X2 by A2,SETFAM_1:def 5;
consider Y1,Y2 being set such that
A4: Y1 in A & Y2 in C & Y = Y1 /\ Y2 by A2,SETFAM_1:def 5;
A5: x = ((X1 /\ X2) \/ Y1) /\ ((X1 /\ X2) \/ Y2) by A2,A3,A4,XBOOLE_1:24
.= (Y1 \/ (X1 /\ X2)) /\ ((Y2 \/ X1) /\ (Y2 \/ X2)) by XBOOLE_1:24
.= ((Y1 \/ X1) /\ (Y1 \/ X2)) /\ ((Y2 \/ X1) /\ (Y2 \/ X2))
by XBOOLE_1:24
.= ((Y1 \/ X1) /\ (Y1 \/ X2) /\ (Y2 \/ X1)) /\ (Y2 \/ X2)
by XBOOLE_1:16;
set A1 = min A, A2 = max A;
A6: A1 c= Y1 & A1 c= X1 by A3,A4,Th28; then
A7: A1 \/ A1 c= Y1 \/ X1 by XBOOLE_1:13;
Y1 c= Y1 \/ X2 by XBOOLE_1:7; then
A1 c= Y1 \/ X2 by A6; then
A8: A1 /\ A1 c= (Y1 \/ X1) /\ (Y1 \/ X2) by A7,XBOOLE_1:27;
A1 c= X1 & X1 c= Y2 \/ X1 by Th28,A3,XBOOLE_1:7; then
A1 c= Y2 \/ X1; then
A9: A1 c= (Y1 \/ X1) /\ (Y1 \/ X2) /\ (Y2 \/ X1) by A8,XBOOLE_1:19;
Y1 c= A2 & X1 c= A2 by A3,A4,Th28; then
(Y1 \/ X1) /\ ((Y1 \/ X2) /\ (Y2 \/ X1)) c= Y1 \/ X1 & Y1 \/ X1 c= A2
by XBOOLE_1:8,17; then
A1 c= (Y1 \/ X1) /\ (Y1 \/ X2) /\ (Y2 \/ X1) &
(Y1 \/ X1) /\ ((Y1 \/ X2) /\ (Y2 \/ X1)) c= A2 by A9;then
A1 c= (Y1 \/ X1) /\ (Y1 \/ X2) /\ (Y2 \/ X1) &
(Y1 \/ X1) /\ (Y1 \/ X2) /\ (Y2 \/ X1) c= A2
by XBOOLE_1:16; then
A10: (Y1 \/ X1) /\ (Y1 \/ X2) /\ (Y2 \/ X1) in A by Th28;
Y2 \/ X2 in UNION (B,C) by A3,A4,SETFAM_1:def 4;
hence thesis by A5,A10,SETFAM_1:def 5;
end;
hence thesis by A1;
end;
theorem
A _\/_ (B _/\_ C) = (A _\/_ B) _/\_ (A _\/_ C)
proof
A1: A _\/_ (B _/\_ C) c= (A _\/_ B) _/\_ (A _\/_ C) by Lm1;
(A _\/_ B) _/\_ (A _\/_ C) c= A _\/_ (B _/\_ C)
proof
let x be object;
assume x in (A _\/_ B) _/\_ (A _\/_ C); then
consider X, Y being set such that
A2: X in UNION (A,B) & Y in UNION (A,C) & x = X /\ Y by SETFAM_1:def 5;
A3: A is non empty ordered Subset-Family of U &
B is non empty ordered Subset-Family of U &
C is non empty ordered Subset-Family of U by Lm4;
x in INTERSECTION (UNION (A,B), UNION (A,C)) by A2,SETFAM_1:def 5;
hence thesis by Th29,A3;
end;
hence thesis by A1;
end;
theorem
A _/\_ (B _\/_ C) = (A _/\_ B) _\/_ (A _/\_ C)
proof
A1: A _/\_ (B _\/_ C) c= (A _/\_ B) _\/_ (A _/\_ C)
proof
let x be object;
assume x in A _/\_ (B _\/_ C); then
consider X, Y being set such that
A2: X in A & Y in UNION (B,C) & x = X /\ Y by SETFAM_1:def 5;
consider Z, W being set such that
A3: Z in B & W in C & Y = Z \/ W by A2,SETFAM_1:def 4;
A4: A is non empty ordered Subset-Family of U &
B is non empty ordered Subset-Family of U &
C is non empty ordered Subset-Family of U by Lm4;
X /\ (Z \/ W) in INTERSECTION (A, UNION (B,C)) by A2,A3,SETFAM_1:def 5;
hence thesis by A2,A3,Th30,A4;
end;
(A _/\_ B) _\/_ (A _/\_ C) c= A _/\_ (B _\/_ C)
proof
let x be object;
assume x in (A _/\_ B) _\/_ (A _/\_ C); then
consider X,Y being set such that
A5: X in INTERSECTION (A,B) & Y in INTERSECTION (A,C) & x = X \/ Y
by SETFAM_1:def 4;
A6: A is non empty ordered Subset-Family of U & B is non empty ordered
Subset-Family of U & C is non empty ordered Subset-Family of U by Lm4;
x in UNION (INTERSECTION (A,B), INTERSECTION (A,C))
by A5,SETFAM_1:def 4;
hence thesis by Th30,A6;
end;
hence thesis by A1;
end;
theorem Th33:
for X being set, A, B being non empty ordered Subset-Family of X holds
INTERSECTION (A, (UNION (A,B))) = A
proof
let X be set;
let A,B be non empty ordered Subset-Family of X;
set A1 = min A, A2 = max A;
A1: INTERSECTION (A, (UNION (A,B))) c= A
proof
let x be object;
assume x in INTERSECTION (A, (UNION (A,B))); then
consider Y,Z being set such that
A2: Y in A & Z in UNION (A,B) & x = Y /\ Z by SETFAM_1:def 5;
consider Z1,Z2 being set such that
A3: Z1 in A & Z2 in B & Z = Z1 \/ Z2 by A2,SETFAM_1:def 4;
A4: x = (Y /\ Z1) \/ (Y /\ Z2) by A2,A3,XBOOLE_1:23;
A5: (A1 c= Y & Y c= A2) & (A1 c= Z1 & Z1 c= A2) by Th28,A2,A3; then
A1 c= Y /\ Z1 & Y /\ Z1 c= A2 /\ A2 by XBOOLE_1:19,27; then
A6: A1 c= Y /\ Z1 & Y /\ Z1 c= A2 & Y /\ Z1 c= (Y /\ Z1) \/ (Y /\ Z2)
by XBOOLE_1:7; then
A7: A1 c= (Y /\ Z1) \/ (Y /\ Z2);
Y /\ Z2 c= Y by XBOOLE_1:17; then
Y /\ Z2 c= A2 by A5; then
(Y /\ Z1) \/ (Y /\ Z2) c= A2 by A6,XBOOLE_1:8;
hence thesis by Th28,A4,A7;
end;
A c= INTERSECTION (A, (UNION (A,B)))
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume A8: x in A;
set b = the Element of B;
A9: x = xx /\ (xx \/ b) by XBOOLE_1:21;
xx \/ b in UNION (A,B) by A8,SETFAM_1:def 4;
hence thesis by A8,A9,SETFAM_1:def 5;
end;
hence thesis by A1;
end;
theorem Th34:
for X being set, A, B being non empty ordered Subset-Family of X holds
UNION (INTERSECTION(A,B),B) = B
proof
let X be set;
let A,B be non empty ordered Subset-Family of X;
A1: UNION (INTERSECTION(A,B),B) c= B
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
set B1 = min B, B2 = max B;
assume x in UNION (INTERSECTION(A,B),B); then
consider Y,Z being set such that
A2: Y in INTERSECTION(A,B) & Z in B & x = Y \/ Z by SETFAM_1:def 4;
consider Y1,Y2 being set such that
A3: Y1 in A & Y2 in B & Y = Y1 /\ Y2 by A2,SETFAM_1:def 5;
B1 c= Y2 & Y2 c= B2 & Y1 /\ Y2 c= Y2 by A3,Th28,XBOOLE_1:17; then
A4: Y1 /\ Y2 c= B2;
Z c= B2 by A2,Th28; then
A5: xx c= B2 by A2,A3,A4,XBOOLE_1:8;
B1 c= Z & Z c= xx by A2,Th28,XBOOLE_1:7; then
B1 c= xx & xx c= B2 by A5;
hence thesis by Th28;
end;
B c= UNION (INTERSECTION(A,B),B)
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume A6: x in B;
set b = the Element of A;
A7: x = xx \/ (xx /\ b) by XBOOLE_1:22;
b /\ xx in INTERSECTION (A,B) by A6,SETFAM_1:def 5;
hence thesis by A7,A6,SETFAM_1:def 4;
end;
hence thesis by A1;
end;
theorem Th35:
A _/\_ (A _\/_ B) = A
proof
A is non empty ordered Subset-Family of U &
B is non empty ordered Subset-Family of U by Lm4;
hence thesis by Th33;
end;
theorem Th36:
(A _/\_ B) _\/_ B = B
proof
A is non empty ordered Subset-Family of U &
B is non empty ordered Subset-Family of U by Lm4;
hence thesis by Th34;
end;
begin :: Families of Subsets
theorem Th37:
for U being non empty set, A, B being Subset-Family of U holds
DIFFERENCE (A,B) is Subset-Family of U
proof
let U be non empty set,
A, B be Subset-Family of U;
DIFFERENCE (A,B) c= bool U
proof
let x be object; assume x in DIFFERENCE (A,B); then
consider Y,Z being set such that A1: Y in A & Z in B & x = Y \ Z
by SETFAM_1:def 6;
Y \ Z c= U by A1,XBOOLE_1:109;
hence thesis by A1;
end;
hence thesis;
end;
theorem Th38:
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}
proof
let U be non empty set;
let A,B be non empty ordered Subset-Family of U;
set A1 = min A, B1 = min B, A2 = max A, B2 = max B;
A1: DIFFERENCE (A,B) c= {C where C is Subset of U :
min A \ max B c= C & C c= max A \ min B}
proof
let x be object;
assume A2: x in DIFFERENCE (A,B); then
consider Y,Z being set such that A3: Y in A & Z in B & x = Y \ Z
by SETFAM_1:def 6;
DIFFERENCE (A,B) is Subset-Family of U by Th37; then
reconsider x as Subset of U by A2;
A1 c= Y & Y c= A2 & B1 c= Z & Z c= B2 by A3,Th28; then
A1 \ B2 c= x & x c= A2 \ B1 by A3,XBOOLE_1:35;
hence thesis;
end;
{C where C is Subset of U : min A \ max B c= C & C c= max A \ min B}
c= DIFFERENCE (A,B)
proof
let x be object;
assume x in {C where C is Subset of U :
min A \ max B c= C & C c= max A \ min B}; then
consider x9 being Subset of U such that
A4: x9 = x & min A \ max B c= x9 & x9 c= max A \ min B;
set A1 = min A, A2 = max A, B1 = min B, B2 = max B;
set z1 = (x9 \/ A1) /\ A2;
set z2 = ((x9 \/ B2`) /\ B1`)`;
B1 c= B2 by Lm2; then
A5: B2` c= B1` by SUBSET_1:12;
(x9 \/ B2`) /\ B1` = (x9 /\ B1`) \/ (B2` /\ B1`) by XBOOLE_1:23
.= (x9 /\ B1`) \/ B2` by A5,XBOOLE_1:28; then
A6: B2` c= (x9 \/ B2`) /\ B1` by XBOOLE_1:7;
(x9 \/ B2`) /\ B1` c= B1` by XBOOLE_1:17; then
A7: ((x9 \/ B2`) /\ B1`)` c= B2`` &
B1`` c= ((x9 \/ B2`) /\ B1`)` by A6,SUBSET_1:12;
z1 = (x9 /\ A2) \/ (A1 /\ A2) by XBOOLE_1:23
.= (x9 /\ A2) \/ A1 by SETFAM_1:2,XBOOLE_1:28; then
A1 c= z1 & z1 c= A2 by XBOOLE_1:7,17; then
A8: z1 in A & z2 in B by Th28,A7;
A9: (x9 \/ (A1 \ B2)) /\ (A2 \ B1) = x9 /\ (A2 \ B1) by A4,XBOOLE_1:12
.= x9 by A4,XBOOLE_1:28;
z1 \ z2 = z1 /\ z2` by SUBSET_1:13
.= (x9 \/ A1) /\ (A2 /\ ((x9 \/ B2`) /\ B1`)) by XBOOLE_1:16
.= (x9 \/ A1) /\ ((x9 \/ B2`) /\ (B1` /\ A2)) by XBOOLE_1:16
.= (x9 \/ A1) /\ ((x9 \/ B2`) /\ (A2 \ B1)) by SUBSET_1:13
.= ((x9 \/ A1) /\ (x9 \/ B2`)) /\ (A2 \ B1) by XBOOLE_1:16
.= (x9 \/ (A1 /\ B2`)) /\ (A2 \ B1) by XBOOLE_1:24
.= x9 by A9,SUBSET_1:13;
hence thesis by A4,A8,SETFAM_1:def 6;
end;
hence thesis by A1;
end;
theorem Th39:
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 }
proof
let U be non empty set;
let A1,A2,B1,B2 be Subset of U;
assume A1 c= A2 & B1 c= B2; then
reconsider A12 = Inter (A1,A2), B12 = Inter (B1,B2)
as non empty ordered Subset-Family of U by Th25;
A1: min A12 = A1 & max A12 = A2 by Th27;
min B12 = B1 & max B12 = B2 by Th27;
hence thesis by Th38,A1;
end;
definition let U be non empty set,
A, B be non empty IntervalSet of U;
func A _\_ B -> IntervalSet of U equals
DIFFERENCE (A, B);
coherence
proof
set IT = DIFFERENCE (A, B);
consider A1, A2 being Subset of U such that
A1: A1 c= A2 & A = Inter (A1, A2) by Th11;
consider B1, B2 being Subset of U such that
A2: B1 c= B2 & B = Inter (B1, B2) by Th11;
set LAB = A1 \ B2;
set UAB = A2 \ B1;
IT = Inter (LAB, UAB) by Th39,A1,A2;
hence thesis;
end;
end;
registration let U be non empty set,
A, B be non empty IntervalSet of U;
cluster A _\_ B -> non empty;
coherence
proof
A _\_ B <> {}
proof
assume A1:A _\_ B = {};
consider A1, A2 being Subset of U such that
A2: A1 c= A2 & A = Inter (A1, A2) by Th11;
consider B1, B2 being Subset of U such that
A3: B1 c= B2 & B = Inter (B1, B2) by Th11;
consider y being set such that A4: y = A1 \ B1;
not (A1 in A & B1 in B & y = A1 \ B1) by A1,SETFAM_1:def 6;
hence thesis by A4,A2,A3;
end;
hence thesis;
end;
end;
theorem Th40:
A _\_ B = Inter (A``1 \ B``2, A``2 \ B``1)
proof
reconsider AA = A, BB = B as non empty ordered Subset-Family of U
by Th26;
AA = Inter (A``1,A``2) & BB = Inter (B``1,B``2) by Th15; then
min AA = A``1 & min BB = B``1 & max AA = A``2 & max BB = B``2 by Th27;
hence thesis by Th38;
end;
theorem Th41:
for X,Y being Subset of U st A = Inter (X,Y) holds
A _\_ C = Inter (X \ C``2, Y \ C``1)
proof
let X,Y be Subset of U;
assume A1: A = Inter (X,Y);
A = Inter (A``1,A``2) by Th15; then
X = A``1 & Y = A``2 by A1,Th6;
hence thesis by Th40;
end;
theorem Th42:
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
let X,Y,W,Z be Subset of U;
assume A1: A = Inter (X,Y) & C = Inter (W,Z);
A= Inter (A``1,A``2) & C = Inter (C``1,C``2) by Th15; then
A``1 = X & A``2 = Y & C``1 = W & C``2 = Z by A1,Th6;
hence thesis by Th40;
end;
theorem Th43:
for U being non empty set holds
Inter ([#]U,[#]U) is non empty IntervalSet of U
proof
let U be non empty set;
Inter ([#]U,[#]U) = {[#]U} by Th8;
hence thesis;
end;
theorem Th44:
for U being non empty set holds Inter ({}U,{}U) is non empty IntervalSet of U
proof
let U be non empty set;
Inter ({}U,{}U) = {{}} by Th8;
hence thesis;
end;
registration let U be non empty set;
cluster Inter ([#]U,[#]U) -> non empty;
coherence by Th43;
cluster Inter ({}U,{}U) -> non empty;
coherence by Th44;
end;
definition let U be non empty set, A be non empty IntervalSet of U;
func A ^ -> non empty IntervalSet of U equals
Inter ([#]U,[#]U) _\_ A;
coherence;
end;
theorem Th45:
for U being non empty set, A being non empty IntervalSet of U holds
A^ = Inter ((A``2)`,(A``1)`) by Th41;
theorem Th46:
for X,Y being Subset of U st A = Inter (X,Y) & X c= Y holds
A^ = Inter (Y`,X`)
proof
let X,Y be Subset of U;
assume A1: A = Inter (X,Y) & X c= Y;
then Inter (X,Y) = Inter (A``1,A``2) by Th15; then
X = A``1 & Y = A``2 by Th6,A1;
hence thesis by Th41;
end;
theorem
(Inter ({}U,{}U))^ = Inter ([#]U,[#]U)
proof
(Inter ({}U,{}U))^ = Inter ([#]U,({}U)`) by Th46;
hence thesis;
end;
theorem
(Inter ([#]U,[#]U))^ = Inter ({}U,{}U)
proof
(Inter ([#]U,[#]U))^ = Inter (([#]U)`,([#]U)`) by Th46
.= Inter ({}U,([#]U)`) by XBOOLE_1:37;
hence thesis by XBOOLE_1:37;
end;
begin :: Counterexamples
theorem
ex A being non empty IntervalSet of U st A _/\_ A^ <> Inter ({}U,{}U)
proof
A1: [#]U in Inter ({}U,[#]U); then
consider A being non empty IntervalSet of U such that
A2: A = Inter ({}U,[#]U);
A3: A^ = Inter (([#]U)`,({}U)`) by A2,Th46
.= Inter ({}U,[#]U);
A^ = Inter (A^``1,A^``2) by Th15; then
A^``1 = {}U & A^``2 = [#]U by Th6,A3; then
A4: A _/\_ A^ = Inter ({}U /\ {}U, [#]U /\ [#]U) by A2,Th18,A3
.= Inter ({}U, [#]U);
not [#]U c= {}U; then
not [#]U in Inter ({}U,{}U) by Th1;
hence thesis by A4,A1;
end;
theorem
ex A being non empty IntervalSet of U st A _\/_ A^ <> Inter ([#]U,[#]U)
proof
not [#]U c= {}U; then
A1: not {}U in Inter ([#]U,[#]U) by Th1;
A2: {}U in Inter ({}U,[#]U); then
consider A being non empty IntervalSet of U such that
A3: A = Inter ({}U,[#]U);
A4: A^ = Inter (([#]U)`,({}U)`) by Th46,A3
.= Inter ({}U,[#]U);
A^ = Inter (A^``1,A^``2) by Th15; then
A^``1 = {}U & A^``2 = [#]U by Th6,A4; then
A _\/_ A^ = Inter ({}U \/ {}U, [#]U \/ [#]U) by Th17,A3,A4
.= Inter ({}U,[#]U);
hence thesis by A2,A1;
end;
theorem
ex A being non empty IntervalSet of U st A _\_ A <> Inter ({}U,{}U)
proof
Inter ({}U,[#]U) <> {} by Th1; then
consider A being non empty IntervalSet of U such that
A1: A = Inter ({}U,[#]U);
A2: A _\_ A = Inter ({}U \ [#]U, [#]U \ {}U) by Th42,A1
.= Inter ({}U, [#]U);
not U c= {}; then
[#]U in Inter ({}U,[#]U) & not [#]U in Inter ({}U,{}U) by Th1;
hence thesis by A2;
end;
theorem
for A being non empty IntervalSet of U holds U in A _\/_ (A^)
proof
let A be non empty IntervalSet of U;
A1: U c= A``2 \/ (A``1)`
proof
let x be object;
assume A2: x in U;
A``1 c= A``2 by Th16; then
A3: (A``2)` c= (A``1)` by SUBSET_1:12;
x in A``2 or x in (A``2)` by A2,XBOOLE_0:def 5;
hence thesis by A3,XBOOLE_0:def 3;
end;
A4: A^ = Inter ((A``2)`,(A``1)`) by Th45;
A^ = Inter (A^``1,A^``2) by Th15; then
A^``1 = (A``2)` & A^``2 = (A``1)` by Th6,A4;
then A _\/_ (A^) = Inter (A``1 \/ (A``2)`, A``2 \/ (A``1)`) by Th17;
hence thesis by A1;
end;
theorem
for A being non empty IntervalSet of U holds {} in A _/\_ (A^)
proof
let A be non empty IntervalSet of U;
A1: A``1 /\ (A``2)` c= {}
proof
let x be object;
A2: A``1 c= A``2 by Th16;
assume x in A``1 /\ (A``2)`; then
x in A``1 & x in (A``2)` by XBOOLE_0:def 4;
hence thesis by A2,XBOOLE_0:def 5;
end;
A3: A^ = Inter ((A``2)`,(A``1)`) by Th45;
A^ = Inter ((A^)``1, (A^)``2) by Th15; then
A^``1 = (A``2)` & A^``2 = (A``1)` by Th6,A3;
then A4: A _/\_ (A^) = Inter (A``1 /\ (A``2)`, A``2 /\ (A``1)`) by Th18;
A``1 /\ (A``2)` c= {} & {} c= A``2 /\ (A``1)` by A1;
hence thesis by A4,Th1;
end;
theorem
for A being non empty IntervalSet of U holds {} in A _\_ A
proof
let A be non empty IntervalSet of U;
A1: A _\_ A = Inter (A``1 \ A``2, A``2 \ A``1) by Th40;
A2: A``1 \ A``2 c= {}
proof
let x be object;
assume x in A``1 \ A``2; then
x in A``1 & not x in A``2 & A``1 c= A``2 by Th16,XBOOLE_0:def 5;
hence thesis;
end;
{} c= A``2 \ A``1;
hence thesis by Th1,A2,A1;
end;
begin :: Lattice of Interval Sets
definition let U be non empty set;
func IntervalSets U -> non empty set means :Def11:
for x being set holds x in it iff x is non empty IntervalSet of U;
existence
proof
defpred P[set] means $1 is non empty IntervalSet of U;
ex X being set st for x being set holds
x in X iff x in bool bool U & P[x] from XFAMILY:sch 1; then
consider X being set such that
A1: for x being set holds x in X iff x in bool bool U & P[x];
set x = the Element of U;
reconsider E = {x} as Subset of U by ZFMISC_1:31;
{E} is non empty IntervalSet of U by Th10; then
reconsider X as non empty set by A1;
take X;
thus thesis by A1;
end;
uniqueness
proof
let S1,S2 be non empty set such that
A2: for x being set holds x in S1 iff x is non empty IntervalSet of U and
A3: for x being set holds x in S2 iff x is non empty IntervalSet of U;
for x being object holds x in S1 iff x in S2
by A3,A2;
hence thesis by TARSKI:2;
end;
end;
definition let U be non empty set;
func InterLatt U -> strict non empty LattStr means :Def12:
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;
existence
proof
set B = IntervalSets U;
defpred P[Element of B,Element of B,Element of B] means
ex a9, b9 being non empty IntervalSet of U st a9 = $1 & b9 = $2 &
$3 = a9 _\/_ b9;
A1: for x,y being Element of B ex z being Element of B st P[x,y,z]
proof
let x,y be Element of B;
reconsider x9 = x, y9 = y as non empty IntervalSet of U by Def11;
reconsider z = x9 _\/_ y9 as Element of B by Def11;
take z;
thus thesis;
end;
consider B1 being BinOp of B such that A2:
for x,y being Element of B holds P[x,y,B1.(x,y)] from BINOP_1:sch 3(A1);
defpred R[Element of B,Element of B,Element of B] means
ex a9, b9 being non empty IntervalSet of U st a9 = $1 & b9 = $2 &
$3 = a9 _/\_ b9;
A3: for x,y being Element of B ex z being Element of B st R[x,y,z]
proof
let x,y be Element of B;
reconsider x9 = x, y9 = y as non empty IntervalSet of U by Def11;
reconsider z = x9 _/\_ y9 as Element of B by Def11;
take z;
thus thesis;
end;
consider B2 being BinOp of B such that
A4: for x,y being Element of B holds R[x,y,B2.(x,y)] from BINOP_1:sch 3(A3);
take IT = LattStr (# B, B1, B2 #);
thus the carrier of IT = IntervalSets U;
let a, b be Element of the carrier of IT,
a9, b9 be non empty IntervalSet of U;
assume
A5: a9 = a & b9 = b;
reconsider x = a, y = b as Element of B;
consider a9, b9 being non empty IntervalSet of U such that
A6: a9 = x & b9 = y & B1.(x,y) = a9 _\/_ b9 by A2;
consider a1, b1 being non empty IntervalSet of U such that
A7: a1 = x & b1 = y & B2.(x,y) = a1 _/\_ b1 by A4;
thus thesis by A6,A7,A5;
end;
uniqueness
proof
let L1,L2 be strict non empty LattStr such that
A8: the carrier of L1 = IntervalSets U &
for a, b being Element of the carrier of L1,
a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds
(the L_join of L1).(a,b) = a9 _\/_ b9 &
(the L_meet of L1).(a,b) = a9 _/\_ b9 and
A9: the carrier of L2 = IntervalSets U &
for a, b being Element of the carrier of L2,
a9, b9 being non empty IntervalSet of U st a9 = a & b9 = b holds
(the L_join of L2).(a,b) = a9 _\/_ b9 &
(the L_meet of L2).(a,b) = a9 _/\_ b9;
for a, b being Element of L1 holds
(the L_join of L1).(a,b) = (the L_join of L2).(a,b)
proof
let a,b be Element of L1;
reconsider a9 = a, b9 = b as non empty IntervalSet of U by A8,Def11;
(the L_join of L1).(a,b) = a9 _\/_ b9 by A8
.= (the L_join of L2).(a,b) by A9,A8;
hence thesis;
end; then
A10: the L_join of L1 = the L_join of L2 by A8,A9,BINOP_1:2;
for a, b being Element of L1 holds
(the L_meet of L1).(a,b) = (the L_meet of L2).(a,b)
proof
let a,b be Element of L1;
reconsider a9 = a, b9 = b as non empty IntervalSet of U by A8,Def11;
(the L_meet of L1).(a,b) = a9 _/\_ b9 by A8
.= (the L_meet of L2).(a,b) by A8,A9;
hence thesis;
end;
hence thesis by A8,A9,A10,BINOP_1:2;
end;
end;
registration let U be non empty set;
cluster InterLatt U -> Lattice-like;
correctness
proof
A1: InterLatt U is join-commutative
proof
for a,b being Element of InterLatt U holds a"\/"b = b"\/"a
proof
let a,b be Element of InterLatt U;
a in the carrier of InterLatt U & b in the carrier of InterLatt U; then
a in IntervalSets U & b in IntervalSets U by Def12; then
reconsider a9 = a, b9 = b as non empty IntervalSet of U by Def11;
a "\/" b = a9 _\/_ b9 by Def12
.= b9 _\/_ a9
.= b "\/" a by Def12;
hence thesis;
end;
hence thesis;
end;
A2: InterLatt U is join-associative
proof
for a,b,c being Element of InterLatt U
holds a"\/"(b"\/"c) = (a"\/"b)"\/"c
proof
let a,b,c be Element of InterLatt U;
a in the carrier of InterLatt U & b in the carrier of InterLatt U &
c in the carrier of InterLatt U; then
a in IntervalSets U & b in IntervalSets U & c in IntervalSets U
by Def12; then
reconsider a9 = a, b9 = b, c9 = c as non empty IntervalSet of U
by Def11;
reconsider bc = b9 _\/_ c9 as non empty IntervalSet of U;
reconsider ab = a9 _\/_ b9 as non empty IntervalSet of U;
bc in IntervalSets U & ab in IntervalSets U by Def11; then
A3: bc in the carrier of InterLatt U & ab in the carrier of InterLatt U
by Def12;
a "\/" (b "\/" c) = (the L_join of InterLatt U).(a,bc) by Def12
.= a9 _\/_ bc by Def12,A3
.= (a9 _\/_ b9) _\/_ c9 by Th23
.= (the L_join of InterLatt U).(ab,c9) by Def12,A3
.= a "\/" b "\/" c by Def12;
hence thesis;
end;
hence thesis;
end;
A4: InterLatt U is meet-absorbing
proof
for a,b being Element of InterLatt U holds (a"/\"b)"\/"b = b
proof
let a,b be Element of InterLatt U;
a in the carrier of InterLatt U & b in the carrier of InterLatt U; then
a in IntervalSets U & b in IntervalSets U by Def12; then
reconsider a9 = a, b9 = b as non empty IntervalSet of U
by Def11;
reconsider ab = a9 _/\_ b9 as non empty IntervalSet of U;
ab in IntervalSets U by Def11; then
A5: ab in the carrier of InterLatt U by Def12;
(a"/\"b)"\/"b = (the L_join of InterLatt U).(ab,b) by Def12
.= ab _\/_ b9 by Def12,A5
.= b by Th36;
hence thesis;
end;
hence thesis;
end;
A6: InterLatt U is meet-associative
proof
for a,b,c being Element of InterLatt U holds
a"/\"(b"/\"c) = (a"/\"b) "/\"c
proof
let a,b,c be Element of InterLatt U;
a in the carrier of InterLatt U & b in the carrier of InterLatt U &
c in the carrier of InterLatt U; then
a in IntervalSets U & b in IntervalSets U & c in IntervalSets U
by Def12; then
reconsider a9 = a, b9 = b, c9 = c as non empty IntervalSet of U
by Def11;
reconsider bc = b9 _/\_ c9, ab = a9 _/\_ b9
as non empty IntervalSet of U;
bc in IntervalSets U & ab in IntervalSets U by Def11; then
A7: bc in the carrier of InterLatt U & ab in the carrier of InterLatt U
by Def12;
a"/\"(b"/\"c) = (the L_meet of InterLatt U).(a,bc) by Def12
.= a9 _/\_ bc by Def12,A7
.= (a9 _/\_ b9) _/\_ c9 by Th24
.= (the L_meet of InterLatt U).(ab,c9) by Def12,A7
.= (a"/\"b)"/\"c by Def12;
hence thesis;
end;
hence thesis;
end;
A8: InterLatt U is join-absorbing
proof
for a,b being Element of the carrier of InterLatt U holds a"/\"(a"\/"b)=a
proof
let a,b be Element of the carrier of InterLatt U;
a in the carrier of InterLatt U & b in the carrier of InterLatt U; then
a in IntervalSets U & b in IntervalSets U by Def12; then
reconsider a9 = a, b9 = b as non empty IntervalSet of U by Def11;
reconsider ab = a9 _\/_ b9 as non empty IntervalSet of U;
ab in IntervalSets U by Def11; then
A9: ab in the carrier of InterLatt U by Def12;
a "/\" (a "\/" b)
= (the L_meet of InterLatt U).(a9,a9 _\/_ b9) by Def12
.= a9 _/\_ ab by Def12,A9
.= a by Th35;
hence thesis;
end;
hence thesis;
end;
InterLatt U is meet-commutative
proof
for a,b being Element of the carrier of InterLatt U holds a"/\"b = b"/\"a
proof
let a,b be Element of the carrier of InterLatt U;
a in the carrier of InterLatt U & b in the carrier of InterLatt U; then
a in IntervalSets U & b in IntervalSets U by Def12; then
reconsider a9 = a, b9 = b as non empty IntervalSet of U by Def11;
a9 _/\_ b9 = b9 _/\_ a9; then
(the L_meet of InterLatt U).(a,b) = b9 _/\_ a9 by Def12
.= (the L_meet of InterLatt U).(b,a) by Def12;
hence thesis;
end;
hence thesis;
end;
hence thesis by A1,A2,A4,A6,A8;
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:
not contradiction;
existence;
end;
theorem Th55:
for X being Tolerance_Space, A being RoughSet of X holds
ex B, C being Subset of X st A = [B,C]
proof
let X be Tolerance_Space,
A be RoughSet of X;
consider A1, A2 being object such that
A1: A1 in bool the carrier of X & A2 in bool the carrier of X & A = [A1,A2]
by ZFMISC_1:def 2;
reconsider A1, A2 as Subset of X by A1;
take A1, A2;
thus thesis by A1;
end;
definition let X be Tolerance_Space, A be Subset of X;
func RS A -> RoughSet of X equals
[LAp A, UAp A];
coherence
proof
[LAp A, UAp A] in [:bool the carrier of X, bool the carrier of X:]
by ZFMISC_1:87;
hence thesis by Def13;
end;
end;
definition let X be Tolerance_Space, A be RoughSet of X;
func LAp A -> Subset of X equals
A`1;
coherence
proof
consider A9, B9 being Subset of X such that
A1: A = [A9, B9] by Th55;
thus thesis by A1;
end;
func UAp A -> Subset of X equals
A`2;
coherence
proof
consider A9, B9 being Subset of X such that
A2: A = [A9, B9] by Th55;
thus thesis by A2;
end;
end;
definition let X be Tolerance_Space; let A, B be RoughSet of X;
redefine pred A = B means :: redefines = (XBOOLE_0, redefinition) → = (HIDDEN, definition)
LAp A = LAp B & UAp A = UAp B;
compatibility
proof
thus A = B implies LAp A = LAp B & UAp A = UAp B;
assume A1: LAp A = LAp B & UAp A = UAp B;
consider A1, B1 being Subset of X such that
A2: A = [A1, B1] by Th55;
consider A2, B2 being Subset of X such that
A3: B = [A2, B2] by Th55;
LAp A = A1 by A2; then
A4: A1 = A2 by A1,A3;
UAp A = B1 by A2;
then B1 = B2 by A1, A3;
hence A = B by A2,A4,A3;
end;
end;
definition let X be Tolerance_Space; let A, B be RoughSet of X;
func A _\/_ B -> RoughSet of X equals
[LAp A \/ LAp B, UAp A \/ UAp B];
coherence
proof
[LAp A \/ LAp B, UAp A \/ UAp B] in
[:bool the carrier of X, bool the carrier of X:] by ZFMISC_1:87;
hence thesis by Def13;
end;
func A _/\_ B -> RoughSet of X equals
[LAp A /\ LAp B, UAp A /\ UAp B];
coherence
proof
[LAp A /\ LAp B, UAp A /\ UAp B] in
[:bool the carrier of X, bool the carrier of X:] by ZFMISC_1:87;
hence thesis by Def13;
end;
end;
reserve X for Tolerance_Space,
A, B, C for RoughSet of X;
theorem
LAp (A _\/_ B) = LAp A \/ LAp B;
theorem
UAp (A _\/_ B) = UAp A \/ UAp B;
theorem
LAp (A _/\_ B) = LAp A /\ LAp B;
theorem
UAp (A _/\_ B) = UAp A /\ UAp B;
:: Properties
theorem
A _\/_ A = A;
theorem Th61:
A _/\_ A = A;
theorem
A _\/_ B = B _\/_ A;
theorem
A _/\_ B = B _/\_ A;
theorem Th64:
A _\/_ B _\/_ C = A _\/_ (B _\/_ C) by XBOOLE_1:4;
theorem Th65:
A _/\_ B _/\_ C = A _/\_ (B _/\_ C) by XBOOLE_1:16;
theorem Th66:
A _/\_ (B _\/_ C) = (A _/\_ B) _\/_ (A _/\_ C) by XBOOLE_1:23;
theorem Th67:
A _\/_ (A _/\_ B) = A by XBOOLE_1:22;
theorem
A _/\_ (A _\/_ B) = A by XBOOLE_1:21;
begin :: Lattice of Rough Sets
definition let X;
func RoughSets X -> set means :Def20:
for x being set holds x in it iff x is RoughSet of X;
existence
proof
defpred P[object] means $1 is RoughSet of X;
consider F being set such that
A1: for x being object holds x in F iff
x in [:bool the carrier of X,bool the carrier of X:] & P[x]
from XBOOLE_0:sch 1;
take F;
let x be set;
thus x in F implies x is RoughSet of X by A1;
assume x is RoughSet of X;
hence thesis by A1;
end;
uniqueness
proof
let F1,F2 be set such that
A2: (for x being set holds x in F1 iff x is RoughSet of X) &
(for x being set holds x in F2 iff x is RoughSet of X);
for x being object holds x in F1 iff x in F2 by A2;
hence thesis by TARSKI:2;
end;
end;
registration let X;
cluster RoughSets X -> non empty;
coherence
proof
set A = the RoughSet of X;
A in RoughSets X by Def20;
hence thesis;
end;
end;
definition let X; let R be Element of RoughSets X;
func @R -> RoughSet of X equals
R;
coherence by Def20;
end;
definition let X; let R be RoughSet of X;
func R@ -> Element of RoughSets X equals
R;
coherence by Def20;
end;
definition let X;
func RSLattice X -> strict LattStr means :Def23:
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;
existence
proof
deffunc U(Element of RoughSets X,
Element of RoughSets X) = (@$1 _\/_ @$2)@;
consider j being BinOp of RoughSets X such that
A1: for x,y being Element of RoughSets X holds j.(x,y) = U(x,y)
from BINOP_1:sch 4;
deffunc W(Element of RoughSets X,
Element of RoughSets X) = (@$1 _/\_ @$2)@;
consider m being BinOp of RoughSets X such that
A2: for x,y being Element of RoughSets X holds m.(x,y) = W(x,y)
from BINOP_1:sch 4;
take IT = LattStr (# RoughSets X, j, m #);
thus the carrier of IT = RoughSets X;
let A, B be Element of RoughSets X,
A9, B9 be RoughSet of X;
assume
A3: A = A9 & B = B9;
thus (the L_join of IT).(A,B) = U(A,B) by A1
.= A9 _\/_ B9 by A3;
thus (the L_meet of IT).(A,B) = W(A,B) by A2
.= A9 _/\_ B9 by A3;
end;
uniqueness
proof
let A1, A2 be strict LattStr such that
A4: the carrier of A1 = 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 A1).(A,B) = A9 _\/_ B9 &
(the L_meet of A1).(A,B) = A9 _/\_ B9 and
A5: the carrier of A2 = 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 A2).(A,B) = A9 _\/_ B9 &
(the L_meet of A2).(A,B) = A9 _/\_ B9;
reconsider a3 = the L_meet of A1, a4 = the L_meet of A2,
a1 = the L_join of A1, a2 = the L_join of A2
as BinOp of RoughSets X by A4,A5;
now let x,y be Element of RoughSets X;
thus a1.(x,y) = @x _\/_ @y by A4
.= a2.(x,y) by A5;
end;
then A6: a1 = a2 by BINOP_1:2;
now let x,y be Element of RoughSets X;
thus a3.(x,y) = @x _/\_ @y by A4
.= a4.(x,y) by A5;
end;
hence thesis by A4,A5,A6,BINOP_1:2;
end;
end;
registration let X;
cluster RSLattice X -> non empty;
coherence
proof
the carrier of RSLattice X = RoughSets X by Def23;
hence thesis;
end;
end;
Lm6: for a,b being Element of RSLattice X holds a "\/" b = b "\/" a
proof
set G = RSLattice X;
let a,b be Element of G;
reconsider a1 = a, b1 = b as Element of RoughSets X by Def23;
reconsider a9 = a1, b9 = b1 as RoughSet of X by Def20;
a "\/" b = a9 _\/_ b9 by Def23
.= b9 _\/_ a9
.= b "\/" a by Def23;
hence thesis;
end;
Lm7:for a,b,c being Element of RSLattice X holds a"\/"(b"\/"c) = (a"\/"b)"\/"c
proof
let a, b, c be Element of RSLattice X;
reconsider a1 = a, b1 = b, c1 = c as Element of RoughSets X by Def23;
reconsider a9 = a1, b9 = b1, c9 = c1 as RoughSet of X by Def20;
set G = RSLattice X;
A1: b9 _\/_ c9 is Element of RoughSets X by Def20;
A2: a9 _\/_ b9 is Element of RoughSets X by Def20;
a"\/"(b"\/"c) = (the L_join of G).(a,(b9 _\/_ c9)) by Def23
.= a9 _\/_ (b9 _\/_ c9) by Def23,A1
.= (a9 _\/_ b9) _\/_ c9 by Th64
.= (the L_join of G).((a9 _\/_ b9), c1) by Def23,A2
.= (a"\/"b)"\/"c by Def23;
hence thesis;
end;
reserve K,L,M for Element of RoughSets X;
Lm8:(the L_join of RSLattice X). ((the L_meet of RSLattice X).(K,L), L) = L
proof
reconsider K9 = K, L9 = L as RoughSet of X by Def20;
A1: K9 _/\_ L9 is Element of RoughSets X by Def20;
thus (the L_join of RSLattice X). ((the L_meet of RSLattice X).(K,L), L) =
(the L_join of RSLattice X).((K9 _/\_ L9),L) by Def23
.= (K9 _/\_ L9) _\/_ L9 by Def23,A1
.= L9 _\/_ (L9 _/\_ K9)
.= L by Th67;
end;
Lm9: for a,b being Element of RSLattice X holds (a"/\"b)"\/"b = b
proof
let a,b be Element of RSLattice X;
set G = RSLattice X;
reconsider a1 = a, b1 = b as Element of RoughSets X by Def23;
thus (a"/\"b)"\/"b = (the L_join of G).((the L_meet of G).(a1,b1), b1)
.= b by Lm8;
end;
Lm10: for a,b being Element of RSLattice X holds a"/\"b = b"/\"a
proof
let a, b be Element of RSLattice X;
reconsider a1 = a, b1 = b as Element of RoughSets X by Def23;
reconsider a9 = a1, b9 = b1 as RoughSet of X by Def20;
a"/\"b = a9 _/\_ b9 by Def23
.= b9 _/\_ a9
.= b"/\"a by Def23;
hence thesis;
end;
Lm11: for a,b,c being Element of RSLattice X holds
a"/\"(b"/\"c) = (a"/\"b)"/\"c
proof
let a, b, c be Element of RSLattice X;
reconsider a1 = a, b1 = b, c1 = c as Element of RoughSets X by Def23;
reconsider a9 = a1, b9 = b1, c9 = c1 as RoughSet of X by Def20;
set G = RSLattice X;
A1: b9 _/\_ c9 is Element of RoughSets X by Def20;
A2: a9 _/\_ b9 is Element of RoughSets X by Def20;
a"/\"(b"/\"c) = (the L_meet of G).(a1,(b9 _/\_ c9)) by Def23
.= a9 _/\_ (b9 _/\_ c9) by Def23,A1
.= (a9 _/\_ b9) _/\_ c9 by Th65
.= (the L_meet of G).((a9 _/\_ b9), c1) by Def23,A2
.= (a"/\"b)"/\"c by Def23;
hence thesis;
end;
Lm12: (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
set G = RSLattice X;
reconsider K9 = K, L9 = L, M9 = M as RoughSet of X by Def20;
A1: L9 _\/_ M9 is Element of RoughSets X by Def20;
A2: K9 _/\_ L9 is Element of RoughSets X by Def20;
A3: K9 _/\_ M9 is Element of RoughSets X by Def20;
(the L_meet of G).(K,(the L_join of G).(L,M)) =
(the L_meet of G).(K,(L9 _\/_ M9)) by Def23
.= K9 _/\_ (L9 _\/_ M9) by Def23,A1
.= (K9 _/\_ L9) _\/_ (K9 _/\_ M9) by Th66
.= (the L_join of G).((K9 _/\_ L9),(K9 _/\_ M9)) by Def23,A2,A3
.= (the L_join of G).((the L_meet of G).(K,L),(K9 _/\_ M9)) by Def23
.= (the L_join of G).((the L_meet of G).(K,L),(the L_meet of G).(K,M))
by Def23;
hence thesis;
end;
Lm13: for a,b being Element of RSLattice X holds a"/\"(a"\/"b)=a
proof
let a, b be Element of RSLattice X;
set G = RSLattice X;
reconsider a1 = a, b1 = b as Element of RoughSets X by Def23;
reconsider a9 = a1 as RoughSet of X by Def20;
thus a"/\"(a"\/"b) = (the L_join of G).((the L_meet of G).(a1,a1),
(the L_meet of G).(a1,b1)) by Lm12
.= (the L_join of G).(a9 _/\_ a9,
(the L_meet of G).(a1,b1)) by Def23
.= a"\/"(a"/\"b) by Th61
.= (a"/\"b)"\/"a by Lm6
.= (b"/\"a)"\/"a by Lm10
.= a by Lm9;
end;
registration let X;
cluster RSLattice X -> Lattice-like;
coherence
proof
set G = RSLattice X;
thus for u,v being Element of G holds u"\/"v = v"\/"u by Lm6;
thus for u,v,w being Element of G holds
u"\/"(v"\/"w) = (u"\/"v)"\/"w by Lm7;
thus for u,v being Element of G holds (u"/\"v)"\/"v = v by Lm9;
thus for u,v being Element of G holds u"/\"v = v"/\"u by Lm10;
thus for u,v,w being Element of G holds
u"/\"(v"/\"w) = (u"/\"v)"/\"w by Lm11;
let u,v be Element of G;
thus u"/\"(u"\/"v) = u by Lm13;
end;
end;
registration let X;
cluster RSLattice X -> distributive;
coherence
proof
let u,v,w be Element of RSLattice X;
reconsider K = u, L = v, M = w as Element of RoughSets X by Def23;
thus u "/\" (v "\/" w) =
(the L_join of RSLattice X).((the L_meet of RSLattice X).(K,L),
(the L_meet of RSLattice X).(K,M)) by Lm12
.= (u "/\" v) "\/" (u "/\" w);
end;
end;
definition let X;
func ERS X -> RoughSet of X equals
[{},{}];
coherence
proof
reconsider A = {} as Subset of X by XBOOLE_1:2;
A = {}X; then
A1: LAp A = {} & UAp A = {} by ROUGHS_1:18,19;
[LAp A, UAp A] in [:bool the carrier of X, bool the carrier of X:]
by ZFMISC_1:87;
hence thesis by Def13,A1;
end;
end;
Lm14:
ERS X in RoughSets X by Def20;
theorem Th69:
for A being RoughSet of X holds ERS X _\/_ A = A;
definition let X;
func TRS X -> RoughSet of X equals
[[#]X,[#]X];
coherence
proof
reconsider A = [#]X as Subset of X;
A1: LAp A = [#]X & UAp A = [#]X by ROUGHS_1:20,21;
[LAp A, UAp A] in [:bool the carrier of X, bool the carrier of X:]
by ZFMISC_1:87;
hence thesis by Def13,A1;
end;
end;
Lm15:
TRS X in RoughSets X by Def20;
theorem Th70:
for A being RoughSet of X holds TRS X _/\_ A = A by XBOOLE_1:28;
registration let X;
cluster RSLattice X -> bounded;
coherence
proof
thus RSLattice X is lower-bounded
proof
reconsider E = ERS X as Element of RoughSets X by Lm14;
reconsider e = E as Element of RSLattice X by Def23;
take e;
let u be Element of RSLattice X;
reconsider K = u as Element of RoughSets X by Def23;
reconsider E9 = E , K9 = K as RoughSet of X by Def20;
e"\/"u = E9 _\/_ K9 by Def23
.= u by Th69; then
e "/\" u = e & u "/\" e = e by LATTICES:def 9;
hence thesis;
end;
thus RSLattice X is upper-bounded
proof
reconsider E = TRS X as Element of RoughSets X by Lm15;
reconsider e = E as Element of RSLattice X by Def23;
take e;
let u be Element of RSLattice X;
reconsider K = u as Element of RoughSets X by Def23;
reconsider E9 = E , K9 = K as RoughSet of X by Def20;
e"/\"u = E9 _/\_ K9 by Def23
.= u by Th70; then
e "\/" u = e & u "\/" e = e by LATTICES:def 8;
hence thesis;
end;
end;
end;
theorem Th71:
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
proof
let X be Tolerance_Space,
A, B be Element of RSLattice X,
A9, B9 be RoughSet of X;
assume
A1: A = A9 & B = B9;
A2: A is Element of RoughSets X & B is Element of RoughSets X by Def23;
thus A [= B implies LAp A9 c= LAp B9 & UAp A9 c= UAp B9
proof
assume A [= B; then
A "\/" B = B; then
A9 _\/_ B9 = B9 by A1,Def23,A2; then
LAp A9 \/ LAp B9 = LAp B9 & UAp A9 \/ UAp B9 = UAp B9;
hence thesis by XBOOLE_1:11;
end;
assume LAp A9 c= LAp B9 & UAp A9 c= UAp B9; then
LAp A9 \/ LAp B9 = LAp B9 & UAp A9 \/ UAp B9 = UAp B9 by XBOOLE_1:12; then
LAp (A9 _\/_ B9) = LAp B9 & UAp (A9 _\/_ B9) = UAp B9; then
A3: A9 _\/_ B9 = B9;
reconsider A1 = A, B1 = B as Element of RoughSets X by Def23;
reconsider A9 = A1, B9 = B1 as RoughSet of X by Def20;
A9 _\/_ B9 = A "\/" B by Def23;
hence thesis by A3,A1;
end;
Lm16: RSLattice X is complete
proof
let Y be Subset of RSLattice X;
ex a being Element of RSLattice X st a is_less_than Y &
for b being Element of RSLattice X st b is_less_than Y holds
b [= a
proof
per cases;
suppose A1: Y is empty;
take a = Top RSLattice X;
for q be Element of RSLattice X st q in Y holds a [= q by A1;
hence a is_less_than Y;
let b be Element of RSLattice X;
assume b is_less_than Y;
thus b [= a by LATTICES:19;
end;
suppose A2: Y is non empty;
set A1 = { LAp a1 where a1 is RoughSet of X : a1 in Y };
set A2 = { UAp a1 where a1 is RoughSet of X : a1 in Y };
set a9 = [ meet A1, meet A2 ];
consider f being object such that
A3: f in Y by A2;
Y is Subset of RoughSets X by Def23; then
reconsider f as RoughSet of X by A3,Def20;
A4: LAp f in A1 by A3; then
A5: A1 <> {};
consider g being object such that
A6: g in Y by A2;
Y is Subset of RoughSets X by Def23; then
reconsider g as RoughSet of X by A6,Def20;
UAp g in A2 by A6; then
A7: A2 <> {};
A8: meet A1 c= the carrier of X
proof
let x be object;
assume x in meet A1; then
A9: for Z being set holds Z in A1 implies x in Z by SETFAM_1:def 1;
consider c being set such that
A10: c in A1 by A4;
consider c9 being RoughSet of X such that
A11: c = LAp c9 & c9 in Y by A10;
A12: c in bool the carrier of X by A11;
x in c by A10,A9;
hence thesis by A12;
end;
a9 is RoughSet of X
proof
meet A2 c= the carrier of X
proof
let x be object;
assume x in meet A2; then
A13: for Z being set holds Z in A2 implies x in Z by SETFAM_1:def 1;
consider c being object such that
A14: c in A2 by A7,XBOOLE_0:def 1;
consider c9 being RoughSet of X such that
A15: c = UAp c9 & c9 in Y by A14;
reconsider c as set by TARSKI:1;
A16: c c= the carrier of X by A15;
x in c by A14,A13;
hence thesis by A16;
end; then
[ meet A1, meet A2 ] in
[:bool the carrier of X, bool the carrier of X:]
by A8,ZFMISC_1:87;
hence thesis by Def13;
end;
then reconsider a9 as RoughSet of X;
a9 in RoughSets X by Def20; then
reconsider a = a9 as Element of RSLattice X by Def23;
take a;
thus a is_less_than Y
proof
let q be Element of RSLattice X;
assume
A17: q in Y;
q in the carrier of RSLattice X; then
q in RoughSets X by Def23; then
reconsider q9 = q as RoughSet of X by Def20;
consider q1, q2 being Subset of X such that
A18: q9 = [q1,q2] by Th55;
A19: q1 = LAp q9 by A18; then
A20: q1 in A1 by A17;
meet A1 c= LAp q9
by A19,A20,SETFAM_1:def 1; then
A21: LAp a9 c= LAp q9;
A22: UAp a9 = meet A2;
A23: q2 = UAp q9 by A18; then
A24: q2 in A2 by A17;
meet A2 c= UAp q9
by A23,A24,SETFAM_1:def 1;
hence a [= q by A21,Th71,A22;
end;
thus for b being Element of RSLattice X st b is_less_than Y holds
b [= a
proof
let b be Element of RSLattice X;
assume
A25: b is_less_than Y;
b is Element of RoughSets X by Def23; then
reconsider b9 = b as RoughSet of X by Def20;
reconsider a9 = a as RoughSet of X;
A26: for q being Element of RSLattice X st q in Y holds b [= q
by A25;
for Z1 be set st Z1 in A1 holds LAp b9 c= Z1
proof
let Z1 be set;
assume Z1 in A1; then
consider c1 being RoughSet of X such that
A27: Z1 = LAp c1 & c1 in Y;
reconsider c19 = c1 as Element of RSLattice X by A27;
b [= c19 by A25,A27;
hence thesis by A27,Th71;
end; then
A28: LAp b9 c= meet A1 by A5,SETFAM_1:5;
A29: LAp b9 c= LAp a9 by A28;
for Z1 be set st Z1 in A2 holds UAp b9 c= Z1
proof
let Z1 be set;
assume Z1 in A2; then
consider c2 being RoughSet of X such that
A30: Z1 = UAp c2 & c2 in Y;
reconsider c29 = c2 as Element of RSLattice X by A30;
b [= c29 by A26,A30;
hence thesis by A30,Th71;
end; then
A31: UAp b9 c= meet A2 by A7,SETFAM_1:5;
UAp b9 c= UAp a9 by A31;
hence thesis by A29,Th71;
end;
end;
end;
hence thesis;
end;
registration let X;
cluster RSLattice X -> complete;
coherence by Lm16;
end;