 8.3. RELOIDAL PRODUCT OF FILTERS

186

Proof.

g

f

6

h

RLD

l

G

F

F

up

f, G

up

g

u

RLD

l

up

h

6

=

⊥ ⇔

RLD

l

(

G

F

)

u

RLD

H

F

up

f, G

up

g, H

up

h

6

=

⊥ ⇔

RLD

l

(

G

F

)

u

H

F

up

f, G

up

g, H

up

h

6

=

⊥ ⇔

F

up

f, G

up

g, H

up

h

:

RLD

((

G

F

)

u

H

)

6

=

⊥ ⇔

F

up

f, G

up

g, H

up

h

:

G

F

6

H

(used properties of generalized filter bases).

Similarly

g

6

h

f

1

⇔ ∀

F

up

f, G

up

g, H

up

h

:

G

6

H

F

1

.

Thus

g

f

6

h

g

6

h

f

1

because

G

F

6

H

G

6

H

F

1

by

proposition

283

.

Theorem

1010

.

For every composable reloids

f

and

g

1

.

g

f

=

d

n

g

F

F

atoms

f

o

.

2

.

g

f

=

d

n

G

f

G

atoms

g

o

.

Proof.

We will prove only the first as the second is dual.

Obviously

d

n

g

F

F

atoms

f

o

v

g

f

. We need to prove

d

n

g

F

F

atoms

f

o

w

g

f

.

Really,

l

g

F

F

atoms

f

w

g

f

x

RLD

(Src

f,

Dst

g

) :

x

6

g

f

x

6

l

g

F

F

atoms

f

x

RLD

(Src

f,

Dst

g

) : (

x

6

g

f

⇒ ∃

F

atoms

f

:

x

6

g

F

)

x

RLD

(Src

f,

Dst

g

) : (

g

1

x

6

f

⇒ ∃

F

atoms

f

:

g

1

x

6

F

)

what is obviously true.

Corollary

1011

.

If

f

and

g

are composable reloids, then

g

f

=

l

G

F

F

atoms

f, G

atoms

g

.

Proof.

g

f

=

d

F

atoms

f

(

g

F

) =

d

F

atoms

f

d

G

atoms

g

(

G

F

) =

d

n

G

F

F

atoms

f,G

atoms

g

o

.

8.3. Reloidal product of filters

Definition

1012

.

Reloidal product of filters

A

and

B

is defined by the formula

A ×

RLD

B

def

=

RLD

l

A

×

B

A

up

A

, B

up

B

.

Obvious

1013

.

• ↑

U

A

×

RLD

V

B

=

RLD

(

U,V

)

(

A

×

B

) for every sets

A

U

,

B

V

.

• ↑

A

×

RLD

B

=

RLD

(

A

×

B

) for every typed sets

A

,

B

.