ThmDex – An index of mathematical definitions, results, and conjectures.
Finite intersection is a lower bound to each set in the intersection
Formulation 0
Let $E_1, \, \ldots, \, E_N$ each be a D11: Set such that
(i) $\bigcap_{n = 1}^N E_n$ is a D76: Set intersection for $E_1, \, \ldots, \, E_N$
Then \begin{equation} \bigcap_{n = 1}^N E_n \subseteq E_1, \quad \bigcap_{n = 1}^N E_n \subseteq E_2, \quad \ldots, \quad \bigcap_{n = 1}^N E_n \subseteq E_N \end{equation}
Formulation 1
Let $E_1, \, \ldots, \, E_N$ each be a D11: Set such that
(i) $\cap E$ is a D76: Set intersection for $E = (E_1, \, \ldots, \, E_N)$
Then \begin{equation} \cap E \subseteq E_1, \quad \cap E \subseteq E_2, \quad \ldots, \quad \cap E \subseteq E_N \end{equation}
Subresults
R4151: Binary intersection is a lower bound to each set in the intersection
Proofs
Proof 0
Let $E_1, \, \ldots, \, E_N$ each be a D11: Set such that
(i) $\bigcap_{n = 1}^N E_n$ is a D76: Set intersection for $E_1, \, \ldots, \, E_N$