 1.11. UNUSUAL NOTATION

13

6

. If

x

f

, then the cardinality of

x

is strictly less than the cardinality of

f

.

1.9.2. Misc.

In this book quantifiers bind tightly. That is

x

A

:

P

(

x

)

Q

and

x

A

:

P

(

x

)

Q

should be read (

x

A

:

P

(

x

))

Q

and (

x

A

:

P

(

x

))

Q

not

x

A

: (

P

(

x

)

Q

) and

x

A

: (

P

(

x

)

Q

).

The set of functions from a set

A

to a set

B

is denoted as

B

A

.

I will often skip parentheses and write

f x

f

(

x

) to denote the result

of a function

f

acting on the argument

x

.

I will denote

h

f

i

X

=

n

β

im

f

α

X

:

αf β

o

(in other words

h

f

i

X

is the image of a

set

X

under a function or binary relation

f

) and

X

[

f

]

Y

⇔ ∃

x

X, y

Y

:

x f y

for sets

X

,

Y

and a binary relation

f

. (Note that functions are a special case of

binary relations.)

By just

h

f

i

and [

f

]

I will denote the corresponding function and relation on

small sets.

Obvious

2

.

For a function

f

we have

h

f

i

X

=

n

f

(

x

)

x

X

o

.

Definition

3

.

f

1

X

is called the

preimage

of a set

X

by a function (or,

more generally, a binary relation)

f

.

Obvious

4

.

{

α

}

[

f

]

{

β

} ⇔

α f β

for every

α

and

β

.

λx

D

:

f

(

x

) =

n

(

x,f

(

x

))

x

D

o

for a set

D

and and a form

f

depending on the

variable

x

. In other words,

λx

D

:

f

(

x

) is the function which maps elements

x

of

a set

D

into

f

(

x

).

I will denote source and destination of a morphism

f

of any category (See

chapter

2

for a definition of a category.) as Src

f

and Dst

f

correspondingly. Note

that below defined domain and image of a funcoid are not the same as its source

and destination.

I will denote GR(

A, B, f

) =

f

for any morphism (

A, B, f

) of either

Set

or

Rel

.

(See definitions of

Set

and

Rel

below.)

1.10. Implicit arguments

Some notation such that

A

,

>

A

,

t

A

,

u

A

have indexes (in these examples

A

).

We will omit these indexes when they can be restored from the context. For

example, having a function

f

:

A

B

where

A

,

B

are posets with least elements,

we will concisely denote

f

=

for

f

A

=

B

. (See below for definitions of these

operations.)

Note

5

.

In the above formula

f

=

we have the first

and the second

denoting different objects.

We will assume (skipping this in actual proofs) that all omitted indexes can be

restored from context. (Note that so called dependent type theory computer proof

assistants do this like we implicitly.)

1.11. Unusual notation

In the chapter

Common knowledge, part 1

” (which you may skip reading if

you are already knowledgeable) some non-standard notation is defined. I summarize

here this notation for the case if you choose to skip reading that chapter:

Partial order is denoted as

v

.

Meets and joins are denoted as

u

,

t

,

d

,

d

.

I call element

b

substractive

from an element

a

(of a distributive lattice

A

) when

the difference

a

\

b

exists. I call

b

complementive

to

a

when there exists

c

A

such