Definition:Finer Subset (Order Theory)

Definition

Let $L = \struct {S, \preceq}$ be a preordered set.

Let $X, Y$ be subsets of $S$.

Then $X$ is finer (subset) than $Y$ if and only if

$\forall x \in X: \exists y \in Y: x \preceq y$

Also See

• Definition:Coarser Subset (Order Theory)

Sources

• Mizar article YELLOW_4:def 1