x y : ℝ
s : Set ℝ
h : BddBelow s
h' : Set.Nonempty s
a : ℝ
⊢ (∀ (ε : ℝ), 0 < ε → sInf s < a + ε) ↔ ∀ (ε : ℝ), 0 < ε → ∃ x, x ∈ s ∧ x < a + ε
x y : ℝ
s : Set ℝ
h : BddBelow s
h' : Set.Nonempty s
a : ℝ
⊢ sInf s ≤ a ↔ ∀ (ε : ℝ), 0 < ε → ∃ x, x ∈ s ∧ x < a + ε
rw [le_iff_forall_pos_lt_add]
case mp
x y : ℝ
s : Set ℝ
h : BddBelow s
h' : Set.Nonempty s
a : ℝ
H : ∀ (ε : ℝ), 0 < ε → sInf s < a + ε
ε : ℝ
ε_pos : 0 < ε
⊢ ∃ x, x ∈ s ∧ x < a + ε

case mpr
x y : ℝ
s : Set ℝ
h : BddBelow s
h' : Set.Nonempty s
a : ℝ
H : ∀ (ε : ℝ), 0 < ε → ∃ x, x ∈ s ∧ x < a + ε
ε : ℝ
ε_pos : 0 < ε
⊢ sInf s < a + ε
x y : ℝ
s : Set ℝ
h : BddBelow s
h' : Set.Nonempty s
a : ℝ
⊢ (∀ (ε : ℝ), 0 < ε → sInf s < a + ε) ↔ ∀ (ε : ℝ), 0 < ε → ∃ x, x ∈ s ∧ x < a + ε
constructor <;> intro H ε ε_pos
no goals
case mp
x y : ℝ
s : Set ℝ
h : BddBelow s
h' : Set.Nonempty s
a : ℝ
H : ∀ (ε : ℝ), 0 < ε → sInf s < a + ε
ε : ℝ
ε_pos : 0 < ε
⊢ ∃ x, x ∈ s ∧ x < a + ε
exact exists_lt_of_csInf_lt h' (H ε ε_pos)
case mpr.intro.intro
x✝ y : ℝ
s : Set ℝ
h : BddBelow s
h' : Set.Nonempty s
a : ℝ
H : ∀ (ε : ℝ), 0 < ε → ∃ x, x ∈ s ∧ x < a + ε
ε : ℝ
ε_pos : 0 < ε
x : ℝ
x_in : x ∈ s
hx : x < a + ε
⊢ sInf s < a + ε
case mpr
x y : ℝ
s : Set ℝ
h : BddBelow s
h' : Set.Nonempty s
a : ℝ
H : ∀ (ε : ℝ), 0 < ε → ∃ x, x ∈ s ∧ x < a + ε
ε : ℝ
ε_pos : 0 < ε
⊢ sInf s < a + ε
rcases H ε ε_pos with ⟨x, x_in, hx⟩
no goals
case mpr.intro.intro
x✝ y : ℝ
s : Set ℝ
h : BddBelow s
h' : Set.Nonempty s
a : ℝ
H : ∀ (ε : ℝ), 0 < ε → ∃ x, x ∈ s ∧ x < a + ε
ε : ℝ
ε_pos : 0 < ε
x : ℝ
x_in : x ∈ s
hx : x < a + ε
⊢ sInf s < a + ε
exact csInf_lt_of_lt h x_in hx