Journal of Formalized Mathematics
Volume 8, 1996
University of Bialystok
Copyright (c) 1996 Association of Mizar Users

### On the Closure Operator and the Closure System of Many Sorted Sets

by
Artur Kornilowicz

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

```environ

vocabulary PBOOLE, FUNCT_1, BOOLE, MSUALG_2, RELAT_1, TARSKI, FRAENKEL,
FUNCT_2, MATRIX_1, CAT_4, PRALG_2, FINSET_1, COMPLEX1, SETFAM_1, FUNCT_4,
ZF_REFLE, MSSUBFAM, CANTOR_1, CAT_1, GRCAT_1, COHSP_1, RELAT_2, MSAFREE2,
BINOP_1, CLOSURE1, MSUALG_1, PRE_TOPC, CLOSURE2;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, SETFAM_1, RELAT_1,
FUNCT_1, PARTFUN1, FUNCT_2, CQC_LANG, FINSET_1, FRAENKEL, FUNCT_4,
PBOOLE, MSUALG_1, MSUALG_2, PRALG_2, CANTOR_1, MBOOLEAN, MSSUBFAM;
constructors CQC_LANG, PRALG_2, PRE_CIRC, CANTOR_1, MSSUBFAM;
clusters ALTCAT_1, FINSET_1, FRAENKEL, FUNCT_1, MSSUBFAM, MSUALG_1, PBOOLE,
RELAT_1, CQC_LANG, RELSET_1, SUBSET_1, FUNCT_2;
requirements SUBSET, BOOLE;

begin  :: Preliminaries

reserve i, x, I for set,
A, B, M for ManySortedSet of I,
f, f1 for Function;

definition let I, A, B;
redefine pred A in B;
synonym A in' B;
end;

definition let I, A, B;
redefine pred A c= B;
synonym A c=' B;
end;

theorem :: CLOSURE2:1
for M being non empty set
for X, Y being Element of M st X c= Y
holds (id M).X c= (id M).Y;

canceled;

theorem :: CLOSURE2:3
for I being non empty set
for A being ManySortedSet of I
for B being ManySortedSubset of A holds
rng B c= union rng bool A;

definition
cluster empty -> functional set;
end;

definition
cluster empty functional set;
end;

definition let f, g be Function;
cluster { f,g } -> functional;
end;

begin  :: Set of Many Sorted Subsets of a Many Sorted Set

definition let I, M;
func Bool M -> set means
:: CLOSURE2:def 1
x in it iff x is ManySortedSubset of M;
end;

definition let I, M;
cluster Bool M -> non empty functional with_common_domain;
end;

definition let I, M;
mode SubsetFamily of M is Subset of Bool M;
canceled;
end;

definition let I, M;
redefine func Bool M -> SubsetFamily of M;
end;

definition let I, M;
cluster non empty functional with_common_domain SubsetFamily of M;
end;

definition let I, M;
cluster empty finite SubsetFamily of M;
end;

reserve SF, SG for SubsetFamily of M;

definition let I, M;
let S be non empty SubsetFamily of M;
redefine mode Element of S -> ManySortedSubset of M;
end;

theorem :: CLOSURE2:4    :: MSSUBFAM:34
SF \/ SG is SubsetFamily of M;

theorem :: CLOSURE2:5   :: MSSUBFAM:35
SF /\ SG is SubsetFamily of M;

theorem :: CLOSURE2:6    :: MSSUBFAM:36
SF \ x is SubsetFamily of M;

theorem :: CLOSURE2:7   :: MSSUBFAM:37
SF \+\ SG is SubsetFamily of M;

theorem :: CLOSURE2:8    :: MSSUBFAM:38
A c= M implies {A} is SubsetFamily of M;

theorem :: CLOSURE2:9    :: MSSUBFAM:39
A c= M & B c= M implies {A,B} is SubsetFamily of M;

reserve E, T for Element of Bool M;

theorem :: CLOSURE2:10
E /\ T in Bool M;

theorem :: CLOSURE2:11
E \/ T in Bool M;

theorem :: CLOSURE2:12
E \ A in Bool M;

theorem :: CLOSURE2:13
E \+\ T in Bool M;

begin  :: Many Sorted Operator corresponding
::  to the Operator on Many Sorted Subsets

definition let S be functional set;
func |. S .| -> Function means
:: CLOSURE2:def 3
ex A being non empty functional set st A = S &
dom it = meet { dom x where x is Element of A : not contradiction } &
for i st i in dom it holds
it.i = { x.i where x is Element of A : not contradiction }
if S <> {}
otherwise it = {};
end;

theorem :: CLOSURE2:14
for SF being non empty SubsetFamily of M holds dom |.SF.| = I;

definition let S be empty functional set;
cluster |. S .| -> empty;
end;

definition let I, M;
let S be SubsetFamily of M;
func |: S :| -> ManySortedSet of I equals
:: CLOSURE2:def 4
|. S .| if S <> {}
otherwise [0]I;
end;

definition let I, M;
let S be empty SubsetFamily of M;
cluster |: S :| -> empty-yielding;
end;

theorem :: CLOSURE2:15
SF is non empty implies
for i st i in I holds
|:SF:|.i = { x.i where x is Element of Bool M : x in SF };

definition let I, M;
let SF be non empty SubsetFamily of M;
cluster |: SF :| -> non-empty;
end;

theorem :: CLOSURE2:16
dom |.{f}.| = dom f;

theorem :: CLOSURE2:17
dom |.{f,f1}.| = dom f /\ dom f1;

theorem :: CLOSURE2:18
i in dom f implies |.{f}.|.i = {f.i};

theorem :: CLOSURE2:19
i in I & SF = {f} implies |:SF:|.i = {f.i};

theorem :: CLOSURE2:20
i in dom |.{f,f1}.| implies |.{f,f1}.|.i = { f.i , f1.i };

theorem :: CLOSURE2:21
i in I & SF = {f,f1} implies |:SF:|.i = { f.i , f1.i };

definition let I, M, SF;
redefine func |:SF:| -> MSSubsetFamily of M;
end;

theorem :: CLOSURE2:22
A in SF implies A in' |:SF:|;

theorem :: CLOSURE2:23
SF = {A,B} implies union |:SF:| = A \/ B;

theorem :: CLOSURE2:24    :: SETFAM_1:12
SF = {E,T} implies meet |:SF:| = E /\ T;

theorem :: CLOSURE2:25    :: MSSUBFAM:4
for Z being ManySortedSubset of M st
for Z1 being ManySortedSet of I st Z1 in SF holds Z c=' Z1 holds
Z c=' meet |:SF:|;

theorem :: CLOSURE2:26
|: Bool M :| = bool M;

definition let I, M;
let IT be SubsetFamily of M;
:: CLOSURE2:def 5
for A, B st A in IT & B in IT holds A \/ B in IT;

:: CLOSURE2:def 6
for F be SubsetFamily of M st F c= IT holds union |:F:| in IT;

attr IT is multiplicative means
:: CLOSURE2:def 7
for A, B st A in IT & B in IT holds A /\ B in IT;

attr IT is absolutely-multiplicative means
:: CLOSURE2:def 8
for F be SubsetFamily of M st F c= IT holds meet |:F:| in IT;

attr IT is properly-upper-bound means
:: CLOSURE2:def 9
M in IT;

attr IT is properly-lower-bound means
:: CLOSURE2:def 10
[0]I in IT;
end;

definition let I, M;
cluster non empty functional with_common_domain
multiplicative absolutely-multiplicative
properly-upper-bound properly-lower-bound
SubsetFamily of M;
end;

definition let I, M;
absolutely-multiplicative properly-upper-bound properly-lower-bound
SubsetFamily of M;
end;

definition let I, M;
end;

definition let I, M;
cluster absolutely-multiplicative -> multiplicative SubsetFamily of M;
end;

definition let I, M;
cluster absolutely-multiplicative ->
properly-upper-bound SubsetFamily of M;
end;

definition let I, M;
cluster properly-upper-bound -> non empty SubsetFamily of M;
end;

definition let I, M;
properly-lower-bound SubsetFamily of M;
end;

definition let I, M;
cluster properly-lower-bound -> non empty SubsetFamily of M;
end;

begin  :: Properties of Closure Operators

definition let I, M;
mode SetOp of M is Function of Bool M, Bool M;
canceled;
end;

definition let I, M;
let f be SetOp of M;
let x be Element of Bool M;
redefine func f.x -> Element of Bool M;
end;

definition let I, M;
let IT be SetOp of M;
attr IT is reflexive means
:: CLOSURE2:def 12
for x being Element of Bool M holds x c=' IT.x;

attr IT is monotonic means
:: CLOSURE2:def 13
for x, y being Element of Bool M st x c=' y holds IT.x c=' IT.y;

attr IT is idempotent means
:: CLOSURE2:def 14
for x being Element of Bool M holds IT.x = IT.(IT.x);

attr IT is topological means
:: CLOSURE2:def 15
for x, y being Element of Bool M holds IT.(x \/ y) = (IT.x) \/ (IT.y);
end;

definition let I, M;
cluster reflexive monotonic idempotent topological SetOp of M;
end;

theorem :: CLOSURE2:27   :: CLOSURE:11
id (Bool A) is reflexive SetOp of A;

theorem :: CLOSURE2:28   :: CLOSURE:12
id (Bool A) is monotonic SetOp of A;

theorem :: CLOSURE2:29    :: CLOSURE:13
id (Bool A) is idempotent SetOp of A;

theorem :: CLOSURE2:30   :: CLOSURE:15
id (Bool A) is topological SetOp of A;

reserve g, h for SetOp of M;

theorem :: CLOSURE2:31   :: CLOSURE:16
E = M & g is reflexive implies E = g.E;

theorem :: CLOSURE2:32   :: CLOSURE:17
(g is reflexive & for X being Element of Bool M holds g.X c= X)
implies g is idempotent;

theorem :: CLOSURE2:33   :: CLOSURE:18
for A being Element of Bool M st A = E /\ T holds
g is monotonic implies g.A c= g.E /\ g.T;

definition let I, M;
cluster topological -> monotonic SetOp of M;
end;

theorem :: CLOSURE2:34   :: CLOSURE:19
for A being Element of Bool M st A = E \ T holds
g is topological implies g.E \ g.T c= g.A;

definition let I, M, h, g;
redefine func g * h -> SetOp of M;
end;

theorem :: CLOSURE2:35   :: CLOSURE:21
g is reflexive & h is reflexive implies g * h is reflexive;

theorem :: CLOSURE2:36   :: CLOSURE:22
g is monotonic & h is monotonic implies g * h is monotonic;

theorem :: CLOSURE2:37    :: CLOSURE:23
g is idempotent & h is idempotent & g*h = h*g implies g * h is idempotent;

theorem :: CLOSURE2:38   :: CLOSURE:25
g is topological & h is topological implies g * h is topological;

begin  :: On the Closure Operator and the Closure System

reserve S for 1-sorted;

definition let S;
struct(many-sorted over S) ClosureStr over S (#
Sorts -> ManySortedSet of the carrier of S,
Family -> SubsetFamily of the Sorts #);
end;

reserve
MS for many-sorted over S;

definition let S;
let IT be ClosureStr over S;
:: CLOSURE2:def 16
the Family of IT is additive;

:: CLOSURE2:def 17
the Family of IT is absolutely-additive;

attr IT is multiplicative means
:: CLOSURE2:def 18
the Family of IT is multiplicative;

attr IT is absolutely-multiplicative means
:: CLOSURE2:def 19
the Family of IT is absolutely-multiplicative;

attr IT is properly-upper-bound means
:: CLOSURE2:def 20
the Family of IT is properly-upper-bound;

attr IT is properly-lower-bound means
:: CLOSURE2:def 21
the Family of IT is properly-lower-bound;
end;

definition let S, MS;
func Full MS -> ClosureStr over S equals
:: CLOSURE2:def 22
ClosureStr (#the Sorts of MS, Bool the Sorts of MS#);
end;

definition let S, MS;
multiplicative absolutely-multiplicative
properly-upper-bound properly-lower-bound;
end;

definition let S;
let MS be non-empty many-sorted over S;
cluster Full MS -> non-empty;
end;

definition let S;
multiplicative absolutely-multiplicative
properly-upper-bound properly-lower-bound ClosureStr over S;
end;

definition let S;
let CS be additive ClosureStr over S;
cluster the Family of CS -> additive;
end;

definition let S;
let CS be absolutely-additive ClosureStr over S;
cluster the Family of CS -> absolutely-additive;
end;

definition let S;
let CS be multiplicative ClosureStr over S;
cluster the Family of CS -> multiplicative;
end;

definition let S;
let CS be absolutely-multiplicative ClosureStr over S;
cluster the Family of CS -> absolutely-multiplicative;
end;

definition let S;
let CS be properly-upper-bound ClosureStr over S;
cluster the Family of CS -> properly-upper-bound;
end;

definition let S;
let CS be properly-lower-bound ClosureStr over S;
cluster the Family of CS -> properly-lower-bound;
end;

definition let S;
let M be non-empty ManySortedSet of the carrier of S;
let F be SubsetFamily of M;
cluster ClosureStr (#M, F#) -> non-empty;
end;

definition let S, MS;
let F be additive SubsetFamily of the Sorts of MS;
cluster ClosureStr (#the Sorts of MS, F#) -> additive;
end;

definition let S, MS;
let F be absolutely-additive SubsetFamily of the Sorts of MS;
cluster ClosureStr (#the Sorts of MS, F#) -> absolutely-additive;
end;

definition let S, MS;
let F be multiplicative SubsetFamily of the Sorts of MS;
cluster ClosureStr (#the Sorts of MS, F#) -> multiplicative;
end;

definition let S, MS;
let F be absolutely-multiplicative SubsetFamily of the Sorts of MS;
cluster ClosureStr (#the Sorts of MS, F#) -> absolutely-multiplicative;
end;

definition let S, MS;
let F be properly-upper-bound SubsetFamily of the Sorts of MS;
cluster ClosureStr (#the Sorts of MS, F#) -> properly-upper-bound;
end;

definition let S, MS;
let F be properly-lower-bound SubsetFamily of the Sorts of MS;
cluster ClosureStr (#the Sorts of MS, F#) -> properly-lower-bound;
end;

definition let S;
end;

definition let S;
cluster absolutely-multiplicative -> multiplicative ClosureStr over S;
end;

definition let S;
cluster absolutely-multiplicative -> properly-upper-bound ClosureStr over S;
end;

definition let S;
cluster absolutely-additive -> properly-lower-bound ClosureStr over S;
end;

definition let S;
mode ClosureSystem of S is absolutely-multiplicative ClosureStr over S;
end;

definition let I, M;
mode ClosureOperator of M is reflexive monotonic idempotent SetOp of M;
end;

theorem :: CLOSURE2:39
for A being ManySortedSet of the carrier of S
for f being reflexive monotonic SetOp of A
for D being SubsetFamily of A st
D = { x where x is Element of Bool A : f.x = x } holds
ClosureStr (#A, D#) is ClosureSystem of S;

definition let S;
let A be ManySortedSet of the carrier of S;
let g be ClosureOperator of A;
func ClOp->ClSys g -> strict ClosureSystem of S means
:: CLOSURE2:def 23
the Sorts of it = A &
the Family of it = { x where x is Element of Bool A : g.x = x };
end;

definition let S;
let A be ClosureSystem of S;
let C be ManySortedSubset of the Sorts of A;
func Cl C -> Element of Bool the Sorts of A means
:: CLOSURE2:def 24
ex F being SubsetFamily of the Sorts of A st
it = meet |:F:| & F = { X where X is Element of Bool the Sorts of A :
C c=' X & X in the Family of A };
end;

theorem :: CLOSURE2:40
for D being ClosureSystem of S
for a being Element of Bool the Sorts of D
for f being SetOp of the Sorts of D st

a in the Family of D &
for x being Element of Bool the Sorts of D holds f.x = Cl x

holds f.a = a;

theorem :: CLOSURE2:41
for D being ClosureSystem of S
for a being Element of Bool the Sorts of D
for f being SetOp of the Sorts of D st

f.a = a &
for x being Element of Bool the Sorts of D holds f.x = Cl x

holds a in the Family of D;

theorem :: CLOSURE2:42
for D being ClosureSystem of S
for f being SetOp of the Sorts of D st
for x being Element of Bool the Sorts of D holds f.x = Cl x
holds f is reflexive monotonic idempotent;

definition let S;
let D be ClosureSystem of S;
func ClSys->ClOp D -> ClosureOperator of the Sorts of D means
:: CLOSURE2:def 25
for x being Element of Bool the Sorts of D holds it.x = Cl x;
end;

theorem :: CLOSURE2:43
for A being ManySortedSet of the carrier of S
for f being ClosureOperator of A holds
ClSys->ClOp (ClOp->ClSys f) = f;

theorem :: CLOSURE2:44
for D being ClosureSystem of S holds
ClOp->ClSys (ClSys->ClOp D) = the ClosureStr of D;
```