Formalizing problems

This is a TIL post. The problem was disguised as a simple inequality exercise in Norman L Biggs' Discrete Mathematics book.

So here's the deal:

Problem: Prove that in a square matrix, the least of the greatest valued members of each row is greater or equal to greatest of the least value members of a each column. (For convenience, I have assumed the matrix consists of only natural numbers)

Formalizing: 

With some help from math.stackexchange.com, I was able to formalize this as:

Prove that Min_y(Max_xf(x,y)) >= Max_x(Min_yf(x,y)) where f(x,y) is basically any value in the matrix and x and y refers to the row and column respectively.

Proof:

Let's break it down. From general definitions of Min and Max, we know that:

f(x,y) >= Min(f(x,y))

and

Max(x,y) >= f(x,y) - (I)

So, it simply boils down to proving the statement:

Max_xf(x, y) >= Min_yf(x, y)

Let x_o be a row at which the value Max_xf(x, y) is found. As a result, f(x_o, y) would be the greatest possible value for any y  in the x_o row - (II)

Let y_o be a column at which the value Min_yf(x, y) is found. As a result, f(x, y_o) would be the lowest possible value for any x in the y_o column. - (III)

From (II),

 f(x_o, y) >= f(x_o, y_o)

And from (III),

f(x_o, y_o)>= f(x, y_o)

What we just proved is that there exists a f(x_o, y_o) that belongs to N, such that

f(x_o, y) >= f(x_o, y_o) and f(x_o, y_o)>= f(x, y_o). 

Hence, we can claim using axioms of inequality and natural numbers that:

 f(x_o, y) >= f(x, y_o)

or in other words,

Max_xf(x, y) >= Min _y f(x, y)

which can further be extended to

Min_y(Max_xf(x,y)) >= Max_x(Min_yf(x,y))

using the reasoning in (I)

Summary

Although it took me a while to understand this problem, it took me much lesser time to identify the mental route to understanding this problem (commonly conveyed as "connecting the dots") once it was formalized and expressed as a statement. So the formalization process was worth it because, it helped me clearly understand the problem I was trying to solve. I have not quite been the fan of formal mathematical representation in the past, but I guess that just might change in the future :)

Another take-away realization from today: there is a lot of meaning in "break down problems before you try to solve them". This is just a simple example.