:: On the Closure Operator and the Closure System of Many Sorted Sets
:: by Artur Korni{\l}owicz
::
:: Copyright (c) 1996-2021 Association of Mizar Users

notation
let I be set ;
let A, B be ManySortedSet of I;
synonym A in' B for A in B;
end;

notation
let I be set ;
let A, B be ManySortedSet of I;
synonym A c=' B for 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 ;

theorem Th2: :: CLOSURE2:2
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))
proof end;

definition
let I be set ;
let M be ManySortedSet of I;
defpred S1[ object ] means $1 is ManySortedSubset of M; func Bool M -> set means :Def1: :: CLOSURE2:def 1 for x being object holds ( x in it iff x is ManySortedSubset of M ); existence ex b1 being set st for x being object holds ( x in b1 iff x is ManySortedSubset of M ) proof end; uniqueness for b1, b2 being set st ( for x being object holds ( x in b1 iff x is ManySortedSubset of M ) ) & ( for x being object holds ( x in b2 iff x is ManySortedSubset of M ) ) holds b1 = b2 proof end; end; :: deftheorem Def1 defines Bool CLOSURE2:def 1 : for I being set for M being ManySortedSet of I for b3 being set holds ( b3 = Bool M iff for x being object holds ( x in b3 iff x is ManySortedSubset of M ) ); registration let I be set ; let M be ManySortedSet of I; coherence ( not Bool M is empty & Bool M is functional & Bool M is with_common_domain ) proof end; end; definition let I be set ; let M be ManySortedSet of I; mode SubsetFamily of M is Subset of (Bool M); end; definition let I be set ; let M be ManySortedSet of I; :: original: Bool redefine func Bool M -> SubsetFamily of M; coherence Bool M is SubsetFamily of M proof end; end; registration let I be set ; let M be ManySortedSet of I; existence ex b1 being SubsetFamily of M st ( not b1 is empty & b1 is functional & b1 is with_common_domain ) proof end; end; registration let I be set ; let M be ManySortedSet of I; existence ex b1 being SubsetFamily of M st ( b1 is empty & b1 is finite ) proof end; end; definition let I be set ; let M be ManySortedSet of I; let S be non empty SubsetFamily of M; :: original: Element redefine mode Element of S -> ManySortedSubset of M; coherence for b1 being Element of S holds b1 is ManySortedSubset of M proof end; end; theorem Th3: :: CLOSURE2:3 for I being set for M being ManySortedSet of I for SF, SG being SubsetFamily of M holds SF \/ SG is SubsetFamily of M ; theorem :: CLOSURE2:4 for I being set for M being ManySortedSet of I for SF, SG being SubsetFamily of M holds SF /\ SG is SubsetFamily of M ; theorem :: CLOSURE2:5 for x, I being set for M being ManySortedSet of I for SF being SubsetFamily of M holds SF \ x is SubsetFamily of M ; theorem :: CLOSURE2:6 for I being set for M being ManySortedSet of I for SF, SG being SubsetFamily of M holds SF \+\ SG is SubsetFamily of M ; theorem Th7: :: CLOSURE2:7 for I being set for A, M being ManySortedSet of I st A c= M holds {A} is SubsetFamily of M proof end; theorem Th8: :: CLOSURE2:8 for I being set for A, B, M being ManySortedSet of I st A c= M & B c= M holds {A,B} is SubsetFamily of M proof end; theorem Th9: :: CLOSURE2:9 for I being set for M being ManySortedSet of I for E, T being Element of Bool M holds E (/\) T in Bool M proof end; theorem Th10: :: CLOSURE2:10 for I being set for M being ManySortedSet of I for E, T being Element of Bool M holds E (\/) T in Bool M proof end; theorem :: CLOSURE2:11 for I being set for A, M being ManySortedSet of I for E being Element of Bool M holds E (\) A in Bool M proof end; theorem :: CLOSURE2:12 for I being set for M being ManySortedSet of I for E, T being Element of Bool M holds E (\+\) T in Bool M proof end; :: to the Operator on Many Sorted Subsets definition let S be functional set ; func |.S.| -> Function means :Def2: :: CLOSURE2:def 2 ex A being non empty functional set st ( A = S & dom it = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom it holds it . i = { (x . i) where x is Element of A : verum } ) ) if S <> {} otherwise it = {} ; existence ( ( S <> {} implies ex b1 being Function ex A being non empty functional set st ( A = S & dom b1 = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom b1 holds b1 . i = { (x . i) where x is Element of A : verum } ) ) ) & ( not S <> {} implies ex b1 being Function st b1 = {} ) ) proof end; uniqueness for b1, b2 being Function holds ( ( S <> {} & ex A being non empty functional set st ( A = S & dom b1 = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom b1 holds b1 . i = { (x . i) where x is Element of A : verum } ) ) & ex A being non empty functional set st ( A = S & dom b2 = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom b2 holds b2 . i = { (x . i) where x is Element of A : verum } ) ) implies b1 = b2 ) & ( not S <> {} & b1 = {} & b2 = {} implies b1 = b2 ) ) proof end; consistency for b1 being Function holds verum ; end; :: deftheorem Def2 defines |. CLOSURE2:def 2 : for S being functional set for b2 being Function holds ( ( S <> {} implies ( b2 = |.S.| iff ex A being non empty functional set st ( A = S & dom b2 = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom b2 holds b2 . i = { (x . i) where x is Element of A : verum } ) ) ) ) & ( not S <> {} implies ( b2 = |.S.| iff b2 = {} ) ) ); theorem Th13: :: CLOSURE2:13 for I being set for M being ManySortedSet of I for SF being non empty SubsetFamily of M holds dom |.SF.| = I proof end; registration let S be empty functional set ; cluster |.S.| -> empty ; coherence |.S.| is empty by Def2; end; definition let I be set ; let M be ManySortedSet of I; let S be SubsetFamily of M; func |:S:| -> ManySortedSet of I equals :Def3: :: CLOSURE2:def 3 |.S.| if S <> {} otherwise EmptyMS I; coherence ( ( S <> {} implies |.S.| is ManySortedSet of I ) & ( not S <> {} implies EmptyMS I is ManySortedSet of I ) ) proof end; consistency for b1 being ManySortedSet of I holds verum ; end; :: deftheorem Def3 defines |: CLOSURE2:def 3 : for I being set for M being ManySortedSet of I for S being SubsetFamily of M holds ( ( S <> {} implies |:S:| = |.S.| ) & ( not S <> {} implies |:S:| = EmptyMS I ) ); registration let I be set ; let M be ManySortedSet of I; let S be empty SubsetFamily of M; cluster |:S:| -> V9() ; coherence proof end; end; theorem Th14: :: CLOSURE2:14 for I being set for M being ManySortedSet of I for SF being SubsetFamily of M st not SF is empty holds for i being set st i in I holds |:SF:| . i = { (x . i) where x is Element of Bool M : x in SF } proof end; registration let I be set ; let M be ManySortedSet of I; let SF be non empty SubsetFamily of M; cluster |:SF:| -> V8() ; coherence |:SF:| is non-empty proof end; end; theorem Th15: :: CLOSURE2:15 for f being Function holds dom = dom f proof end; theorem :: CLOSURE2:16 for f, f1 being Function holds dom |.{f,f1}.| = (dom f) /\ (dom f1) proof end; theorem Th17: :: CLOSURE2:17 for i being set for f being Function st i in dom f holds . i = {(f . i)} proof end; theorem :: CLOSURE2:18 for i, I being set for M being ManySortedSet of I for f being Function for SF being SubsetFamily of M st i in I & SF = {f} holds |:SF:| . i = {(f . i)} proof end; theorem Th19: :: CLOSURE2:19 for i being set for f, f1 being Function st i in dom |.{f,f1}.| holds |.{f,f1}.| . i = {(f . i),(f1 . i)} proof end; theorem Th20: :: CLOSURE2:20 for i, I being set for M being ManySortedSet of I for f, f1 being Function for SF being SubsetFamily of M st i in I & SF = {f,f1} holds |:SF:| . i = {(f . i),(f1 . i)} proof end; definition let I be set ; let M be ManySortedSet of I; let SF be SubsetFamily of M; :: original: |: redefine func |:SF:| -> MSSubsetFamily of M; coherence |:SF:| is MSSubsetFamily of M proof end; end; theorem Th21: :: CLOSURE2:21 for I being set for A, M being ManySortedSet of I for SF being SubsetFamily of M st A in SF holds A in' |:SF:| proof end; theorem Th22: :: CLOSURE2:22 for I being set for A, B, M being ManySortedSet of I for SF being SubsetFamily of M st SF = {A,B} holds union |:SF:| = A (\/) B proof end; theorem Th23: :: CLOSURE2:23 for I being set for M being ManySortedSet of I for SF being SubsetFamily of M for E, T being Element of Bool M st SF = {E,T} holds meet |:SF:| = E (/\) T proof end; theorem Th24: :: CLOSURE2:24 for I being set for M being ManySortedSet of I for SF being SubsetFamily of M 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:| proof end; theorem :: CLOSURE2:25 for I being set for M being ManySortedSet of I holds |:(Bool M):| = bool M proof end; definition let I be set ; let M be ManySortedSet of I; let IT be SubsetFamily of M; attr IT is additive means :: CLOSURE2:def 4 for A, B being ManySortedSet of I st A in IT & B in IT holds A (\/) B in IT; attr IT is absolutely-additive means :: CLOSURE2:def 5 for F being SubsetFamily of M st F c= IT holds union |:F:| in IT; attr IT is multiplicative means :: CLOSURE2:def 6 for A, B being ManySortedSet of I st A in IT & B in IT holds A (/\) B in IT; attr IT is absolutely-multiplicative means :Def7: :: CLOSURE2:def 7 for F being SubsetFamily of M st F c= IT holds meet |:F:| in IT; attr IT is properly-upper-bound means :Def8: :: CLOSURE2:def 8 M in IT; attr IT is properly-lower-bound means :: CLOSURE2:def 9 EmptyMS I in IT; end; :: deftheorem defines additive CLOSURE2:def 4 : for I being set for M being ManySortedSet of I for IT being SubsetFamily of M holds ( IT is additive iff for A, B being ManySortedSet of I st A in IT & B in IT holds A (\/) B in IT ); :: deftheorem defines absolutely-additive CLOSURE2:def 5 : for I being set for M being ManySortedSet of I for IT being SubsetFamily of M holds ( IT is absolutely-additive iff for F being SubsetFamily of M st F c= IT holds union |:F:| in IT ); :: deftheorem defines multiplicative CLOSURE2:def 6 : for I being set for M being ManySortedSet of I for IT being SubsetFamily of M holds ( IT is multiplicative iff for A, B being ManySortedSet of I st A in IT & B in IT holds A (/\) B in IT ); :: deftheorem Def7 defines absolutely-multiplicative CLOSURE2:def 7 : for I being set for M being ManySortedSet of I for IT being SubsetFamily of M holds ( IT is absolutely-multiplicative iff for F being SubsetFamily of M st F c= IT holds meet |:F:| in IT ); :: deftheorem Def8 defines properly-upper-bound CLOSURE2:def 8 : for I being set for M being ManySortedSet of I for IT being SubsetFamily of M holds ( IT is properly-upper-bound iff M in IT ); :: deftheorem defines properly-lower-bound CLOSURE2:def 9 : for I being set for M being ManySortedSet of I for IT being SubsetFamily of M holds ( IT is properly-lower-bound iff EmptyMS I in IT ); Lm1: for I being set for M being ManySortedSet of I holds ( Bool M is additive & Bool M is absolutely-additive & Bool M is multiplicative & Bool M is absolutely-multiplicative & Bool M is properly-upper-bound & Bool M is properly-lower-bound ) proof end; registration let I be set ; let M be ManySortedSet of I; existence ex b1 being SubsetFamily of M st ( not b1 is empty & b1 is functional & b1 is with_common_domain & b1 is additive & b1 is absolutely-additive & b1 is multiplicative & b1 is absolutely-multiplicative & b1 is properly-upper-bound & b1 is properly-lower-bound ) proof end; end; definition let I be set ; let M be ManySortedSet of I; :: original: Bool redefine func Bool M -> additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound SubsetFamily of M; coherence by Lm1; end; registration let I be set ; let M be ManySortedSet of I; coherence for b1 being SubsetFamily of M st b1 is absolutely-additive holds b1 is additive proof end; end; registration let I be set ; let M be ManySortedSet of I; coherence for b1 being SubsetFamily of M st b1 is absolutely-multiplicative holds b1 is multiplicative proof end; end; registration let I be set ; let M be ManySortedSet of I; coherence for b1 being SubsetFamily of M st b1 is absolutely-multiplicative holds b1 is properly-upper-bound proof end; end; registration let I be set ; let M be ManySortedSet of I; cluster properly-upper-bound -> non empty for Element of bool (Bool M); coherence for b1 being SubsetFamily of M st b1 is properly-upper-bound holds not b1 is empty ; end; registration let I be set ; let M be ManySortedSet of I; coherence for b1 being SubsetFamily of M st b1 is absolutely-additive holds b1 is properly-lower-bound proof end; end; registration let I be set ; let M be ManySortedSet of I; cluster properly-lower-bound -> non empty for Element of bool (Bool M); coherence for b1 being SubsetFamily of M st b1 is properly-lower-bound holds not b1 is empty ; end; definition let I be set ; let M be ManySortedSet of I; mode SetOp of M is Function of (Bool M),(Bool M); end; definition let I be set ; let M be ManySortedSet of I; let f be SetOp of M; let x be Element of Bool M; :: original: . redefine func f . x -> Element of Bool M; coherence f . x is Element of Bool M proof end; end; definition let I be set ; let M be ManySortedSet of I; let IT be SetOp of M; attr IT is reflexive means :Def10: :: CLOSURE2:def 10 for x being Element of Bool M holds x c=' IT . x; attr IT is monotonic means :Def11: :: CLOSURE2:def 11 for x, y being Element of Bool M st x c=' y holds IT . x c=' IT . y; attr IT is idempotent means :Def12: :: CLOSURE2:def 12 for x being Element of Bool M holds IT . x = IT . (IT . x); attr IT is topological means :: CLOSURE2:def 13 for x, y being Element of Bool M holds IT . (x (\/) y) = (IT . x) (\/) (IT . y); end; :: deftheorem Def10 defines reflexive CLOSURE2:def 10 : for I being set for M being ManySortedSet of I for IT being SetOp of M holds ( IT is reflexive iff for x being Element of Bool M holds x c=' IT . x ); :: deftheorem Def11 defines monotonic CLOSURE2:def 11 : for I being set for M being ManySortedSet of I for IT being SetOp of M holds ( IT is monotonic iff for x, y being Element of Bool M st x c=' y holds IT . x c=' IT . y ); :: deftheorem Def12 defines idempotent CLOSURE2:def 12 : for I being set for M being ManySortedSet of I for IT being SetOp of M holds ( IT is idempotent iff for x being Element of Bool M holds IT . x = IT . (IT . x) ); :: deftheorem defines topological CLOSURE2:def 13 : for I being set for M being ManySortedSet of I for IT being SetOp of M holds ( IT is topological iff for x, y being Element of Bool M holds IT . (x (\/) y) = (IT . x) (\/) (IT . y) ); registration let I be set ; let M be ManySortedSet of I; existence ex b1 being SetOp of M st ( b1 is reflexive & b1 is monotonic & b1 is idempotent & b1 is topological ) proof end; end; theorem :: CLOSURE2:26 for I being set for A being ManySortedSet of I holds id (Bool A) is reflexive SetOp of A proof end; theorem :: CLOSURE2:27 for I being set for A being ManySortedSet of I holds id (Bool A) is monotonic SetOp of A proof end; theorem :: CLOSURE2:28 for I being set for A being ManySortedSet of I holds id (Bool A) is idempotent SetOp of A proof end; theorem :: CLOSURE2:29 for I being set for A being ManySortedSet of I holds id (Bool A) is topological SetOp of A proof end; theorem :: CLOSURE2:30 for I being set for M being ManySortedSet of I for E being Element of Bool M for g being SetOp of M st E = M & g is reflexive holds E = g . E proof end; theorem :: CLOSURE2:31 for I being set for M being ManySortedSet of I for g being SetOp of M st g is reflexive & ( for X being Element of Bool M holds g . X c= X ) holds g is idempotent proof end; theorem :: CLOSURE2:32 for I being set for M being ManySortedSet of I for E, T being Element of Bool M for g being SetOp of M for A being Element of Bool M st A = E (/\) T & g is monotonic holds g . A c= (g . E) (/\) (g . T) proof end; registration let I be set ; let M be ManySortedSet of I; coherence for b1 being SetOp of M st b1 is topological holds b1 is monotonic proof end; end; theorem :: CLOSURE2:33 for I being set for M being ManySortedSet of I for E, T being Element of Bool M for g being SetOp of M for A being Element of Bool M st A = E (\) T & g is topological holds (g . E) (\) (g . T) c= g . A proof end; definition let I be set ; let M be ManySortedSet of I; let h, g be SetOp of M; :: original: * redefine func g * h -> SetOp of M; coherence h * g is SetOp of M proof end; end; theorem :: CLOSURE2:34 for I being set for M being ManySortedSet of I for g, h being SetOp of M st g is reflexive & h is reflexive holds g * h is reflexive proof end; theorem :: CLOSURE2:35 for I being set for M being ManySortedSet of I for g, h being SetOp of M st g is monotonic & h is monotonic holds g * h is monotonic proof end; theorem :: CLOSURE2:36 for I being set for M being ManySortedSet of I for g, h being SetOp of M st g is idempotent & h is idempotent & g * h = h * g holds g * h is idempotent proof end; theorem :: CLOSURE2:37 for I being set for M being ManySortedSet of I for g, h being SetOp of M st g is topological & h is topological holds g * h is topological proof end; definition let S be 1-sorted ; attr c2 is strict ; struct ClosureStr over S -> many-sorted over S; aggr ClosureStr(# Sorts, Family #) -> ClosureStr over S; sel Family c2 -> SubsetFamily of the Sorts of c2; end; definition let S be 1-sorted ; let IT be ClosureStr over S; attr IT is additive means :Def14: :: CLOSURE2:def 14 the Family of IT is additive ; attr IT is absolutely-additive means :Def15: :: CLOSURE2:def 15 the Family of IT is absolutely-additive ; attr IT is multiplicative means :Def16: :: CLOSURE2:def 16 the Family of IT is multiplicative ; attr IT is absolutely-multiplicative means :Def17: :: CLOSURE2:def 17 the Family of IT is absolutely-multiplicative ; attr IT is properly-upper-bound means :Def18: :: CLOSURE2:def 18 the Family of IT is properly-upper-bound ; attr IT is properly-lower-bound means :Def19: :: CLOSURE2:def 19 the Family of IT is properly-lower-bound ; end; :: deftheorem Def14 defines additive CLOSURE2:def 14 : for S being 1-sorted for IT being ClosureStr over S holds ( IT is additive iff the Family of IT is additive ); :: deftheorem Def15 defines absolutely-additive CLOSURE2:def 15 : for S being 1-sorted for IT being ClosureStr over S holds ( IT is absolutely-additive iff the Family of IT is absolutely-additive ); :: deftheorem Def16 defines multiplicative CLOSURE2:def 16 : for S being 1-sorted for IT being ClosureStr over S holds ( IT is multiplicative iff the Family of IT is multiplicative ); :: deftheorem Def17 defines absolutely-multiplicative CLOSURE2:def 17 : for S being 1-sorted for IT being ClosureStr over S holds ( IT is absolutely-multiplicative iff the Family of IT is absolutely-multiplicative ); :: deftheorem Def18 defines properly-upper-bound CLOSURE2:def 18 : for S being 1-sorted for IT being ClosureStr over S holds ( IT is properly-upper-bound iff the Family of IT is properly-upper-bound ); :: deftheorem Def19 defines properly-lower-bound CLOSURE2:def 19 : for S being 1-sorted for IT being ClosureStr over S holds ( IT is properly-lower-bound iff the Family of IT is properly-lower-bound ); definition let S be 1-sorted ; let MS be many-sorted over S; func Full MS -> ClosureStr over S equals :: CLOSURE2:def 20 ClosureStr(# the Sorts of MS,(Bool the Sorts of MS) #); correctness coherence ClosureStr(# the Sorts of MS,(Bool the Sorts of MS) #) is ClosureStr over S ; ; end; :: deftheorem defines Full CLOSURE2:def 20 : for S being 1-sorted for MS being many-sorted over S holds Full MS = ClosureStr(# the Sorts of MS,(Bool the Sorts of MS) #); registration let S be 1-sorted ; let MS be many-sorted over S; coherence ( Full MS is strict & Full MS is additive & Full MS is absolutely-additive & Full MS is multiplicative & Full MS is absolutely-multiplicative & Full MS is properly-upper-bound & Full MS is properly-lower-bound ) ; end; registration let S be 1-sorted ; let MS be non-empty many-sorted over S; cluster Full MS -> non-empty ; coherence Full MS is non-empty ; end; registration let S be 1-sorted ; existence ex b1 being ClosureStr over S st ( b1 is strict & b1 is non-empty & b1 is additive & b1 is absolutely-additive & b1 is multiplicative & b1 is absolutely-multiplicative & b1 is properly-upper-bound & b1 is properly-lower-bound ) proof end; end; registration let S be 1-sorted ; let CS be additive ClosureStr over S; cluster the Family of CS -> additive ; coherence the Family of CS is additive by Def14; end; registration let S be 1-sorted ; let CS be absolutely-additive ClosureStr over S; cluster the Family of CS -> absolutely-additive ; coherence the Family of CS is absolutely-additive by Def15; end; registration let S be 1-sorted ; let CS be multiplicative ClosureStr over S; cluster the Family of CS -> multiplicative ; coherence the Family of CS is multiplicative by Def16; end; registration let S be 1-sorted ; let CS be absolutely-multiplicative ClosureStr over S; cluster the Family of CS -> absolutely-multiplicative ; coherence the Family of CS is absolutely-multiplicative by Def17; end; registration let S be 1-sorted ; let CS be properly-upper-bound ClosureStr over S; cluster the Family of CS -> properly-upper-bound ; coherence the Family of CS is properly-upper-bound by Def18; end; registration let S be 1-sorted ; let CS be properly-lower-bound ClosureStr over S; cluster the Family of CS -> properly-lower-bound ; coherence the Family of CS is properly-lower-bound by Def19; end; registration let S be 1-sorted ; let M be V8() ManySortedSet of the carrier of S; let F be SubsetFamily of M; cluster ClosureStr(# M,F #) -> non-empty ; coherence ClosureStr(# M,F #) is non-empty ; end; registration let S be 1-sorted ; let MS be many-sorted over S; let F be additive SubsetFamily of the Sorts of MS; cluster ClosureStr(# the Sorts of MS,F #) -> additive ; coherence ClosureStr(# the Sorts of MS,F #) is additive ; end; registration let S be 1-sorted ; let MS be many-sorted over S; let F be absolutely-additive SubsetFamily of the Sorts of MS; cluster ClosureStr(# the Sorts of MS,F #) -> absolutely-additive ; coherence ClosureStr(# the Sorts of MS,F #) is absolutely-additive ; end; registration let S be 1-sorted ; let MS be many-sorted over S; let F be multiplicative SubsetFamily of the Sorts of MS; cluster ClosureStr(# the Sorts of MS,F #) -> multiplicative ; coherence ClosureStr(# the Sorts of MS,F #) is multiplicative ; end; registration let S be 1-sorted ; let MS be many-sorted over S; let F be absolutely-multiplicative SubsetFamily of the Sorts of MS; cluster ClosureStr(# the Sorts of MS,F #) -> absolutely-multiplicative ; coherence ClosureStr(# the Sorts of MS,F #) is absolutely-multiplicative ; end; registration let S be 1-sorted ; let MS be many-sorted over S; let F be properly-upper-bound SubsetFamily of the Sorts of MS; cluster ClosureStr(# the Sorts of MS,F #) -> properly-upper-bound ; coherence ClosureStr(# the Sorts of MS,F #) is properly-upper-bound ; end; registration let S be 1-sorted ; let MS be many-sorted over S; let F be properly-lower-bound SubsetFamily of the Sorts of MS; cluster ClosureStr(# the Sorts of MS,F #) -> properly-lower-bound ; coherence ClosureStr(# the Sorts of MS,F #) is properly-lower-bound ; end; registration let S be 1-sorted ; cluster absolutely-additive -> additive for ClosureStr over S; coherence for b1 being ClosureStr over S st b1 is absolutely-additive holds b1 is additive ; end; registration let S be 1-sorted ; coherence for b1 being ClosureStr over S st b1 is absolutely-multiplicative holds b1 is multiplicative ; end; registration let S be 1-sorted ; coherence for b1 being ClosureStr over S st b1 is absolutely-multiplicative holds b1 is properly-upper-bound ; end; registration let S be 1-sorted ; coherence for b1 being ClosureStr over S st b1 is absolutely-additive holds b1 is properly-lower-bound ; end; definition end; definition let I be set ; let M be ManySortedSet of I; mode ClosureOperator of M is reflexive monotonic idempotent SetOp of M; end; definition let S be 1-sorted ; let A be ManySortedSet of the carrier of S; let g be ClosureOperator of A; func ClOp->ClSys g -> strict ClosureStr over S means :Def21: :: CLOSURE2:def 21 ( the Sorts of it = A & the Family of it = { x where x is Element of Bool A : g . x = x } ); existence ex b1 being strict ClosureStr over S st ( the Sorts of b1 = A & the Family of b1 = { x where x is Element of Bool A : g . x = x } ) proof end; uniqueness for b1, b2 being strict ClosureStr over S st the Sorts of b1 = A & the Family of b1 = { x where x is Element of Bool A : g . x = x } & the Sorts of b2 = A & the Family of b2 = { x where x is Element of Bool A : g . x = x } holds b1 = b2 ; end; :: deftheorem Def21 defines ClOp->ClSys CLOSURE2:def 21 : for S being 1-sorted for A being ManySortedSet of the carrier of S for g being ClosureOperator of A for b4 being strict ClosureStr over S holds ( b4 = ClOp->ClSys g iff ( the Sorts of b4 = A & the Family of b4 = { x where x is Element of Bool A : g . x = x } ) ); registration let S be 1-sorted ; let A be ManySortedSet of the carrier of S; let g be ClosureOperator of A; coherence proof end; end; definition let S be 1-sorted ; 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 :Def22: :: CLOSURE2:def 22 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 ) } ); existence ex b1 being Element of Bool the Sorts of A ex F being SubsetFamily of the Sorts of A st ( b1 = meet |:F:| & F = { X where X is Element of Bool the Sorts of A : ( C c=' X & X in the Family of A ) } ) proof end; uniqueness for b1, b2 being Element of Bool the Sorts of A st ex F being SubsetFamily of the Sorts of A st ( b1 = meet |:F:| & F = { X where X is Element of Bool the Sorts of A : ( C c=' X & X in the Family of A ) } ) & ex F being SubsetFamily of the Sorts of A st ( b2 = meet |:F:| & F = { X where X is Element of Bool the Sorts of A : ( C c=' X & X in the Family of A ) } ) holds b1 = b2 ; end; :: deftheorem Def22 defines Cl CLOSURE2:def 22 : for S being 1-sorted for A being ClosureSystem of S for C being ManySortedSubset of the Sorts of A for b4 being Element of Bool the Sorts of A holds ( b4 = Cl C iff ex F being SubsetFamily of the Sorts of A st ( b4 = meet |:F:| & F = { X where X is Element of Bool the Sorts of A : ( C c=' X & X in the Family of A ) } ) ); theorem Th38: :: CLOSURE2:38 for S being 1-sorted 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 proof end; theorem :: CLOSURE2:39 for S being 1-sorted 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 proof end; theorem Th40: :: CLOSURE2:40 for S being 1-sorted 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 & f is monotonic & f is idempotent ) proof end; definition let S be 1-sorted ; let D be ClosureSystem of S; func ClSys->ClOp D -> ClosureOperator of the Sorts of D means :Def23: :: CLOSURE2:def 23 for x being Element of Bool the Sorts of D holds it . x = Cl x; existence ex b1 being ClosureOperator of the Sorts of D st for x being Element of Bool the Sorts of D holds b1 . x = Cl x proof end; uniqueness for b1, b2 being ClosureOperator of the Sorts of D st ( for x being Element of Bool the Sorts of D holds b1 . x = Cl x ) & ( for x being Element of Bool the Sorts of D holds b2 . x = Cl x ) holds b1 = b2 proof end; end; :: deftheorem Def23 defines ClSys->ClOp CLOSURE2:def 23 : for S being 1-sorted for D being ClosureSystem of S for b3 being ClosureOperator of the Sorts of D holds ( b3 = ClSys->ClOp D iff for x being Element of Bool the Sorts of D holds b3 . x = Cl x ); theorem :: CLOSURE2:41 for S being 1-sorted for A being ManySortedSet of the carrier of S for f being ClosureOperator of A holds ClSys->ClOp () = f proof end; deffunc H1( set ) -> set =$1;

theorem :: CLOSURE2:42
for S being 1-sorted
for D being ClosureSystem of S holds ClOp->ClSys () = ClosureStr(# the Sorts of D, the Family of D #)
proof end;