Commit 2026-06-10 13:05 23100f06

feat(Topology/Algebra/Module/LocallyConvex): a very nice basis of locally convex spaces (#39063) In proving facts about locally convex spaces, you often work with a basis of the neighborhoods of 0 that are open, absolutely convex, antitone, and have the properties that V (n + 1) + V (n + 1) ⊆ V n and closure (V (n + 1)) ⊆ V n. These lemmas construct such a basis. As a bonus, prove that the set of closed, absolutely convex neighbourhoods of zero form a basis of the neighbourhoods of zero. AI Disclosure: During revisions, outlined proofs and had Claude Code fill in details, then revised.