case pos
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.82897
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed U
h : 0 ∈ U
⊢ IsClosed (balancedCore 𝕜 U)

case neg
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.82897
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed U
h : ¬0 ∈ U
⊢ IsClosed (balancedCore 𝕜 U)
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.82897
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed U
⊢ IsClosed (balancedCore 𝕜 U)
by_cases h : (0 : E) ∈ U
case pos
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.82897
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed U
h : 0 ∈ U
⊢ IsClosed (⋂ (r : 𝕜) (_ : 1 ≤ ‖r‖), r • U)
case pos
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.82897
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed U
h : 0 ∈ U
⊢ IsClosed (balancedCore 𝕜 U)
rw [balancedCore_eq_iInter h]
case pos
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.82897
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed U
h : 0 ∈ U
a : 𝕜
⊢ IsClosed (⋂ (_ : 1 ≤ ‖a‖), a • U)
case pos
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.82897
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed U
h : 0 ∈ U
⊢ IsClosed (⋂ (r : 𝕜) (_ : 1 ≤ ‖r‖), r • U)
refine' isClosed_iInter fun a => _
case pos
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.82897
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed U
h : 0 ∈ U
a : 𝕜
ha : 1 ≤ ‖a‖
⊢ IsClosed (a • U)
case pos
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.82897
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed U
h : 0 ∈ U
a : 𝕜
⊢ IsClosed (⋂ (_ : 1 ≤ ‖a‖), a • U)
refine' isClosed_iInter fun ha => _
case pos
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.82897
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed U
h : 0 ∈ U
a : 𝕜
ha : 1 ≤ ‖a‖
ha' : 0 < ‖a‖
⊢ IsClosed (a • U)
case pos
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.82897
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed U
h : 0 ∈ U
a : 𝕜
ha : 1 ≤ ‖a‖
⊢ IsClosed (a • U)
have ha' := lt_of_lt_of_le zero_lt_one ha
case pos
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.82897
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed U
h : 0 ∈ U
a : 𝕜
ha : 1 ≤ ‖a‖
ha' : a ≠ 0
⊢ IsClosed (a • U)
case pos
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.82897
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed U
h : 0 ∈ U
a : 𝕜
ha : 1 ≤ ‖a‖
ha' : 0 < ‖a‖
⊢ IsClosed (a • U)
rw [norm_pos_iff] at ha'
no goals
case pos
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.82897
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed U
h : 0 ∈ U
a : 𝕜
ha : 1 ≤ ‖a‖
ha' : a ≠ 0
⊢ IsClosed (a • U)
exact isClosedMap_smul_of_ne_zero ha' U hU
case neg
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.82897
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed U
h : ¬0 ∈ U
this : balancedCore 𝕜 U = ∅
⊢ IsClosed (balancedCore 𝕜 U)
case neg
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.82897
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed U
h : ¬0 ∈ U
⊢ IsClosed (balancedCore 𝕜 U)
have : balancedCore 𝕜 U = ∅ := by
  contrapose! h
  exact balancedCore_nonempty_iff.mp (Set.nonempty_iff_ne_empty.2 h)
case neg
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.82897
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed U
h : ¬0 ∈ U
this : balancedCore 𝕜 U = ∅
⊢ IsClosed ∅
case neg
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.82897
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed U
h : ¬0 ∈ U
this : balancedCore 𝕜 U = ∅
⊢ IsClosed (balancedCore 𝕜 U)
rw [this]
no goals
case neg
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.82897
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed U
h : ¬0 ∈ U
this : balancedCore 𝕜 U = ∅
⊢ IsClosed ∅
exact isClosed_empty
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.82897
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed U
h : balancedCore 𝕜 U ≠ ∅
⊢ 0 ∈ U
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.82897
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed U
h : ¬0 ∈ U
⊢ balancedCore 𝕜 U = ∅
contrapose! h
no goals
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.82897
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed U
h : balancedCore 𝕜 U ≠ ∅
⊢ 0 ∈ U
exact balancedCore_nonempty_iff.mp (Set.nonempty_iff_ne_empty.2 h)