Talk:Infimum

Problem with second part of definition

Strangely I considered this problem solved as I deleted this talk page afterwards....
An infimum or greatest lower bound (AKA: g.l.b) of a subset [ilmath]A\subseteq X[/ilmath] of a poset [ilmath](X,\preceq)[/ilmath], which we denote: [ilmath]\text{inf}(A)[/ilmath] is a value {{M|\in X} such that:

1. [ilmath]\forall a\in A[\text{inf}(A)\le a][/ilmath] (that [ilmath]\text{inf}(A)[/ilmath] is a lower bound)
2. [ilmath]\forall x\in\underbrace{\{y\in X\ \vert\ \forall a\in A[y\le a]\} }_{\text{The set of all lower bounds} }\ \ [\text{inf}(A)\ge x][/ilmath] (that [ilmath]\text{inf}(A)[/ilmath] is an upper bound of all lower bounds of [ilmath]A[/ilmath])

However I have always thought of (rather than condition (2) above):

• condition 1 and [ilmath]\forall x\in X\exists a\in A[x>\text{inf}(A)\implies a<x][/ilmath]

I believe this is equivalent, that is:

• [ilmath]\forall x\in X\exists a\in A[x>\text{inf}(A)\implies a<x]\iff\forall x\in\underbrace{\{y\in X\ \vert\ \forall a\in A[y\le a]\} }_{\text{The set of all lower bounds} }\ \ [\text{inf}(A)\ge x][/ilmath]

First note:

• [ilmath]\forall x\in\underbrace{\{y\in X\ \vert\ \forall a\in A[y\le a]\} }_{\text{The set of all lower bounds} }\ \ [\text{inf}(A)\ge x]\iff\forall x\in X\left[\left(\forall a\in A[x\le a]\right)\implies x\le\text{inf}(A)\right][/ilmath]

Then note that for the statement:

• [ilmath]\Big[(\forall a\in A[x\le a])\implies x\le\text{inf}(A)\Big]\iff\Big[x>\text{inf}(A)\implies(\exists a\in A[x>a])\Big][/ilmath] (by contrapositive), so condition two is simply:
  • [ilmath]\forall x\in X[x>\text{inf}(A)\implies(\exists a\in A[x>a])][/ilmath], this is a stone's throw away from [ilmath]\forall x\in X\exists a\in A[x>\text{inf}(A)\implies a<x][/ilmath].

Claim:

[ilmath]\Big(\forall x\in X[x>\text{inf}(A)\implies(\exists a\in A[x>a])]\Big)\iff\Big(\forall x\in X\exists a\in A[x>\text{inf}(A)\implies a<x]\Big)[/ilmath]. Warning:(Workings below show this to be false)

LHS [ilmath]\implies[/ilmath] RHS:

• Let [ilmath]x\in X[/ilmath] be given.
  • If [ilmath]x\le\text{inf}(A)[/ilmath] then pick any [ilmath]a\in A[/ilmath], as the LHS of the implication is false, we don't care about the right. Warning:This CLEARLY requires that [ilmath]A\ne\emptyset[/ilmath], which the LHS of the claim does not!
  • If [ilmath]x>\text{inf}(A)[/ilmath] then by hypothesis it is true that "[ilmath]\exists a\in A[x>a][/ilmath]" - pick that [ilmath]a\in A[/ilmath] and the result follows.

RHS [ilmath]\implies[/ilmath] LHS:

• Let [ilmath]x\in X[/ilmath] be given.
  • If [ilmath]x\le\text{inf}(A)[/ilmath] we do not care about the truth or falseness of [ilmath]\exists a\in A[x>a][/ilmath] - so there may or may not [ilmath]\exists a\in A[/ilmath] (at all!) let alone one [ilmath]<x[/ilmath] This confirms the above warning
  • If [ilmath]x>\text{inf}(A)[/ilmath] then by hypothesis [ilmath]\exists a<x[/ilmath] and we're done.

Correct claim:

[ilmath]\Big(\forall x\in X\exists a\in A[x>\text{inf}(A)\implies a<x]\Big)\implies\Big(\forall x\in X[x>\text{inf}(A)\implies(\exists a\in A[x>a])]\Big)[/ilmath] or

If [ilmath]A\ne\emptyset[/ilmath]: [ilmath]\Big(\forall x\in X\exists a\in A[x>\text{inf}(A)\implies a<x]\Big)\implies\Big(\forall x\in X[x>\text{inf}(A)\implies(\exists a\in A[x>a])]\Big)[/ilmath]

• Which may be said as: [ilmath]\exists \varphi\in A\Big[\Big(\forall x\in X\exists a\in A[x>\text{inf}(A)\implies a<x]\Big)\iff\Big(\forall x\in X[x>\text{inf}(A)\implies(\exists a\in A[x>a])]\Big)\Big][/ilmath]

This is an interesting exercise in first-order-logic and shows the importance of being careful!