Definition:Finite Infima Set
Jump to navigation
Jump to search
Definition
Let $P = \struct{S, \preceq}$ be an ordered set.
Let $X$ be a subset of $S$.
Then finite infima set of $X$, denoted $\map {\operatorname{fininfs}} X$, is defined by
- $\leftset {\inf A: A \in \map {\mathit{Fin}} X \land A}$ admits an infimum$\rightset{}$
where $\map {\mathit{Fin}} X$ denotes the set of all finite subsets of $X$.
Sources
- Mizar article WAYBEL_0:def 28