Volume 8, 1996

University of Bialystok

Copyright (c) 1996 Association of Mizar Users

### The abstract of the Mizar article:

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

**by****Artur Kornilowicz**- Received February 7, 1996
- MML identifier: CLOSURE1

- [ Mizar article, MML identifier index ]

environ vocabulary PBOOLE, FUNCT_1, PRALG_1, ZF_REFLE, RELAT_1, FUNCT_4, CAT_1, FINSEQ_4, BOOLE, FUNCT_6, MSUALG_3, MATRIX_1, PRE_CIRC, CAT_4, RELAT_2, MSAFREE2, BINOP_1, FUNCOP_1, FINSET_1, MSUALG_1, MSSUBFAM, GRCAT_1, COHSP_1, MSUALG_2, SETFAM_1, CANTOR_1, CLOSURE1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2, CQC_LANG, FINSET_1, FUNCT_4, PBOOLE, MSUALG_1, MSUALG_2, MSUALG_3, PRALG_1, PRE_CIRC, EXTENS_1, CANTOR_1, MSSUBFAM; constructors AUTALG_1, CQC_LANG, EXTENS_1, MSUALG_3, PRE_CIRC, CANTOR_1, MSSUBFAM; clusters FINSET_1, FUNCT_1, MSSUBFAM, MSUALG_1, PBOOLE, PRALG_1, CQC_LANG, RELSET_1, SUBSET_1, XBOOLE_0; requirements SUBSET, BOOLE; begin :: Preliminaries reserve i, x, I for set, A, M for ManySortedSet of I, f for Function, F for ManySortedFunction of I; scheme MSSUBSET { I() -> set, A() -> non-empty ManySortedSet of I(), B() -> ManySortedSet of I(), P[set] } : (for X being ManySortedSet of I() holds X in A() iff X in B() & P[X]) implies A() c= B(); theorem :: CLOSURE1:1 for X being non empty set for x, y being set st x c= y holds { t where t is Element of X : y c= t } c= { z where z is Element of X : x c= z }; theorem :: CLOSURE1:2 (ex A st A in M) implies M is non-empty; definition let I, F, A; redefine func F..A -> ManySortedSet of I; end; definition let I; let A, B be non-empty ManySortedSet of I; let F be ManySortedFunction of A, B; let X be Element of A; redefine func F..X -> Element of B; end; theorem :: CLOSURE1:3 for A, X being ManySortedSet of I for B being non-empty ManySortedSet of I for F being ManySortedFunction of A, B st X in A holds F..X in B; theorem :: CLOSURE1:4 for F, G being ManySortedFunction of I for A being ManySortedSet of I st A in doms G holds F..(G..A) = (F ** G)..A; theorem :: CLOSURE1:5 F is "1-1" implies for A, B being ManySortedSet of I st A in doms F & B in doms F & F..A = F..B holds A = B; theorem :: CLOSURE1:6 doms F is non-empty & (for A, B being ManySortedSet of I st A in doms F & B in doms F & F..A = F..B holds A = B) implies F is "1-1"; theorem :: CLOSURE1:7 :: FUNCT_2:18 for A, B being non-empty ManySortedSet of I for F, G being ManySortedFunction of A, B st for M st M in A holds F..M = G..M holds F = G; definition let I, M; cluster empty-yielding locally-finite Element of bool M; end; begin :: Properties of Many Sorted Closure Operators definition let I, M; mode MSSetOp of M is ManySortedFunction of bool M, bool M; canceled; end; definition let I, M; let O be MSSetOp of M; let X be Element of bool M; redefine func O..X -> Element of bool M; end; definition let I, M; let IT be MSSetOp of M; attr IT is reflexive means :: CLOSURE1:def 2 for X being Element of bool M holds X c= IT..X; attr IT is monotonic means :: CLOSURE1:def 3 for X, Y being Element of bool M st X c= Y holds IT..X c= IT..Y; attr IT is idempotent means :: CLOSURE1:def 4 for X being Element of bool M holds IT..X = IT..(IT..X); attr IT is topological means :: CLOSURE1:def 5 for X, Y being Element of bool M holds IT..(X \/ Y) = (IT..X) \/ (IT..Y); end; theorem :: CLOSURE1:8 for M being non-empty ManySortedSet of I for X being Element of M holds X = (id M)..X; theorem :: CLOSURE1:9 for M being non-empty ManySortedSet of I for X, Y being Element of M st X c= Y holds (id M)..X c= (id M)..Y; theorem :: CLOSURE1:10 for M being non-empty ManySortedSet of I for X, Y being Element of M st X \/ Y is Element of M holds (id M)..(X \/ Y) = ((id M)..X) \/ ((id M)..Y); theorem :: CLOSURE1:11 for X being Element of bool M for i, x being set st i in I & x in ((id (bool M))..X).i ex Y being locally-finite Element of bool M st Y c= X & x in ((id (bool M))..Y).i; definition let I, M; cluster reflexive monotonic idempotent topological MSSetOp of M; end; theorem :: CLOSURE1:12 id (bool A) is reflexive MSSetOp of A; theorem :: CLOSURE1:13 id (bool A) is monotonic MSSetOp of A; theorem :: CLOSURE1:14 id (bool A) is idempotent MSSetOp of A; theorem :: CLOSURE1:15 id (bool A) is topological MSSetOp of A; reserve P, R for MSSetOp of M, E, T for Element of bool M; theorem :: CLOSURE1:16 E = M & P is reflexive implies E = P..E; theorem :: CLOSURE1:17 (P is reflexive & for X being Element of bool M holds P..X c= X) implies P is idempotent; theorem :: CLOSURE1:18 P is monotonic implies P..(E /\ T) c= P..E /\ P..T; definition let I, M; cluster topological -> monotonic MSSetOp of M; end; theorem :: CLOSURE1:19 P is topological implies P..E \ P..T c= P..(E \ T); definition let I, M, R, P; redefine func P ** R -> MSSetOp of M; end; theorem :: CLOSURE1:20 P is reflexive & R is reflexive implies P ** R is reflexive; theorem :: CLOSURE1:21 P is monotonic & R is monotonic implies P ** R is monotonic; theorem :: CLOSURE1:22 P is idempotent & R is idempotent & P**R = R**P implies P ** R is idempotent; theorem :: CLOSURE1:23 P is topological & R is topological implies P ** R is topological; theorem :: CLOSURE1:24 P is reflexive & i in I & f = P.i implies for x being Element of bool (M.i) holds x c= f.x; theorem :: CLOSURE1:25 P is monotonic & i in I & f = P.i implies for x, y being Element of bool (M.i) st x c= y holds f.x c= f.y; theorem :: CLOSURE1:26 P is idempotent & i in I & f = P.i implies for x being Element of bool (M.i) holds f.x = f.(f.x); theorem :: CLOSURE1:27 P is topological & i in I & f = P.i implies for x, y being Element of bool (M.i) holds f.(x \/ y) = (f.x) \/ (f.y); begin :: On the Many Sorted Closure Operator :: and the Many Sorted Closure System reserve S for 1-sorted; definition let S; struct(many-sorted over S) MSClosureStr over S (# Sorts -> ManySortedSet of the carrier of S, Family -> MSSubsetFamily of the Sorts #); end; reserve MS for many-sorted over S; definition let S; let IT be MSClosureStr over S; attr IT is additive means :: CLOSURE1:def 6 the Family of IT is additive; attr IT is absolutely-additive means :: CLOSURE1:def 7 the Family of IT is absolutely-additive; attr IT is multiplicative means :: CLOSURE1:def 8 the Family of IT is multiplicative; attr IT is absolutely-multiplicative means :: CLOSURE1:def 9 the Family of IT is absolutely-multiplicative; attr IT is properly-upper-bound means :: CLOSURE1:def 10 the Family of IT is properly-upper-bound; attr IT is properly-lower-bound means :: CLOSURE1:def 11 the Family of IT is properly-lower-bound; end; definition let S, MS; func MSFull MS -> MSClosureStr over S equals :: CLOSURE1:def 12 MSClosureStr (#the Sorts of MS, bool the Sorts of MS#); end; definition let S, MS; cluster MSFull 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 MSFull MS -> non-empty; end; definition let S; cluster strict non-empty additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound MSClosureStr over S; end; definition let S; let CS be additive MSClosureStr over S; cluster the Family of CS -> additive; end; definition let S; let CS be absolutely-additive MSClosureStr over S; cluster the Family of CS -> absolutely-additive; end; definition let S; let CS be multiplicative MSClosureStr over S; cluster the Family of CS -> multiplicative; end; definition let S; let CS be absolutely-multiplicative MSClosureStr over S; cluster the Family of CS -> absolutely-multiplicative; end; definition let S; let CS be properly-upper-bound MSClosureStr over S; cluster the Family of CS -> properly-upper-bound; end; definition let S; let CS be properly-lower-bound MSClosureStr 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 MSSubsetFamily of M; cluster MSClosureStr (#M, F#) -> non-empty; end; definition let S, MS; let F be additive MSSubsetFamily of the Sorts of MS; cluster MSClosureStr (#the Sorts of MS, F#) -> additive; end; definition let S, MS; let F be absolutely-additive MSSubsetFamily of the Sorts of MS; cluster MSClosureStr (#the Sorts of MS, F#) -> absolutely-additive; end; definition let S, MS; let F be multiplicative MSSubsetFamily of the Sorts of MS; cluster MSClosureStr (#the Sorts of MS, F#) -> multiplicative; end; definition let S, MS; let F be absolutely-multiplicative MSSubsetFamily of the Sorts of MS; cluster MSClosureStr (#the Sorts of MS, F#) -> absolutely-multiplicative; end; definition let S, MS; let F be properly-upper-bound MSSubsetFamily of the Sorts of MS; cluster MSClosureStr (#the Sorts of MS, F#) -> properly-upper-bound; end; definition let S, MS; let F be properly-lower-bound MSSubsetFamily of the Sorts of MS; cluster MSClosureStr (#the Sorts of MS, F#) -> properly-lower-bound; end; definition let S; cluster absolutely-additive -> additive MSClosureStr over S; end; definition let S; cluster absolutely-multiplicative -> multiplicative MSClosureStr over S; end; definition let S; cluster absolutely-multiplicative -> properly-upper-bound MSClosureStr over S; end; definition let S; cluster absolutely-additive -> properly-lower-bound MSClosureStr over S; end; definition let S; mode MSClosureSystem of S is absolutely-multiplicative MSClosureStr over S; end; definition let I, M; mode MSClosureOperator of M is reflexive monotonic idempotent MSSetOp of M; end; definition let I, M; let F be ManySortedFunction of M, M; func MSFixPoints F -> ManySortedSubset of M means :: CLOSURE1:def 13 for i st i in I holds x in it.i iff ex f being Function st f = F.i & x in dom f & f.x = x; end; definition let I; let M be empty-yielding ManySortedSet of I; let F be ManySortedFunction of M, M; cluster MSFixPoints F -> empty-yielding; end; theorem :: CLOSURE1:28 for F being ManySortedFunction of M, M holds A in M & F..A = A iff A in MSFixPoints F; theorem :: CLOSURE1:29 MSFixPoints id A = A; theorem :: CLOSURE1:30 for A being ManySortedSet of the carrier of S for J being reflexive monotonic MSSetOp of A for D being MSSubsetFamily of A st D = MSFixPoints J holds MSClosureStr (#A, D#) is MSClosureSystem of S; theorem :: CLOSURE1:31 for D being properly-upper-bound MSSubsetFamily of M for X being Element of bool M ex SF being non-empty MSSubsetFamily of M st for Y being ManySortedSet of I holds Y in SF iff Y in D & X c= Y; theorem :: CLOSURE1:32 for D being properly-upper-bound MSSubsetFamily of M for X being Element of bool M for SF being non-empty MSSubsetFamily of M st (for Y being ManySortedSet of I holds Y in SF iff Y in D & X c= Y) holds for i being set, Di being non empty set st i in I & Di = D.i holds SF.i = { z where z is Element of Di : X.i c= z }; theorem :: CLOSURE1:33 for D being properly-upper-bound MSSubsetFamily of M ex J being MSSetOp of M st for X being Element of bool M for SF being non-empty MSSubsetFamily of M st (for Y being ManySortedSet of I holds Y in SF iff Y in D & X c= Y) holds J..X = meet SF; theorem :: CLOSURE1:34 for D being properly-upper-bound MSSubsetFamily of M for A being Element of bool M for J being MSSetOp of M st A in D & for X being Element of bool M for SF being non-empty MSSubsetFamily of M st (for Y being ManySortedSet of I holds Y in SF iff Y in D & X c= Y) holds J..X = meet SF holds J..A = A; theorem :: CLOSURE1:35 for D being absolutely-multiplicative MSSubsetFamily of M for A being Element of bool M for J being MSSetOp of M st J..A = A & for X being Element of bool M for SF being non-empty MSSubsetFamily of M st (for Y being ManySortedSet of I holds Y in SF iff Y in D & X c= Y) holds J..X = meet SF holds A in D; theorem :: CLOSURE1:36 for D being properly-upper-bound MSSubsetFamily of M for J being MSSetOp of M st for X being Element of bool M for SF being non-empty MSSubsetFamily of M st (for Y being ManySortedSet of I holds Y in SF iff Y in D & X c= Y) holds J..X = meet SF holds J is reflexive monotonic; theorem :: CLOSURE1:37 for D being absolutely-multiplicative MSSubsetFamily of M for J being MSSetOp of M st for X being Element of bool M for SF being non-empty MSSubsetFamily of M st (for Y being ManySortedSet of I holds Y in SF iff Y in D & X c= Y) holds J..X = meet SF holds J is idempotent; theorem :: CLOSURE1:38 for D being MSClosureSystem of S for J being MSSetOp of the Sorts of D st for X being Element of bool the Sorts of D for SF being non-empty MSSubsetFamily of the Sorts of D st (for Y being ManySortedSet of the carrier of S holds Y in SF iff Y in the Family of D & X c= Y) holds J..X = meet SF holds J is MSClosureOperator of the Sorts of D; definition let S; let A be ManySortedSet of the carrier of S; let C be MSClosureOperator of A; func ClOp->ClSys C -> MSClosureSystem of S means :: CLOSURE1:def 14 ex D being MSSubsetFamily of A st D = MSFixPoints C & it = MSClosureStr (#A, D#); end; definition let S; let A be ManySortedSet of the carrier of S; let C be MSClosureOperator of A; cluster ClOp->ClSys C -> strict; end; definition let S; let A be non-empty ManySortedSet of the carrier of S; let C be MSClosureOperator of A; cluster ClOp->ClSys C -> non-empty; end; definition let S; let D be MSClosureSystem of S; func ClSys->ClOp D -> MSClosureOperator of the Sorts of D means :: CLOSURE1:def 15 for X being Element of bool the Sorts of D for SF being non-empty MSSubsetFamily of the Sorts of D st (for Y being ManySortedSet of the carrier of S holds Y in SF iff Y in the Family of D & X c= Y) holds it..X = meet SF; end; theorem :: CLOSURE1:39 for A being ManySortedSet of the carrier of S for J being MSClosureOperator of A holds ClSys->ClOp (ClOp->ClSys J) = J; theorem :: CLOSURE1:40 for D being MSClosureSystem of S holds ClOp->ClSys (ClSys->ClOp D) = the MSClosureStr of D;

Back to top