background image

8 Other new theorems

funcoids-are-lters.tm

funcoids-are-frame.tm

Theorem 19.

The set of funcoids is with separable core.

Proof.

Because lters on distributive lattices are with separable core.

Theorem 20.

The set of funcoids is with co-separable core.

[TODO: For pointfree funcoids?]

Proof.

Let

f ; g

2

FCD

(

A

;

B

)

and

f

t

g

= 1

. Then for every

X

2

P

A

we have

h

f

i

X

t h

g

i

X

= 1

,

Cor

h

f

i

X

t

Cor

h

g

i

X

= 1

, h

CoCompl

f

i

X

t h

CoCompl

g

i

X

= 1

:

Thus

h

CoCompl

f

t

CoCompl

g

i

X

= 1

;

f

t

g

= 1

)

CoCompl

f

t

CoCompl

g

= 1

:

(1)

Applying the dual of the formulas (

1

to the formula (

1

we get:

f

t

g

= 1

)

Compl CoCompl

f

t

Compl CoCompl

g

= 1

that is

f

t

g

= 1

)

Cor

f

t

Cor

g

= 1

. So

FCD

(

A

;

B

)

is with co-separable core.

[TODO: Say that

the ltrator of complete funcoids is also with co-separable core.]

Proposition 21.

Compl

FCD

(

A

;

B

)

and Compl

RLD

(

A

;

B

)

are co-brouwerian lattices.

Draw a triangural diagram of correspondence of Compl

FCD

(

A

;

B

)

and Compl

RLD

(

A

;

B

)

and

indexed families of lters.

Proposition 22.

Every semiltered ltrator is ltered.

[TODO: The reverse implication is

already proved.] [TODO: See also http://math.stackexchange.com/questions/1198368/a-question-
on-order-theory-an-ordered-set-and-its-subset]

Proof.

a

=

d

A

up

a

is equivalent to

a

is a greatest lower bound of up

a

. That is the implication

that

b

is lower bound of up

a

implies

a

w

b

.

b

is lower bound of up

a

implies up

b

up

a

. So as it is semiltered

a

w

b

.

8.1 Hyperfuncoids

Let

A

is an indexed family of sets.

Products

are

Q

A

for

A

2

Q

A

.

Hyperfuncoids

are lters

F

¡

on the lattice

¡

of all nite unions of products.

Problem 23.

Is

d

FCD

a bijection from hyperfuncoids

F

¡

to:

1. prestaroids on

A

;

2. staroids on

A

;

3. completary staroids on

A

?

If yes, is up

¡

dening the inverse bijection?

If not, characterize the image of the function

d

FCD

dened on

F

¡

.

8.2 Relationships between funcoids and reloids

Lemma 24.

If

a

,

b

,

c

are lters on powersets and

b

=

/ 0

, then

G

RLD

f

G

F

j

F

2

atoms

RLD

(

a

RLD

b

)

; G

2

atoms

RLD

(

b

RLD

c

)

g

=

a

RLD

c:

Other new theorems

5