 7.4. RESTRICTING RELOID TO A FILTER. DOMAIN AND IMAGE

137

Theorem

753

.

If

S

P

(

F

(

A

)

×

F

(

B

)) for some sets

A

,

B

then

l

A ×

RLD

B

(

A

;

B

)

S

=

l

dom

S

×

RLD

l

im

S.

Proof.

Let

P

=

d

dom

S

,

Q

=

d

im

S

;

l

=

d

n

RLD

B

(

A

;

B

)

S

o

.

P ×

RLD

Q v

l

is obvious.

Let

F

GR(

P ×

RLD

Q

). Then there exist

P

∈ P

and

Q

∈ Q

such that

F

P

×

Q

.

P

=

P

1

∩ · · · ∩

P

n

where

P

i

dom

S

and

Q

=

Q

1

∩ · · · ∩

Q

m

where

Q

j

im

S

.

P

×

Q

=

T

i,j

(

P

i

×

Q

j

).

P

i

×

Q

j

GR(

A ×

RLD

B

) for some (

A

;

B

)

S

.

P

×

Q

=

T

i,j

(

P

i

×

Q

j

)

GR

l

.

So

F

GR

l

.

Corollary

754

.

d

RLD

T

=

A ×

RLD

d

T

if

A

is a filter and

T

is a set of

filters with common base.

Proof.

Take

S

=

{A} ×

T

where

T

is a set of filters.

Then

d

n

RLD

B

B∈

T

o

=

A ×

RLD

d

T

that is

d

RLD

T

=

A ×

RLD

d

T

.

Definition

755

.

I will call a reloid

convex

iff it is a join of direct products.

7.4. Restricting reloid to a filter. Domain and image

Definition

756

.

Identity reloid

for a set

A

is defined by the formula

id

RLD

(

A

)

=

RLD

(

A

;

A

)

id

A

.

Obvious

757

.

(id

RLD

(

A

)

)

1

= id

RLD

(

A

)

.

Definition

758

.

I define

restricting

a reloid

f

to a filter

A

as

f

|

A

=

f

u

(

A ×

RLD

>

F

(Dst

f

)

).

Definition

759

.

Domain

and

image

of a reloid

f

are defined as follows:

dom

f

=

l

Src

f

h

dom

i

GR

f

; im

f

=

l

Src

f

h

im

i

GR

f.

Proposition

760

.

f

v A ×

RLD

B ⇔

dom

f

v A ∧

im

f

v B

for every reloid

f

and filters

A ∈

F

(Src

f

),

B ∈

F

(Dst

f

).

Proof.

. It follows from dom(

A ×

RLD

B

)

v A ∧

im(

A ×

RLD

B

)

v B

.

. dom

f

v A ⇔ ∀

A

∈ A∃

F

GR

f

: dom

F

A

. Analogously

im

f

v B ⇔ ∀

B

∈ B∃

G

GR

f

: im

G

B

.

Let dom

f

v A ∧

im

f

v B

,

A

∈ A

,

B

∈ B

. Then there exist

F, G

GR

f

such that dom

F

A

im

G

B

. Consequently

F

G

GR

f

,

dom(

F

G

)

A

, im(

F

G

)

B

that is

F

G

A

×

B

. So there

exists

H

GR

f

such that

H

A

×

B

for every

A

∈ A

,

B

∈ B

. So

f

v A ×

RLD

B

.

Definition

761

.

I call

restricted identity reloid

for a filter

A

the reloid

id

RLD

A

= (id

RLD

(Base(

A

))

)

|

A

.

Theorem

762

.

id

RLD

A

=

d

n

RLD

(Base(

A

);Base(

A

))

id

A

A

∈A

o

for every filter

A

.