:: Manysorted Sets
:: by Andrzej Trybulec
::
:: Received July 7, 1993
:: Copyright (c) 1993-2018 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 FUNCT_1, RELAT_1, SETFAM_1, XBOOLE_0, SUBSET_1, PARTFUN1,
FUNCOP_1, TARSKI, FUNCT_2, ZFMISC_1, MEMBER_1, FUNCT_4, PBOOLE, NAT_1,
SETLIM_2;
notations TARSKI, ZFMISC_1, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
ORDINAL1, PARTFUN1, FUNCT_2, FUNCT_4, FUNCOP_1;
constructors SETFAM_1, FUNCOP_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_4;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCOP_1, FUNCT_4,
RELAT_1;
requirements BOOLE, SUBSET;
definitions TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, FUNCOP_1;
equalities XBOOLE_0;
expansions TARSKI, XBOOLE_0, RELAT_1, FUNCT_1;
theorems TARSKI, FUNCOP_1, FUNCT_1, RELAT_1, XBOOLE_0, XBOOLE_1, FUNCT_2,
PARTFUN1, FUNCT_4, ZFMISC_1, SETFAM_1;
schemes FUNCT_1, CLASSES1, XBOOLE_0;
begin
reserve i,j,e,u for object;
theorem
for f being Function st f is non-empty holds rng f is
with_non-empty_elements;
theorem
for f being Function holds f is empty-yielding iff f = {} or rng f = {
{} }
proof
let f be Function;
hereby
assume that
A1: f is empty-yielding and
A2: f <> {};
thus rng f = { {} }
proof
thus for i being object st i in rng f holds i in { {} }
by A1;
set e = the Element of dom f;
let i be object;
assume i in { {} };
then
A3: i = {} by TARSKI:def 1;
A4: dom f <> {} by A2;
f.e is empty by A1;
hence thesis by A4,A3,FUNCT_1:def 3;
end;
end;
assume
A5: f = {} or rng f = { {} };
per cases by A5;
suppose
f = {};
hence for i being object st i in dom f holds f.i is empty;
end;
suppose
A6: rng f = { {} };
let i be object;
assume i in dom f;
then f.i in rng f by FUNCT_1:def 3;
hence thesis by A6,TARSKI:def 1;
end;
end;
reserve I for set; :: of indices
registration
let I;
cluster total for I-defined Function;
existence
proof
take I --> {};
thus thesis;
end;
end;
definition
let I;
mode ManySortedSet of I is total I-defined Function;
end;
reserve x,X,Y,Z,V for ManySortedSet of I;
scheme
KuratowskiFunction{A()-> set, F(object) -> set}:
ex f being ManySortedSet of A() st
for e being object st e in A() holds f.e in F(e)
provided
A1: for e being object st e in A() holds F(e) <> {}
proof
defpred P[object,object] means $2 in F($1);
A2: now
let e be object;
set fe = the Element of F(e);
assume
A3: e in A();
reconsider fe as object;
take fe;
F(e) <> {} by A1,A3;
hence P[e,fe];
end;
consider f being Function such that
A4: dom f = A() and
A5: for e being object st e in A() holds P[e,f.e] from CLASSES1:sch 1(A2);
reconsider f as ManySortedSet of A() by A4,PARTFUN1:def 2,RELAT_1:def 18;
take f;
thus thesis by A5;
end;
definition
let I,X,Y;
pred X in Y means
for i being object st i in I holds X.i in Y.i;
pred X c= Y means
for i being object st i in I holds X.i c= Y.i;
reflexivity;
end;
definition
let I be non empty set,X,Y be ManySortedSet of I;
redefine pred X in Y;
asymmetry
proof
let X,Y be ManySortedSet of I;
assume
A1: for i being object st i in I holds X.i in Y.i;
not for i st i in I holds Y.i in X.i
proof
assume
A2: for i st i in I holds Y.i in X.i;
consider i being object such that
A3: i in I by XBOOLE_0:def 1;
X.i in Y.i by A1,A3;
hence thesis by A2,A3;
end;
hence thesis;
end;
end;
scheme
PSeparation { I()-> set, A() -> ManySortedSet of I(), P[object,object] } :
ex X being ManySortedSet of I() st
for i being object st i in I()
for e being object holds e in X.i iff e in A().i & P[i,e];
defpred R[object,object] means
ex A being set st A = $2 &
for e being object holds e in A iff e in A().$1 & P[ $1,e];
A1: now
let i be object such that
i in I();
defpred Q[object] means P[i,$1];
ex u being set
st for e being object holds e in u iff e in A().i & Q[e]
from XBOOLE_0:sch 1;
hence ex u being object st R[i,u];
end;
consider f being Function such that
A2: dom f = I() and
A3: for i being object st i in I() holds R[i,f.i] from CLASSES1:sch 1(A1);
reconsider f as ManySortedSet of I() by A2,PARTFUN1:def 2,RELAT_1:def 18;
take f;
let i be object;
assume i in I();
then R[i,f.i] by A3;
hence thesis;
end;
theorem Th3:
(for i being object st i in I holds X.i = Y.i) implies X = Y
proof
dom X = I & dom Y = I by PARTFUN1:def 2;
hence thesis;
end;
definition
let I;
func EmptyMS I -> ManySortedSet of I equals
I --> {};
coherence;
correctness;
let X,Y;
func X (\/) Y -> ManySortedSet of I means
:Def4:
for i being object st i in I holds it.i = X.i \/ Y.i;
existence
proof
deffunc F(object) = X.$1 \/ Y.$1;
consider f being Function such that
A1: dom f = I and
A2: for i being object st i in I holds f.i = F(i) from FUNCT_1:sch 3;
f is ManySortedSet of I by A1,PARTFUN1:def 2,RELAT_1:def 18;
hence thesis by A2;
end;
uniqueness
proof
let A1, A2 be ManySortedSet of I such that
A3: for i being object st i in I holds A1.i = X.i \/ Y.i and
A4: for i being object st i in I holds A2.i = X.i \/ Y.i;
now
let i be object;
assume
A5: i in I;
hence A1.i = X.i \/ Y.i by A3
.= A2.i by A4,A5;
end;
hence thesis by Th3;
end;
commutativity;
idempotence;
func X (/\) Y -> ManySortedSet of I means
:Def5:
for i being object st i in I holds it.i = X.i /\ Y.i;
existence
proof
deffunc F(object) = X.$1 /\ Y.$1;
consider f being Function such that
A6: dom f = I and
A7: for i being object st i in I holds f.i = F(i) from FUNCT_1:sch 3;
f is ManySortedSet of I by A6,PARTFUN1:def 2,RELAT_1:def 18;
hence thesis by A7;
end;
uniqueness
proof
let A1, A2 be ManySortedSet of I such that
A8: for i being object st i in I holds A1.i = X.i /\ Y.i and
A9: for i being object st i in I holds A2.i = X.i /\ Y.i;
now
let i be object;
assume
A10: i in I;
hence A1.i = X.i /\ Y.i by A8
.= A2.i by A9,A10;
end;
hence thesis by Th3;
end;
commutativity;
idempotence;
func X (\) Y -> ManySortedSet of I means
:Def6:
for i being object st i in I holds it.i = X.i \ Y.i;
existence
proof
deffunc F(object) = X.$1 \ Y.$1;
consider f being Function such that
A11: dom f = I and
A12: for i being object st i in I holds f.i = F(i) from FUNCT_1:sch 3;
f is ManySortedSet of I by A11,PARTFUN1:def 2,RELAT_1:def 18;
hence thesis by A12;
end;
uniqueness
proof
let A1, A2 be ManySortedSet of I such that
A13: for i being object st i in I holds A1.i = X.i \ Y.i and
A14: for i being object st i in I holds A2.i = X.i \ Y.i;
now
let i be object;
assume
A15: i in I;
hence A1.i = X.i \ Y.i by A13
.= A2.i by A14,A15;
end;
hence thesis by Th3;
end;
pred X overlaps Y means
for i being object st i in I holds X.i meets Y.i;
symmetry;
pred X misses Y means
for i being object st i in I holds X.i misses Y.i;
symmetry;
end;
notation
let I;
let X,Y;
antonym X meets Y for X misses Y;
end;
definition
let I,X,Y;
func X (\+\) Y -> ManySortedSet of I equals
(X (\) Y) (\/) (Y (\) X);
correctness;
commutativity;
end;
theorem Th4:
for i st i in I holds (X (\+\) Y).i = X.i \+\ Y.i
proof
let i such that
A1: i in I;
thus (X (\+\) Y).i = (X (\) Y).i \/ (Y (\) X).i by A1,Def4
.= X.i \ Y.i \/ (Y (\) X).i by A1,Def6
.= X.i \+\ Y.i by A1,Def6;
end;
theorem Th5:
for i being object holds EmptyMS I.i = {}
proof let i be object;
per cases;
suppose
i in I;
hence thesis by FUNCOP_1:7;
end;
suppose
not i in I;
then not i in dom EmptyMS I by FUNCOP_1:13;
hence thesis by FUNCT_1:def 2;
end;
end;
theorem Th6:
(for i being object st i in I holds X.i = {}) implies X = EmptyMS I
proof
assume
A1: for i being object st i in I holds X.i = {};
now
let i be object;
assume i in I;
hence X.i = {} by A1
.= EmptyMS I.i by Th5;
end;
hence thesis by Th3;
end;
theorem Th7:
x in X or x in Y implies x in X (\/) Y
proof
assume
A1: x in X or x in Y;
let i be object;
assume
A2: i in I;
then x.i in X.i or x.i in Y.i by A1;
then x.i in X.i \/ Y.i by XBOOLE_0:def 3;
hence thesis by A2,Def4;
end;
theorem Th8:
x in X (/\) Y iff x in X & x in Y
proof
hereby
assume
A1: x in X (/\) Y;
thus x in X
proof
let i be object;
assume
A2: i in I;
then x.i in (X (/\) Y).i by A1;
then x.i in X.i /\ Y.i by A2,Def5;
hence thesis by XBOOLE_0:def 4;
end;
thus x in Y
proof
let i be object;
assume
A3: i in I;
then x.i in (X (/\) Y).i by A1;
then x.i in X.i /\ Y.i by A3,Def5;
hence thesis by XBOOLE_0:def 4;
end;
end;
assume
A4: x in X & x in Y;
let i be object;
assume
A5: i in I;
then x.i in X.i & x.i in Y.i by A4;
then x.i in X.i /\ Y.i by XBOOLE_0:def 4;
hence thesis by A5,Def5;
end;
theorem Th9:
x in X & X c= Y implies x in Y
proof
assume
A1: x in X & X c= Y;
let i be object;
assume i in I;
then x.i in X.i & X.i c= Y.i by A1;
hence thesis;
end;
theorem Th10:
x in X & x in Y implies X overlaps Y
proof
assume
A1: x in X & x in Y;
let i be object;
assume i in I;
then x.i in X.i & x.i in Y.i by A1;
hence thesis by XBOOLE_0:3;
end;
theorem Th11:
X overlaps Y implies ex x st x in X & x in Y
proof
deffunc F(object) = X.$1 /\ Y.$1;
assume
A1: X overlaps Y;
A2: for i being object st i in I holds F(i) <> {} by XBOOLE_0:def 7,A1;
consider x being ManySortedSet of I such that
A3: for i being object st i in I holds x.i in F(i)
from KuratowskiFunction(A2);
take x;
now
let i be object;
assume i in I;
then x.i in X.i /\ Y.i by A3;
hence x.i in X.i by XBOOLE_0:def 4;
end;
hence x in X;
now
let i be object;
assume i in I;
then x.i in X.i /\ Y.i by A3;
hence x.i in Y.i by XBOOLE_0:def 4;
end;
hence thesis;
end;
theorem
x in X (\) Y implies x in X
proof
assume
A1: x in X (\) Y;
thus x in X
proof
let i be object;
assume
A2: i in I;
then x.i in (X (\) Y).i by A1;
then x.i in X.i \ Y.i by A2,Def6;
hence thesis;
end;
end;
begin :: Lattice properties
Lm1:
X c= Y & Y c= X implies X = Y
proof
assume X c= Y & Y c= X;
then for i be object st i in I holds X.i = Y.i;
hence thesis by Th3;
end;
definition
let I,X,Y;
redefine pred X = Y means
for i being object st i in I holds X.i = Y.i;
compatibility by Th3;
end;
theorem Th13:
X c= Y & Y c= Z implies X c= Z
proof
assume that
A1: X c= Y and
A2: Y c= Z;
let i be object such that
A3: i in I;
let e be object;
assume
A4: e in X.i;
X.i c= Y.i by A1,A3;
then
A5: e in Y.i by A4;
Y.i c= Z.i by A2,A3;
hence thesis by A5;
end;
theorem Th14:
X c= X (\/) Y
proof
let i be object such that
A1: i in I;
let e be object;
assume e in X.i;
then e in X.i \/ Y.i by XBOOLE_0:def 3;
hence thesis by A1,Def4;
end;
theorem Th15:
X (/\) Y c= X
proof
let i be object such that
A1: i in I;
let e be object;
assume e in (X (/\) Y).i;
then e in X.i /\ Y.i by A1,Def5;
hence thesis by XBOOLE_0:def 4;
end;
theorem Th16:
X c= Z & Y c= Z implies X (\/) Y c= Z
proof
assume
A1: X c= Z & Y c= Z;
let i be object;
assume
A2: i in I;
then X.i c= Z.i & Y.i c= Z.i by A1;
then X.i \/ Y.i c= Z.i by XBOOLE_1:8;
hence thesis by A2,Def4;
end;
theorem Th17:
Z c= X & Z c= Y implies Z c= X (/\) Y
proof
assume
A1: Z c= X & Z c= Y;
let i be object;
assume
A2: i in I;
then Z.i c= X.i & Z.i c= Y.i by A1;
then Z.i c= X.i /\ Y.i by XBOOLE_1:19;
hence thesis by A2,Def5;
end;
theorem
X c= Y implies X (\/) Z c= Y (\/) Z
proof
assume
A1: X c= Y;
A2: Z c= Y (\/) Z by Th14;
Y c= Y (\/) Z by Th14;
then X c= Y (\/) Z by A1,Th13;
hence X (\/) Z c= Y (\/) Z by A2,Th16;
end;
theorem Th19:
X c= Y implies X (/\) Z c= Y (/\) Z
proof
assume
A1: X c= Y;
A2: X (/\) Z c= Z by Th15;
X (/\) Z c= X by Th15;
then X (/\) Z c= Y by A1,Th13;
hence X (/\) Z c= Y (/\) Z by A2,Th17;
end;
theorem Th20:
X c= Y & Z c= V implies X (\/) Z c= Y (\/) V
proof
assume that
A1: X c= Y and
A2: Z c= V;
V c= Y (\/) V by Th14;
then
A3: Z c= Y (\/) V by A2,Th13;
Y c= Y (\/) V by Th14;
then X c= Y (\/) V by A1,Th13;
hence thesis by A3,Th16;
end;
theorem
X c= Y & Z c= V implies X (/\) Z c= Y (/\) V
proof
assume that
A1: X c= Y and
A2: Z c= V;
X (/\) Z c= Z by Th15;
then
A3: X (/\) Z c= V by A2,Th13;
X (/\) Z c= X by Th15;
then X (/\) Z c= Y by A1,Th13;
hence thesis by A3,Th17;
end;
theorem Th22:
X c= Y implies X (\/) Y = Y
proof
assume X c= Y;
then
A1: X (\/) Y c= Y by Th16;
Y c= X (\/) Y by Th14;
hence thesis by A1,Lm1;
end;
theorem Th23:
X c= Y implies X (/\) Y = X
proof
assume
A1: X c= Y;
A2: X (/\) Y c= X by Th15;
X c= X (/\) Y by A1,Th17;
hence thesis by A2,Lm1;
end;
theorem
X (/\) Y c= X (\/) Z
proof
X (/\) Y c= X & X c= X (\/) Z by Th14,Th15;
hence thesis by Th13;
end;
theorem
X c= Z implies X (\/) Y (/\) Z = (X (\/) Y) (/\) Z
proof
assume
A1: X c= Z;
let i be object;
assume
A2: i in I;
then
A3: X.i c= Z.i by A1;
thus (X (\/) Y (/\) Z).i = X.i \/ (Y (/\) Z).i by A2,Def4
.= X.i \/ Y.i /\ Z.i by A2,Def5
.= (X.i \/ Y.i) /\ Z.i by A3,XBOOLE_1:30
.= (X (\/) Y).i /\ Z.i by A2,Def4
.= ((X (\/) Y) (/\) Z).i by A2,Def5;
end;
theorem
X = Y (\/) Z iff Y c= X & Z c= X & for V st Y c= V & Z c= V holds X c= V
proof
thus X = Y (\/) Z implies Y c= X & Z c= X & for V st Y c= V & Z c= V holds X
c= V by Th14,Th16;
assume that
A1: Y c= X & Z c= X and
A2: Y c= V & Z c= V implies X c= V;
Y c= Y (\/) Z & Z c= Y (\/) Z by Th14;
then
A3: X c= Y (\/) Z by A2;
Y (\/) Z c= X by A1,Th16;
hence thesis by A3,Lm1;
end;
theorem
X = Y (/\) Z iff X c= Y & X c= Z & for V st V c= Y & V c= Z holds V c= X
proof
thus X = Y (/\) Z implies X c= Y & X c= Z & for V st V c= Y & V c= Z holds V
c= X by Th15,Th17;
assume that
A1: X c= Y & X c= Z and
A2: V c= Y & V c= Z implies V c= X;
A3: X c= Y (/\) Z by A1,Th17;
Y (/\) Z c= Y & Y (/\) Z c= Z implies Y (/\) Z c= X by A2;
hence thesis by A3,Lm1,Th15;
end;
theorem Th28:
(X (\/) Y) (\/) Z = X (\/) (Y (\/) Z)
proof
let i be object;
assume
A1: i in I;
hence (X (\/) Y (\/) Z).i = (X (\/) Y).i \/ Z.i by Def4
.= X.i \/ Y.i \/ Z.i by A1,Def4
.= X.i \/ (Y.i \/ Z.i) by XBOOLE_1:4
.= X.i \/ (Y (\/) Z).i by A1,Def4
.= (X (\/) (Y (\/) Z)).i by A1,Def4;
end;
theorem Th29:
(X (/\) Y) (/\) Z = X (/\) (Y (/\) Z)
proof
let i be object;
assume
A1: i in I;
hence (X (/\) Y (/\) Z).i = (X (/\) Y).i /\ Z.i by Def5
.= X.i /\ Y.i /\ Z.i by A1,Def5
.= X.i /\ (Y.i /\ Z.i) by XBOOLE_1:16
.= X.i /\ (Y (/\) Z).i by A1,Def5
.= (X (/\) (Y (/\) Z)).i by A1,Def5;
end;
theorem Th30:
X (/\) (X (\/) Y) = X
proof
X c= X (\/) Y by Th14;
then
A1: X c= X (/\) (X (\/) Y) by Th17;
X (/\) (X (\/) Y) c= X by Th15;
hence X (/\) (X (\/) Y) = X by A1,Lm1;
end;
theorem Th31:
X (\/) (X (/\) Y) = X
proof
X (/\) Y c= X by Th15;
then
A1: X (\/) (X (/\) Y) c= X by Th16;
X c= X (\/) (X (/\) Y) by Th14;
hence X (\/) (X (/\) Y) = X by A1,Lm1;
end;
theorem Th32:
X (/\) (Y (\/) Z) = X (/\) Y (\/) X (/\) Z
proof
let i be object;
assume
A1: i in I;
hence (X (/\) (Y (\/) Z)).i = X.i /\ (Y (\/) Z).i by Def5
.= X.i /\ (Y.i \/ Z.i) by A1,Def4
.= X.i /\ Y.i \/ X.i /\ Z.i by XBOOLE_1:23
.= (X (/\) Y).i \/ X.i /\ Z.i by A1,Def5
.= (X (/\) Y).i \/ (X (/\) Z).i by A1,Def5
.= (X (/\) Y (\/) X (/\) Z).i by A1,Def4;
end;
theorem Th33:
X (\/) Y (/\) Z = (X (\/) Y) (/\) (X (\/) Z)
proof
thus X (\/) Y (/\) Z = X (\/) X (/\) Z (\/) Y (/\) Z by Th31
.= X (\/) (X (/\) Z (\/) Y (/\) Z) by Th28
.= X (\/) (X (\/) Y) (/\) Z by Th32
.= (X (\/) Y) (/\) X (\/) (X (\/) Y) (/\) Z by Th30
.= (X (\/) Y) (/\) (X (\/) Z) by Th32;
end;
theorem
(X (/\) Y) (\/) (X (/\) Z) = X implies X c= Y (\/) Z
proof
assume (X (/\) Y) (\/) (X (/\) Z) = X;
then X = X (/\) (Y (\/) Z) by Th32;
hence thesis by Th15;
end;
theorem
(X (\/) Y) (/\) (X (\/) Z) = X implies Y (/\) Z c= X
proof
assume (X (\/) Y) (/\) (X (\/) Z) = X;
then X = X (\/) (Y (/\) Z) by Th33;
hence thesis by Th14;
end;
theorem
(X (/\) Y) (\/) (Y (/\) Z) (\/) (Z (/\) X)
= (X (\/) Y) (/\) (Y (\/) Z) (/\) (Z (\/) X)
proof
thus X (/\) Y (\/) Y (/\) Z (\/) Z (/\) X
= (X (/\) Y (\/) Y (/\) Z (\/) Z) (/\) (X (/\) Y (\/) Y (/\) Z (\/) X)
by Th33
.= (X (/\) Y (\/) (Y (/\) Z (\/) Z)) (/\) (X (/\) Y (\/) Y (/\) Z (\/) X)
by Th28
.= (X (/\) Y (\/) Z) (/\) (X (/\) Y (\/) Y (/\) Z (\/) X) by Th31
.= (X (/\) Y (\/) Z) (/\) (X (/\) Y (\/) X (\/) Y (/\) Z) by Th28
.= (X (/\) Y (\/) Z) (/\) (X (\/) Y (/\) Z) by Th31
.= (X (\/) Z) (/\) (Y (\/) Z) (/\) (X (\/) Y (/\) Z) by Th33
.= (X (\/) Z) (/\) (Y (\/) Z) (/\) ((X (\/) Y) (/\) (X (\/) Z)) by Th33
.= (X (\/) Y) (/\) ((Y (\/) Z) (/\) (X (\/) Z) (/\) (X (\/) Z)) by Th29
.= (X (\/) Y) (/\) ((Y (\/) Z) (/\) ((X (\/) Z) (/\) (X (\/) Z))) by Th29
.= (X (\/) Y) (/\) (Y (\/) Z) (/\) (Z (\/) X) by Th29;
end;
theorem
X (\/) Y c= Z implies X c= Z
proof
X c= X (\/) Y by Th14;
hence thesis by Th13;
end;
theorem
X c= Y (/\) Z implies X c= Y
proof
Y (/\) Z c= Y by Th15;
hence thesis by Th13;
end;
theorem
X (\/) Y (\/) Z = (X (\/) Z) (\/) (Y (\/) Z)
proof
thus X (\/) Y (\/) Z = X (\/) (Y (\/) (Z (\/) Z)) by Th28
.= X (\/) (Z (\/) Y (\/) Z) by Th28
.= (X (\/) Z) (\/) (Y (\/) Z) by Th28;
end;
theorem
X (/\) Y (/\) Z = (X (/\) Z) (/\) (Y (/\) Z)
proof
thus X (/\) Y (/\) Z = X (/\) (Y (/\) (Z (/\) Z)) by Th29
.= X (/\) (Z (/\) Y (/\) Z) by Th29
.= (X (/\) Z) (/\) (Y (/\) Z) by Th29;
end;
theorem
X (\/) (X (\/) Y) = X (\/) Y
proof
thus X (\/) (X (\/) Y) = X (\/) X (\/) Y by Th28
.= X (\/) Y;
end;
theorem
X (/\) (X (/\) Y) = X (/\) Y
proof
thus X (/\) (X (/\) Y) = X (/\) X (/\) Y by Th29
.= X (/\) Y;
end;
begin :: ManySortedSet with empty components
theorem Th43:
EmptyMS I c= X
proof
let i be object such that
A1: i in I;
let e be object;
assume e in EmptyMS I.i;
hence thesis by A1,FUNCOP_1:7;
end;
theorem Th44:
X c= EmptyMS I implies X = EmptyMS I
proof
assume X c= EmptyMS I;
then X c= EmptyMS I & EmptyMS I c= X by Th43;
hence thesis by Lm1;
end;
theorem
X c= Y & X c= Z & Y (/\) Z = EmptyMS I implies X = EmptyMS I by Th17,Th44;
theorem
X c= Y & Y (/\) Z = EmptyMS I implies X (/\) Z = EmptyMS I by Th44,Th19;
theorem
X (\/) EmptyMS I = X & EmptyMS I (\/) X = X by Th22,Th43;
theorem
X (\/) Y = EmptyMS I implies X = EmptyMS I by Th44,Th14;
theorem
X (/\) EmptyMS I = EmptyMS I by Th23,Th43;
theorem
X c= (Y (\/) Z) & X (/\) Z = EmptyMS I implies X c= Y
proof
assume that
A1: X c= (Y (\/) Z) and
A2: X (/\) Z = EmptyMS I;
X (/\) (Y (\/) Z)= X by A1,Th23;
then Y (/\) X (\/) EmptyMS I = X by A2,Th32;
then Y (/\) X = X by Th22,Th43;
hence thesis by Th15;
end;
theorem
Y c= X & X (/\) Y = EmptyMS I implies Y = EmptyMS I by Th23;
begin :: Difference and symmetric difference
theorem Th52:
X (\) Y = EmptyMS I iff X c= Y
proof
hereby
assume
A1: X (\) Y = EmptyMS I;
now
let i be object;
assume i in I;
then X.i \ Y.i = (X (\) Y).i by Def6
.= {} by A1,Th5;
hence X.i c= Y.i by XBOOLE_1:37;
end;
hence X c= Y;
end;
assume
A2: X c= Y;
now
let i be object;
assume
A3: i in I;
then
A4: X.i c= Y.i by A2;
thus (X (\) Y).i = X.i \ Y.i by A3,Def6
.= {} by A4,XBOOLE_1:37;
end;
hence thesis by Th6;
end;
theorem Th53:
X c= Y implies X (\) Z c= Y (\) Z
proof
assume
A1: X c= Y;
now
let i be object;
assume
A2: i in I;
then
A3: (X (\) Z).i = X.i \ Z.i & (Y (\) Z).i = Y.i \ Z.i by Def6;
X.i c= Y.i by A1,A2;
hence (X (\) Z).i c= (Y (\) Z).i by A3,XBOOLE_1:33;
end;
hence thesis;
end;
theorem Th54:
X c= Y implies Z (\) Y c= Z (\) X
proof
assume
A1: X c= Y;
now
let i be object;
assume
A2: i in I;
then
A3: (Z (\) X).i = Z.i \ X.i & (Z (\) Y).i = Z.i \ Y.i by Def6;
X.i c= Y.i by A1,A2;
hence (Z (\) Y).i c= (Z (\) X).i by A3,XBOOLE_1:34;
end;
hence thesis;
end;
theorem
X c= Y & Z c= V implies X (\) V c= Y (\) Z
proof
assume X c= Y & Z c= V;
then X (\) V c= Y (\) V & Y (\) V c= Y (\) Z by Th53,Th54;
hence thesis by Th13;
end;
theorem Th56:
X (\) Y c= X
proof
now
let i be object such that
A1: i in I;
X.i \ Y.i c= X.i;
hence (X (\) Y).i c= X.i by A1,Def6;
end;
hence thesis;
end;
theorem
X c= Y (\) X implies X = EmptyMS I
proof
assume
A1: X c= Y (\) X;
let i be object;
assume
A2: i in I;
then X.i c= (Y (\) X).i by A1;
then X.i c= Y.i \ X.i by A2,Def6;
hence X.i = {} by XBOOLE_1:38
.= EmptyMS I.i by Th5;
end;
theorem
X (\) X = EmptyMS I by Th52;
theorem Th59:
X (\) EmptyMS I = X
proof
let i be object;
assume i in I;
hence (X (\) EmptyMS I).i = X.i \ EmptyMS I.i by Def6
.= X.i \ {} by Th5
.= X.i;
end;
theorem Th60:
EmptyMS I (\) X = EmptyMS I
by Th43,Th52;
theorem
X (\) (X (\/) Y) = EmptyMS I
by Th14,Th52;
theorem Th62:
X (/\) (Y (\) Z) = (X (/\) Y) (\) Z
proof
let i be object;
assume
A1: i in I;
hence (X (/\) (Y (\) Z)).i = X.i /\ (Y (\) Z).i by Def5
.= X.i /\ (Y.i \ Z.i) by A1,Def6
.= X.i /\ Y.i \ Z.i by XBOOLE_1:49
.= (X (/\) Y).i \ Z.i by A1,Def5
.= ((X (/\) Y) (\) Z).i by A1,Def6;
end;
theorem Th63:
(X (\) Y) (/\) Y = EmptyMS I
proof
A1: Y (/\) X c= Y by Th15;
thus (X (\) Y) (/\) Y = (Y (/\) X) (\) Y by Th62
.= EmptyMS I by A1,Th52;
thus thesis;
end;
theorem Th64:
X (\) (Y (\) Z) = (X (\) Y) (\/) X (/\) Z
proof
let i be object;
assume
A1: i in I;
hence (X (\) (Y (\) Z)).i = X.i \ (Y (\) Z).i by Def6
.= X.i \ (Y.i \ Z.i) by A1,Def6
.= X.i \ Y.i \/ X.i /\ Z.i by XBOOLE_1:52
.= X.i \ Y.i \/ (X (/\) Z).i by A1,Def5
.= (X (\) Y).i \/ (X (/\) Z).i by A1,Def6
.= ((X (\) Y) (\/) X (/\) Z).i by A1,Def4;
end;
theorem Th65:
(X (\) Y) (\/) X (/\) Y = X
proof
thus X (\) Y (\/) X (/\) Y = X (\) (Y (\) Y) by Th64
.= X (\) EmptyMS I by Th52
.= X by Th59;
end;
theorem
X c= Y implies Y = X (\/) (Y (\) X)
proof
assume
A1: X c= Y;
thus Y = (Y (\) X) (\/) Y (/\) X by Th65
.= X (\/) (Y (\) X) by A1,Th23;
end;
theorem Th67:
X (\/) (Y (\) X) = X (\/) Y
proof
thus X (\/) (Y (\) X) = X (\/) Y (/\) X (\/) (Y (\) X) by Th31
.= X (\/) (Y (/\) X (\/) (Y (\) X)) by Th28
.= X (\/) Y by Th65;
end;
theorem Th68:
X (\) (X (\) Y) = X (/\) Y
proof
thus X (\) (X (\) Y) = (X (\) X) (\/) X (/\) Y by Th64
.= EmptyMS I (\/) X (/\) Y by Th52
.= X (/\) Y by Th22,Th43;
end;
theorem Th69:
X (\) (Y (/\) Z) = (X (\) Y) (\/) (X (\) Z)
proof
let i be object;
assume
A1: i in I;
hence (X (\) (Y (/\) Z)).i = X.i \ (Y (/\) Z).i by Def6
.= X.i \ Y.i /\ Z.i by A1,Def5
.= X.i \ Y.i \/ (X.i \ Z.i) by XBOOLE_1:54
.= X.i \ Y.i \/ (X (\) Z).i by A1,Def6
.= (X (\) Y).i \/ (X (\) Z).i by A1,Def6
.= ((X (\) Y) (\/) (X (\) Z)).i by A1,Def4;
end;
theorem Th70:
X (\) X (/\) Y = X (\) Y
proof
thus X (\) X (/\) Y = (X (\) X) (\/) (X (\) Y) by Th69
.= EmptyMS I (\/) (X (\) Y) by Th52
.= X (\) Y by Th22,Th43;
end;
theorem
X (/\) Y = EmptyMS I iff X (\) Y = X
proof
hereby
assume
A1: X (/\) Y = EmptyMS I;
thus X (\) Y = X (\) X (/\) Y by Th70
.= X by A1,Th59;
end;
thus thesis by Th63;
end;
theorem Th72:
(X (\/) Y) (\) Z = (X (\) Z) (\/) (Y (\) Z)
proof
let i be object;
assume
A1: i in I;
hence ((X (\/) Y) (\) Z).i = (X (\/) Y).i \ Z.i by Def6
.= X.i \/ Y.i \ Z.i by A1,Def4
.= X.i \ Z.i \/ (Y.i \ Z.i) by XBOOLE_1:42
.= X.i \ Z.i \/ (Y (\) Z).i by A1,Def6
.= (X (\) Z).i \/ (Y (\) Z).i by A1,Def6
.= ((X (\) Z) (\/) (Y (\) Z)).i by A1,Def4;
end;
theorem Th73:
(X (\) Y) (\) Z = X (\) (Y (\/) Z)
proof
let i be object;
assume
A1: i in I;
hence ((X (\) Y) (\) Z).i = (X (\) Y).i \ Z.i by Def6
.= X.i \ Y.i \ Z.i by A1,Def6
.= X.i \ (Y.i \/ Z.i) by XBOOLE_1:41
.= X.i \ (Y (\/) Z).i by A1,Def4
.= (X (\) (Y (\/) Z)).i by A1,Def6;
end;
theorem
(X (/\) Y) (\) Z = (X (\) Z) (/\) (Y (\) Z)
proof
A1: X (\) Z c= X by Th56;
thus (X (/\) Y) (\) Z = (X (\) Z) (/\) Y by Th62
.= (X (\) Z) (\) ((X (\) Z) (\) Y) by Th68
.= (X (\) Z) (\) (X (\) (Z (\/) Y)) by Th73
.= ((X (\) Z) (\) X) (\/) ((X (\) Z) (/\) (Z (\/) Y)) by Th64
.= EmptyMS I (\/) ((X (\) Z) (/\) (Z (\/) Y)) by A1,Th52
.= (X (\) Z) (/\) (Y (\/) Z) by Th22,Th43
.= (X (\) Z) (/\) ((Y (\) Z) (\/) Z) by Th67
.= (X (\) Z) (/\) (Y (\) Z) (\/) (X (\) Z) (/\) Z by Th32
.= (X (\) Z) (/\) (Y (\) Z) (\/) EmptyMS I by Th63
.= (X (\) Z) (/\) (Y (\) Z) by Th22,Th43;
end;
theorem Th75:
(X (\/) Y) (\) Y = X (\) Y
proof
thus (X (\/) Y) (\) Y = X (\) Y (\/) (Y (\) Y) by Th72
.= X (\) Y (\/) EmptyMS I by Th52
.= X (\) Y by Th22,Th43;
end;
theorem
X c= Y (\/) Z implies X (\) Y c= Z & X (\) Z c= Y
proof
assume
A1: X c= Y (\/) Z;
then X (\) Y c= Z (\/) Y (\) Y by Th53;
then
A2: X (\) Y c= Z (\) Y by Th75;
Z (\) Y c= Z by Th56;
hence X (\) Y c= Z by A2,Th13;
X (\) Z c= Y (\/) Z (\) Z by A1,Th53;
then
A3: X (\) Z c= Y (\) Z by Th75;
Y (\) Z c= Y by Th56;
hence thesis by A3,Th13;
end;
theorem Th77:
(X (\/) Y) (\) (X (/\) Y) = (X (\) Y) (\/) (Y (\) X)
proof
thus (X (\/) Y) (\) (X (/\) Y) = X (\) (X (/\) Y) (\/) (Y (\) (X (/\) Y))
by Th72
.= X (\) Y (\/) (Y (\) (X (/\) Y)) by Th70
.= (X (\) Y) (\/) (Y (\) X) by Th70;
end;
theorem Th78:
(X (\) Y) (\) Y = X (\) Y
proof
thus (X (\) Y) (\) Y = X (\) (Y (\/) Y) by Th73
.= X (\) Y;
end;
theorem
X (\) (Y (\/) Z) = (X (\) Y) (/\) (X (\) Z)
proof
thus X (\) (Y (\/) Z) = X (\) Y (\) Z by Th73
.= (X (\) Y) (/\) X (\) Z by Th56,Th23
.= (X (\) Y) (/\) (X (\) Z) by Th62;
end;
theorem
X (\) Y = Y (\) X implies X = Y
proof
assume X (\) Y = Y (\) X;
hence X = Y (\) X (\/) Y (/\) X by Th65
.= Y by Th65;
end;
theorem
X (/\) (Y (\) Z) = X (/\) Y (\) X (/\) Z
proof
A1: X (/\) Y c= X by Th15;
X (/\) Y (\) X (/\) Z = ((X (/\) Y) (\) X) (\/) ((X (/\) Y) (\) Z) by Th69
.= EmptyMS I (\/) ((X (/\) Y) (\) Z) by A1,Th52
.= (X (/\) Y) (\) Z by Th22,Th43;
hence thesis by Th62;
end;
theorem
X (\) Y c= Z implies X c= Y (\/) Z
proof
assume
A1: X (\) Y c= Z;
X (/\) Y c= Y by Th15;
then X (/\) Y (\/) (X (\) Y) c= Y (\/) Z by A1,Th20;
hence thesis by Th65;
end;
theorem
X (\) Y c= X (\+\) Y by Th14;
theorem
X (\+\) EmptyMS I = X
proof
thus X (\+\) EmptyMS I = X (\/) (EmptyMS I (\) X) by Th59
.= X (\/) EmptyMS I by Th60
.= X by Th22,Th43;
end;
theorem
X (\+\) X = EmptyMS I by Th52;
theorem
X (\/) Y = (X (\+\) Y) (\/) X (/\) Y
proof
thus X (\/) Y = ((X (\) Y) (\/) X (/\) Y) (\/) Y by Th65
.= (X (\) Y) (\/) (X (/\) Y (\/) Y) by Th28
.= (X (\) Y) (\/) Y by Th31
.= (X (\) Y) (\/) ((Y (\) X) (\/) (Y (/\) X)) by Th65
.= (X (\+\) Y) (\/) X (/\) Y by Th28;
end;
theorem Th87:
X (\+\) Y = (X (\/) Y) (\) X (/\) Y
proof
thus X (\+\) Y = (X (\) X (/\) Y) (\/) (Y (\) X) by Th70
.= (X (\) X (/\) Y) (\/) (Y (\) X (/\) Y) by Th70
.= (X (\/) Y) (\) X (/\) Y by Th72;
end;
theorem
(X (\+\) Y) (\) Z = (X (\) (Y (\/) Z)) (\/) (Y (\) (X (\/) Z))
proof
thus (X (\+\) Y) (\) Z = (X (\) Y (\) Z) (\/) (Y (\) X (\) Z) by Th72
.= (X (\) (Y (\/) Z)) (\/) (Y (\) X (\) Z) by Th73
.= (X (\) (Y (\/) Z)) (\/) (Y (\) (X (\/) Z)) by Th73;
end;
theorem
X (\) (Y (\+\) Z) = X (\) (Y (\/) Z) (\/) X (/\) Y (/\) Z
proof
thus X (\) (Y (\+\) Z) = X (\) ((Y (\/) Z) (\) Y (/\) Z) by Th87
.= X (\) (Y (\/) Z) (\/) X (/\) (Y (/\) Z) by Th64
.= X (\) (Y (\/) Z) (\/) X (/\) Y (/\) Z by Th29;
end;
theorem Th90:
(X (\+\) Y) (\+\) Z = X (\+\) (Y (\+\) Z)
proof
set S1 = X (\) (Y (\/) Z), S2 = Y (\) (X (\/) Z), S3 = Z (\) (X (\/) Y),
S4 = X (/\) Y (/\)
Z;
thus (X (\+\) Y) (\+\) Z
= (((X (\) Y) (\) Z) (\/) ((Y (\) X) (\) Z))
(\/) (Z (\) ((X (\) Y) (\/) (Y (\) X))) by Th72
.= ( S1 (\/) ((Y (\) X) (\) Z)) (\/) (Z (\) ((X (\) Y) (\/) (Y (\) X)))
by Th73
.= ( S1 (\/) S2) (\/) (Z (\) ((X (\) Y) (\/) (Y (\) X))) by Th73
.= ( S1 (\/) S2) (\/) (Z (\) ((X (\/) Y) (\) (X (/\) Y))) by Th77
.= (S1 (\/) S2) (\/) (S4 (\/) S3) by Th64
.= (S1 (\/) S2 (\/) S4) (\/) S3 by Th28
.= (S1 (\/) S4 (\/) S2) (\/) S3 by Th28
.= (S1 (\/) S4) (\/) (S2 (\/) S3) by Th28
.= (S1 (\/) X (/\) (Y (/\) Z)) (\/) (S2 (\/) S3) by Th29
.= X (\) ((Y (\/) Z) (\) (Y (/\) Z)) (\/) (S2 (\/) S3) by Th64
.= X (\) ((Y (\) Z) (\/) (Z (\) Y)) (\/) (S2 (\/) (Z (\) (Y (\/) X)))
by Th77
.= X (\) ((Y (\) Z) (\/) (Z (\) Y)) (\/) ((Y (\) (Z (\/) X))
(\/) (Z (\) Y (\) X)) by Th73
.= X (\) ((Y (\) Z) (\/) (Z (\) Y)) (\/) ((Y (\) Z (\) X)
(\/) (Z (\) Y (\) X)) by Th73
.= X (\+\) (Y (\+\) Z) by Th72;
end;
theorem
X (\) Y c= Z & Y (\) X c= Z implies X (\+\) Y c= Z by Th16;
theorem Th92:
X (\/) Y = X (\+\) (Y (\) X)
proof
thus X (\/) Y = Y (\/) (X (\/) X)
.= X (\/) Y (\/) X by Th28
.= (X (\) Y) (\/) Y (\/) X by Th67
.= (X (\) Y) (\/) (X (\/) Y) by Th28
.= (X (\) Y) (\/) (X (\/) (Y (\) X)) by Th67
.= (X (\) Y) (\/) X (/\) X (\/) (Y (\) X) by Th28
.= (X (\) (Y (\) X)) (\/) (Y (\) X) by Th64
.= X (\+\) (Y (\) X) by Th78;
end;
theorem Th93:
X (/\) Y = X (\+\) (X (\) Y)
proof
A1: X (\) Y c= X by Th56;
thus X (/\) Y = X (\) (X (\) Y) by Th68
.= (X (\) (X (\) Y)) (\/) EmptyMS I by Th22,Th43
.= X (\+\) (X (\) Y) by A1,Th52;
end;
theorem Th94:
X (\) Y = X (\+\) (X (/\) Y)
proof
A1: X (/\) Y c= X by Th15;
thus X (\) Y = X (\) (X (/\) Y) by Th70
.= (X (\) (X (/\) Y)) (\/) EmptyMS I by Th22,Th43
.= X (\+\) (X (/\) Y) by A1,Th52;
end;
theorem Th95:
Y (\) X = X (\+\) (X (\/) Y)
proof
A1: X c= Y (\/) X by Th14;
thus Y (\) X = ((Y (\/) X) (\) X) by Th75
.= EmptyMS I (\/) ((Y (\/) X) (\) X) by Th22,Th43
.= X (\+\) (X (\/) Y) by A1,Th52;
end;
theorem
X (\/) Y = X (\+\) Y (\+\) X (/\) Y
proof
thus X (\/) Y = X (\+\) (Y (\) X) by Th92
.= X (\+\) (Y (\+\) X (/\) Y) by Th94
.= X (\+\) Y (\+\) X (/\) Y by Th90;
end;
theorem
X (/\) Y = X (\+\) Y (\+\) (X (\/) Y)
proof
thus X (/\) Y = X (\+\) (X (\) Y) by Th93
.= X (\+\) (Y (\+\) (X (\/) Y)) by Th95
.= X (\+\) Y (\+\) (X (\/) Y) by Th90;
end;
begin :: Meeting and overlap(p?)ing
theorem
X overlaps Y or X overlaps Z implies X overlaps Y (\/) Z
proof
assume
A1: X overlaps Y or X overlaps Z;
per cases by A1;
suppose
X overlaps Y;
then consider x such that
A2: x in X and
A3: x in Y by Th11;
x in Y (\/) Z by A3,Th7;
hence thesis by A2,Th10;
end;
suppose
X overlaps Z;
then consider x such that
A4: x in X and
A5: x in Z by Th11;
x in Y (\/) Z by A5,Th7;
hence thesis by A4,Th10;
end;
end;
theorem Th99:
X overlaps Y & Y c= Z implies X overlaps Z
proof
assume that
A1: X overlaps Y and
A2: Y c= Z;
consider x such that
A3: x in X and
A4: x in Y by A1,Th11;
x in Z by A2,A4,Th9;
hence thesis by A3,Th10;
end;
theorem Th100:
X overlaps Y & X c= Z implies Z overlaps Y
proof
assume that
A1: X overlaps Y and
A2: X c= Z;
consider x such that
A3: x in X and
A4: x in Y by A1,Th11;
x in Z by A2,A3,Th9;
hence thesis by A4,Th10;
end;
theorem Th101:
X c= Y & Z c= V & X overlaps Z implies Y overlaps V
proof
assume that
A1: X c= Y and
A2: Z c= V;
assume X overlaps Z;
then Y overlaps Z by A1,Th100;
hence thesis by A2,Th99;
end;
theorem
X overlaps Y (/\) Z implies X overlaps Y & X overlaps Z
proof
assume X overlaps Y (/\) Z;
then consider x such that
A1: x in X and
A2: x in Y (/\) Z by Th11;
x in Y & x in Z by A2,Th8;
hence thesis by A1,Th10;
end;
theorem
X overlaps Z & X c= V implies X overlaps Z (/\) V
proof
assume that
A1: X overlaps Z and
A2: X c= V;
consider x such that
A3: x in X and
A4: x in Z by A1,Th11;
x in V by A2,A3,Th9;
then x in Z (/\) V by A4,Th8;
hence thesis by A3,Th10;
end;
theorem
X overlaps Y (\) Z implies X overlaps Y by Th56,Th99;
theorem
Y does not overlap Z implies X (/\) Y does not overlap X (/\) Z
proof
assume
A1: Y does not overlap Z;
X (/\) Y c= Y & X (/\) Z c= Z by Th15;
hence thesis by A1,Th101;
end;
theorem
X overlaps Y (\) Z implies Y overlaps X (\) Z
proof
assume
A1: X overlaps Y (\) Z;
let i be object;
assume
A2: i in I;
then X.i meets (Y (\) Z).i by A1;
then X.i meets Y.i \ Z.i by A2,Def6;
then Y.i meets X.i \ Z.i by XBOOLE_1:81;
hence thesis by A2,Def6;
end;
theorem Th107:
X meets Y & Y c= Z implies X meets Z
proof
assume that
A1: X meets Y and
A2: Y c= Z;
consider i being object such that
A3: i in I and
A4: X.i meets Y.i by A1;
take i;
Y.i c= Z.i by A2,A3;
hence thesis by A3,A4,XBOOLE_1:63;
end;
theorem Th108:
Y misses X (\) Y
proof
now
let i be object;
assume i in I;
then (X (\) Y).i = X.i \ Y.i by Def6;
hence Y.i misses (X (\) Y).i by XBOOLE_1:79;
end;
hence thesis;
end;
theorem
X (/\) Y misses X (\) Y
proof
X (/\) Y c= Y & X (\) Y misses Y by Th15,Th108;
hence thesis by Th107;
end;
theorem
X (/\) Y misses X (\+\) Y
proof
now
let i be object;
assume i in I;
then (X (/\) Y).i = X.i /\ Y.i & (X (\+\) Y).i = X.i \+\ Y.i by Def5,Th4;
hence (X (/\) Y).i misses (X (\+\) Y).i by XBOOLE_1:103;
end;
hence thesis;
end;
theorem Th111:
X misses Y implies X (/\) Y = EmptyMS I
proof
assume
A1: X misses Y;
now
let i be object;
assume
A2: i in I;
then
A3: X.i misses Y.i by A1;
thus (X (/\) Y).i = X.i /\ Y.i by A2,Def5
.= {} by A3;
end;
hence thesis by Th6;
end;
theorem
X <> EmptyMS I implies X meets X
proof
X = X (/\) X;
hence thesis by Th111;
end;
theorem
X c= Y & X c= Z & Y misses Z implies X = EmptyMS I
proof
assume
A1: X c= Y & X c= Z;
assume Y misses Z;
then Y (/\) Z = EmptyMS I by Th111;
hence thesis by A1,Th17,Th44;
end;
theorem
Z (\/) V = X (\/) Y & X misses Z & Y misses V implies X = V & Y = Z
proof
assume
A1: Z (\/) V = X (\/) Y;
assume X misses Z & Y misses V;
then
A2: X (/\) Z = EmptyMS I & Y (/\) V = EmptyMS I by Th111;
thus X = X (/\) (Z (\/) V) by Th23,A1,Th14
.= X (/\) Z (\/) X (/\) V by Th32
.= (X (\/) Y) (/\) V by A2,Th32
.= V by A1,Th14,Th23;
thus Y = Y (/\) (Z (\/) V) by Th23,A1,Th14
.= Y (/\) Z (\/) Y (/\) V by Th32
.= (X (\/) Y) (/\) Z by A2,Th32
.= Z by A1,Th14,Th23;
end;
theorem Th115:
X misses Y implies X (\) Y = X
proof
assume
A1: X misses Y;
let i be object;
assume
A2: i in I;
then
A3: (X (\) Y).i = X.i \ Y.i by Def6;
X.i misses Y.i by A1,A2;
hence (X (\) Y).i = X.i by A3,XBOOLE_1:83;
end;
theorem
X misses Y implies (X (\/) Y) (\) Y = X
proof
(X (\/) Y) (\) Y = X (\) Y by Th75;
hence thesis by Th115;
end;
theorem
X (\) Y = X implies X misses Y
proof
assume
A1: X (\) Y = X;
let i be object;
assume i in I;
then X.i \ Y.i = X.i by A1,Def6;
hence thesis by XBOOLE_1:83;
end;
theorem
X (\) Y misses Y (\) X
proof
let i be object;
assume i in I;
then (X (\) Y).i = X.i \ Y.i & (Y (\) X).i = Y.i \ X.i by Def6;
hence thesis by XBOOLE_1:82;
end;
begin :: Roughly speaking
definition
let I,X,Y;
pred X [= Y means
for x st x in X holds x in Y;
reflexivity;
end;
theorem
X c= Y implies X [= Y
proof
assume
A1: X c= Y;
let x such that
A2: x in X;
let i be object;
assume
A3: i in I;
then
A4: X.i c= Y.i by A1;
x.i in X.i by A2,A3;
hence thesis by A4;
end;
theorem
X [= Y & Y [= Z implies X [= Z;
begin :: Non empty set of sorts
theorem
EmptyMS {} in EmptyMS {};
theorem
for X being ManySortedSet of {} holds X = {};
reserve I for non empty set,
x,X,Y for ManySortedSet of I;
theorem
X overlaps Y implies X meets Y
proof
set i = the Element of I;
assume X overlaps Y;
then X.i meets Y.i;
hence thesis;
end;
theorem Th124:
not ex x st x in EmptyMS I
proof
set i = the Element of I;
given x such that
A1: x in EmptyMS I;
x.i in EmptyMS I.i by A1;
hence contradiction by FUNCOP_1:7;
end;
theorem
x in X & x in Y implies X (/\) Y <> EmptyMS I
by Th8,Th124;
theorem
X does not overlap EmptyMS I
proof
assume X overlaps EmptyMS I;
then ex x st x in X & x in EmptyMS I by Th11;
hence contradiction by Th124;
end;
theorem Th127:
X (/\) Y = EmptyMS I implies X does not overlap Y
proof
assume
A1: X (/\) Y = EmptyMS I;
assume X overlaps Y;
then consider x such that
A2: x in X & x in Y by Th11;
x in X (/\) Y by A2,Th8;
hence contradiction by A1,Th124;
end;
theorem
X overlaps X implies X <> EmptyMS I
proof
X = X (/\) X;
hence thesis by Th127;
end;
begin :: Empty and non-empty ManySortedSets
reserve I for set,
x,X,Y,Z for ManySortedSet of I;
definition
let I be set;
let X be ManySortedSet of I;
redefine attr X is empty-yielding means
for i being object st i in I holds X.i is empty;
compatibility
proof
dom X = I by PARTFUN1:def 2;
hence thesis;
end;
redefine attr X is non-empty means
:Def13:
for i being object st i in I holds X.i is non empty;
compatibility
proof
dom X = I by PARTFUN1:def 2;
hence thesis;
end;
end;
registration
let I be set;
cluster empty-yielding for ManySortedSet of I;
existence
proof
take EmptyMS I;
let i be object;
assume i in I;
thus thesis by Th5;
end;
cluster non-empty for ManySortedSet of I;
existence
proof
set e = the set;
reconsider M = I --> {e} as ManySortedSet of I;
take M;
let i be object;
assume i in I;
hence thesis by FUNCOP_1:7;
end;
end;
registration
let I be non empty set;
cluster non-empty -> non empty-yielding for ManySortedSet of I;
coherence
proof
set i = the Element of I;
let M be ManySortedSet of I;
assume
A1: M is non-empty;
take i;
thus i in I;
thus thesis by A1;
end;
cluster empty-yielding -> non non-empty for ManySortedSet of I;
coherence;
end;
theorem
X is empty-yielding iff X = EmptyMS I
proof
hereby
assume X is empty-yielding;
then for i being object st i in I holds X.i = {};
hence X = EmptyMS I by Th6;
end;
assume
A1: X = EmptyMS I;
let i be object;
assume i in I;
thus thesis by A1,Th5;
end;
theorem
Y is empty-yielding & X c= Y implies X is empty-yielding
proof
assume
A1: Y is empty-yielding & X c= Y;
let i be object;
assume i in I;
then X.i c= Y.i & Y.i is empty by A1;
hence thesis;
end;
theorem Th131:
X is non-empty & X c= Y implies Y is non-empty
proof
assume
A1: X is non-empty & X c= Y;
let i be object;
assume i in I;
then X.i c= Y.i & X.i is non empty by A1;
hence thesis;
end;
theorem Th132:
X is non-empty & X [= Y implies X c= Y
proof
assume that
A1: X is non-empty and
A2: X [= Y;
deffunc F(object) = X.$1;
A3: for i being object st i in I holds F(i) <> {} by A1;
consider f being ManySortedSet of I such that
A4: for i being object st i in I holds f.i in F(i)
from KuratowskiFunction(A3);
let i be object such that
A5: i in I;
let e be object;
deffunc G(object) = IFEQ(i,$1,e,f.$1);
consider g being Function such that
A6: dom g = I and
A7: for u being object st u in I holds g.u = G(u) from FUNCT_1:sch 3;
reconsider g as ManySortedSet of I by A6,PARTFUN1:def 2,RELAT_1:def 18;
A8: g.i = IFEQ(i,i,e,f.i) by A5,A7
.= e by FUNCOP_1:def 8;
assume
A9: e in X.i;
g in X
proof
let u be object such that
A10: u in I;
per cases;
suppose
u = i;
hence thesis by A8,A9;
end;
suppose
A11: u <> i;
g.u = IFEQ(i,u,e,f.u) by A7,A10
.= f.u by A11,FUNCOP_1:def 8;
hence thesis by A4,A10;
end;
end;
then g in Y by A2;
hence thesis by A5,A8;
end;
theorem
X is non-empty & X [= Y implies Y is non-empty
proof
assume
A1: X is non-empty;
assume X [= Y;
then X c= Y by A1,Th132;
hence thesis by A1,Th131;
end;
reserve X for non-empty ManySortedSet of I;
theorem
ex x st x in X
proof
deffunc F(object) = X.$1;
A1: for i being object st i in I holds F(i) <> {} by Def13;
consider f being ManySortedSet of I such that
A2: for i being object st i in I holds f.i in F(i)
from KuratowskiFunction(A1);
take f;
let i be object;
thus thesis by A2;
end;
theorem Th135:
(for x holds x in X iff x in Y) implies X = Y
proof
deffunc F(object) = X.$1;
A1: for i being object st i in I holds F(i) <> {} by Def13;
consider f being ManySortedSet of I such that
A2: for i being object st i in I holds f.i in F(i)
from KuratowskiFunction(A1);
assume
A3: for x holds x in X iff x in Y;
now
let i be object such that
A4: i in I;
now
let e be object;
deffunc G(object) = IFEQ(i,$1,e,f.$1);
consider g being Function such that
A5: dom g = I and
A6: for u being object st u in I holds g.u = G(u) from FUNCT_1:sch 3;
reconsider g as ManySortedSet of I by A5,PARTFUN1:def 2,RELAT_1:def 18;
A7: g.i = IFEQ(i,i,e,f.i) by A4,A6
.= e by FUNCOP_1:def 8;
hereby
assume
A8: e in X.i;
g in X
proof
let u be object such that
A9: u in I;
per cases;
suppose
u = i;
hence thesis by A7,A8;
end;
suppose
A10: u <> i;
g.u = IFEQ(i,u,e,f.u) by A6,A9
.= f.u by A10,FUNCOP_1:def 8;
hence thesis by A2,A9;
end;
end;
then g in Y by A3;
hence e in Y.i by A4,A7;
end;
assume
A11: e in Y.i;
g in Y
proof
let u be object such that
A12: u in I;
per cases;
suppose
u = i;
hence thesis by A7,A11;
end;
suppose
A13: u <> i;
f in X by A2;
then
A14: f in Y by A3;
g.u = IFEQ(i,u,e,f.u) by A6,A12
.= f.u by A13,FUNCOP_1:def 8;
hence thesis by A12,A14;
end;
end;
then g in X by A3;
hence e in X.i by A4,A7;
end;
hence X.i = Y.i by TARSKI:2;
end;
hence thesis;
end;
theorem
(for x holds x in X iff x in Y & x in Z) implies X = Y (/\) Z
proof
assume
A1: for x holds x in X iff x in Y & x in Z;
now
let x;
hereby
assume x in X;
then x in Y & x in Z by A1;
hence x in Y (/\) Z by Th8;
end;
assume x in Y (/\) Z;
then x in Y & x in Z by Th8;
hence x in X by A1;
end;
hence thesis by Th135;
end;
begin :: Addenda
scheme
MSSEx { I() -> set, P[object,object] }:
ex f being ManySortedSet of I() st
for i being object st i in I() holds P[i,f.i]
provided
A1: for i being object st i in I() ex j being object st P[i,j]
proof
consider f being Function such that
A2: dom f = I() and
A3: for i being object st i in I() holds P[i,f.i] from CLASSES1:sch 1(A1);
reconsider f as ManySortedSet of I() by A2,PARTFUN1:def 2,RELAT_1:def 18;
take f;
thus thesis by A3;
end;
scheme
MSSLambda { I() -> set, F(object) -> object }:
ex f being ManySortedSet of I() st
for i being object st i in I() holds f.i = F(i);
consider f being Function such that
A1: dom f = I() and
A2: for i being object st i in I() holds f.i = F(i) from FUNCT_1:sch 3;
reconsider f as ManySortedSet of I() by A1,PARTFUN1:def 2,RELAT_1:def 18;
take f;
thus thesis by A2;
end;
registration
let I be set;
cluster Function-yielding for ManySortedSet of I;
existence
proof
set f = the Function;
reconsider F = I --> f as ManySortedSet of I;
take F;
let x be object;
assume x in dom F;
thus thesis;
end;
end;
definition
let I be set;
mode ManySortedFunction of I is Function-yielding ManySortedSet of I;
end;
theorem
not ex M being non-empty ManySortedSet of I st {} in rng M
proof
let M be non-empty ManySortedSet of I;
A1: dom M = I by PARTFUN1:def 2;
assume {} in rng M;
then ex i being object st i in I & M.i = {} by A1,FUNCT_1:def 3;
hence contradiction by Def13;
end;
definition
let M be Function;
mode Component of M is Element of rng M;
end;
theorem
for I being non empty set for M being ManySortedSet of I, A being
Component of M ex i being object st i in I & A = M.i
proof
let I be non empty set;
let M be ManySortedSet of I, A be Component of M;
A1: dom M = I by PARTFUN1:def 2;
then rng M <> {} by RELAT_1:42;
hence thesis by A1,FUNCT_1:def 3;
end;
theorem
for M being ManySortedSet of I, i st i in I holds M.i is Component of M
proof
let M be ManySortedSet of I, i;
assume
A1: i in I;
dom M = I by PARTFUN1:def 2;
hence thesis by A1,FUNCT_1:def 3;
end;
definition
let I;
let B be ManySortedSet of I;
mode Element of B -> ManySortedSet of I means
for i being object st i in I holds it.i is Element of B.i;
existence
proof
defpred Q[object,object] means $2 is Element of B.$1;
A1: for i being object st i in I ex j being object st Q[i,j]
proof
let i be object such that
i in I;
set j = the Element of B.i;
reconsider j as set;
take j;
thus thesis;
end;
thus ex f being ManySortedSet of I st
for i being object st i in I holds Q[i,f.i] from
MSSEx(A1);
end;
end;
begin :: Many Sorted Functions
definition
let I;
let A be ManySortedSet of I, B be ManySortedSet of I;
mode ManySortedFunction of A,B -> ManySortedSet of I means
:Def15: for i st i in I holds it.i is Function of A.i, B.i;
correctness
proof
defpred P[object,object] means $2 is Function of A.$1,B.$1;
A1: for i being object st i in I ex j being object st P[i,j]
proof
let i be object such that
i in I;
set j = the Function of A.i,B.i;
reconsider j as set;
take j;
thus thesis;
end;
consider f being ManySortedSet of I such that
A2: for i being object st i in I holds P[i,f.i] from MSSEx(A1);
f is Function-yielding
proof
let i be object;
assume i in dom f;
then i in I by PARTFUN1:def 2;
hence thesis by A2;
end;
then reconsider f as ManySortedFunction of I;
take f;
let i;
assume i in I;
hence thesis by A2;
end;
end;
registration
let I;
let A be ManySortedSet of I, B be ManySortedSet of I;
cluster ->Function-yielding for ManySortedFunction of A,B;
coherence
proof
let f be ManySortedFunction of A,B;
let i be object;
assume i in dom f;
then i in I by PARTFUN1:def 2;
hence thesis by Def15;
end;
end;
registration
let I be set;
let J be non empty set;
let O be Function of I,J;
let F be ManySortedSet of J;
cluster F*O -> total for I-defined Function;
coherence
proof
A1: dom F = J by PARTFUN1:def 2;
rng O c= J & dom O = I by FUNCT_2:def 1,RELAT_1:def 19;
then dom(F*O) = I by A1,RELAT_1:27;
hence thesis by PARTFUN1:def 2;
end;
end;
reserve D for non empty set,
n for Nat;
scheme
LambdaDMS {D()->non empty set, F(object)->object}:
ex X be ManySortedSet of D() st
for d be Element of D() holds X.d = F(d) proof
consider f be Function such that
A1: dom f = D() and
A2: for d be Element of D() holds f.d = F(d) from FUNCT_1:sch 4;
f is ManySortedSet of D() by A1,PARTFUN1:def 2,RELAT_1:def 18;
hence thesis by A2;
end;
registration
let J be non empty set, B be non-empty ManySortedSet of J, j be Element of J;
cluster B.j -> non empty;
coherence by Def13;
end;
reserve X,Y for ManySortedSet of I;
definition
let I, X,Y;
func [|X,Y|] -> ManySortedSet of I means
for i being object st i in I holds it.i = [:X.i,Y.i:];
existence
proof
deffunc F(object) = [:X.$1,Y.$1:];
consider f be Function such that
A1: dom f = I &
for i being object st i in I holds f.i = F(i) from FUNCT_1:sch 3;
reconsider f as ManySortedSet of I by A1,PARTFUN1:def 2,RELAT_1:def 18;
take f;
thus thesis by A1;
end;
uniqueness
proof
let f,g be ManySortedSet of I;
assume that
A2: for i being object st i in I holds f.i = [:X.i,Y.i:] and
A3: for i being object st i in I holds g.i = [:X.i,Y.i:];
for x be object st x in I holds f.x = g.x
proof
let x be object;
assume
A4: x in I;
then f.x = [:X.x,Y.x:] by A2;
hence thesis by A3,A4;
end;
hence thesis;
end;
end;
definition
let I, X, Y;
deffunc F(object) = Funcs(X.$1,Y.$1);
func (Funcs) (X,Y) -> ManySortedSet of I means
for i being object st i in I holds it.i = Funcs(X.i,Y.i);
existence
proof
thus ex M being ManySortedSet of I st
for i being object st i in I holds M.i = F(i) from MSSLambda;
end;
uniqueness
proof
let F1, F2 be ManySortedSet of I such that
A1: for i being object st i in I holds F1.i = Funcs(X.i, Y.i) and
A2: for i being object st i in I holds F2.i = Funcs(X.i, Y.i);
now
let i be object;
assume
A3: i in I;
hence F1.i = Funcs(X.i, Y.i) by A1
.= F2.i by A2,A3;
end;
hence thesis;
end;
end;
definition
let I be set, M be ManySortedSet of I;
mode ManySortedSubset of M -> ManySortedSet of I means
:Def18:
it c= M;
existence;
end;
registration
let I be set, M be non-empty ManySortedSet of I;
cluster non-empty for ManySortedSubset of M;
existence
proof
reconsider N= M as ManySortedSubset of M by Def18;
take N;
thus thesis;
end;
end;
definition
let F,G be Function-yielding Function;
func G**F -> Function means
:Def19:
dom it = (dom F) /\ (dom G) &
for i be object st i in dom it holds it.i = (G.i)*(F.i);
existence
proof
defpred P[object,object] means $2 = (G.$1)*(F.$1);
A1: for i be object st i in dom F /\ dom G ex u be object st P[i,u];
ex H being Function st
dom H = dom F /\ dom G & for i be object st i in dom F /\ dom G holds
P[i,H.i] from CLASSES1:sch 1(A1);
hence thesis;
end;
uniqueness
proof
let H1,H2 be Function;
assume that
A2: dom H1 = dom F /\ dom G and
A3: for i be object st i in dom H1 holds H1.i = (G.i)*(F.i) and
A4: dom H2 = dom F /\ dom G and
A5: for i be object st i in dom H2 holds H2.i = (G.i)*(F.i);
now
let i be object;
reconsider f = F.i as Function;
reconsider g = G.i as Function;
assume
A6: i in dom F /\ dom G;
then H1.i = g*f by A2,A3;
hence H1.i = H2.i by A4,A5,A6;
end;
hence thesis by A2,A4;
end;
end;
registration
let F,G be Function-yielding Function;
cluster G**F -> Function-yielding;
coherence
proof
set H = G**F;
let x be object;
reconsider f = F.x as Function;
reconsider g = G.x as Function;
assume x in dom H;
then H.x = g*f by Def19;
hence thesis;
end;
end;
definition
let I be set, A be ManySortedSet of I, F be ManySortedFunction of I;
func F.:.:A -> ManySortedSet of I means
for i be set st i in I holds it.i = (F.i).:(A.i);
existence
proof
defpred P[object,object] means $2 = (F.$1).:(A.$1);
A1: for i be object st i in I ex u be object st P[i,u];
consider g being Function such that
A2: dom g = I & for i be object st i in I holds P[i,g.i] from CLASSES1:
sch 1( A1);
reconsider g as ManySortedSet of I by A2,PARTFUN1:def 2,RELAT_1:def 18;
take g;
thus thesis by A2;
end;
uniqueness
proof
let B,B1 be ManySortedSet of I;
assume that
A3: for i be set st i in I holds B.i = (F.i).:(A.i) and
A4: for i be set st i in I holds B1.i = (F.i).:(A.i);
now
let i be object;
reconsider f = F.i as Function;
assume
A5: i in I;
then B.i = f.:(A.i) by A3;
hence B.i = B1.i by A4,A5;
end;
hence thesis;
end;
end;
registration
let I;
cluster EmptyMS I -> empty-yielding;
coherence
by FUNCOP_1:13;
end;
scheme
MSSExD { I() -> non empty set, P[object,object] }:
ex f being ManySortedSet of I()
st for i being Element of I() holds P[i,f.i]
provided
A1: for i being Element of I() ex j being object st P[i,j];
A2: for i being object st i in I() ex j being object st P[i,j] by A1;
consider f being ManySortedSet of I() such that
A3: for i being object st i in I() holds P[i,f.i] from MSSEx(A2);
take f;
let i be Element of I();
thus thesis by A3;
end;
registration
let A be non empty set;
cluster non-empty -> non empty-yielding for ManySortedSet of A;
coherence;
end;
registration
let X be non empty set;
cluster -> non empty for ManySortedSet of X;
coherence;
end;
theorem
for F, G, H be Function-yielding Function holds
(H ** G) ** F = H ** (G ** F)
proof
let F, G, H be Function-yielding Function;
set f = (H ** G) ** F, g = H ** (G ** F);
now
A1: dom f = (dom (H ** G)) /\ dom F by Def19
.= (dom H) /\ (dom G) /\ (dom F) by Def19;
then
A2: dom f = (dom H) /\ ((dom G) /\ dom F) by XBOOLE_1:16;
hence
A3: dom f = (dom H) /\ (dom (G ** F)) by Def19
.= dom g by Def19;
let x be object;
assume
A4: x in dom f;
then x in (dom H) /\ (dom G) by A1,XBOOLE_0:def 4;
then
A5: x in dom (H ** G) by Def19;
x in (dom G) /\ (dom F) by A2,A4,XBOOLE_0:def 4;
then
A6: x in dom (G ** F) by Def19;
thus f.x = ((H**G).x) * (F.x) by A4,Def19
.= (H.x)*(G.x)*(F.x) by A5,Def19
.= (H.x)*((G.x)*(F.x)) by RELAT_1:36
.= (H.x)*((G**F).x) by A6,Def19
.= g.x by A3,A4,Def19;
end;
hence thesis;
end;
registration
let I be set, f be non-empty ManySortedSet of I;
cluster total for I-defined f-compatible Function;
existence
proof
deffunc F(object) = f.$1;
A1: for e being object st e in I holds F(e) <> {};
consider g being ManySortedSet of I such that
A2: for e being object st e in I holds g.e in F(e)
from KuratowskiFunction(A1);
g is f-compatible
proof let x be object;
assume x in dom g;
then x in I by PARTFUN1:def 2;
hence g.x in f.x by A2;
end;
then reconsider g as I-defined f-compatible Function;
take g;
thus g is total;
end;
end;
theorem
for I being set, f being non-empty ManySortedSet of I
for p being f-compatible I-defined Function
ex s being f-compatible ManySortedSet of I st p c= s
proof
let I be set, f being non-empty ManySortedSet of I;
let p be f-compatible I-defined Function;
set h = the (f)-compatible ManySortedSet of I;
take h+*p;
thus p c= h+*p by FUNCT_4:25;
end;
theorem
for I,A be set
for s,ss being ManySortedSet of I
holds (ss +* s | A) | A = s | A
proof
let I,A be set;
let s,ss be ManySortedSet of I;
dom s = I by PARTFUN1:def 2
.= dom ss by PARTFUN1:def 2;
then A /\ dom ss c= A /\ dom s;
hence thesis by FUNCT_4:88;
end;
registration
let X be non empty set, Y be set;
cluster X-valued for ManySortedSet of Y;
existence
proof
take M = Y --> the Element of X;
A1: {the Element of X} c= X by ZFMISC_1:31;
rng M c= {the Element of X} by FUNCOP_1:13;
hence rng M c= X by A1;
end;
end;
theorem
for I,Y being non empty set, M be Y-valued ManySortedSet of I,
x be Element of I
holds M.x = M/.x
proof
let I,Y be non empty set, M be Y-valued ManySortedSet of I,
x be Element of I;
dom M = I by PARTFUN1:def 2;
hence M.x = M/.x by PARTFUN1:def 6;
end;
theorem
for f being Function, M being ManySortedSet of I
holds (f+*M)|I = M
proof
let f be Function, M be ManySortedSet of I;
A1: dom(f|I) c= I by RELAT_1:58;
A2: dom M = I by PARTFUN1:def 2;
thus (f+*M)|I = f|I +* M|I by FUNCT_4:71
.= f|I +* M
.= M by A1,A2,FUNCT_4:19;
end;
theorem
for I being set, Y being non empty set
for p being Y-valued I-defined Function
ex s being Y-valued ManySortedSet of I st p c= s
proof
let I be set, Y being non empty set;
let p be Y-valued I-defined Function;
set h = the Y-valued ManySortedSet of I;
take h+*p;
thus p c= h+*p by FUNCT_4:25;
end;
theorem
X c= Y & Y c= X implies X = Y by Lm1;
definition let I be non empty set, A,B be ManySortedSet of I;
redefine pred A = B means
for i being Element of I holds A.i = B.i;
compatibility;
end;
registration
let X be with_non-empty_elements set;
cluster id X -> non-empty;
coherence by SETFAM_1:def 8;
end;
scheme
MSSLambda { I() -> set, F(object) -> object }:
ex f being ManySortedSet of I() st
for i being set st i in I() holds f.i = F(i);
consider f being Function such that
A1: dom f = I() and
A2: for i being object st i in I() holds f.i = F(i) from FUNCT_1:sch 3;
reconsider f as ManySortedSet of I() by A1,PARTFUN1:def 2,RELAT_1:def 18;
take f;
thus thesis by A2;
end;