Commit 2022-02-07 15:41 0354e56f

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.