ThmDex – An index of mathematical definitions, results, and conjectures.
Result R1110 on D668: Maximum element
Isotonicity of maximum
Also known as
Monotonicity of maximum
Proofs
Proof 0
Let $P = (X, {\preceq})$ be a D1103: Partially ordered set.
Let $\mathsf{Max} = \mathsf{Max}(P)$ be the D4461: Set of internally upper-bounded sets in $P$.
Let $E, F \in \mathsf{Max}$ such that $E \subseteq F$. Denote $n : = \max(E)$ and $m : = \max(F)$. Now $x \preceq n$ for every $x \in E$ and $y \preceq m$ for every $y \in F$. Since $E$ is contained in $F$, then particularly $x \preceq m$ for every $x \in E$. Since $n \in E$, this implies that $n \preceq m$. $\square$