Compact Element iff Existence of Finite Subset that Element equals Intersection and Includes Subset

== Theorem ==
Let $X, E$ be sets.
Let $P = \struct {\powerset X, \precsim}$ be an inclusion ordered set
where
:$\powerset X$ denotes the power set of $X$
:$\mathord \precsim = \mathord \subseteq \cap \paren {\powerset X \times \powerset X}$
Let $L = \struct {S, \preceq}$ be a continuous lattice subframe of $P$.
Then $E$ is compact element in $L$ :
:$\exists F \in \map {\mathit {Fin} } X: E = \bigcap \set {I \in S: F \subseteq I} \land F \subseteq E$
where $\map {\mathit {Fin} } X$ denotes the set of all finite subsets of $X$.
== Proof ==
By Power Set is Complete Lattice:
:$P$ is a complete lattice.
By Infima Inheriting Ordered Subset of Complete Lattice is Complete Lattice:
:$L$ is a complete lattice.
By Image of Operator Generated by Closure System is Set of Closure System:
:$\map {\operatorname {operator} } L \sqbrk {\powerset X} = S$
where $\map {\operatorname {operator} } L$ denotes the operator generated by $L$.
By Closure Operator Preserves Directed Suprema iff Image of Closure Operator Inherits Directed Suprema:
:$\map {\operatorname {operator} } L$ preserves directed suprema.
By Image of Compact Subset under Directed Suprema Preserving Closure Operator:
:$\map {\operatorname {operator} } L \sqbrk {\map K P} = \map K {\paren {\map {\operatorname {operator} } L \sqbrk {\powerset X}, \precsim'} }$
where $\map K P$ denotes the compact subset of $P$.
By Image of Operator Generated by Closure System is Set of Closure System:
::$ = \map K L$
=== Sufficient Condition ===
Assume that
:$E$ is compact element in $L$.
By definition of compact subset:
:$E \in \map K L$
By definition of image of set:
:$\exists x \in \map K P: E = \map {\map {\operatorname {operator} } L} x$
By definition of closure operator/inflationary:
:$x \precsim \map {\map {\operatorname {operator} } L} x$
By definition of $\precsim$:
:$x \subseteq E$
By definition of compact subset:
:$x$ is compact in $P$.
By Element is Finite iff Element is Compact in Lattice of Power Set:
:$x$ is finite.
we will prove that
:$x^\succsim \cap S = \set {I \in S: x \subseteq I}$
Let $y \in \powerset X$
:$y \in x^\succsim \cap S$
:$y \in x^\succsim$ and $y \in S$ by definition of intersection
:$y \succsim x$ and $y \in S$ by definition of upper closure of element
:$x \subseteq y$ and $y \in S$ by definition of $\precsim$
:$y \in \set {I \in S: x \subseteq I}$
By definition of operator genereted by ordered subset:
:$\map {\map {\operatorname {operator} } L} x = \map {\inf_P} {x^\succsim \cap S}$
By the proof of Power Set is Complete Lattice:
:$E = \bigcap \set {I \in S: x \subseteq I}$
Hence $\exists F \in \map {\mathit {Fin} } X: E = \bigcap \set {I \in S: F \subseteq I} \land F \subseteq E$
=== Necessary Condition ===
Assume that:
:$\exists F \in \map {\mathit {Fin} } X: E = \bigcap \set {I \in S: F \subseteq I} \land F \subseteq E$
By Element is Finite iff Element is Compact in Lattice of Power Set:
:$F$ is compact element in $P$,
By definition of compact subset:
:$F \in \map K P$
Then
:$F^\succsim \cap S = \set {I \in S: F \subseteq I}$
By definition of operator generated by ordered subset:
:$\map {\map {\operatorname {operator} } L} F = \map {\inf_P} {F^\succsim \cap S}$
By the proof of Power Set is Complete Lattice:
:$\map {\map {\operatorname {operator} } L} F = E$
By definition of image of set:
:$E \in \map K L$
Thus by definition of compact subset:
:$E$ is a compact element in $L$.
== Sources ==
* 
* 
Category:Join and Meet Semilattices
Category:Way Below Relation