background image

7.10. FUNCOIDAL PRODUCT OF FILTERS

165

Corollary

885

.

f

|

A

=

f

u

(

A ×

FCD

>

F

(Dst

f

)

) for every funcoid

f

and

A ∈

F

(Src

f

).

Proof.

f

u

(

A ×

FCD

>

F

(Dst

f

)

) = id

FCD

>

F

(Dst

f

)

f

id

FCD

A

=

f

id

FCD

A

=

f

|

A

.

Corollary

886

.

f

6 A ×

FCD

B ⇔ A

[

f

]

B

for every funcoid

f

and

A ∈

F

(Src

f

),

B ∈

F

(Dst

f

).

Proof.

f

6 A ×

FCD

B ⇔

f

u

(

A ×

FCD

B

)

> 6

=

⊥ ⇔

D

id

FCD

B

f

id

FCD

A

E

> 6

=

⊥ ⇔

D

id

FCD

B

E

h

f

i

D

id

FCD

A

E

> 6

=

⊥ ⇔

B u h

f

i

(

A u >

)

6

=

⊥ ⇔

B u h

f

iA 6

=

⊥ ⇔

A

[

f

]

B

.

Corollary

887

.

Every filtrator of funcoids is star-separable.

Proof.

The set of funcoidal products of principal filters is a separation subset

of the lattice of funcoids.

Theorem

888

.

Let

A

,

B

be sets. If

S

P

(

F

(

A

)

×

F

(

B

)) then

l

(

A

,

B

)

S

(

A ×

FCD

B

) =

l

dom

S

×

FCD

l

im

S.

Proof.

If

x

atoms

F

(

A

)

then by theorem

875

*

l

(

A

,

B

)

S

(

A ×

FCD

B

)

+

x

=

l

(

A

,

B

)

S

A ×

FCD

B

x.

If

x

6

d

dom

S

then

(

A

,

B

)

S

: (

x

u A 6

=

⊥ ∧

A ×

FCD

B

x

=

B

);

A ×

FCD

B

x

(

A

,

B

)

S

)

= im

S

;

if

x

d

dom

S

then

(

A

,

B

)

S

: (

x

u A

=

⊥ ∧

A ×

FCD

B

x

=

);

A ×

FCD

B

x

(

A

,

B

)

S

)

3 ⊥

.

So

*

l

(

A

,

B

)

S

(

A ×

FCD

B

)

+

x

=

(

d

im

S

if

x

6

d

dom

S

F

(

B

)

if

x

d

dom

S.

From this the statement of the theorem follows.

Corollary

889

.

For every

A

0

,

A

1

F

(

A

),

B

0

,

B

1

F

(

B

) (for every sets

A

,

B

)

(

A

0

×

FCD

B

0

)

u

(

A

1

×

FCD

B

1

) = (

A

0

u A

1

)

×

FCD

(

B

0

u B

1

)

.