Finite Infima Set of Coarser Subset is Coarser than Finite Infima Set

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $L = \left({S, \wedge, \preceq}\right)$ be a meet semilattice.

Let $A, B$ be subsets of $S$ such that

$A$ is coarser than $B$.


Then $\operatorname{fininfs} \left({A}\right)$ is coarser than $\operatorname{fininfs} \left({B}\right)$

where $\operatorname{fininfs} \left({B}\right)$ denotes the finite infima set of $B$.


Proof

Let $x \in \operatorname{fininfs} \left({A}\right)$

By definition of finite infima set:

$\exists Y \in \mathit{Fin}\left({A}\right): x = \inf Y$ and $Y$ admits an infimum,

where $\mathit{Fin}\left({A}\right)$ denotes the set of all finite subsets of $A$.

By definition of coarset subset:

$\forall y \in Y: \exists z \in B: z \preceq y$

By Axiom of Choice:

$\exists f:Y \to B: \forall y \in Y: f\left({y}\right) \preceq y$

We will prove that

$f\left[{Y}\right]$ admits an infimum.

In the case when $Y = \varnothing$:

By Image of Empty Set is Empty Set/Corollary:

$f\left[{Y}\right] = \varnothing$

Thus

$f\left[{Y}\right]$ admits an infimum.

In the case when $Y \ne \varnothing$

By definition of non-empty set:

$\exists y: y \in Y$

By definition of image of set:

$f\left({y}\right) \in f\left[{Y}\right]$

By Image of Mapping from Finite Set is Finite:

$f\left[{Y}\right]$ is a finite set.

Thus by Existence of Non-Empty Finite Infima in Meet Semilattice:

$f\left[{Y}\right]$ admits an infimum.

$\Box$

We will prove that

$\inf f\left[{Y}\right]$ is lower bound for $Y$.

Let $y \in Y$.

By definition of $f$:

$f\left({y}\right) \preceq y$

By definition of image of set:

$f\left({y}\right) \in f\left[{Y}\right]$

By definitions of infimum and lower bound:

$\inf f\left[{Y}\right] \preceq f\left({y}\right)$

Thus by definition of transitivity:

$\inf f\left[{Y}\right] \preceq y$

$\Box$

By definition of infimum:

$\inf f\left[{Y}\right] \preceq x$

By definition of finite infima set:

$\inf f\left[{Y}\right] \in \operatorname{fininfs} \left({B}\right)$

Thus

$\exists y \in \operatorname{fininfs} \left({B}\right): y \preceq x$

$\blacksquare$


Sources