Potential typo in Section 6.3?

[daikonradish]

analysis/Analysis/Section_6_2.lean

Line 174 in 801fd1b

theorem EReal.inf_ge_upper (E: Set EReal) {M:EReal} (hM: M ∈ lowerBounds E) : sInf E ≥ M := by sorry

Hi, i think this should read inf_ge_lower? At least I think that's what the intention is. I can submit a PR if that's the case.

[rkirov]

Yeah, I think it is a typo (likely copy from sup_le_upper). You can open a PR.