𝕜 : Type u_2
E : Type u_1
ι : Type ?u.67976
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : 0 ∈ s
⊢ balancedCoreAux 𝕜 s ⊆ balancedCore 𝕜 s
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.67976
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : 0 ∈ s
⊢ balancedCore 𝕜 s = ⋂ (r : 𝕜) (_ : 1 ≤ ‖r‖), r • s
refine' balancedCore_subset_balancedCoreAux.antisymm _
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.67976
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : 0 ∈ s
⊢ 0 ∈ balancedCoreAux 𝕜 s
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.67976
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : 0 ∈ s
⊢ balancedCoreAux 𝕜 s ⊆ balancedCore 𝕜 s
refine' (balancedCoreAux_balanced _).subset_balancedCore_of_subset (balancedCoreAux_subset s)
no goals
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.67976
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : 0 ∈ s
⊢ 0 ∈ balancedCoreAux 𝕜 s
exact balancedCore_subset_balancedCoreAux (balancedCore_zero_mem hs)