background image

4.4. PRODUCT OF TYPED SETS

67

Obvious

393

.

Restriction of a

Rel

-morphism is

Rel

-morphism.

Obvious

394

.

f

|

A

=

f

u

(

A

× >

T

Dst

f

) for every

Rel

-morphism

f

and

A

T

Src

f

.

Obvious

395

.

h

f

i

X

=

h

f

i

(

X

u

dom

f

) = im(

f

|

X

) for every

Rel

-morphism

f

and

X

T

Src

f

.

Obvious

396

.

f

v

A

×

B

dom

f

v

A

im

f

v

B

for every

Rel

-morphism

f

and

A

T

Src

f

,

B

T

Dst

f

.

Theorem

397

.

Let

A

,

B

be sets. If

S

P

(

T

A

×

T

B

) then

l

(

A,B

)

S

(

A

×

B

) =

l

dom

S

×

l

im

S.

Proof.

For every atomic

x

T

A

,

y

T

B

we have

x

×

y

v

l

(

A,B

)

S

(

A

×

B

)

⇔ ∀

(

A, B

)

S

:

x

×

y

v

A

×

B

(

A, B

)

S

: (

x

v

A

y

v

B

)

⇔ ∀

A

dom

S

:

x

v

A

∧ ∀

B

im

S

:

y

v

B

x

v

l

dom

S

y

v

l

im

S

x

×

y

v

l

dom

S

×

l

im

S.

Obvious

398

.

If

U

,

W

are sets and

A

T

(

U

) then

A

×

is a complete homo-

morphism from the lattice

T

(

W

) to the lattice

Rel

(

U, W

), if also

A

6

=

then it

is an order embedding.