feat(order/complete_lattice): infi_le_iff (#11810)
Add missing lemma `infi_le_iff {s : ι → α} : infi s ≤ a ↔ (∀ b, (∀ i, b ≤ s i) → b ≤ a)`
Also take the opportunity to restate `Inf_le_iff` to restore consistency with `le_Sup_iff` that was broken in #10607 and move `le_supr_iff` close to `le_Sup_iff` and remove a couple of unneeded parentheses.
