no goals
𝕜 : Type ?u.187149
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.187155
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.187250
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.187340
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y : E
s t : Set E
a : ℝ
⊢ Set.Nonempty (interior (Ioi a))
simp
no goals
𝕜 : Type ?u.187149
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type ?u.187155
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type ?u.187250
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.187340
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
x y : E
s t : Set E
a : ℝ
⊢ a ∈ closure (Ioi a)
simp