English
The neighborhood system at 0 has a basis consisting of open AbsConvex sets as well.
Русский
У нуля базис окрестностей можно выбрать из открытых AbsConvex множеств.
LaTeX
$$$$ (\\mathcal{N}(0)).HasBasis (s \\mapsto (0 \\in s) \\land IsOpen s \\land AbsConvex 𝕜 s) id. $$$$
Lean4
theorem nhds_hasBasis_absConvex_open : (𝓝 (0 : E)).HasBasis (fun s => (0 : E) ∈ s ∧ IsOpen s ∧ AbsConvex 𝕜 s) id :=
by
refine (nhds_hasBasis_absConvex 𝕜 E).to_hasBasis ?_ ?_
· rintro s ⟨hs_nhds, hs_balanced, hs_convex⟩
refine ⟨interior s, ?_, interior_subset⟩
exact
⟨mem_interior_iff_mem_nhds.mpr hs_nhds, isOpen_interior,
hs_balanced.interior (mem_interior_iff_mem_nhds.mpr hs_nhds), hs_convex.interior⟩
rintro s ⟨hs_zero, hs_open, hs_balanced, hs_convex⟩
exact ⟨s, ⟨hs_open.mem_nhds hs_zero, hs_balanced, hs_convex⟩, rfl.subset⟩
