English
The neighborhood system at 0 has a basis consisting of AbsConvex sets.
Русский
Система окрестностей нуля имеет базис, состоящий из абсолю́тно выпуклых множеств.
LaTeX
$$$$ (\\mathcal{N}(0)) hasBasis (s \\mapsto s \\in \\mathcal{N}(0) \\land AbsConvex 𝕜 s) id. $$$$
Lean4
theorem nhds_hasBasis_absConvex : (𝓝 (0 : E)).HasBasis (fun s : Set E => s ∈ 𝓝 (0 : E) ∧ AbsConvex 𝕜 s) id :=
by
refine
(LocallyConvexSpace.convex_basis_zero ℝ E).to_hasBasis (fun s hs => ?_) fun s hs => ⟨s, ⟨hs.1, hs.2.2⟩, rfl.subset⟩
refine ⟨convexHull ℝ (balancedCore 𝕜 s), ?_, convexHull_min (balancedCore_subset s) hs.2⟩
refine ⟨Filter.mem_of_superset (balancedCore_mem_nhds_zero hs.1) (subset_convexHull ℝ _), ?_⟩
refine ⟨(balancedCore_balanced s).convexHull, ?_⟩
exact convex_convexHull ℝ (balancedCore 𝕜 s)
