Definition A set $latex S$ of binary relations is a base of a funcoid $latex f$ when all elements of $latex S$ are above $latex f$ and $latex \forall X \in \mathrm{up}\, f \exists T \in S : T \sqsubseteq X$.
It was easy to show:
Proposition A set $latex S$ of binary relations is a base of a funcoid iff it is a base of $latex \bigsqcap^{\mathsf{FCD}} S$.
Today I’ve proved the following important theorem:
Theorem If $latex S$ is a filter base on the set of funcoids then $latex S$ is a base of $latex \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.
1 thought on “A new theorem proved”