A new theorem proved

Definition A set S of binary relations is a base of a funcoid f when all elements of S are above f and \forall X \in \mathrm{up}\, f \exists T \in S : T \sqsubseteq X.

It was easy to show:

Proposition A set S of binary relations is a base of a funcoid iff it is a base of \bigsqcap^{\mathsf{FCD}} S.

Today I’ve proved the following important theorem:

Theorem If S is a filter base on the set of funcoids then S is a base of \bigsqcap^{\mathsf{FCD}} S.

The proof is currently located in this PDF file.

It is yet unknown whether the converse theorem holds, that is whether every base of a funcoid is a filter base on the set of funcoids.

One comment

Leave a Reply