ThmDex – An index of mathematical definitions, results, and conjectures.
Result R1120 on D667: Minimum element
Antitonicity of minimum
Formulation 0
Let $P = (X, {\preceq})$ be a D1103: Partially ordered set.
Let $\mathsf{Min} = \mathsf{Min}(P)$ be the D4459: Set of internally lower-bounded sets in $P$.
Then \begin{equation} \forall \, E, F \in \mathsf{Min} \, (E \subseteq F \quad \Rightarrow \quad \min(E) \succeq \min(F)) \end{equation}
Proofs
Proof 0
Let $P = (X, {\preceq})$ be a D1103: Partially ordered set.
Let $\mathsf{Min} = \mathsf{Min}(P)$ be the D4459: Set of internally lower-bounded sets in $P$.
Let $E, F \in \mathsf{Min}$ such that $E \subseteq F$. Denote $n : = \min(E)$ and $m : = \min(F)$. Now $n \preceq x$ for every $x \in E$ and $m \preceq y$ for every $y \in F$. Since $E$ is contained in $F$, then particularly $m \preceq x$ for every $x \in E$. Since $n \in E$, this implies that $m \preceq n$. $\square$