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$ if and only if:

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

if and only if

$y \in x^\succsim$ and $y \in S$ by definition of intersection

if and only if

$y \succsim x$ and $y \in S$ by definition of upper closure of element

if and only if

$x \subseteq y$ and $y \in S$ by definition of $\precsim$

if and only if

$y \in \set {I \in S: x \subseteq I}$

$\Box$

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$

$\Box$

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

$\blacksquare$

Sources

• 1980: G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M.W. Mislove and D.S. Scott: A Compendium of Continuous Lattices

• Mizar article WAYBEL13:7