# Complete lattice generated by a partitioning of a lattice element

In this post I defined strong partitioning of an element of a complete lattice. For me it was seeming obvious that the complete lattice generated by the set $S$ where $S$ is a strong partitioning is equal to $\left\{ \bigcup{}^{\mathfrak{A}}X | X\in\mathscr{P}S \right\}$. But when I actually tried to write down the proof of this statement I found that it is not obvious to prove. So I present this to you as a conjecture:

Conjecture The complete lattice generated by a strong partitioning $S$ of an element of a complete lattice $\mathfrak{A}$ is equal to $\left\{ \bigcup{}^{\mathfrak{A}}X | X\in\mathscr{P}S \right\}$.

Proposition Provided that this conjecture is true, we can prove that the complete lattice $[S]$ generated by a strong partitioning $S$ of an element of a complete lattice is a complete atomic boolean lattice with the set of its atoms being $S$ (Note: So $[S]$ is completely distributive).

Proof Completeness of $[S]$ is obvious. Let $A\in[S]$. Then exists $X\in\mathscr{P}S$ such that $A=\bigcup{}^{\mathfrak{A}}X$. Let $B=\bigcup{}^{\mathfrak{A}}(S\setminus X)$. Then $B\in[S]$ and $A\cap B=0$. $A\cup B=\bigcup{}^{\mathfrak{A}}S$ is the biggest element of $[S]$. So we have proved that $[S]$ is a boolean lattice.

Now let prove that $[S]$ is atomic with the set of atoms being $S$. Let $z\in S$ and $A\in[S]$. If $A\neq z$ then either $A=0$ or $x\in X$ where $A=\bigcup^{\mathfrak{A}}X$, $X\in\mathscr{P}S$ and $x\neq z$. Because $S$ is a strong partitioning, $\bigcup^{\mathfrak{A}}(X\setminus\{z\})\cap^{\mathfrak{A}}z=0$ and $\bigcup^{\mathfrak{A}}(X\setminus\{z\})\neq 0$. So $A=\bigcup^{\mathfrak{A}}X=\bigcup^{\mathfrak{A}}(X\setminus\{z\})\cup^{\mathfrak{A}}z\nsubseteq z$.

Finally we will prove that elements of $[S]\setminus S$ are not atoms. Let $A\in[S]\setminus S$ and $A\neq 0$. Then $A\supseteq x\cup^{\mathfrak{A}}y$ where $x,y\in S$ and $x\neq y$. If $A$ is an atom then $A=x=y$ what is impossible. QED

The above conjecture as a step to solution to the original conjecture may also be considered for the polymath research problem. Or maybe we should research both these two problems in a single polymath set, as the solution of one of them may inspire the solution of the other of these two problems.