# Elegance of mathematical definitions

As I was working my way through “How To Prove It” by Daniel Velleman, I came across this definition in section 4.4 Ordering Relations:

Definition 4.4.4. Suppose R is a partial order on a set A, B A, and b B. Then b is called an R-smallest element of B (or just a smallest element if R is clear from the context) if x B(bRx). It is called an R-minimal element (or just a minimal element) if ¬∃x B(x Rb x ̸= b).

The definition for R-smallest element was intuitive to me, all it says is that for all x in B, b <= x, i.e. b is smaller than any element in B given all of them are comparable.

The definition for R-minimal was a little trickier to me. Later in the book it’s shown that it’s equivalent to x B(x Rb x = bwhich is a bit easier to grasp, but still was not intuitive to me.

So the R-minimal is similar to R-smallest one, with the difference that it only applies to comparable elements, and uses xRb instead of bRx.

Given my programming background, I tried to come up with a more intuitive definition:
…b is called an R-minimal element if:
∀x, y ∈ B:
1. b R x (b <= x)
2. y R x (y <= x)
3. b R y or y R b (b <= y or y <= b, i.e. b and y are comparable)
Imply
b R y (b <= y)
This says that for any elements x and y, b will always be lower than those, given they are comparable.

This definition, although a bit larger than the original (elegant) one, made things clearer for me. But how can I verify if this definition is really equivalent to the original one? I tried to come up with a proof and had amnn from #haskell freenode to verify it for me (thanks!). Here’s the proof:

`I. b is R-minimal if ∀x ∈ B: x R b → x = bII. b is R-minimal if ∀x, y ∈ B: b R x ∧ y R x ∧ (b R y ∨ y R b) → b R yR partial order: reflexive, antisymmetric, transitive.Prove (or disprove) that I ↔ II.(→): Suppose ∀x ∈ B: x R b → x = b.Further suppose that y, z are arbitrary in B: b R y ∧ z R y ∧ (b R z ∨ z R b).Prove that b R z.Proof:Case b R z: Holds trivially.Case z R b: z = b → b R z.(←): Suppose ∀x, y ∈ B: b R x ∧ y R x ∧ (b R y ∨ y R b) -> b R y.Further suppose z is arbitrary in B: z R b.Prove that z = b.Proof:Using universal instantiation, let x = b, y = z: b R b ∧ (z R b ∨ b R z) → b R z.So given R is partial order (reflexive) we have b R b and we also have z R b from the givens.With this, we can conclude b R z.So since R is a partial order and thus antisymmetric,from b R z and z R b we can conclude that b = z.`

After spending some more time on thinking about the original definition, it is quite simple actually, because all it says that nothing is smaller than b. This definition is elegant in my opinion, because it “says” so much stuff with a few simple symbols. It is what inspired me to write this post.