Definition:Directed Suprema Inheriting

Definition

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

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

Then $S$ inherits directed suprema if and only if

for all directed subsets $A$ of $Y$: if $A$ admits a supremum in $L$, then $\sup_L A \in Y$

Also see

• Supremum in Ordered Subset

Sources

• Mizar article WAYBEL_0:def 4