The abstract of the Mizar article:

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

by

Artur Kornilowicz

Received February 7, 1996

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;
 attr IT is additive means
:: CLOSURE2:def 5
    for A, B st A in IT & B in IT holds A \/ B in IT;

 attr IT is absolutely-additive means
:: 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
          additive absolutely-additive
           multiplicative absolutely-multiplicative
            properly-upper-bound properly-lower-bound
             SubsetFamily of M;
end;

definition let I, M;
 redefine func Bool M -> additive absolutely-additive multiplicative
       absolutely-multiplicative properly-upper-bound properly-lower-bound
        SubsetFamily of M;
end;

definition let I, M;
 cluster absolutely-additive -> additive SubsetFamily of 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;
 cluster absolutely-additive ->
                 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;
 attr IT is additive means
:: CLOSURE2:def 16
  the Family of IT is additive;

 attr IT is absolutely-additive means
:: 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;
 cluster Full MS -> strict additive absolutely-additive
                    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;
 cluster strict non-empty additive absolutely-additive
         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;
 cluster absolutely-additive -> additive ClosureStr over 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;