Definition:Operator Generated by Ordered Subset

Definition

Let $L = \struct {X, \precsim}$ be an ordered set.

Let $S = \struct {T, \preceq}$ be an ordered subset of $L$.

The operator generated by ordered set $S$ is defined by

$\forall x \in X: \map {\map {\operatorname {operator} } S} x := \map {\inf_L} {x^\succeq \cap T}$

where $x^\succeq$ denotes the upper closure of $x$.

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 WAYBEL10:def 5