Top equals to Relative Pseudocomplement in Brouwerian Lattice

Theorem

Let $\struct {S, \vee, \wedge, \preceq}$ be a Brouwerian lattice with greatest element $\top$.

Let $a, b \in S$.

Then

$\top = a \to b$ if and only if $a \preceq b$

Proof

Sufficient Condition

Let:

$\top = a \to b$

By definition of reflexivity:

$\top \preceq a \to b$

By Inequality with Meet Operation is Equivalent to Inequality with Relative Pseudocomplement in Brouwerian Lattice:

$\top \wedge a \preceq b$

Thus

$a \preceq b$

$\Box$

Necessary Condition

Let:

$a \preceq b$

Then:

$a \wedge \top \preceq b$

By Inequality with Meet Operation is Equivalent to Inequality with Relative Pseudocomplement in Brouwerian Lattice:

$\top \preceq a \to b$

By definition of greatest element:

$a \to b \preceq \top$

By definition of ordered set:

$\top = a \to b$

$\blacksquare$

Sources

• 1980: G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M.W. Mislove and D.S. Scott: A Compendium of Continuous Lattices

• Mizar article WAYBEL_1:69