CHAPTER 10

Product of funcoids over a filter

The following definition is inspired by the usual definition of Tychonoff product

of topological spaces.

Definition

2081

.

Let

f

be an indexed family of funcoids. Let

F

be a filter

on dom

f

.

a

[

F

]

Y

f

b

⇔ ∃

N

∈ F ∀

i

N

:

RLD

Pr

i

a

[

f

i

]

RLD

Pr

i

b

for atomic reloids

a

and

b

.

Remark

2082

.

We are especially interested in the special case when

F

is the

cofinite filter. In this case

a

h

Q

[

F

]

f

i

b

is defined by the condition that Pr

RLD

i

a

[

f

i

]

Pr

RLD

i

for an infinite number of indexes

i

.

Obvious

2083

.

a

h

Q

[

>

F

(dom

f

)

]

f

i

b

a

h

Q

(

A

)

f

i

b

.

Proposition

2084

.

¬

(

X

[

f

]

Y

) implies

¬

(

X

[

f

]

Y

) for some

X

up

X

,

Y

up

Y

.

Proof.

Suppose

¬

(

X

[

f

]

Y

). Then

Y  h

f

iX

. Thus by separability of core

for filters

Y

h

f

iX

for some

Y

up

Y

, that is

¬

(

X

[

f

]

Y

). Apply this result

twice.

Lemma

2085

.

X

Y

i

D

up

a

i

, Y

Y

i

D

up

b

i

x

Y

i

D

atoms

X

i

, y

Y

i

D

atoms

Y

i

N

∈ F ∀

j

N

:

x

j

[

f

j

]

y

j

implies

N

∈ F ∀

i

N

:

a

i

[

f

i

]

b

i

.

Proof.

Suppose for the contrary

¬

(

a

i

[

f

i

]

b

i

) for all

i

N

where

N

∈ F

(i.e.

for an infinite number of indexes if

F

is the cofinite filter). Then (lemma above)

there are

X

i

up

a

i

and

Y

i

up

b

i

such that

¬

(

X

i

[

f

j

]

Y

i

) for

i

N

. Thus

¬

(

x

i

[

f

i

]

y

i

) for

i

N

, contrary to the condition.

Proposition

2086

.

The funcoid

Q

[

F

]

f

exists.

Proof.

We need to prove that

X

up

a, Y

up

b

x

atoms

RLD

X, y

atoms

RLD

Y

:

x

(

A

2)

Y

f

y

implies

a

h

Q

[

F

]

f

i

b

.

Equivalently transforming it:

FiXme

: More detailed proof.

X

up

a, Y

up

b

x

atoms

RLD

X, y

atoms

RLD

Y

N

∈ F ∀

i

N

: Pr

RLD

i

x

[

f

i

] Pr

RLD

i

y

;

X

up

a, Y

up

b

x

Q

i

dom

f

atoms

RLD

X

i

, y

Q

i

dom

f

atoms

RLD

Y

i

N

∈ F ∀

i

N

:

x

i

[

f

i

]

y

i

;

35