Journal of Formalized Mathematics
Volume 5, 1993
University of Bialystok
Copyright (c) 1993 Association of Mizar Users

### Many-sorted Sets

by
Andrzej Trybulec

MML identifier: PBOOLE
[ Mizar article, MML identifier index ]

```environ

vocabulary FUNCT_1, MATRIX_1, RELAT_1, CARD_1, BOOLE, ZF_REFLE, AMI_1,
FUNCOP_1, CAT_4, LATTICES, CQC_LANG, PBOOLE;
notation TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCOP_1, CQC_LANG,
CARD_1, AMI_1, MATRIX_1;
constructors AMI_1, MATRIX_1, FUNCOP_1, MEMBERED, XBOOLE_0;
clusters FUNCT_1, RELAT_1, FUNCOP_1, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0;
requirements BOOLE, SUBSET;

begin

reserve i,e,u for set;

definition let f be Function;
redefine attr f is empty-yielding means
:: PBOOLE:def 1
for i st i in dom f holds f.i is empty;
end;

definition
cluster empty-yielding Function;
end;

theorem :: PBOOLE:1
for f being Function st f is non-empty
holds rng f is with_non-empty_elements;

theorem :: PBOOLE:2
for f being Function holds
f is empty-yielding iff f = {} or rng f = { {} };

reserve I for set; :: of indices

definition let I;
canceled;

mode ManySortedSet of I -> Function means
:: PBOOLE:def 3
dom it = I;
end;

reserve x,X,Y,Z,V for ManySortedSet of I;

scheme Kuratowski_Function{A()-> set, F(set) -> set}:
ex f being ManySortedSet of A() st
for e st e in A() holds f.e in F(e)
provided
for e st e in A() holds F(e) <> {};

definition let I,X,Y;
pred X in Y means
:: PBOOLE:def 4
for i st i in I holds X.i in Y.i;
pred X c= Y means
:: PBOOLE:def 5
for i 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;
end;

scheme PSeparation { I()-> set, A() -> ManySortedSet of I(), P[set,set] } :
ex X being ManySortedSet of I() st
for i being set st i in I()
for e holds e in X.i iff e in A().i & P[i,e];

theorem :: PBOOLE:3
(for i st i in I holds X.i = Y.i) implies X = Y;

definition
let I;
func I -> ManySortedSet of I equals
:: PBOOLE:def 6
I --> {};
let X,Y;
func X \/ Y -> ManySortedSet of I means
:: PBOOLE:def 7
for i st i in I holds it.i = X.i \/ Y.i;
commutativity;
idempotence;

func X /\ Y -> ManySortedSet of I means
:: PBOOLE:def 8
for i st i in I holds it.i = X.i /\ Y.i;
commutativity;
idempotence;

func X \ Y -> ManySortedSet of I means
:: PBOOLE:def 9
for i st i in I holds it.i = X.i \ Y.i;
pred X overlaps Y means
:: PBOOLE:def 10
for i st i in I holds X.i meets Y.i;
symmetry;
antonym X does_not_overlap Y;
pred X misses Y means
:: PBOOLE:def 11
for i st i in I holds X.i misses Y.i;
symmetry;
antonym X meets Y;
end;

definition let I,X,Y;
func X \+\ Y -> ManySortedSet of I equals
:: PBOOLE:def 12
(X \ Y) \/ (Y \ X);
commutativity;
end;

theorem :: PBOOLE:4
for i st i in I holds (X \+\ Y).i = X.i \+\ Y.i;

theorem :: PBOOLE:5
for i st i in I holds I.i = {};

theorem :: PBOOLE:6
(for i st i in I holds X.i = {}) implies X = I;

theorem :: PBOOLE:7
x in X or x in Y implies x in X \/ Y;

theorem :: PBOOLE:8
x in X /\ Y iff x in X & x in Y;

theorem :: PBOOLE:9
x in X & X c= Y implies x in Y;

theorem :: PBOOLE:10
x in X & x in Y implies X overlaps Y;

theorem :: PBOOLE:11
X overlaps Y implies ex x st x in X & x in Y;

theorem :: PBOOLE:12
x in X \ Y implies x in X;

begin :: Lattice properties

theorem :: PBOOLE:13
X c= X;

definition let I,X,Y;
redefine pred X = Y means
:: PBOOLE:def 13
X c= Y & Y c= X;
end;

canceled;

theorem :: PBOOLE:15
X c= Y & Y c= Z implies X c= Z;

theorem :: PBOOLE:16
X c= X \/ Y & Y c= X \/ Y;

theorem :: PBOOLE:17
X /\ Y c= X & X /\ Y c= Y;

theorem :: PBOOLE:18
X c= Z & Y c= Z implies X \/ Y c= Z;

theorem :: PBOOLE:19
Z c= X & Z c= Y implies Z c= X /\ Y;

theorem :: PBOOLE:20
X c= Y implies X \/ Z c= Y \/ Z & Z \/ X c= Z \/ Y;

theorem :: PBOOLE:21
X c= Y implies X /\ Z c= Y /\ Z & Z /\ X c= Z /\ Y;

theorem :: PBOOLE:22
X c= Y & Z c= V implies X \/ Z c= Y \/ V;

theorem :: PBOOLE:23
X c= Y & Z c= V implies X /\ Z c= Y /\ V;

theorem :: PBOOLE:24
X c= Y implies X \/ Y = Y & Y \/ X = Y;

theorem :: PBOOLE:25
X c= Y implies X /\ Y = X & Y /\ X = X;

theorem :: PBOOLE:26
X /\ Y c= X \/ Z;

theorem :: PBOOLE:27
X c= Z implies X \/ Y /\ Z = (X \/ Y) /\ Z;

theorem :: PBOOLE:28
X = Y \/ Z iff Y c= X & Z c= X & for V st Y c= V & Z c= V holds X c= V;

theorem :: PBOOLE:29
X = Y /\ Z iff X c= Y & X c= Z & for V st V c= Y & V c= Z holds V c= X;

canceled 4;

theorem :: PBOOLE:34
(X \/ Y) \/ Z = X \/ (Y \/ Z);

theorem :: PBOOLE:35
(X /\ Y) /\ Z = X /\ (Y /\ Z);

theorem :: PBOOLE:36
X /\ (X \/ Y) = X & (X \/ Y) /\ X = X & X /\ (Y \/ X) = X & (Y \/ X) /\ X = X;

theorem :: PBOOLE:37
X \/ (X /\ Y) = X & (X /\ Y) \/ X = X & X \/ (Y /\ X) = X & (Y /\ X) \/ X = X;

theorem :: PBOOLE:38
X /\ (Y \/ Z) = X /\ Y \/ X /\ Z;

theorem :: PBOOLE:39
X \/ Y /\ Z = (X \/ Y) /\ (X \/ Z) & Y /\ Z \/ X = (Y \/ X) /\ (Z \/ X);

theorem :: PBOOLE:40
(X /\ Y) \/ (X /\ Z) = X implies X c= Y \/ Z;

theorem :: PBOOLE:41
(X \/ Y) /\ (X \/ Z) = X implies Y /\ Z c= X;

theorem :: PBOOLE:42
(X /\ Y) \/ (Y /\ Z) \/ (Z /\ X) = (X \/ Y) /\ (Y \/ Z) /\ (Z \/ X);

theorem :: PBOOLE:43 :: SETWISEO:7
X \/ Y c= Z implies X c= Z & Y c= Z;

theorem :: PBOOLE:44 :: SYSREL:4
X c= Y /\ Z implies X c= Y & X c= Z;

theorem :: PBOOLE:45 :: SYSREL:2
X \/ Y \/ Z = (X \/ Z) \/ (Y \/ Z) &
X \/ (Y \/ Z) = (X \/ Y) \/ (X \/ Z);

theorem :: PBOOLE:46
X /\ Y /\ Z = (X /\ Z) /\ (Y /\ Z) &
X /\ (Y /\ Z) = (X /\ Y) /\ (X /\ Z);

theorem :: PBOOLE:47 :: SYSREL:3
X \/ (X \/ Y) = X \/ Y & X \/ Y \/ Y = X \/ Y;

theorem :: PBOOLE:48
X /\ (X /\ Y) = X /\ Y & X /\ Y /\ Y = X /\ Y;

begin :: ManySortedSet with empty components

theorem :: PBOOLE:49
I c= X;

theorem :: PBOOLE:50
X c= I implies X = I;

theorem :: PBOOLE:51
X c= Y & X c= Z & Y /\ Z = I implies X = I;

theorem :: PBOOLE:52
X c= Y & Y /\ Z = I implies X /\ Z = I;

theorem :: PBOOLE:53
X \/ I = X & I \/ X = X;

theorem :: PBOOLE:54
X \/ Y = I implies X = I & Y = I;

theorem :: PBOOLE:55
X /\ I = I & I /\ X = I;

theorem :: PBOOLE:56
X c= (Y \/ Z) & X /\ Z = I implies X c= Y;

theorem :: PBOOLE:57
Y c= X & X /\ Y = I implies Y = I;

begin :: Difference and symmetric difference

theorem :: PBOOLE:58
X \ Y = I iff X c= Y;

theorem :: PBOOLE:59
X c= Y implies X \ Z c= Y \ Z;

theorem :: PBOOLE:60
X c= Y implies Z \ Y c= Z \ X;

theorem :: PBOOLE:61
X c= Y & Z c= V implies X \ V c= Y \ Z;

theorem :: PBOOLE:62
X \ Y c= X;

theorem :: PBOOLE:63
X c= Y \ X implies X = I;

theorem :: PBOOLE:64
X \ X = I;

theorem :: PBOOLE:65
X \ I = X;

theorem :: PBOOLE:66
I \ X = I;

theorem :: PBOOLE:67
X \ (X \/ Y) = I & X \ (Y \/ X) = I;

theorem :: PBOOLE:68
X /\ (Y \ Z) = (X /\ Y) \ Z;

theorem :: PBOOLE:69
(X \ Y) /\ Y = I & Y /\ (X \ Y) = I;

theorem :: PBOOLE:70
X \ (Y \ Z) = (X \ Y) \/ X /\ Z;

theorem :: PBOOLE:71
(X \ Y) \/ X /\ Y = X & X /\ Y \/ (X \ Y) = X;

theorem :: PBOOLE:72
X c= Y implies Y = X \/ (Y \ X) & Y = (Y \ X) \/ X;

theorem :: PBOOLE:73
X \/ (Y \ X) = X \/ Y & (Y \ X) \/ X = Y \/ X;

theorem :: PBOOLE:74
X \ (X \ Y) = X /\ Y;

theorem :: PBOOLE:75
X \ (Y /\ Z) = (X \ Y) \/ (X \ Z);

theorem :: PBOOLE:76
X \ X /\ Y = X \ Y & X \ Y /\ X = X \ Y;

theorem :: PBOOLE:77
X /\ Y = I iff X \ Y = X;

theorem :: PBOOLE:78
(X \/ Y) \ Z = (X \ Z) \/ (Y \ Z);

theorem :: PBOOLE:79
(X \ Y) \ Z = X \ (Y \/ Z);

theorem :: PBOOLE:80 ::  TSEP_1, LEMMA3
(X /\ Y) \ Z = (X \ Z) /\ (Y \ Z);

theorem :: PBOOLE:81
(X \/ Y) \ Y = X \ Y;

theorem :: PBOOLE:82
X c= Y \/ Z implies X \ Y c= Z & X \ Z c= Y;

theorem :: PBOOLE:83
(X \/ Y) \ (X /\ Y) = (X \ Y) \/ (Y \ X);

theorem :: PBOOLE:84
(X \ Y) \ Y = X \ Y;

theorem :: PBOOLE:85
X \ (Y \/ Z) = (X \ Y) /\ (X \ Z);

theorem :: PBOOLE:86
X \ Y = Y \ X implies X = Y;

theorem :: PBOOLE:87
X /\ (Y \ Z) = X /\ Y \ X /\ Z;

theorem :: PBOOLE:88 :: NORMFORM:2
X \ Y c= Z implies X c= Y \/ Z;

theorem :: PBOOLE:89
X \ Y c= X \+\ Y;

canceled;

theorem :: PBOOLE:91
X \+\ I = X & I \+\ X = X;

theorem :: PBOOLE:92
X \+\ X = I;

canceled;

theorem :: PBOOLE:94
X \/ Y = (X \+\ Y) \/ X /\ Y;

theorem :: PBOOLE:95
X \+\ Y = (X \/ Y) \ X /\ Y;

theorem :: PBOOLE:96
(X \+\ Y) \ Z = (X \ (Y \/ Z)) \/ (Y \ (X \/ Z));

theorem :: PBOOLE:97
X \ (Y \+\ Z) = X \ (Y \/ Z) \/ X /\ Y /\ Z;

theorem :: PBOOLE:98
(X \+\ Y) \+\ Z = X \+\ (Y \+\ Z);

theorem :: PBOOLE:99
X \ Y c= Z & Y \ X c= Z implies X \+\ Y c= Z;

theorem :: PBOOLE:100  :: FINSUB_1:3
X \/ Y = X \+\ (Y \ X);

theorem :: PBOOLE:101
X /\ Y = X \+\ (X \ Y);

theorem :: PBOOLE:102  :: FINSUB_1:5
X \ Y = X \+\ (X /\ Y);

theorem :: PBOOLE:103
Y \ X = X \+\ (X \/ Y);

theorem :: PBOOLE:104 :: FINSUB_1:4
X \/ Y = X \+\ Y \+\ X /\ Y;

theorem :: PBOOLE:105 :: FINSUB_1:6
X /\ Y = X \+\ Y \+\ (X \/ Y);

begin :: Meeting and overlap(p?)ing

theorem :: PBOOLE:106
X overlaps Y or X overlaps Z implies X overlaps Y \/ Z;

canceled;

theorem :: PBOOLE:108
X overlaps Y & Y c= Z implies X overlaps Z;

theorem :: PBOOLE:109
X overlaps Y & X c= Z implies Z overlaps Y;

theorem :: PBOOLE:110  :: NORMFORM:1
X c= Y & Z c= V & X overlaps Z implies Y overlaps V;

theorem :: PBOOLE:111
X overlaps Y /\ Z implies X overlaps Y & X overlaps Z;

theorem :: PBOOLE:112 :: BORSUK_1:1
X overlaps Z & X c= V implies X overlaps Z /\ V;

theorem :: PBOOLE:113
X overlaps Y \ Z implies X overlaps Y;

theorem :: PBOOLE:114 :: PROB_2:7, RPR_1:36
Y does_not_overlap Z implies X /\ Y does_not_overlap X /\ Z;

theorem :: PBOOLE:115 :: AMI_2:1
X overlaps Y \ Z implies Y overlaps X \ Z;

theorem :: PBOOLE:116
X meets Y & Y c= Z implies X meets Z;

canceled;

theorem :: PBOOLE:118
Y misses X \ Y;

theorem :: PBOOLE:119
X /\ Y misses X \ Y;

theorem :: PBOOLE:120
X /\ Y misses X \+\ Y;

theorem :: PBOOLE:121
X misses Y implies X /\ Y = I;

theorem :: PBOOLE:122
X <> I implies X meets X;

theorem :: PBOOLE:123
X c= Y & X c= Z & Y misses Z implies X = I;

theorem :: PBOOLE:124  :: SETWISEO:9
Z \/ V = X \/ Y & X misses Z & Y misses V
implies X = V & Y = Z;

canceled;

theorem :: PBOOLE:126  :: FINSUB_1:1
X misses Y implies X \ Y = X;

theorem :: PBOOLE:127 :: FINSUB_1:2
X misses Y implies (X \/ Y) \ Y = X;

theorem :: PBOOLE:128 :: RPR_1:32
X \ Y = X implies X misses Y;

theorem :: PBOOLE:129 :: RLVECT_2:102
X \ Y misses Y \ X;

begin :: Roughly speaking

definition let I,X,Y;
pred X [= Y means
:: PBOOLE:def 14
for x st x in X holds x in Y;
reflexivity;
end;

theorem :: PBOOLE:130
X c= Y implies X [= Y;

theorem :: PBOOLE:131
X [= X;

theorem :: PBOOLE:132
X [= Y & Y [= Z implies X [= Z;

begin :: Non empty set of sorts

theorem :: PBOOLE:133
{} in {};

theorem :: PBOOLE:134
for X being ManySortedSet of {} holds X = {};

reserve I for non empty set,
x,X,Y for ManySortedSet of I;

theorem :: PBOOLE:135
X overlaps Y implies X meets Y;

theorem :: PBOOLE:136
not ex x st x in I;

theorem :: PBOOLE:137
x in X & x in Y implies X /\ Y <> I;

theorem :: PBOOLE:138
X does_not_overlap I & I does_not_overlap X;

theorem :: PBOOLE:139
X /\ Y = I implies X does_not_overlap Y;

theorem :: PBOOLE:140
X overlaps X implies X <> I;

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
:: PBOOLE:def 15
for i st i in I holds X.i is empty;
attr X is non-empty means
:: PBOOLE:def 16
for i st i in I holds X.i is non empty;
end;

definition let I be set;
cluster empty-yielding ManySortedSet of I;
cluster non-empty ManySortedSet of I;
end;

definition let I be non empty set;
cluster non-empty -> non empty-yielding ManySortedSet of I;
cluster empty-yielding -> non non-empty ManySortedSet of I;
end;

theorem :: PBOOLE:141
X is empty-yielding iff X = I;

theorem :: PBOOLE:142
Y is empty-yielding & X c= Y implies X is empty-yielding;

theorem :: PBOOLE:143
X is non-empty & X c= Y implies Y is non-empty;

theorem :: PBOOLE:144
X is non-empty & X [= Y implies X c= Y;

theorem :: PBOOLE:145
X is non-empty & X [= Y implies Y is non-empty;

reserve X for non-empty ManySortedSet of I;

theorem :: PBOOLE:146
ex x st x in X;

theorem :: PBOOLE:147
(for x holds x in X iff x in Y) implies X = Y;

theorem :: PBOOLE:148
(for x holds x in X iff x in Y & x in Z) implies X = Y /\ Z;

```