Funcoid bases/Reduce to meets of applying funcoids to ultrafilters

From Virtual scientific conference
Revision as of 18:30, 11 April 2017 by Victor Porton (talk | contribs) (Created page with "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...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

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$.

The below is a chain of equalities attempting the proof:

$\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$