Commit 2026-09-16 20:50 92fc6042

View on Github →

refactor(Analysis/LocallyConvex): state hulls via ClosureOperator (#42517) Restate balancedHull and the neighborhood bases of the origin in terms of the ClosureOperator API, and add the general lemmas that make this possible:

  • ClosureOperator.closure_binop_le: a closure operator is sub-f for any monotone binary operation f whose closed elements are stable under f; balancedHull_add_subset and absConvexHull_add_subset are instances.
  • Filter.HasBasis.and_isClosed: combine a basis of p-sets with a basis of c-closed sets when c preserves p.
  • Topology.closureOperator: topological closure, bundled.
  • Balanced.sUnion, and Balanced.closure generalized to SeminormedRing. balancedCore keeps its definition as a union of balanced subsets, but its API is now derived from the hull side; balancedCoreAux is removed in favour of lemmas stated directly about ⋂ (r : 𝕜) (_ : 1 ≤ ‖r‖), r • s. The new nhds_basis_open_balanced joins nhds_basis_closed_balanced, nhds_hasBasis_absConvex_open and nhds_hasBasis_absConvex_closed, all four proved through and_isClosed. AI Disclosure: Much of the refactoring work across files was performed by Claude Opus 5 after being given examples I wrote.

Estimated changes

added theorem balancedCore.balanced
modified def balancedCore
deleted theorem balancedCore_balanced
added theorem balancedCore_mono
modified theorem balancedHull.balanced
modified def balancedHull
modified theorem balancedHull_add_subset
added theorem balancedHull_eq_iUnion
modified theorem balancedHull_mono
added theorem balanced_iInter_smul
added theorem iInter_smul_subset
modified theorem mem_balancedHull_iff
modified theorem subset_balancedHull
added theorem Balanced.sUnion