Definition:Finite Suprema 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 suprema set of $X$, denoted $\map {\mathrm {finsups} } X$, is defined by:
- $\leftset {\sup A: A \in \map {\mathit {Fin} } X \land A}$ admits a supremum$\rightset{}$
where $\map {\mathit {Fin} } X$ denotes the set of all finite subsets of $X$.
Sources
- Mizar article WAYBEL_0:def 27