case h
R : Type ?u.824078
R' : Type ?u.824081
𝕜 : Type u_2
𝕜₂ : Type ?u.824087
𝕜₃ : Type ?u.824090
𝕝 : Type ?u.824093
E : Type u_1
E₂ : Type ?u.824099
E₃ : Type ?u.824102
F : Type ?u.824105
G : Type ?u.824108
ι : Type ?u.824111
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
x✝ y✝ : E
r✝ : ℝ
x : E
r : ℝ
y : E
⊢ y ∈ closedBall p x r ↔ y ∈ ⋂ (ρ : ℝ) (_ : ρ > r), ball p x ρ
R : Type ?u.824078
R' : Type ?u.824081
𝕜 : Type u_2
𝕜₂ : Type ?u.824087
𝕜₃ : Type ?u.824090
𝕝 : Type ?u.824093
E : Type u_1
E₂ : Type ?u.824099
E₃ : Type ?u.824102
F : Type ?u.824105
G : Type ?u.824108
ι : Type ?u.824111
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
x✝ y : E
r✝ : ℝ
x : E
r : ℝ
⊢ closedBall p x r = ⋂ (ρ : ℝ) (_ : ρ > r), ball p x ρ
ext y
no goals
case h
R : Type ?u.824078
R' : Type ?u.824081
𝕜 : Type u_2
𝕜₂ : Type ?u.824087
𝕜₃ : Type ?u.824090
𝕝 : Type ?u.824093
E : Type u_1
E₂ : Type ?u.824099
E₃ : Type ?u.824102
F : Type ?u.824105
G : Type ?u.824108
ι : Type ?u.824111
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
x✝ y✝ : E
r✝ : ℝ
x : E
r : ℝ
y : E
⊢ y ∈ closedBall p x r ↔ y ∈ ⋂ (ρ : ℝ) (_ : ρ > r), ball p x ρ
simp_rw [mem_closedBall, mem_iInter₂, mem_ball, ← forall_lt_iff_le']