case intro
R : Type ?u.1084542
R' : Type ?u.1084545
𝕜 : Type u_1
𝕜₂ : Type ?u.1084551
𝕜₃ : Type ?u.1084554
𝕝 : Type ?u.1084557
E : Type u_2
E₂ : Type ?u.1084563
E₃ : Type ?u.1084566
F : Type ?u.1084569
G : Type ?u.1084572
ι : Type u_3
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p✝ : Seminorm 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ≥0
⊢ closedBall (Finset.sup s p) x ↑r = ⋂ (i : ι) (_ : i ∈ s), closedBall (p i) x ↑r
R : Type ?u.1084542
R' : Type ?u.1084545
𝕜 : Type u_1
𝕜₂ : Type ?u.1084551
𝕜₃ : Type ?u.1084554
𝕝 : Type ?u.1084557
E : Type u_2
E₂ : Type ?u.1084563
E₃ : Type ?u.1084566
F : Type ?u.1084569
G : Type ?u.1084572
ι : Type u_3
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p✝ : Seminorm 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ
hr : 0 ≤ r
⊢ closedBall (Finset.sup s p) x r = ⋂ (i : ι) (_ : i ∈ s), closedBall (p i) x r
lift r to NNReal using hr
no goals
case intro
R : Type ?u.1084542
R' : Type ?u.1084545
𝕜 : Type u_1
𝕜₂ : Type ?u.1084551
𝕜₃ : Type ?u.1084554
𝕝 : Type ?u.1084557
E : Type u_2
E₂ : Type ?u.1084563
E₃ : Type ?u.1084566
F : Type ?u.1084569
G : Type ?u.1084572
ι : Type u_3
inst✝⁶ : SeminormedRing 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SeminormedRing 𝕜₂
inst✝² : AddCommGroup E₂
inst✝¹ : Module 𝕜₂ E₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
p✝ : Seminorm 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ≥0
⊢ closedBall (Finset.sup s p) x ↑r = ⋂ (i : ι) (_ : i ∈ s), closedBall (p i) x ↑r
simp_rw [closedBall, iInter_setOf, finset_sup_apply, NNReal.coe_le_coe, Finset.sup_le_iff, ←
  NNReal.coe_le_coe, coe_mk]