ofBasisZero — Mathlib

English

From a specified family of convex neighborhoods around 0, the space is locally convex.

Русский

Исходя из заданной семейства выпуклых окрестностей вокруг 0, пространство является локально выпуклым.

LaTeX

$$$LocallyConvexSpace 𝕜 E \Leftarrow \text{ existence of convex basis at 0}$$$

Lean4

theorem ofBasisZero {ι : Type*} (b : ι → Set E) (p : ι → Prop) (hbasis : (𝓝 0).HasBasis p b)
    (hconvex : ∀ i, p i → Convex 𝕜 (b i)) : LocallyConvexSpace 𝕜 E :=
  by
  refine
    LocallyConvexSpace.ofBases 𝕜 E (fun (x : E) (i : ι) => (x + ·) '' b i) (fun _ => p) (fun x => ?_) fun x i hi =>
      (hconvex i hi).translate x
  rw [← map_add_left_nhds_zero]
  exact hbasis.map _

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