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.

src/order/complete_lattice.lean

@@ -90,12 +90,15 @@ le_trans h (le_Sup hb)
 theorem Sup_le_Sup (h : s ⊆ t) : Sup s ≤ Sup t :=
 (is_lub_Sup s).mono (is_lub_Sup t) h
 
-@[simp] theorem Sup_le_iff : Sup s ≤ a ↔ (∀b ∈ s, b ≤ a) :=
+@[simp] theorem Sup_le_iff : Sup s ≤ a ↔ ∀b ∈ s, b ≤ a :=
 is_lub_le_iff (is_lub_Sup s)
 
-lemma le_Sup_iff : a ≤ Sup s ↔ (∀ b ∈ upper_bounds s, a ≤ b) :=
+lemma le_Sup_iff : a ≤ Sup s ↔ ∀ b ∈ upper_bounds s, a ≤ b :=
 ⟨λ h b hb, le_trans h (Sup_le hb), λ hb, hb _ (λ x, le_Sup)⟩
 
+lemma le_supr_iff {s : ι → α} : a ≤ supr s ↔ ∀ b, (∀ i, s i ≤ b) → a ≤ b :=
+by simp [supr, le_Sup_iff, upper_bounds]
+
 theorem Sup_le_Sup_of_forall_exists_le (h : ∀ x ∈ s, ∃ y ∈ t, x ≤ y) : Sup s ≤ Sup t :=
 le_Sup_iff.2 $ λ b hb, Sup_le $ λ a ha, let ⟨c, hct, hac⟩ := h a ha in hac.trans (hb hct)
 
@@ -138,9 +141,12 @@ theorem Inf_le_Inf (h : s ⊆ t) : Inf t ≤ Inf s :=
 le_is_glb_iff (is_glb_Inf s)
 
 lemma Inf_le_iff :
-  Inf s ≤ a ↔ (∀ b, (∀ x ∈ s, b ≤ x) → b ≤ a) :=
+  Inf s ≤ a ↔ (∀ b ∈ lower_bounds s, b ≤ a) :=
 ⟨λ h b hb, le_trans (le_Inf hb) h, λ hb, hb _ (λ x, Inf_le)⟩
 
+lemma infi_le_iff {s : ι → α} : infi s ≤ a ↔ (∀ b, (∀ i, b ≤ s i) → b ≤ a) :=
+by simp [infi, Inf_le_iff, lower_bounds]
+
 theorem Inf_le_Inf_of_forall_exists_le (h : ∀ x ∈ s, ∃ y ∈ t, y ≤ x) : Inf t ≤ Inf s :=
 le_of_forall_le begin
   simp only [le_Inf_iff],
@@ -467,7 +473,7 @@ theorem bsupr_le_bsupr' {p q : ι → Prop} (hpq : ∀ i, p i → q i) {f : ι 
   (⨆ i (hpi : p i), f i) ≤ ⨆ i (hqi : q i), f i :=
 supr_le_supr $ λ i, supr_le_supr_const (hpq i)
 
-@[simp] theorem supr_le_iff : supr s ≤ a ↔ (∀i, s i ≤ a) :=
+@[simp] theorem supr_le_iff : supr s ≤ a ↔ ∀ i, s i ≤ a :=
 (is_lub_le_iff is_lub_supr).trans forall_range_iff
 
 theorem supr_lt_iff : supr s < a ↔ ∃ b < a, ∀ i, s i ≤ b :=
@@ -493,9 +499,6 @@ begin
     exact supr_le (λ ts, Sup_le_Sup (λ x xt, ⟨t, ts, xt⟩)) }
 end
 
-lemma le_supr_iff : (a ≤ supr s) ↔ (∀ b, (∀ i, s i ≤ b) → a ≤ b) :=
-⟨λ h b hb, le_trans h (supr_le hb), λ h, h _ $ λ i, le_supr s i⟩
-
 lemma monotone.le_map_supr [complete_lattice β] {f : α → β} (hf : monotone f) :
   (⨆ i, f (s i)) ≤ f (supr s) :=
 supr_le $ λ i, hf $ le_supr _ _