English
Let E be a locally convex space over a field 𝕜. Then the neighborhood filter at 0, 𝓝(0), has a basis consisting of sets that contain 0, are open, and are convex.
Русский
Пусть E — локально выпуктое пространство над полем 𝕜. Фильтр окрестностей нуля 𝓝(0) имеет базис из подмножеств, содержащих 0, открытых и выпуклых.
LaTeX
$$$\left(\mathcal{N}(0) : \text{Filter}(E)\right).\text{HasBasis}(\lambda s \; (0 \in s \wedge \text{IsOpen}(s) \wedge \text{Convex}(\,s)))(\operatorname{id})$$$
Lean4
theorem convex_open_basis_zero [LocallyConvexSpace 𝕜 E] :
(𝓝 0 : Filter E).HasBasis (fun s => (0 : E) ∈ s ∧ IsOpen s ∧ Convex 𝕜 s) id :=
(LocallyConvexSpace.convex_basis_zero 𝕜 E).to_hasBasis
(fun s hs => ⟨interior s, ⟨mem_interior_iff_mem_nhds.mpr hs.1, isOpen_interior, hs.2.interior⟩, interior_subset⟩)
fun s hs => ⟨s, ⟨hs.2.1.mem_nhds hs.1, hs.2.2⟩, subset_rfl⟩
