𝕜 : Type u_1
𝕝 : Type ?u.185016
E : Type u_2
ι : Sort ?u.185022
κ : ι → Sort ?u.185027
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
h : 0 ∈ _root_.interior A
⊢ Balanced 𝕜 ({0} ∪ _root_.interior A)
𝕜 : Type u_1
𝕝 : Type ?u.185016
E : Type u_2
ι : Sort ?u.185022
κ : ι → Sort ?u.185027
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
h : 0 ∈ _root_.interior A
⊢ Balanced 𝕜 (_root_.interior A)
rw [← union_eq_self_of_subset_left (singleton_subset_iff.2 h)]
no goals
𝕜 : Type u_1
𝕝 : Type ?u.185016
E : Type u_2
ι : Sort ?u.185022
κ : ι → Sort ?u.185027
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
h : 0 ∈ _root_.interior A
⊢ Balanced 𝕜 ({0} ∪ _root_.interior A)
exact balanced_zero_union_interior hA