Commit 2025-02-17 21:24 ae232e46

View on Github →

refactor(Analysis/LocallyConvex/AbsConvexOpen): Break out AbsConvexOpenSets into its own file (#21928) Break out AbsConvexOpenSets into its own file. This allows Mathlib.Analysis.LocallyConvex.AbsConvex to be imported without also pulling in Mathlib.Analysis.LocallyConvex.WithSeminorms and Mathlib.Analysis.Convex.Gauge.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/LocallyConvex/AbsConvex.lean

deleted theorem AbsConvexOpenSets.coe_balanced

deleted theorem AbsConvexOpenSets.coe_convex

deleted theorem AbsConvexOpenSets.coe_isOpen

deleted theorem AbsConvexOpenSets.coe_nhds

deleted theorem AbsConvexOpenSets.coe_zero_mem

deleted def AbsConvexOpenSets

deleted theorem gaugeSeminormFamily_ball

deleted theorem with_gaugeSeminormFamily

Created Mathlib/Analysis/LocallyConvex/AbsConvexOpen.lean

added theorem AbsConvexOpenSets.coe_balanced

added theorem AbsConvexOpenSets.coe_convex

added theorem AbsConvexOpenSets.coe_isOpen

added theorem AbsConvexOpenSets.coe_nhds

added theorem AbsConvexOpenSets.coe_zero_mem

added def AbsConvexOpenSets

added theorem gaugeSeminormFamily_ball

added theorem with_gaugeSeminormFamily