α : Type u
β : Type v
γ : Type w
x ε : ℝ
⊢ TotallyBounded (Ioo (x - ε) (x + ε))
α : Type u
β : Type v
γ : Type w
x ε : ℝ
⊢ TotallyBounded (ball x ε)
rw [Real.ball_eq_Ioo]
no goals
α : Type u
β : Type v
γ : Type w
x ε : ℝ
⊢ TotallyBounded (Ioo (x - ε) (x + ε))
apply totallyBounded_Ioo