# Funcoid bases/Reduce to meets of applying funcoids to ultrafilters

The idea behind this attempted proof is to reduce behavior of funcoids $\langle f\rangle$ with better known behavior of filters $\langle f\rangle x$ for an arbitrary ultrafilter $x$ (I remind that knowing $\langle f\rangle x$ for all ultrafilters $x$ on the domain, it's possible to restore funcoid $f$) and then to replace $\langle X_0 \sqcap^{\mathsf{FCD}} \ldots \sqcap^{\mathsf{FCD}} X_n\rangle x$ with $\langle X_0 \rangle x \sqcap \dots \sqcap \langle X_n \rangle x$.

Let's assume $\forall X, Y \in S : \operatorname{up} (X \sqcap^{\mathsf{FCD}} Y) \subseteq S$.

Prove the conclusion by induction:

For $n = 1$ the theorem takes form $\operatorname{up} (X) \subseteq S$ what follows from $\operatorname{up} (X \sqcap^{\mathsf{FCD}} X) \subseteq S$.

Let the theorem holds for $n - 1$.

The below is my attempted proof (trying to reduce the statement for $n$ to the statement for $n-1$):

Let $X_i\in S$. We need to prove for every binary relations $Q \in \operatorname{up} (X_0 \sqcap^{\mathsf{FCD}} \ldots \sqcap^{\mathsf{FCD}} X_n)$ that is for every ultrafilter $x$ we have $\langle Q \rangle x \sqsupseteq \langle X_0 \rangle x \sqcap \ldots \sqcap \langle X_n \rangle x$ that is $\operatorname{up} \langle Q \rangle x \subseteq \left\{ K_0 \sqcap \ldots \sqcap K_n \mid \forall i : K_i \in \operatorname{up} \langle X_i \rangle x \right\}$ that $Q \in S$.

The below is a chain of equalities attempting the proof:

$\operatorname{up} \langle Q \rangle x \subseteq \left\{ K_0 \sqcap \ldots \sqcap K_n \mid \forall i : K_i \in \operatorname{up} \langle X_i \rangle x \right\} = \\ \left\{ P \sqcap K_n \mid P \in \operatorname{up} (\langle X_0 \rangle x \sqcap \ldots \sqcap \langle X_{n - 1} \rangle x) \wedge K_n \in \operatorname{up} \langle X_n \rangle x \right\} = \\ \left\{ P \sqcap K_n \mid P \in \operatorname{up} \langle X_0 \sqcap^{\mathsf{FCD}} \ldots \sqcap^{\mathsf{FCD}} X_{n - 1} \rangle x \wedge K_n \in \operatorname{up} \langle X_n \rangle x \right\} = \\ \left\{ P \sqcap K_n \mid K \in \operatorname{up} (X_0 \sqcap^{\mathsf{FCD}} \ldots \sqcap^{\mathsf{FCD}} X_{n - 1}), P \in \operatorname{up} \langle K \rangle x \wedge K_n \in \operatorname{up} \langle X_n \rangle x \right\} = \\ \bigcup_{K \in \operatorname{up} (X_0 \sqcap^{\mathsf{FCD}} \ldots \sqcap^{\mathsf{FCD}} X_{n - 1})} \left\{ P \sqcap K_n \mid P \in \operatorname{up} \langle K \rangle x \wedge K_n \in \operatorname{up} \langle X_n \rangle x \right\} = \\ \bigcup_{K \in \operatorname{up} (X_0 \sqcap^{\mathsf{FCD}} \ldots \sqcap^{\mathsf{FCD}} X_{n - 1})} \operatorname{up} (\langle K \rangle x \sqcap \langle X_n \rangle x) = \\ \bigcup_{K \in \operatorname{up} (X_0 \sqcap^{\mathsf{FCD}} \ldots \sqcap^{\mathsf{FCD}} X_{n - 1})} \operatorname{up} \langle K \sqcap^{\mathsf{FCD}} X_n \rangle x \subseteq \bigcup_{K \in \operatorname{up} (X_0 \sqcap^{\mathsf{FCD}} \ldots \sqcap^{\mathsf{FCD}} X_{n - 1})} Q_K$

because $\langle K \rangle x \sqcap \langle X_n \rangle x = \langle K \sqcap^{\mathsf{FCD}} X_n \rangle x \sqsupseteq Q_K$ for $Q_K \in S$

The remaining attempt to prove our conjecture is stalled.

The proof above uses the following lemma:

Lemma For every funcoid $f$ and filter $\mathcal{X} \in \mathscr{F} (\operatorname{Src} f)$ $$\operatorname{up} \langle f \rangle \mathcal{X} = \bigcup_{F \in \operatorname{up} f} \operatorname{up} \langle F \rangle \mathcal{X} = \left\{ K \in \operatorname{up} \langle F \rangle \mathcal{X} \mid F \in \operatorname{up} f \right\} .$$

Proof $\bigcup_{F \in \operatorname{up} f} \operatorname{up} \langle F \rangle \mathcal{X} = \left\{ K \in \operatorname{up} \langle F \rangle \mathcal{X} \mid F \in \operatorname{up} f \right\}$ is obvious.

$\bigcup_{F \in \operatorname{up} f} \operatorname{up} \langle F \rangle \mathcal{X} \subseteq \operatorname{up} \langle f \rangle \mathcal{X}$ is obvious.

Let $G \in \operatorname{up} \langle f \rangle \mathcal{X}$. Then $G \in \operatorname{up} \bigwedge_{X \in \operatorname{up} \mathcal{X}} \langle f \rangle X$. By properties of generalized filter bases, there is an $X \in \operatorname{up} \mathcal{X}$ such that $G \sqsupseteq \langle f \rangle X$. Then $G \sqsupseteq \left\langle \left( \overline{X} \times^{\mathsf{FCD}} \top \right) \sqcup (X \times^{\mathsf{FCD}} G) \right\rangle X$.

So $G \in \operatorname{up} \langle F \rangle \mathcal{X}$ where $F = \left( \overline{X} \times^{\mathsf{FCD}} \top \right) \sqcup (X \times^{\mathsf{FCD}} G)$ and thus $F \in \operatorname{up} f$. Thus $G \in \bigcup_{F \in \operatorname{up} f} \operatorname{up} \langle F \rangle \mathcal{X}$.