Publish here. Donate

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

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
The idea behind this 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$.
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 $\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 \sqsupseteq \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$.
$\operatorname{up} \langle Q \rangle x \sqsupseteq \left\{ K_0 \sqcap \ldots \sqcap K_n \hspace{1em} | \hspace{1em} \forall i : K_i \in \operatorname{up} \langle X_i \rangle x \right\} = \left\{ P \sqcap K_n \hspace{1em} | \hspace{1em} 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 \hspace{1em} | \hspace{1em} 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 \hspace{1em} | \hspace{1em} 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$