background image

13.6 Domain and range of a pointfree funcoid: The definition and properties of funcoid image (and
domain) are rewritten.

13.7 Category of pointfree funcoids:

I

A

FCD

(

A

)

id

A

FCD

(

A

)

Theorem 13.59 and its proof: 1.

⊆ → ⊑

; 2. up

up

(

A

;

Z

0

)

.

Proof of proposition 13.64: More detailed proof.

Proof of proposition 13.65:

⊆ → ⊑

.

Proposition 13.72: meet-semilattice

meet-semilattice with least element.

Proof of theorem 13.73: Corrected wrong theorem reference.

Proof of theorem 13.75:

B

FCD

(

A

;

B

)

.

Proposition 13.79:

⊔ → ∪

.

Proof of proposition 13.80:

∪ → ⊔

.

Theorem 13.88:

h

f

i

Z

0

S

→ h

f

i

F

Z

0

S

.

Proof of theorem 13.88: Replaced a wrong formula reference with a true formula.

Theorem 13.89: Added “atomic”.

Theorem 13.89 and its proof: Removed superfluous conditions.

Proposition 13.91: Removed unnecessary condition “and

Z

0

is a complete boolean lattice”.

Definition 13.92: Added “atomistic”.

Obvuous 13.95: Turned into a proposition and added a proof.

Obvious 13.98: Removed as wrong in the case if our posets are not meet-semilattices.

Thereom 13.98: Added “with least element”; added that

B

is atomic.

Proof of thereom 13.98: 1.

A

→ ⊓

A

; 2. added more explicit proposition references; 3.

0

0

B

.

Theorem 13.99:

⊓ → ⊓

Z

0

.

Proof of theorem 13.99: rewritten.

Theorem 13.99:

Z

0

Z

1

.

13.14 Elements closed regarding a pointfree funcoid: Removed superfluous “with least element”.

Proof of theorem 13.101: 1.

⊆ → ⊑

; 2. Added “(used separability of

A

)”.

Proposition 13.104: Added “with join-closed core”.

14.2 Limit:

{

a

} → ↑

Src

µ

{

a

}

;

h

f

i → h

f

i

;

∩ → ⊓

;

0

Dst

f

0

F

(

Dst

f

)

.

14.3 Generalized limit: “group of permutations of”

“permutation group on”.

14.3.1 :

h

µ

i

{

x

} → h

µ

i

{

x

}

. “We will assume that the funcoid

f

is defined on

h

µ

i

{

x

}

.”

“We

will assume that the dom

f

⊒ h

µ

i

{

x

}

.”

Proof of proposition 14.11:

⊑ → ⊒

.

Proof of proposition 14.20: Removed “where

x

D

”.

Proof of proposition 14.21: More detailed proof;

h

ν

ih

f

ih

µ

i

{

x

} → h

ν

ih

f

i{

x

}

.

Proof of theorem 14.23:

⊒ →

=

.

Corollary 14.24:

h

µ

i{

x

} → h

µ

i

{

x

}

.

bijective

injective.

5