Notes:Infimum

Definition problem

The actual definition:

1. [ilmath]\forall a\in A[\text{inf}(A)\preceq a][/ilmath]
2. [ilmath]\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][/ilmath]
   • Reformulation: [ilmath]\forall x\in X[(\forall a\in A[x\preceq a])\implies \text{inf}(A)\succeq x][/ilmath]

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

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