Lower Bound is Lower Bound for Subset
Jump to navigation
Jump to search
Theorem
Let $\struct {S, \preceq}$ be a preordered set.
Let $A, B$ be subsets of $S$ such that
- $B \subseteq A$
Let $L$ be an element of $S$.
Let $L$ be a lower bound for $A$.
Then $L$ is a lower bound for $B$.
Proof
Let $L$ be a lower bound for $A$.
By definition of lower bound:
- $\forall x \in A: L \preceq x$
By definition of subset:
- $\forall x \in B: x \in A$
Hence:
- $\forall x \in B: L \preceq x$
Thus by definition:
- $L$ is a lower bound for $B$.
$\blacksquare$
Sources
- Mizar article YELLOW_0:9