𝕜 : Type u_2
E : Type u_1
F : Type ?u.8459
G : Type ?u.8462
ι : Type ?u.8465
s✝ : Set E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module ℝ E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0 ∧ Convex ℝ s
⊢ ∃ i', (i' ∈ 𝓝 0 ∧ Balanced 𝕜 i' ∧ Convex ℝ i') ∧ id i' ⊆ id s
𝕜 : Type u_2
E : Type u_1
F : Type ?u.8459
G : Type ?u.8462
ι : Type ?u.8465
s : Set E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module ℝ E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul 𝕜 E
⊢ Filter.HasBasis (𝓝 0) (fun s => s ∈ 𝓝 0 ∧ Balanced 𝕜 s ∧ Convex ℝ s) id
refine'
  (LocallyConvexSpace.convex_basis_zero ℝ E).to_hasBasis (fun s hs => _) fun s hs =>
    ⟨s, ⟨hs.1, hs.2.2⟩, rfl.subset⟩
𝕜 : Type u_2
E : Type u_1
F : Type ?u.8459
G : Type ?u.8462
ι : Type ?u.8465
s✝ : Set E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module ℝ E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0 ∧ Convex ℝ s
⊢ ↑(convexHull ℝ).toOrderHom (balancedCore 𝕜 s) ∈ 𝓝 0 ∧
    Balanced 𝕜 (↑(convexHull ℝ).toOrderHom (balancedCore 𝕜 s)) ∧
      Convex ℝ (↑(convexHull ℝ).toOrderHom (balancedCore 𝕜 s))
𝕜 : Type u_2
E : Type u_1
F : Type ?u.8459
G : Type ?u.8462
ι : Type ?u.8465
s✝ : Set E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module ℝ E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0 ∧ Convex ℝ s
⊢ ∃ i', (i' ∈ 𝓝 0 ∧ Balanced 𝕜 i' ∧ Convex ℝ i') ∧ id i' ⊆ id s
refine' ⟨convexHull ℝ (balancedCore 𝕜 s), _, convexHull_min (balancedCore_subset s) hs.2⟩
𝕜 : Type u_2
E : Type u_1
F : Type ?u.8459
G : Type ?u.8462
ι : Type ?u.8465
s✝ : Set E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module ℝ E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0 ∧ Convex ℝ s
⊢ Balanced 𝕜 (↑(convexHull ℝ).toOrderHom (balancedCore 𝕜 s)) ∧ Convex ℝ (↑(convexHull ℝ).toOrderHom (balancedCore 𝕜 s))
𝕜 : Type u_2
E : Type u_1
F : Type ?u.8459
G : Type ?u.8462
ι : Type ?u.8465
s✝ : Set E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module ℝ E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0 ∧ Convex ℝ s
⊢ ↑(convexHull ℝ).toOrderHom (balancedCore 𝕜 s) ∈ 𝓝 0 ∧
    Balanced 𝕜 (↑(convexHull ℝ).toOrderHom (balancedCore 𝕜 s)) ∧
      Convex ℝ (↑(convexHull ℝ).toOrderHom (balancedCore 𝕜 s))
refine' ⟨Filter.mem_of_superset (balancedCore_mem_nhds_zero hs.1) (subset_convexHull ℝ _), _⟩
𝕜 : Type u_2
E : Type u_1
F : Type ?u.8459
G : Type ?u.8462
ι : Type ?u.8465
s✝ : Set E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module ℝ E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0 ∧ Convex ℝ s
⊢ Convex ℝ (↑(convexHull ℝ).toOrderHom (balancedCore 𝕜 s))
𝕜 : Type u_2
E : Type u_1
F : Type ?u.8459
G : Type ?u.8462
ι : Type ?u.8465
s✝ : Set E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module ℝ E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0 ∧ Convex ℝ s
⊢ Balanced 𝕜 (↑(convexHull ℝ).toOrderHom (balancedCore 𝕜 s)) ∧ Convex ℝ (↑(convexHull ℝ).toOrderHom (balancedCore 𝕜 s))
refine' ⟨balanced_convexHull_of_balanced (balancedCore_balanced s), _⟩
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.8459
G : Type ?u.8462
ι : Type ?u.8465
s✝ : Set E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module ℝ E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0 ∧ Convex ℝ s
⊢ Convex ℝ (↑(convexHull ℝ).toOrderHom (balancedCore 𝕜 s))
exact convex_convexHull ℝ (balancedCore 𝕜 s)