𝕜 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K✝ K : Set (E →L[𝕜] F)
r s ε : ℝ
⊢ IsOpen (⋃ (L : E →L[𝕜] F) (_ : L ∈ K), A f L r ε ∩ A f L s ε)
𝕜 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K✝ K : Set (E →L[𝕜] F)
r s ε : ℝ
⊢ IsOpen (B f K r s ε)
simp only [B]
no goals
𝕜 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K✝ K : Set (E →L[𝕜] F)
r s ε : ℝ
⊢ IsOpen (⋃ (L : E →L[𝕜] F) (_ : L ∈ K), A f L r ε ∩ A f L s ε)
exact isOpen_iUnion fun _ => isOpen_iUnion fun _ => (isOpen_a _ _ _).inter (isOpen_a _ _ _)