α : Type u
β : Type v
γ : Type w
s : Set ℝ
bdd : Metric.Bounded s
⊢ BddBelow s ∧ BddAbove s
α : Type u
β : Type v
γ : Type w
s : Set ℝ
⊢ Metric.Bounded s → BddBelow s ∧ BddAbove s
intro bdd
case intro
α : Type u
β : Type v
γ : Type w
s : Set ℝ
bdd : Metric.Bounded s
r : ℝ
hr : s ⊆ closedBall 0 r
⊢ BddBelow s ∧ BddAbove s
α : Type u
β : Type v
γ : Type w
s : Set ℝ
bdd : Metric.Bounded s
⊢ BddBelow s ∧ BddAbove s
rcases (bounded_iff_subset_ball 0).1 bdd with ⟨r, hr⟩
case intro
α : Type u
β : Type v
γ : Type w
s : Set ℝ
bdd : Metric.Bounded s
r : ℝ
hr : s ⊆ Icc (0 - r) (0 + r)
⊢ BddBelow s ∧ BddAbove s

α : Type u
β : Type v
γ : Type w
s : Set ℝ
bdd : Metric.Bounded s
⊢ OfNat ℝ 0
case intro
α : Type u
β : Type v
γ : Type w
s : Set ℝ
bdd : Metric.Bounded s
r : ℝ
hr : s ⊆ closedBall 0 r
⊢ BddBelow s ∧ BddAbove s
rw [Real.closedBall_eq_Icc] at hr
no goals
case intro
α : Type u
β : Type v
γ : Type w
s : Set ℝ
bdd : Metric.Bounded s
r : ℝ
hr : s ⊆ Icc (0 - r) (0 + r)
⊢ BddBelow s ∧ BddAbove s

α : Type u
β : Type v
γ : Type w
s : Set ℝ
bdd : Metric.Bounded s
⊢ OfNat ℝ 0
exact ⟨bddBelow_Icc.mono hr, bddAbove_Icc.mono hr⟩