Superset of Order Generating is Order Generating

Theorem

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a complete lattice.

Let $X, Y$ be subsets of $S$ such that

$X$ is order generating

and

$X \subseteq Y$

Then $Y$ is order generating.

Proof

Let $x \in S$.

Thus by definition of complete lattice:

$x^\succeq \cap Y$ admits an infimum.

By definition of complete lattice:

$x^\succeq$ admits an infimum

and

$x^\succeq \cap X$ admits an infimum.

By Intersection is Subset:

$x^\succeq \cap Y \subseteq x^\succeq$

By Infimum of Subset:

$\map \inf {x^\succeq} \preceq \map \inf {x^\succeq \cap Y}$

By Infimum of Upper Closure of Element:

$x \preceq \map \inf {x^\succeq \cap Y}$

By Set Intersection Preserves Subsets/Corollary:

$x^\succeq \cap X \subseteq x^\succeq \cap Y$

By Infimum of Subset:

$\map \inf {x^\succeq \cap Y} \preceq \map \inf {x^\succeq \cap X}$

By definition of order generating:

$\map \inf {x^\succeq \cap Y} \preceq x$

Thus by definition of antisymmetry:

$x = \map \inf {x^\succeq \cap Y}$

$\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 WAYBEL_6:19