locallyConvexSpace_iff — Mathlib

English

Locally convexity of a space is equivalent to the basis of neighborhoods consisting of convex sets.

Русский

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

LaTeX

$$$LocallyConvexSpace 𝕜 E \iff \forall x: E, (\\nhds x).HasBasis (\\lambda i, Convex 𝕜 i) (\\something)$$$

Lean4

theorem locallyConvexSpace_iff :
    LocallyConvexSpace 𝕜 E ↔ ∀ x : E, (𝓝 x).HasBasis (fun s : Set E => s ∈ 𝓝 x ∧ Convex 𝕜 s) id :=
  ⟨fun _ ↦ LocallyConvexSpace.convex_basis, LocallyConvexSpace.mk⟩

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