locallyConvexSpace_iff_zero — Mathlib

English

Locally convexity is equivalent to the zero-based convex basis condition.

Русский

Локальная выпуклость эквивалентна условию выпуклой базы при нуле.

LaTeX

$$$LocallyConvexSpace 𝕜 E \iff (\mathrm{nhds}0) \text{ has convex basis}$$$

Lean4

theorem locallyConvexSpace_iff_zero :
    LocallyConvexSpace 𝕜 E ↔ (𝓝 0 : Filter E).HasBasis (fun s : Set E => s ∈ (𝓝 0 : Filter E) ∧ Convex 𝕜 s) id :=
  ⟨fun _ => LocallyConvexSpace.convex_basis 0, fun h => LocallyConvexSpace.ofBasisZero 𝕜 E _ _ h fun _ => And.right⟩

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