convex_basis_zero — Mathlib

English

If one has a family of convex neighborhoods forming a basis of local neighborhoods with appropriate translations, then the space is locally convex.

Русский

Если имеем семейство выпуклых окрестностей, образующее базис локальных окрестностей, то пространство локально выпукло.

LaTeX

$$$\text{LocallyConvexSpace } 𝕜 E \text{ from convex basis data}$$$

Lean4

theorem convex_basis_zero [LocallyConvexSpace 𝕜 E] :
    (𝓝 0 : Filter E).HasBasis (fun s => s ∈ (𝓝 0 : Filter E) ∧ Convex 𝕜 s) id :=
  LocallyConvexSpace.convex_basis 0

Похожие утверждения