𝕜 : Type u_2
E : Type u_1
ι : Type ?u.37359
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
⊢ ∀ (a : E), ∃ i h, ¬a ∈ ∅
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.37359
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
⊢ balancedCoreAux 𝕜 ∅ = ∅
simp_rw [balancedCoreAux, iInter₂_eq_empty_iff, smul_set_empty]
no goals
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.37359
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
⊢ ∀ (a : E), ∃ i h, ¬a ∈ ∅
exact fun _ => ⟨1, norm_one.ge, not_mem_empty _⟩