background image

CHAPTER 6

Interior funcoids

Having a funcoid

f

let define

interior funcoid

f

.

Definition

2217

.

Let

f

FCD

(

A, B

) =

pFCD

(

T

A,

T

B

) be a co-complete

funcoid. Then

f

pFCD

(dual

T

A,

dual

T

B

) is defined by the formula

h

f

i

X

=

h

f

i

X

.

Proposition

2218

.

Pointfree funcoid

f

exists and is unique.

Proof.

X

7→ h

f

i

X

is a component of pointfree funcoid dual

T

A

dual

T

B

iff

h

f

i

is a component of the corresponding pointfree funcoid

T

A

T

B

that is

essentially component of the corresponding funcoid

FCD

(

A, B

) what holds for a

unique funcoid.

It can be also defined for arbitrary funcoids by the formula

f

= (CoCompl

f

)

.

Obvious

2219

.

f

is co-complete.

Theorem

2220

.

The following values are pairwise equal for a co-complete

funcoid

f

and

X

T

Src

f

:

1

.

h

f

i

X

;

2

.

n

y

Dst

f

h

f

1

i

{

y

}v

X

o

3

.

d

n

Y

T

Dst

f

h

f

1

i

Y

v

X

o

4

.

d

n

Y∈

F

Dst

f

h

f

1

iYv

X

o

Proof.

1

=

2

.

n

y

Dst

f

h

f

1

i

{

y

}v

X

o

=

n

x

Dst

f

h

f

1

i

{

x

}

X

o

=

n

x

Dst

f

{

x

}h

f

i

X

o

=

h

f

i

X

=

h

f

i

X

.

2

=

3

If

f

1

Y

v

X

then (by completeness of

f

1

)

Y

=

n

y

Y

h

f

1

i

{

y

}v

X

o

and

thus

l

Y

T

Dst

f

h

f

1

i

Y

v

X

v

y

Dst

f

h

f

1

i

{

y

} v

X

.

The reverse inequality is obvious.

3

=

4

It’s enough to prove that if

f

1

Y v

X

for

Y ∈

F

Dst

f

then exists

Y

up

Y

such that

h

f

1

i

Y

v

X

.

Really let

f

1

Y v

X

.

Then

d

hh

f

1

i

i

up

Y v

X

and thus exists

Y

up

Y

such that

h

f

1

i

Y

v

X

by properties of generalized filter bases.

This coincides with the customary definition of interior in topological spaces.

Proposition

2221

.

f

◦◦

=

f

for every funcoid

f

.

Proof.

h

f

◦◦

i

X

=

¬¬h

f

i¬¬

X

=

h

f

i

X

.

Proposition

2222

.

Let

g

FCD

(

A, B

),

f

FCD

(

B, C

),

h

FCD

(

A, C

) for

some sets

A

.

B

,

C

.

g

v

f

h

f

1

g

v

h

, provided

f

and

h

are co-complete.

38