Suprema Preserving Mapping on Ideals is Increasing
Jump to navigation
Jump to search
Theorem
Let $\struct {S, \preceq}$ and $\struct {T, \precsim}$ be ordered sets.
Let $f: S \to T$ be a mapping.
For every ideal $I$ in $\struct {S, \preceq}$, let $f$ preserve the supremum on $I$.
Then $f$ is increasing.
Proof
Let $x, y \in S$ such that:
- $x \preceq y$
- $\set x$ and $\set y$ admit suprema in $\struct {S, \preceq}$
By Supremum of Lower Closure of Set:
- $\set x^\preceq$ and $\set y^\preceq$ admit suprema in $\struct {S, \preceq}$
where $\set x^\preceq$ denotes the lower closure of $\set x$
By Lower Closure of Singleton:
- $x^\preceq$ and $y^\preceq$ admit suprema in $\struct {S, \preceq}$
By Lower Closure of Element is Ideal:
- $x^\preceq$ and $y^\preceq$ are ideals in $\struct {S, \preceq}$
By assumption and definition of mapping preserves the supremum on subset:
- $\map {f^\to} {x^\preceq}$ and $\map {f^\to} {y^\preceq}$ admit suprema in $\struct {T, \precsim}$
and:
- $\map \sup {\map {f^\to} {x^\preceq} } = \map f {\map \sup {x^\preceq} }$
and:
- $\map \sup {\map {f^\to} {y^\preceq} } = \map f {\map \sup {y^\preceq} }$
By Supremum of Lower Closure of Element:
- $\map \sup {x^\preceq} = x$ and $\map \sup {y^\preceq} = y$
By Lower Closure is Increasing:
- $x^\preceq \subseteq y^\preceq$
By Image of Subset under Mapping is Subset of Image:
- $\map {f^\to} {x^\preceq} \subseteq \map {f^\to} {y^\preceq}$
Thus by Supremum of Subset:
- $\map f x \precsim \map f y$
Thus by definition:
- $f$ is increasing.
$\blacksquare$
Sources
- 1980: G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M.W. Mislove and D.S. Scott: A Compendium of Continuous Lattices
- Mizar article WAYBEL_0:72