Commit 2025-06-11 15:42 e1bee928

feat(Order/CompleteLattice/Defs): add lt_biSup_iff (#25648) Added lt_biSup_iff, biInf_lt_iff. These are bi versions of the results already stated for iSup/iInf.
Motivation: although the result can be proven by simp with a single named theorem when one doesn't know, it isn't clear that this is the way to do it. Having this theorem here completes the standard versions of the results and eases automation.