Notes:Infimum

Definition problem

The actual definition:

1. $\forall a\in A[\text{inf}(A)\preceq a]$
2. $\forall x\in\underbrace{\{y\in X\ \vert\ \forall a\in A[y\preceq a]\} }_\text{the set of all lower bounds}[\text{inf}(A)\succeq x]$
   • Reformulation: $\forall x\in X[(\forall a\in A[x\preceq a])\implies \text{inf}(A)\succeq x]$

I claimed that definition (2) is the same as:

• $\forall x\in X\exists a\in A[x\succ\text{inf}(A)\implies a\prec x]$ - that anything larger than the infimum isn't a lower bound. This is not madness. Note the contrapositive:
  • $\forall x\in X\exists a\in A[x\preceq a\implies x\preceq\text{inf}(A)]$ - this looks VERY similar to point 2.