I’ve written a short note about suprema and infima in formal math:
Toward formalization of partial infima and suprema
It is especially useful for these who do math formally (in proof assistants), but may be inspiring for regular mathematicians too.