ofBases — Mathlib

English

The neighborhood basis at 0 consists of convex sets.

Русский

Базис окрестностей в точке 0 состоит из выпуклых множеств.

LaTeX

$$$\\mathcal{N}(0) \text{ has a convex basis}$$$

Lean4

theorem ofBases {ι : Type*} (b : E → ι → Set E) (p : E → ι → Prop) (hbasis : ∀ x : E, (𝓝 x).HasBasis (p x) (b x))
    (hconvex : ∀ x i, p x i → Convex 𝕜 (b x i)) : LocallyConvexSpace 𝕜 E :=
  ⟨fun x =>
    (hbasis x).to_hasBasis (fun i hi => ⟨b x i, ⟨⟨(hbasis x).mem_of_mem hi, hconvex x i hi⟩, le_refl (b x i)⟩⟩)
      fun s hs => ⟨(hbasis x).index s hs.1, ⟨(hbasis x).property_index hs.1, (hbasis x).set_index_subset hs.1⟩⟩⟩

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