:: CLOSURE3 semantic presentation

registration

let c₁ be non empty 1-sorted ;
cluster 1-sorted(# the carrier of a₁ #) -> non empty ;
coherence by STRUCT_0:def 1;

end;

theorem Th1: :: CLOSURE3:1

for b₁ being non empty set
for b₂, b₃ being ManySortedSet of b₁ holds b₂ +* b₃ = b₃

proof end;

theorem Th2: :: CLOSURE3:2

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁
for b₄ being SubsetFamily of b₂ st b₃ in b₄ holds
meet |:b₄:| c=' b₃

proof end;

theorem Th3: :: CLOSURE3:3

for b₁ being non empty non void ManySortedSign
for b₂ being strict non-empty MSAlgebra of b₁
for b₃ being SubsetFamily of the Sorts of b₂ st b₃ c= SubSort b₂ holds
for b₄ being MSSubset of b₂ st b₄ = meet |:b₃:| holds
b₄ is opers_closed

proof end;

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
let c₃, c₄ be SubsetFamily of c₂;
pred c₄ is_finer_than c₃ means :Def1: :: CLOSURE3:def 1
for b₁ being set st b₁ in a₄ holds
ex b₂ being set st
( b₂ in a₃ & b₁ c= b₂ );
reflexivity ;
pred c₃ is_coarser_than c₄ means :Def2: :: CLOSURE3:def 2
for b₁ being set st b₁ in a₃ holds
ex b₂ being set st
( b₂ in a₄ & b₂ c= b₁ );
reflexivity ;

end;

:: deftheorem Def1 defines is_finer_than CLOSURE3:def 1 :

:: deftheorem Def2 defines is_coarser_than CLOSURE3:def 2 :

theorem Th4: :: CLOSURE3:4

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃, b₄, b₅ being SubsetFamily of b₂ st b₃ is_finer_than b₄ & b₄ is_finer_than b₅ holds
b₃ is_finer_than b₅

proof end;

theorem Th5: :: CLOSURE3:5

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃, b₄, b₅ being SubsetFamily of b₂ st b₃ is_coarser_than b₄ & b₄ is_coarser_than b₅ holds
b₃ is_coarser_than b₅

proof end;

definition

let c₁ be non empty set ;
let c₂ be ManySortedSet of c₁;
func supp c₂ -> set means :Def3: :: CLOSURE3:def 3
a₃ = { b₁ where B is Element of a₁ : a₂ . b₁ <> {} } ;
correctness ;

end;

:: deftheorem Def3 defines supp CLOSURE3:def 3 :

theorem Th6: :: CLOSURE3:6

for b₁ being non empty set
for b₂ being V3 ManySortedSet of b₁ holds b₂ = ([0] b₁) +* (b₂ | (supp b₂))

proof end;

theorem Th7: :: CLOSURE3:7

for b₁ being non empty set
for b₂, b₃ being V3 ManySortedSet of b₁ st supp b₂ = supp b₃ & b₂ | (supp b₂) = b₃ | (supp b₃) holds
b₂ = b₃

proof end;

theorem Th8: :: CLOSURE3:8

for b₁ being non empty set
for b₂ being ManySortedSet of b₁
for b₃ being Element of b₁ st not b₃ in supp b₂ holds
b₂ . b₃ = {}

proof end;

theorem Th9: :: CLOSURE3:9

for b₁ being non empty set
for b₂ being ManySortedSet of b₁
for b₃ being Element of Bool b₂
for b₄ being Element of b₁
for b₅ being set st b₅ in b₃ . b₄ holds
ex b₆ being Element of Bool b₂ st
( b₅ in b₆ . b₄ & b₆ is locally-finite & supp b₆ is finite & b₆ c= b₃ )

proof end;

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
let c₃ be SubsetFamily of c₂;
func MSUnion c₃ -> ManySortedSubset of a₂ means :Def4: :: CLOSURE3:def 4
for b₁ being set st b₁ in a₁ holds
a₄ . b₁ = union { (b₂ . b₁) where B is Element of Bool a₂ : b₂ in a₃ } ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines MSUnion CLOSURE3:def 4 :

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
let c₃ be non empty SubsetFamily of c₂;
redefine mode Element as Element of c₃ -> ManySortedSet of a₁;
coherence

proof end;

end;

registration

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
let c₃ be empty SubsetFamily of c₂;
cluster MSUnion a₃ -> V4 ;
coherence

proof end;

end;

theorem Th10: :: CLOSURE3:10

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃ being SubsetFamily of b₂ holds MSUnion b₃ = union |:b₃:|

proof end;

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
let c₃, c₄ be SubsetFamily of c₂;
redefine func \/ as c₃ \/ c₄ -> SubsetFamily of a₂;
correctness by CLOSURE2:4;

end;

theorem Th11: :: CLOSURE3:11

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃, b₄ being SubsetFamily of b₂ holds MSUnion (b₃ \/ b₄) = (MSUnion b₃) \/ (MSUnion b₄)

proof end;

theorem Th12: :: CLOSURE3:12

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃, b₄ being SubsetFamily of b₂ st b₃ c= b₄ holds
MSUnion b₃ c= MSUnion b₄

proof end;

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
let c₃, c₄ be SubsetFamily of c₂;
redefine func /\ as c₃ /\ c₄ -> SubsetFamily of a₂;
correctness by CLOSURE2:5;

end;

theorem Th13: :: CLOSURE3:13

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃, b₄ being SubsetFamily of b₂ holds MSUnion (b₃ /\ b₄) c= (MSUnion b₃) /\ (MSUnion b₄)

proof end;

theorem Th14: :: CLOSURE3:14

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃ being set st ( for b₄ being set st b₄ in b₃ holds
b₄ is SubsetFamily of b₂ ) holds
for b₄, b₅ being SubsetFamily of b₂ st b₅ = { (MSUnion b₆) where B is SubsetFamily of b₂ : b₆ in b₃ } & b₄ = union b₃ holds
MSUnion b₅ = MSUnion b₄

proof end;

definition

let c₁ be non empty set ;
let c₂ be ManySortedSet of c₁;
let c₃ be SetOp of c₂;
attr a₃ is algebraic means :: CLOSURE3:def 5
for b₁ being Element of Bool a₂ st b₁ = a₃ . b₁ holds
ex b₂ being SubsetFamily of a₂ st
( b₂ = { (a₃ . b₃) where B is Element of Bool a₂ : ( b₃ is locally-finite & supp b₃ is finite & b₃ c= b₁ ) } & b₁ = MSUnion b₂ );

end;

:: deftheorem Def5 defines algebraic CLOSURE3:def 5 :

registration

let c₁ be non empty set ;
let c₂ be ManySortedSet of c₁;
cluster reflexive monotonic idempotent algebraic M4( Bool a₂, Bool a₂);
existence

proof end;

end;

definition

let c₁ be non empty 1-sorted ;
let c₂ be ClosureSystem of c₁;
attr a₂ is algebraic means :: CLOSURE3:def 6
ClSys->ClOp a₂ is algebraic;

end;

:: deftheorem Def6 defines algebraic CLOSURE3:def 6 :

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
func SubAlgCl c₂ -> strict ClosureStr of 1-sorted(# the carrier of a₁ #) means :Def7: :: CLOSURE3:def 7
( the Sorts of a₃ = the Sorts of a₂ & the Family of a₃ = SubSort a₂ );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def7 defines SubAlgCl CLOSURE3:def 7 :

theorem Th15: :: CLOSURE3:15

canceled;

theorem Th16: :: CLOSURE3:16

for b₁ being non empty non void ManySortedSign
for b₂ being strict non-empty MSAlgebra of b₁ holds SubSort b₂ is absolutely-multiplicative SubsetFamily of the Sorts of b₂

proof end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be strict non-empty MSAlgebra of c₁;
cluster SubAlgCl a₂ -> strict absolutely-multiplicative ;
coherence

proof end;

end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be strict non-empty MSAlgebra of c₁;
cluster SubAlgCl a₂ -> strict absolutely-multiplicative algebraic ;
coherence

proof end;

end;