Definition:Infima Inheriting
Jump to navigation
Jump to search
Definition
Let $L = \struct {S, \preceq}$ be an ordered set.
Let $R = \struct {T, \preceq'}$ be an ordered subset of $L$.
Then $R$ inherits infima of $L$ if and only if
- for all subsets $X$ of $T$ if $X$ admits an infimum of $L$, then
- $X$ admits an infimum of $R$ and $\inf_R X = \inf_L X$
Sources
- Mizar article YELLOW_0:def 18