Definition:Directed Suprema Inheriting
Jump to navigation
Jump to search
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
Sources
- Mizar article WAYBEL_0:def 4