English
If a family of seminorms p generates the topology of a space E, then E is a locally convex space over ℝ. This provides a convex neighborhood basis at each point compatible with the vector space structure.
Русский
Если семейство семинорм p порождает топологию пространства E, то E является локально выпуклым пространством над ℝ. Это обеспечивает выпуклотеперечный базис окрестностей в каждой точке, совместимый с векторной структурой.
LaTeX
$$$ WithSeminorms p \\Rightarrow LocallyConvexSpace \\mathbb{R} E $$$
Lean4
theorem toLocallyConvexSpace {p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms p) : LocallyConvexSpace ℝ E :=
by
have := hp.topologicalAddGroup
apply ofBasisZero ℝ E id fun s => s ∈ p.basisSets
· rw [hp.1, AddGroupFilterBasis.nhds_eq _, AddGroupFilterBasis.N_zero]
exact FilterBasis.hasBasis _
· intro s hs
change s ∈ Set.iUnion _ at hs
simp_rw [Set.mem_iUnion, Set.mem_singleton_iff] at hs
rcases hs with ⟨I, r, _, rfl⟩
exact convex_ball _ _ _
