background image

Proof.

g

f

/

h

,

9

a

2

atoms

F

(

A

)

; c

2

atoms

F

(

C

)

:

a

[(

g

f

)

u

h

]

c

,

9

a

2

atoms

F

(

A

)

; c

2

atoms

F

(

C

)

: (

a

[

g

f

]

c

^

a

[

h

]

c

)

,

9

a

2

atoms

F

(

A

)

; b

2

atoms

F

(

B

)

; c

2

atoms

F

(

C

)

: (

a

[

f

]

b

^

b

[

g

]

c

^

a

[

h

]

c

)

,

9

b

2

atoms

F

(

B

)

; c

2

atoms

F

(

C

)

: (

b

[

g

]

c

^

b

[

h

f

¡

1

]

c

)

,

9

b

2

atoms

F

(

B

)

; c

2

atoms

F

(

C

)

:

b

[

g

u

(

h

f

¡

1

)]

c

,

g

/

h

f

¡

1

:

6.9 Direct product of lters

A generalization of Cartesian product of two sets is funcoidal product of two lters:

Denition 6.71.

Funcoidal product

of lters

A

and

B

is such a funcoid

FCD

B 2

FCD

(

Base

(

A

);

Base

(

B

))

that for every

X 2

F

(

Base

(

A

))

,

Y 2

F

(

Base

(

B

))

X

[

FCD

B

]

Y , X 

/

A ^ Y 

/

B

:

Proposition 6.72.

FCD

B

is really a funcoid and

hA 

FCD

BiX

=

(

B

if

/

A

0

F

(

Base

(

B

))

if

X  A

:

Proof.

Obvious.

Obvious 6.73.

"

FCD

(

U

;

V

)

(

A

B

) =

"

U

A

FCD

"

V

B

for sets

A

U

and

B

V

.

Proposition 6.74.

f

v A 

FCD

B ,

dom

f

v A ^

im

f

v B

for every

f

2

FCD

(

A

;

B

)

and

A 2

F

(

A

)

,

B 2

F

(

B

)

.

Proof.

If

f

v A 

FCD

B

then dom

f

v

dom

(

FCD

B

)

v A

, im

f

v

im

(

FCD

B

)

v B

. If

dom

f

v A ^

im

f

v B

then

8X 2

F

(

A

)

;

Y 2

F

(

B

):

¡

X

[

f

]

Y ) X u A

=

/ 0

F

(

A

)

^ Y u B

=

/ 0

F

(

B

)

;

consequently

f

v A 

FCD

B

.

The following theorem gives a formula for calculating an important particular case of a meet

on the lattice of funcoids:

Theorem 6.75.

f

u

(

FCD

B

) =

id

B

FCD

f

id

A

FCD

for every funcoid

f

and

A 2

F

(

Src

f

)

,

B 2

F

(

Dst

f

)

.

Proof.

h

=

def

id

B

FCD

f

id

A

FCD

. For every

X 2

F

(

Src

f

)

h

h

iX

=

h

id

B

FCD

ih

f

ih

id

A

FCD

iX

=

B u h

f

i

(

A u X

)

:

From this, as easy to show,

h

v

f

and

h

v A 

FCD

B

. If

g

v

f

^

g

v A 

FCD

B

for a

g

2

FCD

(

Src

f

;

Dst

f

)

then dom

g

v A

, im

g

v B

,

h

g

iX

=

B u h

g

i

(

A u X

)

v B u h

f

i

(

A u X

) =

h

id

B

FCD

ih

f

ih

id

A

FCD

iX

=

h

h

iX

;

g

v

h

. So

h

=

f

u

(

FCD

B

)

.

Corollary 6.76.

f

j

A

=

f

u

¡

FCD

1

F

(

Dst

f

)

for every funcoid

f

and

A 2

F

(

Src

f

)

.

6.9 Direct product of filters

107