Lower bound for set bounds sInf

Stream: Is there code for X?

[Terence Tao]

Why isn't this lemma in MathLib?? (le_sInf doesn't work because ℝ isn't an instance of CompleteSemilatticeInf.) (Also there should be a Real.sSup_le' in which the upper bound a is not required to be non-negative, but the set is now required to be non-empty.)

import Mathlib

lemma Real.le_sInf {s : Set ℝ} {a : ℝ} (h : BddBelow s) (h' : Set.Nonempty s) (hS : ∀ (x : ℝ), x ∈ s → a ≤ x) : a ≤ sInf s := by
  by_contra ha
  simp at ha
  let ε := a - sInf s
  have hε : 0 < ε/2 := by linarith
  have : sInf s ≤ a - ε/2 := by linarith
  rw [Real.sInf_le_iff h h'] at this
  replace this := this (ε/2) hε
  rcases this with ⟨ x, ⟨ hx, hx' ⟩ ⟩
  replace hS := hS x hx
  linarith

[Andrew Yang]

I think docs#le_csInf_iff is what you need.

[Terence Tao]

OK, thanks. (Somehow I had missed this in my initial search of MathLib.)

[Sebastien Gouezel]

The best way to find this kind of lemma is to use exact?, as in

import Mathlib

lemma Real.le_sInf {s : Set ℝ} {a : ℝ} (h : BddBelow s) (h' : Set.Nonempty s)
    (hS : ∀ (x : ℝ), x ∈ s → a ≤ x) : a ≤ sInf s := by
  exact?

https://loogle.lean-lang.org/ is also extremely useful.