R : Type ?u.1093501
R' : Type ?u.1093504
𝕜 : Type u_1
𝕜₂ : Type ?u.1093510
𝕜₃ : Type ?u.1093513
𝕝 : Type ?u.1093516
E : Type u_2
E₂ : Type ?u.1093522
E₃ : Type ?u.1093525
F : Type ?u.1093528
G : Type ?u.1093531
ι : 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 = ⨅ (a : ι) (_ : a ∈ s), ball (p a) x r
R : Type ?u.1093501
R' : Type ?u.1093504
𝕜 : Type u_1
𝕜₂ : Type ?u.1093510
𝕜₃ : Type ?u.1093513
𝕝 : Type ?u.1093516
E : Type u_2
E₂ : Type ?u.1093522
E₃ : Type ?u.1093525
F : Type ?u.1093528
G : Type ?u.1093531
ι : 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 = Finset.inf s fun i => ball (p i) x r
rw [Finset.inf_eq_iInf]
no goals
R : Type ?u.1093501
R' : Type ?u.1093504
𝕜 : Type u_1
𝕜₂ : Type ?u.1093510
𝕜₃ : Type ?u.1093513
𝕝 : Type ?u.1093516
E : Type u_2
E₂ : Type ?u.1093522
E₃ : Type ?u.1093525
F : Type ?u.1093528
G : Type ?u.1093531
ι : 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 = ⨅ (a : ι) (_ : a ∈ s), ball (p a) x r
exact ball_finset_sup_eq_iInter _ _ _ hr