case h
α : Type u
β : Type v
X : Type ?u.39254
ι : Type ?u.39257
inst✝ : PseudoMetricSpace α
x y✝ z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
y : α
⊢ y ∈ closedBall x ε ↔ y ∈ ⋂ (δ : ℝ) (_ : δ > ε), ball x δ
α : Type u
β : Type v
X : Type ?u.39254
ι : Type ?u.39257
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
⊢ closedBall x ε = ⋂ (δ : ℝ) (_ : δ > ε), ball x δ
ext y
case h
α : Type u
β : Type v
X : Type ?u.39254
ι : Type ?u.39257
inst✝ : PseudoMetricSpace α
x y✝ z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
y : α
⊢ (∀ ⦃c : ℝ⦄, ε < c → dist y x < c) ↔ ∀ (i : ℝ), i > ε → y ∈ ball x i
case h
α : Type u
β : Type v
X : Type ?u.39254
ι : Type ?u.39257
inst✝ : PseudoMetricSpace α
x y✝ z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
y : α
⊢ y ∈ closedBall x ε ↔ y ∈ ⋂ (δ : ℝ) (_ : δ > ε), ball x δ
rw [mem_closedBall, ← forall_lt_iff_le', mem_iInter₂]
no goals
case h
α : Type u
β : Type v
X : Type ?u.39254
ι : Type ?u.39257
inst✝ : PseudoMetricSpace α
x y✝ z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
y : α
⊢ (∀ ⦃c : ℝ⦄, ε < c → dist y x < c) ↔ ∀ (i : ℝ), i > ε → y ∈ ball x i
rfl