case intro
R : Type ?u.1073638
R' : Type ?u.1073641
𝕜 : Type u_1
𝕜₂ : Type ?u.1073647
𝕜₃ : Type ?u.1073650
𝕝 : Type ?u.1073653
E : Type u_2
E₂ : Type ?u.1073659
E₃ : Type ?u.1073662
F : Type ?u.1073665
G : Type ?u.1073668
ι : 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
hr : 0 < ↑r
⊢ ball (Finset.sup s p) x ↑r = ⋂ (i : ι) (_ : i ∈ s), ball (p i) x ↑r
R : Type ?u.1073638
R' : Type ?u.1073641
𝕜 : Type u_1
𝕜₂ : Type ?u.1073647
𝕜₃ : Type ?u.1073650
𝕝 : Type ?u.1073653
E : Type u_2
E₂ : Type ?u.1073659
E₃ : Type ?u.1073662
F : Type ?u.1073665
G : Type ?u.1073668
ι : 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
⊢ ball (Finset.sup s p) x r = ⋂ (i : ι) (_ : i ∈ s), ball (p i) x r
lift r to NNReal using hr.le
no goals
case intro
R : Type ?u.1073638
R' : Type ?u.1073641
𝕜 : Type u_1
𝕜₂ : Type ?u.1073647
𝕜₃ : Type ?u.1073650
𝕝 : Type ?u.1073653
E : Type u_2
E₂ : Type ?u.1073659
E₃ : Type ?u.1073662
F : Type ?u.1073665
G : Type ?u.1073668
ι : 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
hr : 0 < ↑r
⊢ ball (Finset.sup s p) x ↑r = ⋂ (i : ι) (_ : i ∈ s), ball (p i) x ↑r
simp_rw [ball, iInter_setOf, finset_sup_apply, NNReal.coe_lt_coe,
  Finset.sup_lt_iff (show ⊥ < r from hr), ← NNReal.coe_lt_coe, coe_mk]