:: by Agnieszka Julia Marasik

::

:: Received June 23, 1997

:: Copyright (c) 1997-2018 Association of Mizar Users

registration
end;

theorem :: CLOSURE3:2

for I being set

for M, N being ManySortedSet of I

for F being SubsetFamily of M st N in F holds

meet |:F:| c=' N by CLOSURE2:21, MSSUBFAM:43;

for M, N being ManySortedSet of I

for F being SubsetFamily of M st N in F holds

meet |:F:| c=' N by CLOSURE2:21, MSSUBFAM:43;

theorem Th3: :: CLOSURE3:3

for S being non empty non void ManySortedSign

for MA being strict non-empty MSAlgebra over S

for F being SubsetFamily of the Sorts of MA st F c= SubSort MA holds

for B being MSSubset of MA st B = meet |:F:| holds

B is opers_closed

for MA being strict non-empty MSAlgebra over S

for F being SubsetFamily of the Sorts of MA st F c= SubSort MA holds

for B being MSSubset of MA st B = meet |:F:| holds

B is opers_closed

proof end;

Lm1: now :: thesis: for I being non empty set

for M being ManySortedSet of I holds support M = { x where x is Element of I : M . x <> {} }

for M being ManySortedSet of I holds support M = { x where x is Element of I : M . x <> {} }

let I be non empty set ; :: thesis: for M being ManySortedSet of I holds support M = { x where x is Element of I : M . x <> {} }

let M be ManySortedSet of I; :: thesis: support M = { x where x is Element of I : M . x <> {} }

set F = { x where x is Element of I : M . x <> {} } ;

thus support M = { x where x is Element of I : M . x <> {} } :: thesis: verum

end;
let M be ManySortedSet of I; :: thesis: support M = { x where x is Element of I : M . x <> {} }

set F = { x where x is Element of I : M . x <> {} } ;

thus support M = { x where x is Element of I : M . x <> {} } :: thesis: verum

proof

thus
support M c= { x where x is Element of I : M . x <> {} }
:: according to XBOOLE_0:def 10 :: thesis: { x where x is Element of I : M . x <> {} } c= support M

assume x in { x where x is Element of I : M . x <> {} } ; :: thesis: x in support M

then ex i being Element of I st

( x = i & M . i <> {} ) ;

hence x in support M by PRE_POLY:def 7; :: thesis: verum

end;
proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is Element of I : M . x <> {} } or x in support M )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support M or x in { x where x is Element of I : M . x <> {} } )

A1: dom M = I by PARTFUN1:def 2;

A2: support M c= dom M by PRE_POLY:37;

assume A3: x in support M ; :: thesis: x in { x where x is Element of I : M . x <> {} }

then M . x <> {} by PRE_POLY:def 7;

hence x in { x where x is Element of I : M . x <> {} } by A1, A2, A3; :: thesis: verum

end;
A1: dom M = I by PARTFUN1:def 2;

A2: support M c= dom M by PRE_POLY:37;

assume A3: x in support M ; :: thesis: x in { x where x is Element of I : M . x <> {} }

then M . x <> {} by PRE_POLY:def 7;

hence x in { x where x is Element of I : M . x <> {} } by A1, A2, A3; :: thesis: verum

assume x in { x where x is Element of I : M . x <> {} } ; :: thesis: x in support M

then ex i being Element of I st

( x = i & M . i <> {} ) ;

hence x in support M by PRE_POLY:def 7; :: thesis: verum

definition

let I be non empty set ;

let M be ManySortedSet of I;

for b_{1} being set holds

( b_{1} = support M iff b_{1} = { x where x is Element of I : M . x <> {} } )
by Lm1;

end;
let M be ManySortedSet of I;

:: original: support

redefine func support M -> set equals :: CLOSURE3:def 1

{ x where x is Element of I : M . x <> {} } ;

compatibility redefine func support M -> set equals :: CLOSURE3:def 1

{ x where x is Element of I : M . x <> {} } ;

for b

( b

:: deftheorem defines support CLOSURE3:def 1 :

for I being non empty set

for M being ManySortedSet of I holds support M = { x where x is Element of I : M . x <> {} } ;

for I being non empty set

for M being ManySortedSet of I holds support M = { x where x is Element of I : M . x <> {} } ;

theorem :: CLOSURE3:5

for I being non empty set

for M being V8() ManySortedSet of I holds M = (EmptyMS I) +* (M | (support M))

for M being V8() ManySortedSet of I holds M = (EmptyMS I) +* (M | (support M))

proof end;

theorem :: CLOSURE3:6

for I being non empty set

for M1, M2 being V8() ManySortedSet of I st M1 | (support M1) = M2 | (support M2) holds

M1 = M2

for M1, M2 being V8() ManySortedSet of I st M1 | (support M1) = M2 | (support M2) holds

M1 = M2

proof end;

::$CT

theorem Th7: :: CLOSURE3:8

for I being non empty set

for M being ManySortedSet of I

for x being Element of Bool M

for i being Element of I

for y being set st y in x . i holds

ex a being Element of Bool M st

( y in a . i & a is V45() & support a is finite & a c= x )

for M being ManySortedSet of I

for x being Element of Bool M

for i being Element of I

for y being set st y in x . i holds

ex a being Element of Bool M st

( y in a . i & a is V45() & support a is finite & a c= x )

proof end;

definition

let I be set ;

let M be ManySortedSet of I;

let A be SubsetFamily of M;

ex b_{1} being ManySortedSubset of M st

for i being set st i in I holds

b_{1} . i = union { (f . i) where f is Element of Bool M : f in A }

for b_{1}, b_{2} being ManySortedSubset of M st ( for i being set st i in I holds

b_{1} . i = union { (f . i) where f is Element of Bool M : f in A } ) & ( for i being set st i in I holds

b_{2} . i = union { (f . i) where f is Element of Bool M : f in A } ) holds

b_{1} = b_{2}

end;
let M be ManySortedSet of I;

let A be SubsetFamily of M;

func MSUnion A -> ManySortedSubset of M means :Def2: :: CLOSURE3:def 2

for i being set st i in I holds

it . i = union { (f . i) where f is Element of Bool M : f in A } ;

existence for i being set st i in I holds

it . i = union { (f . i) where f is Element of Bool M : f in A } ;

ex b

for i being set st i in I holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def2 defines MSUnion CLOSURE3:def 2 :

for I being set

for M being ManySortedSet of I

for A being SubsetFamily of M

for b_{4} being ManySortedSubset of M holds

( b_{4} = MSUnion A iff for i being set st i in I holds

b_{4} . i = union { (f . i) where f is Element of Bool M : f in A } );

for I being set

for M being ManySortedSet of I

for A being SubsetFamily of M

for b

( b

b

registration

let I be set ;

let M be ManySortedSet of I;

let A be empty SubsetFamily of M;

coherence

MSUnion A is empty-yielding

end;
let M be ManySortedSet of I;

let A be empty SubsetFamily of M;

coherence

MSUnion A is empty-yielding

proof end;

theorem :: CLOSURE3:9

for I being set

for M being ManySortedSet of I

for A being SubsetFamily of M holds MSUnion A = union |:A:|

for M being ManySortedSet of I

for A being SubsetFamily of M holds MSUnion A = union |:A:|

proof end;

definition

let I be set ;

let M be ManySortedSet of I;

let A, B be SubsetFamily of M;

:: original: \/

redefine func A \/ B -> SubsetFamily of M;

correctness

coherence

A \/ B is SubsetFamily of M;

by CLOSURE2:3;

end;
let M be ManySortedSet of I;

let A, B be SubsetFamily of M;

:: original: \/

redefine func A \/ B -> SubsetFamily of M;

correctness

coherence

A \/ B is SubsetFamily of M;

by CLOSURE2:3;

theorem :: CLOSURE3:10

for I being set

for M being ManySortedSet of I

for A, B being SubsetFamily of M holds MSUnion (A \/ B) = (MSUnion A) (\/) (MSUnion B)

for M being ManySortedSet of I

for A, B being SubsetFamily of M holds MSUnion (A \/ B) = (MSUnion A) (\/) (MSUnion B)

proof end;

theorem :: CLOSURE3:11

for I being set

for M being ManySortedSet of I

for A, B being SubsetFamily of M st A c= B holds

MSUnion A c= MSUnion B

for M being ManySortedSet of I

for A, B being SubsetFamily of M st A c= B holds

MSUnion A c= MSUnion B

proof end;

definition

let I be set ;

let M be ManySortedSet of I;

let A, B be SubsetFamily of M;

:: original: /\

redefine func A /\ B -> SubsetFamily of M;

correctness

coherence

A /\ B is SubsetFamily of M;

by CLOSURE2:4;

end;
let M be ManySortedSet of I;

let A, B be SubsetFamily of M;

:: original: /\

redefine func A /\ B -> SubsetFamily of M;

correctness

coherence

A /\ B is SubsetFamily of M;

by CLOSURE2:4;

theorem :: CLOSURE3:12

for I being set

for M being ManySortedSet of I

for A, B being SubsetFamily of M holds MSUnion (A /\ B) c= (MSUnion A) (/\) (MSUnion B)

for M being ManySortedSet of I

for A, B being SubsetFamily of M holds MSUnion (A /\ B) c= (MSUnion A) (/\) (MSUnion B)

proof end;

theorem :: CLOSURE3:13

for I being set

for M being ManySortedSet of I

for AA being set st ( for x being set st x in AA holds

x is SubsetFamily of M ) holds

for A, B being SubsetFamily of M st B = { (MSUnion X) where X is SubsetFamily of M : X in AA } & A = union AA holds

MSUnion B = MSUnion A

for M being ManySortedSet of I

for AA being set st ( for x being set st x in AA holds

x is SubsetFamily of M ) holds

for A, B being SubsetFamily of M st B = { (MSUnion X) where X is SubsetFamily of M : X in AA } & A = union AA holds

MSUnion B = MSUnion A

proof end;

:: deftheorem defines algebraic CLOSURE3:def 3 :

for I being non empty set

for M being ManySortedSet of I

for S being SetOp of M holds

( S is algebraic iff for x being Element of Bool M st x = S . x holds

ex A being SubsetFamily of M st

( A = { (S . a) where a is Element of Bool M : ( a is V45() & support a is finite & a c= x ) } & x = MSUnion A ) );

for I being non empty set

for M being ManySortedSet of I

for S being SetOp of M holds

( S is algebraic iff for x being Element of Bool M st x = S . x holds

ex A being SubsetFamily of M st

( A = { (S . a) where a is Element of Bool M : ( a is V45() & support a is finite & a c= x ) } & x = MSUnion A ) );

registration

let I be non empty set ;

let M be ManySortedSet of I;

ex b_{1} being SetOp of M st

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

end;
let M be ManySortedSet of I;

cluster non empty Relation-like Bool M -defined Bool M -valued Function-like V17( Bool M) quasi_total reflexive monotonic idempotent algebraic for SetOp of ;

existence ex b

( b

proof end;

:: deftheorem defines algebraic CLOSURE3:def 4 :

for S being non empty 1-sorted

for IT being ClosureSystem of S holds

( IT is algebraic iff ClSys->ClOp IT is algebraic );

for S being non empty 1-sorted

for IT being ClosureSystem of S holds

( IT is algebraic iff ClSys->ClOp IT is algebraic );

definition

let S be non empty non void ManySortedSign ;

let MA be non-empty MSAlgebra over S;

ex b_{1} being strict ClosureStr over 1-sorted(# the carrier of S #) st

( the Sorts of b_{1} = the Sorts of MA & the Family of b_{1} = SubSort MA )

for b_{1}, b_{2} being strict ClosureStr over 1-sorted(# the carrier of S #) st the Sorts of b_{1} = the Sorts of MA & the Family of b_{1} = SubSort MA & the Sorts of b_{2} = the Sorts of MA & the Family of b_{2} = SubSort MA holds

b_{1} = b_{2}
;

end;
let MA be non-empty MSAlgebra over S;

func SubAlgCl MA -> strict ClosureStr over 1-sorted(# the carrier of S #) means :Def5: :: CLOSURE3:def 5

( the Sorts of it = the Sorts of MA & the Family of it = SubSort MA );

existence ( the Sorts of it = the Sorts of MA & the Family of it = SubSort MA );

ex b

( the Sorts of b

proof end;

uniqueness for b

b

:: deftheorem Def5 defines SubAlgCl CLOSURE3:def 5 :

for S being non empty non void ManySortedSign

for MA being non-empty MSAlgebra over S

for b_{3} being strict ClosureStr over 1-sorted(# the carrier of S #) holds

( b_{3} = SubAlgCl MA iff ( the Sorts of b_{3} = the Sorts of MA & the Family of b_{3} = SubSort MA ) );

for S being non empty non void ManySortedSign

for MA being non-empty MSAlgebra over S

for b

( b

theorem Th13: :: CLOSURE3:14

for S being non empty non void ManySortedSign

for MA being strict non-empty MSAlgebra over S holds SubSort MA is absolutely-multiplicative SubsetFamily of the Sorts of MA

for MA being strict non-empty MSAlgebra over S holds SubSort MA is absolutely-multiplicative SubsetFamily of the Sorts of MA

proof end;

registration

let S be non empty non void ManySortedSign ;

let MA be strict non-empty MSAlgebra over S;

coherence

SubAlgCl MA is absolutely-multiplicative

end;
let MA be strict non-empty MSAlgebra over S;

coherence

SubAlgCl MA is absolutely-multiplicative

proof end;

registration

let S be non empty non void ManySortedSign ;

let MA be strict non-empty MSAlgebra over S;

coherence

SubAlgCl MA is algebraic

end;
let MA be strict non-empty MSAlgebra over S;

coherence

SubAlgCl MA is algebraic

proof end;