:: by Artur Korni{\l}owicz

::

:: Received February 7, 1996

:: Copyright (c) 1996-2012 Association of Mizar Users

begin

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))

for A being ManySortedSet of I

for B being ManySortedSubset of A holds rng B c= union (rng (bool A))

proof end;

begin

definition

let I be set ;

let M be ManySortedSet of I;

defpred S_{1}[ set ] means $1 is ManySortedSubset of M;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff x is ManySortedSubset of M )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff x is ManySortedSubset of M ) ) & ( for x being set holds

( x in b_{2} iff x is ManySortedSubset of M ) ) holds

b_{1} = b_{2}

end;
let M be ManySortedSet of I;

defpred S

func Bool M -> set means :Def1: :: CLOSURE2:def 1

for x being set holds

( x in it iff x is ManySortedSubset of M );

existence for x being set holds

( x in it iff x is ManySortedSubset of M );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def1 defines Bool CLOSURE2:def 1 :

for I being set

for M being ManySortedSet of I

for b_{3} being set holds

( b_{3} = Bool M iff for x being set holds

( x in b_{3} iff x is ManySortedSubset of M ) );

for I being set

for M being ManySortedSet of I

for b

( b

( x in b

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 )

end;
let M be ManySortedSet of I;

coherence

( not Bool M is empty & Bool M is functional & Bool M is with_common_domain )

proof end;

definition
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

end;
let M be ManySortedSet of I;

:: original: Bool

redefine func Bool M -> SubsetFamily of M;

coherence

Bool M is SubsetFamily of M

proof end;

registration

let I be set ;

let M be ManySortedSet of I;

existence

ex b_{1} being SubsetFamily of M st

( not b_{1} is empty & b_{1} is functional & b_{1} is with_common_domain )

end;
let M be ManySortedSet of I;

existence

ex b

( not b

proof end;

registration

let I be set ;

let M be ManySortedSet of I;

existence

ex b_{1} being SubsetFamily of M st

( b_{1} is empty & b_{1} is finite )

end;
let M be ManySortedSet of I;

existence

ex b

( b

proof 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 b_{1} being Element of S holds b_{1} is ManySortedSubset of M

end;
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 b

proof 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 ;

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 ;

for M being ManySortedSet of I

for SF, SG being SubsetFamily of M holds SF /\ SG is SubsetFamily of M ;

theorem :: CLOSURE2:5

for I, x being set

for M being ManySortedSet of I

for SF being SubsetFamily of M holds SF \ x is SubsetFamily of M ;

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 ;

for M being ManySortedSet of I

for SF, SG being SubsetFamily of M holds SF \+\ SG is SubsetFamily of M ;

theorem Th8: :: CLOSURE2:8

for I being set

for A, M, B being ManySortedSet of I st A c= M & B c= M holds

{A,B} is SubsetFamily of M

for A, M, B 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

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

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

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

for M being ManySortedSet of I

for E, T being Element of Bool M holds E \+\ T in Bool M

proof end;

begin

:: to the Operator on Many Sorted Subsets

definition

let S be functional set ;

( ( S <> {} implies ex b_{1} being Function ex A being non empty functional set st

( A = S & dom b_{1} = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom b_{1} holds

b_{1} . i = { (x . i) where x is Element of A : verum } ) ) ) & ( not S <> {} implies ex b_{1} being Function st b_{1} = {} ) )

for b_{1}, b_{2} being Function holds

( ( S <> {} & ex A being non empty functional set st

( A = S & dom b_{1} = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom b_{1} holds

b_{1} . i = { (x . i) where x is Element of A : verum } ) ) & ex A being non empty functional set st

( A = S & dom b_{2} = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom b_{2} holds

b_{2} . i = { (x . i) where x is Element of A : verum } ) ) implies b_{1} = b_{2} ) & ( not S <> {} & b_{1} = {} & b_{2} = {} implies b_{1} = b_{2} ) )

for b_{1} being Function holds verum
;

end;
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 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 = {} ;

( ( S <> {} implies ex b

( A = S & dom b

b

proof end;

uniqueness for b

( ( S <> {} & ex A being non empty functional set st

( A = S & dom b

b

( A = S & dom b

b

proof end;

consistency for b

:: deftheorem Def2 defines |. CLOSURE2:def 2 :

for S being functional set

for b_{2} being Function holds

( ( S <> {} implies ( b_{2} = |.S.| iff ex A being non empty functional set st

( A = S & dom b_{2} = meet { (dom x) where x is Element of A : verum } & ( for i being set st i in dom b_{2} holds

b_{2} . i = { (x . i) where x is Element of A : verum } ) ) ) ) & ( not S <> {} implies ( b_{2} = |.S.| iff b_{2} = {} ) ) );

for S being functional set

for b

( ( S <> {} implies ( b

( A = S & dom b

b

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

for M being ManySortedSet of I

for SF being non empty SubsetFamily of M holds dom |.SF.| = I

proof end;

registration
end;

definition

let I be set ;

let M be ManySortedSet of I;

let S be SubsetFamily of M;

coherence

( ( S <> {} implies |.S.| is ManySortedSet of I ) & ( not S <> {} implies [[0]] I is ManySortedSet of I ) )

for b_{1} being ManySortedSet of I holds verum
;

end;
let M be ManySortedSet of I;

let S be SubsetFamily of M;

coherence

( ( S <> {} implies |.S.| is ManySortedSet of I ) & ( not S <> {} implies [[0]] I is ManySortedSet of I ) )

proof end;

consistency for b

:: 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:| = [[0]] I ) );

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:| = [[0]] I ) );

registration

let I be set ;

let M be ManySortedSet of I;

let S be empty SubsetFamily of M;

coherence

|:S:| is empty-yielding

end;
let M be ManySortedSet of I;

let S be empty SubsetFamily of M;

coherence

|:S:| is empty-yielding

proof 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 }

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;

coherence

|:SF:| is non-empty

end;
let M be ManySortedSet of I;

let SF be non empty SubsetFamily of M;

coherence

|:SF:| is non-empty

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)}

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)}

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)}

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

end;
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;

theorem Th21: :: CLOSURE2:21

for I being set

for M, A being ManySortedSet of I

for SF being SubsetFamily of M st A in SF holds

A in' |:SF:|

for M, A 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 M, A, B being ManySortedSet of I

for SF being SubsetFamily of M st SF = {A,B} holds

union |:SF:| = A \/ B

for M, A, B 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

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:|

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;

definition

let I be set ;

let M be ManySortedSet of I;

let IT be SubsetFamily of M;

end;
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;

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 :Def5: :: CLOSURE2:def 5

for F being SubsetFamily of M st F c= IT holds

union |:F:| in IT;

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;

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;

for F being SubsetFamily of M st F c= IT holds

meet |:F:| in IT;

:: 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 );

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 Def5 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 );

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 );

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 );

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 );

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 Def9 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 [[0]] I in IT );

for I being set

for M being ManySortedSet of I

for IT being SubsetFamily of M holds

( IT is properly-lower-bound iff [[0]] 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;

ex b_{1} being SubsetFamily of M st

( not b_{1} is empty & b_{1} is functional & b_{1} is with_common_domain & b_{1} is additive & b_{1} is absolutely-additive & b_{1} is multiplicative & b_{1} is absolutely-multiplicative & b_{1} is properly-upper-bound & b_{1} is properly-lower-bound )

end;
let M be ManySortedSet of I;

cluster non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound for Element of bool (Bool M);

existence ex b

( not b

proof 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

Bool M is additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound SubsetFamily of M by Lm1;

end;
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

Bool M is additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound SubsetFamily of M by Lm1;

registration

let I be set ;

let M be ManySortedSet of I;

coherence

for b_{1} being SubsetFamily of M st b_{1} is absolutely-additive holds

b_{1} is additive

end;
let M be ManySortedSet of I;

coherence

for b

b

proof end;

registration

let I be set ;

let M be ManySortedSet of I;

coherence

for b_{1} being SubsetFamily of M st b_{1} is absolutely-multiplicative holds

b_{1} is multiplicative

end;
let M be ManySortedSet of I;

coherence

for b

b

proof end;

registration

let I be set ;

let M be ManySortedSet of I;

coherence

for b_{1} being SubsetFamily of M st b_{1} is absolutely-multiplicative holds

b_{1} is properly-upper-bound

end;
let M be ManySortedSet of I;

coherence

for b

b

proof end;

registration

let I be set ;

let M be ManySortedSet of I;

coherence

for b_{1} being SubsetFamily of M st b_{1} is properly-upper-bound holds

not b_{1} is empty
by Def8;

end;
let M be ManySortedSet of I;

coherence

for b

not b

registration

let I be set ;

let M be ManySortedSet of I;

coherence

for b_{1} being SubsetFamily of M st b_{1} is absolutely-additive holds

b_{1} is properly-lower-bound

end;
let M be ManySortedSet of I;

coherence

for b

b

proof end;

registration

let I be set ;

let M be ManySortedSet of I;

coherence

for b_{1} being SubsetFamily of M st b_{1} is properly-lower-bound holds

not b_{1} is empty
by Def9;

end;
let M be ManySortedSet of I;

coherence

for b

not b

begin

definition
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

end;
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;

definition

let I be set ;

let M be ManySortedSet of I;

let IT be SetOp of M;

end;
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;

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;

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);

for x being Element of Bool M holds IT . x = IT . (IT . x);

:: 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 );

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 );

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) );

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 Def13 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) );

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;

ex b_{1} being SetOp of M st

( b_{1} is reflexive & b_{1} is monotonic & b_{1} is idempotent & b_{1} is topological )

end;
let M be ManySortedSet of I;

cluster non empty Relation-like Function-like V17( Bool M) quasi_total reflexive monotonic idempotent topological for Element of bool [:(Bool M),(Bool M):];

existence ex b

( b

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

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

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)

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;

for b_{1} being SetOp of M st b_{1} is topological holds

b_{1} is monotonic

end;
let M be ManySortedSet of I;

cluster Function-like quasi_total topological -> monotonic for Element of bool [:(Bool M),(Bool M):];

coherence for b

b

proof 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

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

end;
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;

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

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

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

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

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;

begin

definition

let S be 1-sorted ;

attr c_{2} is strict ;

struct ClosureStr over S -> many-sorted over S;

aggr ClosureStr(# Sorts, Family #) -> ClosureStr over S;

sel Family c_{2} -> SubsetFamily of the Sorts of c_{2};

end;
attr c

struct ClosureStr over S -> many-sorted over S;

aggr ClosureStr(# Sorts, Family #) -> ClosureStr over S;

sel Family c

definition

let S be 1-sorted ;

let IT be ClosureStr over S;

end;
let IT be ClosureStr over S;

attr IT is absolutely-additive means :Def15: :: CLOSURE2:def 15

the Family of IT is absolutely-additive ;

the Family of IT is absolutely-additive ;

attr IT is absolutely-multiplicative means :Def17: :: CLOSURE2:def 17

the Family of IT is absolutely-multiplicative ;

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 ;

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 ;

the Family of IT is properly-lower-bound ;

:: 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 );

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 );

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 );

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 );

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 );

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 );

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;

coherence

ClosureStr(# the Sorts of MS,(Bool the Sorts of MS) #) is ClosureStr over S;

;

end;
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 ClosureStr(# the Sorts of MS,(Bool the Sorts of MS) #);

coherence

ClosureStr(# the Sorts of MS,(Bool the Sorts of MS) #) is ClosureStr over S;

;

:: 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) #);

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;

( 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;
let MS be many-sorted over S;

cluster Full MS -> strict additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ;

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 )

proof end;

registration

let S be 1-sorted ;

let MS be non-empty many-sorted over S;

coherence

Full MS is non-empty by MSUALG_1:def 3;

end;
let MS be non-empty many-sorted over S;

coherence

Full MS is non-empty by MSUALG_1:def 3;

registration

let S be 1-sorted ;

ex b_{1} being ClosureStr over S st

( b_{1} is strict & b_{1} is non-empty & b_{1} is additive & b_{1} is absolutely-additive & b_{1} is multiplicative & b_{1} is absolutely-multiplicative & b_{1} is properly-upper-bound & b_{1} is properly-lower-bound )

end;
cluster non-empty strict additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound for ClosureStr over S;

existence ex b

( b

proof end;

registration

let S be 1-sorted ;

let CS be additive ClosureStr over S;

coherence

the Family of CS is additive by Def14;

end;
let CS be additive ClosureStr over S;

coherence

the Family of CS is additive by Def14;

registration

let S be 1-sorted ;

let CS be absolutely-additive ClosureStr over S;

coherence

the Family of CS is absolutely-additive by Def15;

end;
let CS be absolutely-additive ClosureStr over S;

coherence

the Family of CS is absolutely-additive by Def15;

registration

let S be 1-sorted ;

let CS be multiplicative ClosureStr over S;

coherence

the Family of CS is multiplicative by Def16;

end;
let CS be multiplicative ClosureStr over S;

coherence

the Family of CS is multiplicative by Def16;

registration

let S be 1-sorted ;

let CS be absolutely-multiplicative ClosureStr over S;

coherence

the Family of CS is absolutely-multiplicative by Def17;

end;
let CS be absolutely-multiplicative ClosureStr over S;

coherence

the Family of CS is absolutely-multiplicative by Def17;

registration

let S be 1-sorted ;

let CS be properly-upper-bound ClosureStr over S;

coherence

the Family of CS is properly-upper-bound by Def18;

end;
let CS be properly-upper-bound ClosureStr over S;

coherence

the Family of CS is properly-upper-bound by Def18;

registration

let S be 1-sorted ;

let CS be properly-lower-bound ClosureStr over S;

coherence

the Family of CS is properly-lower-bound by Def19;

end;
let CS be properly-lower-bound ClosureStr over S;

coherence

the Family of CS is properly-lower-bound by Def19;

registration

let S be 1-sorted ;

let M be V8() ManySortedSet of the carrier of S;

let F be SubsetFamily of M;

coherence

ClosureStr(# M,F #) is non-empty

end;
let M be V8() ManySortedSet of the carrier of S;

let F be SubsetFamily of M;

coherence

ClosureStr(# M,F #) is non-empty

proof end;

registration

let S be 1-sorted ;

let MS be many-sorted over S;

let F be additive SubsetFamily of the Sorts of MS;

coherence

ClosureStr(# the Sorts of MS,F #) is additive by Def14;

end;
let MS be many-sorted over S;

let F be additive SubsetFamily of the Sorts of MS;

coherence

ClosureStr(# the Sorts of MS,F #) is additive by Def14;

registration

let S be 1-sorted ;

let MS be many-sorted over S;

let F be absolutely-additive SubsetFamily of the Sorts of MS;

coherence

ClosureStr(# the Sorts of MS,F #) is absolutely-additive by Def15;

end;
let MS be many-sorted over S;

let F be absolutely-additive SubsetFamily of the Sorts of MS;

coherence

ClosureStr(# the Sorts of MS,F #) is absolutely-additive by Def15;

registration

let S be 1-sorted ;

let MS be many-sorted over S;

let F be multiplicative SubsetFamily of the Sorts of MS;

coherence

ClosureStr(# the Sorts of MS,F #) is multiplicative by Def16;

end;
let MS be many-sorted over S;

let F be multiplicative SubsetFamily of the Sorts of MS;

coherence

ClosureStr(# the Sorts of MS,F #) is multiplicative by Def16;

registration

let S be 1-sorted ;

let MS be many-sorted over S;

let F be absolutely-multiplicative SubsetFamily of the Sorts of MS;

coherence

ClosureStr(# the Sorts of MS,F #) is absolutely-multiplicative by Def17;

end;
let MS be many-sorted over S;

let F be absolutely-multiplicative SubsetFamily of the Sorts of MS;

coherence

ClosureStr(# the Sorts of MS,F #) is absolutely-multiplicative by Def17;

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;

coherence

ClosureStr(# the Sorts of MS,F #) is properly-upper-bound by Def18;

end;
let MS be many-sorted over S;

let F be properly-upper-bound SubsetFamily of the Sorts of MS;

coherence

ClosureStr(# the Sorts of MS,F #) is properly-upper-bound by Def18;

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;

coherence

ClosureStr(# the Sorts of MS,F #) is properly-lower-bound by Def19;

end;
let MS be many-sorted over S;

let F be properly-lower-bound SubsetFamily of the Sorts of MS;

coherence

ClosureStr(# the Sorts of MS,F #) is properly-lower-bound by Def19;

registration

let S be 1-sorted ;

coherence

for b_{1} being ClosureStr over S st b_{1} is absolutely-additive holds

b_{1} is additive

end;
coherence

for b

b

proof end;

registration

let S be 1-sorted ;

coherence

for b_{1} being ClosureStr over S st b_{1} is absolutely-multiplicative holds

b_{1} is multiplicative

end;
coherence

for b

b

proof end;

registration

let S be 1-sorted ;

coherence

for b_{1} being ClosureStr over S st b_{1} is absolutely-multiplicative holds

b_{1} is properly-upper-bound

end;
coherence

for b

b

proof end;

registration

let S be 1-sorted ;

coherence

for b_{1} being ClosureStr over S st b_{1} is absolutely-additive holds

b_{1} is properly-lower-bound

end;
coherence

for b

b

proof 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;
let M be ManySortedSet of I;

mode ClosureOperator of M is reflexive monotonic idempotent SetOp of M;

definition

let S be 1-sorted ;

let A be ManySortedSet of the carrier of S;

let g be ClosureOperator of A;

ex b_{1} being strict ClosureStr over S st

( the Sorts of b_{1} = A & the Family of b_{1} = { x where x is Element of Bool A : g . x = x } )

for b_{1}, b_{2} being strict ClosureStr over S st the Sorts of b_{1} = A & the Family of b_{1} = { x where x is Element of Bool A : g . x = x } & the Sorts of b_{2} = A & the Family of b_{2} = { x where x is Element of Bool A : g . x = x } holds

b_{1} = b_{2}
;

end;
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 ( the Sorts of it = A & the Family of it = { x where x is Element of Bool A : g . x = x } );

ex b

( the Sorts of b

proof end;

uniqueness for b

b

:: 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 b_{4} being strict ClosureStr over S holds

( b_{4} = ClOp->ClSys g iff ( the Sorts of b_{4} = A & the Family of b_{4} = { x where x is Element of Bool A : g . x = x } ) );

for S being 1-sorted

for A being ManySortedSet of the carrier of S

for g being ClosureOperator of A

for b

( b

registration

let S be 1-sorted ;

let A be ManySortedSet of the carrier of S;

let g be ClosureOperator of A;

coherence

ClOp->ClSys g is absolutely-multiplicative

end;
let A be ManySortedSet of the carrier of S;

let g be ClosureOperator of A;

coherence

ClOp->ClSys g is absolutely-multiplicative

proof end;

definition

let S be 1-sorted ;

let A be ClosureSystem of S;

let C be ManySortedSubset of the Sorts of A;

ex b_{1} being Element of Bool the Sorts of A ex F being SubsetFamily of the Sorts of A st

( b_{1} = meet |:F:| & F = { X where X is Element of Bool the Sorts of A : ( C c=' X & X in the Family of A ) } )

for b_{1}, b_{2} being Element of Bool the Sorts of A st ex F being SubsetFamily of the Sorts of A st

( b_{1} = 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

( b_{2} = meet |:F:| & F = { X where X is Element of Bool the Sorts of A : ( C c=' X & X in the Family of A ) } ) holds

b_{1} = b_{2}
;

end;
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 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 ) } );

ex b

( b

proof end;

uniqueness for b

( b

( b

b

:: 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 b_{4} being Element of Bool the Sorts of A holds

( b_{4} = Cl C iff ex F being SubsetFamily of the Sorts of A st

( b_{4} = meet |:F:| & F = { X where X is Element of Bool the Sorts of A : ( C c=' X & X in the Family of A ) } ) );

for S being 1-sorted

for A being ClosureSystem of S

for C being ManySortedSubset of the Sorts of A

for b

( b

( b

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

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

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 )

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;

ex b_{1} being ClosureOperator of the Sorts of D st

for x being Element of Bool the Sorts of D holds b_{1} . x = Cl x

for b_{1}, b_{2} being ClosureOperator of the Sorts of D st ( for x being Element of Bool the Sorts of D holds b_{1} . x = Cl x ) & ( for x being Element of Bool the Sorts of D holds b_{2} . x = Cl x ) holds

b_{1} = b_{2}

end;
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 for x being Element of Bool the Sorts of D holds it . x = Cl x;

ex b

for x being Element of Bool the Sorts of D holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def23 defines ClSys->ClOp CLOSURE2:def 23 :

for S being 1-sorted

for D being ClosureSystem of S

for b_{3} being ClosureOperator of the Sorts of D holds

( b_{3} = ClSys->ClOp D iff for x being Element of Bool the Sorts of D holds b_{3} . x = Cl x );

for S being 1-sorted

for D being ClosureSystem of S

for b

( b

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 (ClOp->ClSys f) = f

for A being ManySortedSet of the carrier of S

for f being ClosureOperator of A holds ClSys->ClOp (ClOp->ClSys f) = f

proof end;

deffunc H

theorem :: CLOSURE2:42

for S being 1-sorted

for D being ClosureSystem of S holds ClOp->ClSys (ClSys->ClOp D) = ClosureStr(# the Sorts of D, the Family of D #)

for D being ClosureSystem of S holds ClOp->ClSys (ClSys->ClOp D) = ClosureStr(# the Sorts of D, the Family of D #)

proof end;